src/Tools/random_word.ML
changeset 25742 1051ef9d87c4
parent 25728 71e33d95ac55
child 30161 c26e515f1c29
equal deleted inserted replaced
25741:2d102ddaca8b 25742:1051ef9d87c4
     7 randomness.
     7 randomness.
     8 *)
     8 *)
     9 
     9 
    10 signature RANDOM_WORD =
    10 signature RANDOM_WORD =
    11 sig
    11 sig
    12   val range: int
    12   val max_word: word
    13   val range_real: real
    13   val step: word -> word
    14   val next: unit -> word
    14   val next_word: unit -> word
    15   val next_bit: unit -> bool
    15   val next_bool: unit -> bool
       
    16   val next_int: int -> int -> int
       
    17   val next_real: unit -> real
       
    18   val pick_any: 'a list -> 'a
       
    19   val pick_weighted: (int * 'a) list -> 'a
    16 end;
    20 end;
    17 
    21 
    18 structure RandomWord: RANDOM_WORD =
    22 structure RandomWord: RANDOM_WORD =
    19 struct
    23 struct
    20 
    24 
       
    25 (* random words: 0w0 <= result <= max_word *)
       
    26 
    21 (*minimum length of unboxed words on all supported ML platforms*)
    27 (*minimum length of unboxed words on all supported ML platforms*)
    22 val _ = Word.wordSize >= 30 orelse raise Fail ("Bad platform word size");
    28 val _ = Word.wordSize >= 30
       
    29   orelse raise Fail ("Bad platform word size");
    23 
    30 
    24 val range = 0x40000000;
    31 val max_word = 0wx3FFFFFFF;
    25 val range_real = 1073741824.0;
    32 val top_bit = 0wx20000000;
    26 val mask = Word.fromInt (range - 1);
       
    27 val max_bit = Word.fromInt (range div 2);
       
    28 
    33 
    29 (*multiplier according to Borosh and Niederreiter (for m = 2^30),
    34 (*multiplier according to Borosh and Niederreiter (for modulus = 2^30),
    30   cf. http://random.mat.sbg.ac.at/~charly/server/server.html*)
    35   see http://random.mat.sbg.ac.at/~charly/server/server.html*)
    31 val a = 0w777138309;
    36 val a = 0w777138309;
       
    37 fun step x = Word.andb (a * x + 0w1, max_word);
    32 
    38 
    33 (*generator*)
    39 local val rand = ref 0w1
    34 val rand = ref 0w0;
    40 in fun next_word () = (change rand step; ! rand) end;
    35 fun next () = (rand := Word.andb (a * ! rand + 0w1, mask); ! rand);
    41 
    36 fun next_bit () = Word.andb (next (), max_bit) = 0w0;
    42 (*NB: higher bits are more random than lower ones*)
       
    43 fun next_bool () = Word.andb (next_word (), top_bit) = 0w0;
       
    44 
       
    45 
       
    46 (* random integers: i <= result <= j *)
       
    47 
       
    48 val max_int = Word.toInt max_word;
       
    49 
       
    50 fun next_int i j =
       
    51   let val k = j - i in
       
    52     if k < 0 orelse k > max_int then raise Fail ("next_int: out of range")
       
    53     else if k < max_int then i + Word.toInt (Word.mod (next_word (), Word.fromInt (k + 1)))
       
    54     else i + Word.toInt (next_word ())
       
    55   end;
       
    56 
       
    57 
       
    58 (* random reals: 0.0 <= result < 1.0 *)
       
    59 
       
    60 val scaling = real max_int + 1.0;
       
    61 fun next_real () = real (Word.toInt (next_word ())) / scaling;
       
    62 
       
    63 
       
    64 (* random list elements *)
       
    65 
       
    66 fun pick_any [] = raise Empty
       
    67   | pick_any xs = nth xs (next_int 0 (length xs - 1));
       
    68 
       
    69 fun pick_weighted xs =
       
    70   let
       
    71     val total = fold (fn (k, _) => fn i =>
       
    72       if k < 0 then raise Fail ("Bad weight: " ^ string_of_int k) else k + i) xs 0;
       
    73     fun pick n ((k, x) :: xs) =
       
    74         if n <= k then x else pick (n - k) xs
       
    75       | pick _ [] = raise Empty;
       
    76   in if total = 0 then raise Empty else pick (next_int 1 total) xs end;
    37 
    77 
    38 end;
    78 end;
    39 
    79