# HG changeset patch
# User wenzelm
# Date 1198329024 -3600
# Node ID 1051ef9d87c4124dc36984b01afbebc5fb974671
# Parent  2d102ddaca8b8dd223428a7c716b025a78b1312d
added int/real/list operations;
tuned interface;
tuned;

diff -r 2d102ddaca8b -r 1051ef9d87c4 src/Tools/random_word.ML
--- a/src/Tools/random_word.ML	Sat Dec 22 14:10:22 2007 +0100
+++ b/src/Tools/random_word.ML	Sat Dec 22 14:10:24 2007 +0100
@@ -9,31 +9,71 @@
 
 signature RANDOM_WORD =
 sig
-  val range: int
-  val range_real: real
-  val next: unit -> word
-  val next_bit: unit -> bool
+  val max_word: word
+  val step: word -> word
+  val next_word: unit -> word
+  val next_bool: unit -> bool
+  val next_int: int -> int -> int
+  val next_real: unit -> real
+  val pick_any: 'a list -> 'a
+  val pick_weighted: (int * 'a) list -> 'a
 end;
 
 structure RandomWord: RANDOM_WORD =
 struct
 
+(* random words: 0w0 <= result <= max_word *)
+
 (*minimum length of unboxed words on all supported ML platforms*)
-val _ = Word.wordSize >= 30 orelse raise Fail ("Bad platform word size");
+val _ = Word.wordSize >= 30
+  orelse raise Fail ("Bad platform word size");
+
+val max_word = 0wx3FFFFFFF;
+val top_bit = 0wx20000000;
 
-val range = 0x40000000;
-val range_real = 1073741824.0;
-val mask = Word.fromInt (range - 1);
-val max_bit = Word.fromInt (range div 2);
+(*multiplier according to Borosh and Niederreiter (for modulus = 2^30),
+  see http://random.mat.sbg.ac.at/~charly/server/server.html*)
+val a = 0w777138309;
+fun step x = Word.andb (a * x + 0w1, max_word);
+
+local val rand = ref 0w1
+in fun next_word () = (change rand step; ! rand) end;
+
+(*NB: higher bits are more random than lower ones*)
+fun next_bool () = Word.andb (next_word (), top_bit) = 0w0;
+
+
+(* random integers: i <= result <= j *)
+
+val max_int = Word.toInt max_word;
 
-(*multiplier according to Borosh and Niederreiter (for m = 2^30),
-  cf. http://random.mat.sbg.ac.at/~charly/server/server.html*)
-val a = 0w777138309;
+fun next_int i j =
+  let val k = j - i in
+    if k < 0 orelse k > max_int then raise Fail ("next_int: out of range")
+    else if k < max_int then i + Word.toInt (Word.mod (next_word (), Word.fromInt (k + 1)))
+    else i + Word.toInt (next_word ())
+  end;
+
+
+(* random reals: 0.0 <= result < 1.0 *)
+
+val scaling = real max_int + 1.0;
+fun next_real () = real (Word.toInt (next_word ())) / scaling;
+
 
-(*generator*)
-val rand = ref 0w0;
-fun next () = (rand := Word.andb (a * ! rand + 0w1, mask); ! rand);
-fun next_bit () = Word.andb (next (), max_bit) = 0w0;
+(* random list elements *)
+
+fun pick_any [] = raise Empty
+  | pick_any xs = nth xs (next_int 0 (length xs - 1));
+
+fun pick_weighted xs =
+  let
+    val total = fold (fn (k, _) => fn i =>
+      if k < 0 then raise Fail ("Bad weight: " ^ string_of_int k) else k + i) xs 0;
+    fun pick n ((k, x) :: xs) =
+        if n <= k then x else pick (n - k) xs
+      | pick _ [] = raise Empty;
+  in if total = 0 then raise Empty else pick (next_int 1 total) xs end;
 
 end;