src/Tools/random_word.ML
changeset 32740 9dd0a2f83429
parent 30161 c26e515f1c29
child 33513 b2259183e282
equal deleted inserted replaced
32739:31e75ad9ae17 32740:9dd0a2f83429
    33 (*multiplier according to Borosh and Niederreiter (for modulus = 2^30),
    33 (*multiplier according to Borosh and Niederreiter (for modulus = 2^30),
    34   see http://random.mat.sbg.ac.at/~charly/server/server.html*)
    34   see http://random.mat.sbg.ac.at/~charly/server/server.html*)
    35 val a = 0w777138309;
    35 val a = 0w777138309;
    36 fun step x = Word.andb (a * x + 0w1, max_word);
    36 fun step x = Word.andb (a * x + 0w1, max_word);
    37 
    37 
    38 local val rand = ref 0w1
    38 local val rand = Unsynchronized.ref 0w1
    39 in fun next_word () = (change rand step; ! rand) end;
    39 in fun next_word () = (Unsynchronized.change rand step; ! rand) end;
    40 
    40 
    41 (*NB: higher bits are more random than lower ones*)
    41 (*NB: higher bits are more random than lower ones*)
    42 fun next_bool () = Word.andb (next_word (), top_bit) = 0w0;
    42 fun next_bool () = Word.andb (next_word (), top_bit) = 0w0;
    43 
    43 
    44 
    44