src/Tools/random_word.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/random_word.ML	Thu Dec 20 14:33:40 2007 +0100
@@ -0,0 +1,39 @@
+(*  Title:      Tools/random_word.ML
+    ID:         $Id$
+    Author:     Makarius
+
+Simple generator for pseudo-random numbers, using unboxed word
+arithmetic only.  Unprotected concurrency introduces some true
+randomness.
+*)
+
+signature RANDOM_WORD =
+sig
+  val range: int
+  val range_real: real
+  val next: unit -> word
+  val next_bit: unit -> bool
+end;
+
+structure RandomWord: RANDOM_WORD =
+struct
+
+(*minimum length of unboxed words on all supported ML platforms*)
+val _ = Word.wordSize >= 30 orelse raise Fail ("Bad platform word size");
+
+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 m = 2^30),
+  cf. http://random.mat.sbg.ac.at/~charly/server/server.html*)
+val a = 0w777138309;
+
+(*generator*)
+val rand = ref 0w0;
+fun next () = (rand := Word.andb (a * ! rand + 0w1, mask); ! rand);
+fun next_bit () = Word.andb (next (), max_bit) = 0w0;
+
+end;
+