author | wenzelm |
Wed, 19 Dec 2007 23:49:28 +0100 | |
changeset 25720 | 71e0a5cb2885 |
parent 25719 | a51430528fe0 |
child 25721 | 5ae1dc2bb5ea |
permissions | -rw-r--r-- |
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 | 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 | 20 |
(*minimum length of unboxed words on all supported ML platforms*) |
25719 | 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 | 23 |
val range = 0x40000000; |
24 |
val mask = Word.fromInt (range - 1); |
|
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 |