src/Tools/random_word.ML
changeset 25728 71e33d95ac55
child 25742 1051ef9d87c4
equal deleted inserted replaced
25727:e43d91f31118 25728:71e33d95ac55
       
     1 (*  Title:      Tools/random_word.ML
       
     2     ID:         $Id$
       
     3     Author:     Makarius
       
     4 
       
     5 Simple generator for pseudo-random numbers, using unboxed word
       
     6 arithmetic only.  Unprotected concurrency introduces some true
       
     7 randomness.
       
     8 *)
       
     9 
       
    10 signature RANDOM_WORD =
       
    11 sig
       
    12   val range: int
       
    13   val range_real: real
       
    14   val next: unit -> word
       
    15   val next_bit: unit -> bool
       
    16 end;
       
    17 
       
    18 structure RandomWord: RANDOM_WORD =
       
    19 struct
       
    20 
       
    21 (*minimum length of unboxed words on all supported ML platforms*)
       
    22 val _ = Word.wordSize >= 30 orelse raise Fail ("Bad platform word size");
       
    23 
       
    24 val range = 0x40000000;
       
    25 val range_real = 1073741824.0;
       
    26 val mask = Word.fromInt (range - 1);
       
    27 val max_bit = Word.fromInt (range div 2);
       
    28 
       
    29 (*multiplier according to Borosh and Niederreiter (for m = 2^30),
       
    30   cf. http://random.mat.sbg.ac.at/~charly/server/server.html*)
       
    31 val a = 0w777138309;
       
    32 
       
    33 (*generator*)
       
    34 val rand = ref 0w0;
       
    35 fun next () = (rand := Word.andb (a * ! rand + 0w1, mask); ! rand);
       
    36 fun next_bit () = Word.andb (next (), max_bit) = 0w0;
       
    37 
       
    38 end;
       
    39