# HG changeset patch
# User wenzelm
# Date 1198101974 -3600
# Node ID 76fa068a021f632b1653b6c0b49dc3c3e0b18a07
# Parent  1c45623e0edf5da5e787dea646ac225efe41a990
Simple generator for pseudo-random numbers, using unboxed word arithmetic only.

diff -r 1c45623e0edf -r 76fa068a021f src/Pure/General/random_word.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/random_word.ML	Wed Dec 19 23:06:14 2007 +0100
@@ -0,0 +1,38 @@
+(*  Title:      Pure/General/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: word
+  val next: unit -> word
+  val next_bit: unit -> bool
+end;
+
+structure RandomWord: RANDOM_WORD =
+struct
+
+(*minimal length of unboxed words on all known platforms*)
+val bits = 30;
+val _ = Word.wordSize >= bits orelse raise Fail ("Bad platform word size");
+
+val range = 0wx40000000;
+val mask = range - 0w1;
+val max_bit = Word.>> (range, 0w1);
+
+(*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;
+