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