--- /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;
+