Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned RandomWord interface;
authorwenzelm
Sat, 22 Dec 2007 14:10:25 +0100
changeset 25743 6810d07f29de
parent 25742 1051ef9d87c4
child 25744 e2002b3657ba
tuned RandomWord interface;
src/Tools/Metis/metis.ML file | annotate | diff | comparison | revisions
src/Tools/Metis/src/PortableIsabelle.sml file | annotate | diff | comparison | revisions 
--- a/src/Tools/Metis/metis.ML	Sat Dec 22 14:10:24 2007 +0100
+++ b/src/Tools/Metis/metis.ML	Sat Dec 22 14:10:25 2007 +0100
@@ -100,12 +100,12 @@
 (* Generating random values.                                                 *)
 (* ------------------------------------------------------------------------- *)
 
-val randomWord = RandomWord.next;
-val randomBool = RandomWord.next_bit;
-fun randomInt n = Word.toInt (Word.mod (randomWord (), Word.fromInt n));
-fun randomReal () = real (Word.toInt (RandomWord.next ())) / RandomWord.range_real;
-
-end
+val randomWord = RandomWord.next_word;
+val randomBool = RandomWord.next_bool;
+fun randomInt n = RandomWord.next_int 0 (n - 1);
+val randomReal = RandomWord.next_real;
+
+end;
 
 (* ------------------------------------------------------------------------- *)
 (* Quotations a la Moscow ML.                                                *)
--- a/src/Tools/Metis/src/PortableIsabelle.sml	Sat Dec 22 14:10:24 2007 +0100
+++ b/src/Tools/Metis/src/PortableIsabelle.sml	Sat Dec 22 14:10:25 2007 +0100
@@ -33,12 +33,12 @@
 (* Generating random values.                                                 *)
 (* ------------------------------------------------------------------------- *)
 
-val randomWord = RandomWord.next;
-val randomBool = RandomWord.next_bit;
-fun randomInt n = Word.toInt (Word.mod (randomWord (), Word.fromInt n));
-fun randomReal () = real (Word.toInt (RandomWord.next ())) / RandomWord.range_real;
+val randomWord = RandomWord.next_word;
+val randomBool = RandomWord.next_bool;
+fun randomInt n = RandomWord.next_int 0 (n - 1);
+val randomReal = RandomWord.next_real;
 
-end
+end;
 
 (* ------------------------------------------------------------------------- *)
 (* Quotations a la Moscow ML.                                                *)
isabelle