74189
|
1 |
(* Title: Tools/Spec_Check/base_generator.ML
|
|
2 |
Author: Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
|
|
3 |
Author: Christopher League
|
|
4 |
|
|
5 |
Basic random generators.
|
|
6 |
*)
|
|
7 |
|
|
8 |
signature BASE_GENERATOR =
|
|
9 |
sig
|
|
10 |
|
|
11 |
type rand
|
|
12 |
type 'a gen = rand -> 'a * rand
|
|
13 |
type ('a, 'b) co = 'a -> 'b gen -> 'b gen
|
|
14 |
|
|
15 |
val new : unit -> rand
|
|
16 |
val range : int * int -> rand -> int * rand
|
|
17 |
type ('a, 'b) reader = 'b -> ('a * 'b) option
|
|
18 |
|
|
19 |
val lift : 'a -> 'a gen
|
|
20 |
val select : 'a vector -> 'a gen
|
|
21 |
val choose : 'a gen vector -> 'a gen
|
|
22 |
val choose' : (int * 'a gen) vector -> 'a gen
|
|
23 |
val selectL : 'a list -> 'a gen
|
|
24 |
val chooseL : 'a gen list -> 'a gen
|
|
25 |
val chooseL' : (int * 'a gen) list -> 'a gen
|
|
26 |
val filter : ('a -> bool) -> 'a gen -> 'a gen
|
|
27 |
|
|
28 |
val zip : ('a gen * 'b gen) -> ('a * 'b) gen
|
|
29 |
val zip3 : ('a gen * 'b gen * 'c gen) -> ('a * 'b * 'c) gen
|
|
30 |
val zip4 : ('a gen * 'b gen * 'c gen * 'd gen) -> ('a * 'b * 'c * 'd) gen
|
|
31 |
val map : ('a -> 'b) -> 'a gen -> 'b gen
|
|
32 |
val map2 : ('a * 'b -> 'c) -> ('a gen * 'b gen) -> 'c gen
|
|
33 |
val map3 : ('a * 'b * 'c -> 'd) -> ('a gen * 'b gen * 'c gen) -> 'd gen
|
|
34 |
val map4 : ('a * 'b * 'c * 'd -> 'e) -> ('a gen * 'b gen * 'c gen * 'd gen) -> 'e gen
|
|
35 |
|
|
36 |
val flip : bool gen
|
|
37 |
val flip' : int * int -> bool gen
|
|
38 |
|
|
39 |
val list : bool gen -> 'a gen -> 'a list gen
|
|
40 |
val option : bool gen -> 'a gen -> 'a option gen
|
|
41 |
val vector : (int * (int -> 'a) -> 'b) -> int gen * 'a gen -> 'b gen
|
|
42 |
|
|
43 |
val variant : (int, 'b) co
|
|
44 |
val arrow : ('a, 'b) co * 'b gen -> ('a -> 'b) gen
|
|
45 |
val cobool : (bool, 'b) co
|
|
46 |
val colist : ('a, 'b) co -> ('a list, 'b) co
|
|
47 |
val coopt : ('a, 'b) co -> ('a option, 'b) co
|
|
48 |
|
|
49 |
type stream
|
|
50 |
val start : rand -> stream
|
|
51 |
val limit : int -> 'a gen -> ('a, stream) reader
|
|
52 |
|
|
53 |
end
|
|
54 |
|
|
55 |
structure Base_Generator : BASE_GENERATOR =
|
|
56 |
struct
|
|
57 |
|
|
58 |
(* random number engine *)
|
|
59 |
|
|
60 |
type rand = real
|
|
61 |
|
|
62 |
val a = 16807.0
|
|
63 |
val m = 2147483647.0
|
|
64 |
|
|
65 |
fun nextrand seed =
|
|
66 |
let
|
|
67 |
val t = a * seed
|
|
68 |
in
|
|
69 |
t - m * real (floor (t / m))
|
|
70 |
end
|
|
71 |
|
|
72 |
val new = nextrand o Time.toReal o Time.now
|
|
73 |
|
|
74 |
fun range (min, max) =
|
|
75 |
if min > max then raise Domain (* TODO: raise its own error *)
|
|
76 |
else fn r => (min + (floor (real (max - min + 1) * r / m)), nextrand r)
|
|
77 |
|
|
78 |
fun split r =
|
|
79 |
let
|
|
80 |
val r = r / a
|
|
81 |
val r0 = real (floor r)
|
|
82 |
val r1 = r - r0
|
|
83 |
in
|
|
84 |
(nextrand r0, nextrand r1)
|
|
85 |
end
|
|
86 |
|
|
87 |
(* generators *)
|
|
88 |
|
|
89 |
type 'a gen = rand -> 'a * rand
|
|
90 |
type ('a, 'b) reader = 'b -> ('a * 'b) option
|
|
91 |
|
|
92 |
fun lift obj r = (obj, r)
|
|
93 |
|
|
94 |
local (* Isabelle does not use vectors? *)
|
|
95 |
fun explode ((freq, gen), acc) =
|
|
96 |
List.tabulate (freq, fn _ => gen) @ acc
|
|
97 |
in
|
|
98 |
fun choose v r =
|
|
99 |
let val (i, r) = range(0, Vector.length v - 1) r
|
|
100 |
in Vector.sub (v, i) r end
|
|
101 |
fun choose' v = choose (Vector.fromList (Vector.foldr explode [] v))
|
|
102 |
fun select v = choose (Vector.map lift v)
|
|
103 |
end
|
|
104 |
|
|
105 |
fun chooseL l = choose (Vector.fromList l)
|
|
106 |
fun chooseL' l = choose' (Vector.fromList l)
|
|
107 |
fun selectL l = select (Vector.fromList l)
|
|
108 |
|
|
109 |
fun zip (g1, g2) = g1 #-> (fn x1 => g2 #-> (fn x2 => pair (x1, x2)))
|
|
110 |
|
|
111 |
fun zip3 (g1, g2, g3) =
|
|
112 |
zip (g1, zip (g2, g3)) #-> (fn (x1, (x2, x3)) => pair (x1, x2, x3))
|
|
113 |
|
|
114 |
fun zip4 (g1, g2, g3, g4) =
|
|
115 |
zip (zip (g1, g2), zip (g3, g4)) #-> (fn ((x1, x2), (x3, x4)) => pair (x1, x2, x3, x4))
|
|
116 |
|
|
117 |
fun map f g = apfst f o g
|
|
118 |
|
|
119 |
fun map2 f = map f o zip
|
|
120 |
fun map3 f = map f o zip3
|
|
121 |
fun map4 f = map f o zip4
|
|
122 |
|
|
123 |
fun filter p gen r =
|
|
124 |
let
|
|
125 |
fun loop (x, r) = if p x then (x, r) else loop (gen r)
|
|
126 |
in
|
|
127 |
loop (gen r)
|
|
128 |
end
|
|
129 |
|
|
130 |
val flip = selectL [true, false]
|
|
131 |
fun flip' (p, q) = chooseL' [(p, lift true), (q, lift false)]
|
|
132 |
|
|
133 |
fun list flip g r =
|
|
134 |
case flip r of
|
|
135 |
(true, r) => ([], r)
|
|
136 |
| (false, r) =>
|
|
137 |
let
|
|
138 |
val (x,r) = g r
|
|
139 |
val (xs,r) = list flip g r
|
|
140 |
in (x::xs, r) end
|
|
141 |
|
|
142 |
fun option flip g r =
|
|
143 |
case flip r of
|
|
144 |
(true, r) => (NONE, r)
|
|
145 |
| (false, r) => map SOME g r
|
|
146 |
|
|
147 |
fun vector tabulate (int, elem) r =
|
|
148 |
let
|
|
149 |
val (n, r) = int r
|
|
150 |
val p = Unsynchronized.ref r
|
|
151 |
fun g _ =
|
|
152 |
let
|
|
153 |
val (x,r) = elem(!p)
|
|
154 |
in x before p := r end
|
|
155 |
in
|
|
156 |
(tabulate(n, g), !p)
|
|
157 |
end
|
|
158 |
|
|
159 |
type stream = rand Unsynchronized.ref * int
|
|
160 |
|
|
161 |
fun start r = (Unsynchronized.ref r, 0)
|
|
162 |
|
|
163 |
fun limit max gen =
|
|
164 |
let
|
|
165 |
fun next (p, i) =
|
|
166 |
if i >= max then NONE
|
|
167 |
else
|
|
168 |
let val (x, r) = gen(!p)
|
|
169 |
in SOME(x, (p, i+1)) before p := r end
|
|
170 |
in
|
|
171 |
next
|
|
172 |
end
|
|
173 |
|
|
174 |
type ('a, 'b) co = 'a -> 'b gen -> 'b gen
|
|
175 |
|
|
176 |
fun variant v g r =
|
|
177 |
let
|
|
178 |
fun nth (i, r) =
|
|
179 |
let val (r1, r2) = split r
|
|
180 |
in if i = 0 then r1 else nth (i-1, r2) end
|
|
181 |
in
|
|
182 |
g (nth (v, r))
|
|
183 |
end
|
|
184 |
|
|
185 |
fun arrow (cogen, gen) r =
|
|
186 |
let
|
|
187 |
val (r1, r2) = split r
|
|
188 |
fun g x = fst (cogen x gen r1)
|
|
189 |
in (g, r2) end
|
|
190 |
|
|
191 |
fun cobool false = variant 0
|
|
192 |
| cobool true = variant 1
|
|
193 |
|
|
194 |
fun colist _ [] = variant 0
|
|
195 |
| colist co (x::xs) = variant 1 o co x o colist co xs
|
|
196 |
|
|
197 |
fun coopt _ NONE = variant 0
|
|
198 |
| coopt co (SOME x) = variant 1 o co x
|
|
199 |
|
|
200 |
end
|
|
201 |
|