src/Pure/General/random_word.ML
author wenzelm
Wed, 19 Dec 2007 23:49:28 +0100
changeset 25720 71e0a5cb2885
parent 25719 a51430528fe0
child 25721 5ae1dc2bb5ea
permissions -rw-r--r--
tuned comments;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
25714
76fa068a021f Simple generator for pseudo-random numbers, using unboxed word arithmetic only.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/General/random_word.ML
76fa068a021f Simple generator for pseudo-random numbers, using unboxed word arithmetic only.
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
76fa068a021f Simple generator for pseudo-random numbers, using unboxed word arithmetic only.
wenzelm
parents:
diff changeset
     3
    Author:     Makarius
76fa068a021f Simple generator for pseudo-random numbers, using unboxed word arithmetic only.
wenzelm
parents:
diff changeset
     4
76fa068a021f Simple generator for pseudo-random numbers, using unboxed word arithmetic only.
wenzelm
parents:
diff changeset
     5
Simple generator for pseudo-random numbers, using unboxed word
76fa068a021f Simple generator for pseudo-random numbers, using unboxed word arithmetic only.
wenzelm
parents:
diff changeset
     6
arithmetic only.  Unprotected concurrency introduces some true
76fa068a021f Simple generator for pseudo-random numbers, using unboxed word arithmetic only.
wenzelm
parents:
diff changeset
     7
randomness.
76fa068a021f Simple generator for pseudo-random numbers, using unboxed word arithmetic only.
wenzelm
parents:
diff changeset
     8
*)
76fa068a021f Simple generator for pseudo-random numbers, using unboxed word arithmetic only.
wenzelm
parents:
diff changeset
     9
76fa068a021f Simple generator for pseudo-random numbers, using unboxed word arithmetic only.
wenzelm
parents:
diff changeset
    10
signature RANDOM_WORD =
76fa068a021f Simple generator for pseudo-random numbers, using unboxed word arithmetic only.
wenzelm
parents:
diff changeset
    11
sig
25719
a51430528fe0 tuned RandomWord signature;
wenzelm
parents: 25714
diff changeset
    12
  val range: int
25714
76fa068a021f Simple generator for pseudo-random numbers, using unboxed word arithmetic only.
wenzelm
parents:
diff changeset
    13
  val next: unit -> word
76fa068a021f Simple generator for pseudo-random numbers, using unboxed word arithmetic only.
wenzelm
parents:
diff changeset
    14
  val next_bit: unit -> bool
76fa068a021f Simple generator for pseudo-random numbers, using unboxed word arithmetic only.
wenzelm
parents:
diff changeset
    15
end;
76fa068a021f Simple generator for pseudo-random numbers, using unboxed word arithmetic only.
wenzelm
parents:
diff changeset
    16
76fa068a021f Simple generator for pseudo-random numbers, using unboxed word arithmetic only.
wenzelm
parents:
diff changeset
    17
structure RandomWord: RANDOM_WORD =
76fa068a021f Simple generator for pseudo-random numbers, using unboxed word arithmetic only.
wenzelm
parents:
diff changeset
    18
struct
76fa068a021f Simple generator for pseudo-random numbers, using unboxed word arithmetic only.
wenzelm
parents:
diff changeset
    19
25720
71e0a5cb2885 tuned comments;
wenzelm
parents: 25719
diff changeset
    20
(*minimum length of unboxed words on all supported ML platforms*)
25719
a51430528fe0 tuned RandomWord signature;
wenzelm
parents: 25714
diff changeset
    21
val _ = Word.wordSize >= 30 orelse raise Fail ("Bad platform word size");
25714
76fa068a021f Simple generator for pseudo-random numbers, using unboxed word arithmetic only.
wenzelm
parents:
diff changeset
    22
25719
a51430528fe0 tuned RandomWord signature;
wenzelm
parents: 25714
diff changeset
    23
val range = 0x40000000;
a51430528fe0 tuned RandomWord signature;
wenzelm
parents: 25714
diff changeset
    24
val mask = Word.fromInt (range - 1);
a51430528fe0 tuned RandomWord signature;
wenzelm
parents: 25714
diff changeset
    25
val max_bit = Word.fromInt (range div 2);
25714
76fa068a021f Simple generator for pseudo-random numbers, using unboxed word arithmetic only.
wenzelm
parents:
diff changeset
    26
76fa068a021f Simple generator for pseudo-random numbers, using unboxed word arithmetic only.
wenzelm
parents:
diff changeset
    27
(*multiplier according to Borosh and Niederreiter (for m = 2^30),
76fa068a021f Simple generator for pseudo-random numbers, using unboxed word arithmetic only.
wenzelm
parents:
diff changeset
    28
  cf. http://random.mat.sbg.ac.at/~charly/server/server.html*)
76fa068a021f Simple generator for pseudo-random numbers, using unboxed word arithmetic only.
wenzelm
parents:
diff changeset
    29
val a = 0w777138309;
76fa068a021f Simple generator for pseudo-random numbers, using unboxed word arithmetic only.
wenzelm
parents:
diff changeset
    30
76fa068a021f Simple generator for pseudo-random numbers, using unboxed word arithmetic only.
wenzelm
parents:
diff changeset
    31
(*generator*)
76fa068a021f Simple generator for pseudo-random numbers, using unboxed word arithmetic only.
wenzelm
parents:
diff changeset
    32
val rand = ref 0w0;
76fa068a021f Simple generator for pseudo-random numbers, using unboxed word arithmetic only.
wenzelm
parents:
diff changeset
    33
fun next () = (rand := Word.andb (a * ! rand + 0w1, mask); ! rand);
76fa068a021f Simple generator for pseudo-random numbers, using unboxed word arithmetic only.
wenzelm
parents:
diff changeset
    34
fun next_bit () = Word.andb (next (), max_bit) = 0w0;
76fa068a021f Simple generator for pseudo-random numbers, using unboxed word arithmetic only.
wenzelm
parents:
diff changeset
    35
76fa068a021f Simple generator for pseudo-random numbers, using unboxed word arithmetic only.
wenzelm
parents:
diff changeset
    36
end;
76fa068a021f Simple generator for pseudo-random numbers, using unboxed word arithmetic only.
wenzelm
parents:
diff changeset
    37