author | wenzelm |
Sat, 29 Mar 2008 19:14:03 +0100 | |
changeset 26481 | 92e901171cc8 |
parent 25742 | 1051ef9d87c4 |
child 30161 | c26e515f1c29 |
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 |
25742 | 12 |
val max_word: word |
13 |
val step: word -> word |
|
14 |
val next_word: unit -> word |
|
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 |
|
25728
71e33d95ac55
moved Pure/General/random_word.ML to Tools/random_word.ML;
wenzelm
parents:
diff
changeset
|
20 |
end; |
71e33d95ac55
moved Pure/General/random_word.ML to Tools/random_word.ML;
wenzelm
parents:
diff
changeset
|
21 |
|
71e33d95ac55
moved Pure/General/random_word.ML to Tools/random_word.ML;
wenzelm
parents:
diff
changeset
|
22 |
structure RandomWord: RANDOM_WORD = |
71e33d95ac55
moved Pure/General/random_word.ML to Tools/random_word.ML;
wenzelm
parents:
diff
changeset
|
23 |
struct |
71e33d95ac55
moved Pure/General/random_word.ML to Tools/random_word.ML;
wenzelm
parents:
diff
changeset
|
24 |
|
25742 | 25 |
(* random words: 0w0 <= result <= max_word *) |
26 |
||
25728
71e33d95ac55
moved Pure/General/random_word.ML to Tools/random_word.ML;
wenzelm
parents:
diff
changeset
|
27 |
(*minimum length of unboxed words on all supported ML platforms*) |
25742 | 28 |
val _ = Word.wordSize >= 30 |
29 |
orelse raise Fail ("Bad platform word size"); |
|
30 |
||
31 |
val max_word = 0wx3FFFFFFF; |
|
32 |
val top_bit = 0wx20000000; |
|
25728
71e33d95ac55
moved Pure/General/random_word.ML to Tools/random_word.ML;
wenzelm
parents:
diff
changeset
|
33 |
|
25742 | 34 |
(*multiplier according to Borosh and Niederreiter (for modulus = 2^30), |
35 |
see http://random.mat.sbg.ac.at/~charly/server/server.html*) |
|
36 |
val a = 0w777138309; |
|
37 |
fun step x = Word.andb (a * x + 0w1, max_word); |
|
38 |
||
39 |
local val rand = ref 0w1 |
|
40 |
in fun next_word () = (change rand step; ! rand) end; |
|
41 |
||
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; |
|
25728
71e33d95ac55
moved Pure/General/random_word.ML to Tools/random_word.ML;
wenzelm
parents:
diff
changeset
|
49 |
|
25742 | 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 |
||
25728
71e33d95ac55
moved Pure/General/random_word.ML to Tools/random_word.ML;
wenzelm
parents:
diff
changeset
|
63 |
|
25742 | 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; |
|
25728
71e33d95ac55
moved Pure/General/random_word.ML to Tools/random_word.ML;
wenzelm
parents:
diff
changeset
|
77 |
|
71e33d95ac55
moved Pure/General/random_word.ML to Tools/random_word.ML;
wenzelm
parents:
diff
changeset
|
78 |
end; |
71e33d95ac55
moved Pure/General/random_word.ML to Tools/random_word.ML;
wenzelm
parents:
diff
changeset
|
79 |