1 (* Title: Tools/Spec_Check/generator.ML |
|
2 Author: Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen |
|
3 Author: Christopher League |
|
4 |
|
5 Random generators for Isabelle/ML's types. |
|
6 *) |
|
7 |
|
8 signature GENERATOR = sig |
|
9 include BASE_GENERATOR |
|
10 (* text generators *) |
|
11 val char : char gen |
|
12 val charRange : char * char -> char gen |
|
13 val charFrom : string -> char gen |
|
14 val charByType : (char -> bool) -> char gen |
|
15 val string : (int gen * char gen) -> string gen |
|
16 val substring : string gen -> substring gen |
|
17 val cochar : (char, 'b) co |
|
18 val costring : (string, 'b) co |
|
19 val cosubstring : (substring, 'b) co |
|
20 (* integer generators *) |
|
21 val int : int gen |
|
22 val int_pos : int gen |
|
23 val int_neg : int gen |
|
24 val int_nonpos : int gen |
|
25 val int_nonneg : int gen |
|
26 val coint : (int, 'b) co |
|
27 (* real generators *) |
|
28 val real : real gen |
|
29 val real_frac : real gen |
|
30 val real_pos : real gen |
|
31 val real_neg : real gen |
|
32 val real_nonpos : real gen |
|
33 val real_nonneg : real gen |
|
34 val real_finite : real gen |
|
35 (* function generators *) |
|
36 val function_const : 'c * 'b gen -> ('a -> 'b) gen |
|
37 val function_strict : int -> ''a gen * 'b gen -> (''a -> 'b) gen |
|
38 val function_lazy : ''a gen * 'b gen -> (''a -> 'b) gen |
|
39 val unit : unit gen |
|
40 val ref' : 'a gen -> 'a Unsynchronized.ref gen |
|
41 (* more generators *) |
|
42 val term : int -> term gen |
|
43 val typ : int -> typ gen |
|
44 |
|
45 val stream : stream |
|
46 end |
|
47 |
|
48 structure Generator : GENERATOR = |
|
49 struct |
|
50 |
|
51 open Base_Generator |
|
52 |
|
53 val stream = start (new()) |
|
54 |
|
55 type 'a gen = rand -> 'a * rand |
|
56 type ('a, 'b) co = 'a -> 'b gen -> 'b gen |
|
57 |
|
58 (* text *) |
|
59 |
|
60 type char = Char.char |
|
61 type string = String.string |
|
62 type substring = Substring.substring |
|
63 |
|
64 |
|
65 val char = map Char.chr (range (0, Char.maxOrd)) |
|
66 fun charRange (lo, hi) = map Char.chr (range (Char.ord lo, Char.ord hi)) |
|
67 |
|
68 fun charFrom s = |
|
69 choose (Vector.tabulate (String.size s, fn i => lift (String.sub (s, i)))) |
|
70 |
|
71 fun charByType p = filter p char |
|
72 |
|
73 val string = vector CharVector.tabulate |
|
74 |
|
75 fun substring gen r = |
|
76 let |
|
77 val (s, r') = gen r |
|
78 val (i, r'') = range (0, String.size s) r' |
|
79 val (j, r''') = range (0, String.size s - i) r'' |
|
80 in |
|
81 (Substring.substring (s, i, j), r''') |
|
82 end |
|
83 |
|
84 fun cochar c = |
|
85 if Char.ord c = 0 then variant 0 |
|
86 else variant 1 o cochar (Char.chr (Char.ord c div 2)) |
|
87 |
|
88 fun cosubstring s = Substring.foldr (fn (c,v) => cochar c o v) (variant 0) s |
|
89 |
|
90 fun costring s = cosubstring (Substring.full s) |
|
91 |
|
92 (* integers *) |
|
93 val digit = charRange (#"0", #"9") |
|
94 val nonzero = string (lift 1, charRange (#"1", #"9")) |
|
95 fun digits' n = string (range (0, n-1), digit) |
|
96 fun digits n = map2 op^ (nonzero, digits' n) |
|
97 |
|
98 val maxDigits = 64 |
|
99 val ratio = 49 |
|
100 |
|
101 fun pos_or_neg f r = |
|
102 let |
|
103 val (s, r') = digits maxDigits r |
|
104 in (f (the (Int.fromString s)), r') end |
|
105 |
|
106 val int_pos = pos_or_neg I |
|
107 val int_neg = pos_or_neg Int.~ |
|
108 val zero = lift 0 |
|
109 |
|
110 val int_nonneg = chooseL' [(1, zero), (ratio, int_pos)] |
|
111 val int_nonpos = chooseL' [(1, zero), (ratio, int_neg)] |
|
112 val int = chooseL [int_nonneg, int_nonpos] |
|
113 |
|
114 fun coint n = |
|
115 if n = 0 then variant 0 |
|
116 else if n < 0 then variant 1 o coint (~ n) |
|
117 else variant 2 o coint (n div 2) |
|
118 |
|
119 (* reals *) |
|
120 val digits = string (range(1, Real.precision), charRange(#"0", #"9")) |
|
121 |
|
122 fun real_frac r = |
|
123 let val (s, r') = digits r |
|
124 in (the (Real.fromString s), r') end |
|
125 |
|
126 val {exp=minExp,...} = Real.toManExp Real.minPos |
|
127 val {exp=maxExp,...} = Real.toManExp Real.posInf |
|
128 |
|
129 val ratio = 99 |
|
130 |
|
131 fun mk r = |
|
132 let |
|
133 val (a, r') = digits r |
|
134 val (b, r'') = digits r' |
|
135 val (e, r''') = range (minExp div 4, maxExp div 4) r'' |
|
136 val x = String.concat [a, ".", b, "E", Int.toString e] |
|
137 in |
|
138 (the (Real.fromString x), r''') |
|
139 end |
|
140 |
|
141 val real_pos = chooseL' (List.map ((pair 1) o lift) |
|
142 [Real.posInf, Real.maxFinite, Real.minPos, Real.minNormalPos] @ [(ratio, mk)]) |
|
143 |
|
144 val real_neg = map Real.~ real_pos |
|
145 |
|
146 val real_zero = Real.fromInt 0 |
|
147 val real_nonneg = chooseL' [(1, lift real_zero), (ratio, real_pos)] |
|
148 val real_nonpos = chooseL' [(1, lift real_zero), (ratio, real_neg)] |
|
149 |
|
150 val real = chooseL [real_nonneg, real_nonpos] |
|
151 |
|
152 val real_finite = filter Real.isFinite real |
|
153 |
|
154 (*alternate list generator - uses an integer generator to determine list length*) |
|
155 fun list' int gen = vector List.tabulate (int, gen); |
|
156 |
|
157 (* more function generators *) |
|
158 |
|
159 fun function_const (_, gen2) r = |
|
160 let |
|
161 val (v, r') = gen2 r |
|
162 in (fn _ => v, r') end; |
|
163 |
|
164 fun function_strict size (gen1, gen2) r = |
|
165 let |
|
166 val (def, r') = gen2 r |
|
167 val (table, r'') = list' (fn s => (size, s)) (zip (gen1, gen2)) r' |
|
168 in (fn v1 => the_default def (AList.lookup (op =) table v1), r'') end; |
|
169 |
|
170 fun function_lazy (gen1, gen2) r = |
|
171 let |
|
172 val (initial1, r') = gen1 r |
|
173 val (initial2, internal) = gen2 r' |
|
174 val seed = Unsynchronized.ref internal |
|
175 val table = Unsynchronized.ref [(initial1, initial2)] |
|
176 fun new_entry k = |
|
177 let |
|
178 val (new_val, new_seed) = gen2 (!seed) |
|
179 val _ = seed := new_seed |
|
180 val _ = table := AList.update (op =) (k, new_val) (!table) |
|
181 in new_val end |
|
182 in |
|
183 (fn v1 => |
|
184 case AList.lookup (op =) (!table) v1 of |
|
185 NONE => new_entry v1 |
|
186 | SOME v2 => v2, r') |
|
187 end; |
|
188 |
|
189 (* unit *) |
|
190 |
|
191 fun unit r = ((), r); |
|
192 |
|
193 (* references *) |
|
194 |
|
195 fun ref' gen r = |
|
196 let val (value, r') = gen r |
|
197 in (Unsynchronized.ref value, r') end; |
|
198 |
|
199 (* types and terms *) |
|
200 |
|
201 val sort_string = selectL ["sort1", "sort2", "sort3"]; |
|
202 val type_string = selectL ["TCon1", "TCon2", "TCon3"]; |
|
203 val tvar_string = selectL ["a", "b", "c"]; |
|
204 |
|
205 val const_string = selectL ["c1", "c2", "c3"]; |
|
206 val var_string = selectL ["x", "y", "z"]; |
|
207 val index = selectL [0, 1, 2, 3]; |
|
208 val bound_index = selectL [0, 1, 2, 3]; |
|
209 |
|
210 val sort = list (flip' (1, 2)) sort_string; |
|
211 |
|
212 fun typ n = |
|
213 let |
|
214 fun type' m = map Type (zip (type_string, list (flip' (1, 3)) (typ m))) |
|
215 val tfree = map TFree (zip (tvar_string, sort)) |
|
216 val tvar = map TVar (zip (zip (tvar_string, index), sort)) |
|
217 in |
|
218 if n = 0 then chooseL [tfree, tvar] |
|
219 else chooseL [type' (n div 2), tfree, tvar] |
|
220 end; |
|
221 |
|
222 fun term n = |
|
223 let |
|
224 val const = map Const (zip (const_string, typ 10)) |
|
225 val free = map Free (zip (var_string, typ 10)) |
|
226 val var = map Var (zip (zip (var_string, index), typ 10)) |
|
227 val bound = map Bound bound_index |
|
228 fun abs m = map Abs (zip3 (var_string, typ 10, term m)) |
|
229 fun app m = map (op $) (zip (term m, term m)) |
|
230 in |
|
231 if n = 0 then chooseL [const, free, var, bound] |
|
232 else chooseL [const, free, var, bound, abs (n - 1), app (n div 2)] |
|
233 end; |
|
234 |
|
235 end |
|