|
1 (* Title: HOL/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 open Vector (* Isabelle does not use vectors? *) |
|
95 fun explode ((freq, gen), acc) = |
|
96 List.tabulate (freq, fn _ => gen) @ acc |
|
97 in fun choose v r = |
|
98 let val (i, r) = range(0, length v - 1) r |
|
99 in sub (v, i) r |
|
100 end |
|
101 fun choose' v = choose (fromList (foldr explode nil v)) |
|
102 fun select v = choose (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) => (nil, 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 |