62585
|
1 |
(* Title: Pure/General/random.ML
|
59172
|
2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
3 |
|
|
4 |
Pseudo random numbers.
|
|
5 |
*)
|
|
6 |
|
|
7 |
signature RANDOM =
|
|
8 |
sig
|
|
9 |
val random: unit -> real
|
|
10 |
exception RANDOM
|
|
11 |
val random_range: int -> int -> int
|
|
12 |
end;
|
|
13 |
|
|
14 |
structure Random: RANDOM =
|
|
15 |
struct
|
|
16 |
|
|
17 |
fun rmod x y = x - y * Real.realFloor (x / y);
|
|
18 |
|
|
19 |
local
|
|
20 |
val a = 16807.0;
|
|
21 |
val m = 2147483647.0;
|
|
22 |
val random_seed = Synchronized.var "random_seed" 1.0;
|
|
23 |
in
|
|
24 |
|
|
25 |
fun random () =
|
|
26 |
Synchronized.change_result random_seed
|
|
27 |
(fn r => let val r' = rmod (a * r) m in (r', r') end);
|
|
28 |
|
|
29 |
end;
|
|
30 |
|
|
31 |
exception RANDOM;
|
|
32 |
|
|
33 |
fun random_range l h =
|
|
34 |
if h < l orelse l < 0 then raise RANDOM
|
|
35 |
else l + Real.floor (rmod (random ()) (real (h - l + 1)));
|
|
36 |
|
|
37 |
end;
|
|
38 |
|