equal
deleted
inserted
replaced
1 (* Title: Pure/General/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 |
|