22528
|
1 |
(* ID: $Id$
|
|
2 |
Author: Florian Haftmann, TU Muenchen
|
|
3 |
*)
|
|
4 |
|
26038
|
5 |
header {* A simple term generator *}
|
22528
|
6 |
|
|
7 |
theory Random
|
26038
|
8 |
imports State_Monad Code_Index List Eval
|
22528
|
9 |
begin
|
|
10 |
|
26038
|
11 |
subsection {* The random engine *}
|
|
12 |
|
|
13 |
types seed = "index \<times> index"
|
22528
|
14 |
|
26038
|
15 |
definition
|
|
16 |
"next" :: "seed \<Rightarrow> index \<times> seed"
|
|
17 |
where
|
|
18 |
"next s = (let
|
|
19 |
(v, w) = s;
|
|
20 |
k = v div 53668;
|
|
21 |
v' = 40014 * (v - k * 53668) - k * 12211;
|
|
22 |
v'' = (if v' < 0 then v' + 2147483563 else v');
|
|
23 |
l = w div 52774;
|
|
24 |
w' = 40692 * (w - l * 52774) - l * 3791;
|
|
25 |
w'' = (if w' < 0 then w' + 2147483399 else w');
|
|
26 |
z = v'' - w'';
|
|
27 |
z' = (if z < 1 then z + 2147483562 else z)
|
|
28 |
in (z', (v'', w'')))"
|
22528
|
29 |
|
|
30 |
definition
|
26038
|
31 |
split_seed :: "seed \<Rightarrow> seed \<times> seed"
|
|
32 |
where
|
|
33 |
"split_seed s = (let
|
|
34 |
(v, w) = s;
|
|
35 |
(v', w') = snd (next s);
|
|
36 |
v'' = (if v = 2147483562 then 1 else v + 1);
|
|
37 |
s'' = (v'', w');
|
|
38 |
w'' = (if w = 2147483398 then 1 else w + 1);
|
|
39 |
s''' = (v', w'')
|
|
40 |
in (s'', s'''))"
|
|
41 |
|
|
42 |
text {* Base selectors *}
|
|
43 |
|
|
44 |
primrec
|
|
45 |
pick :: "(nat \<times> 'a) list \<Rightarrow> nat \<Rightarrow> 'a"
|
|
46 |
where
|
|
47 |
"pick (x#xs) n = (if n < fst x then snd x else pick xs (n - fst x))"
|
22528
|
48 |
|
26038
|
49 |
function
|
|
50 |
iLogBase :: "index \<Rightarrow> index \<Rightarrow> index"
|
|
51 |
where
|
|
52 |
"iLogBase b i = (if b \<le> 1 \<or> i < b then 1 else 1 + iLogBase b (i div b))"
|
|
53 |
by pat_completeness auto
|
|
54 |
termination
|
|
55 |
by (relation "measure (nat_of_index o snd)")
|
|
56 |
(auto simp add: index)
|
22528
|
57 |
|
26038
|
58 |
function
|
|
59 |
range_aux :: "index \<Rightarrow> index \<Rightarrow> seed \<Rightarrow> index \<times> seed"
|
|
60 |
where
|
|
61 |
"range_aux k l s = (if k = 0 then (l, s) else
|
|
62 |
let (v, s') = next s
|
|
63 |
in range_aux (k - 1) (v + l * 2147483561) s')"
|
|
64 |
by pat_completeness auto
|
|
65 |
termination
|
|
66 |
by (relation "measure (nat_of_index o fst)")
|
|
67 |
(auto simp add: index)
|
22528
|
68 |
|
|
69 |
definition
|
26038
|
70 |
range :: "index \<Rightarrow> seed \<Rightarrow> index \<times> seed"
|
|
71 |
where
|
|
72 |
"range k s = (let
|
|
73 |
b = 2147483561;
|
|
74 |
n = iLogBase b k;
|
|
75 |
(v, s') = range_aux n 1 s
|
|
76 |
in (v mod k, s'))"
|
|
77 |
|
22528
|
78 |
definition
|
26038
|
79 |
select :: "'a list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed"
|
|
80 |
where
|
|
81 |
[simp]: "select xs s = (let
|
|
82 |
(k, s') = range (index_of_nat (length xs)) s
|
|
83 |
in (nth xs (nat_of_index k), s'))"
|
22528
|
84 |
|
26038
|
85 |
definition
|
|
86 |
select_weight :: "(nat \<times> 'a) list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed"
|
|
87 |
where
|
|
88 |
[simp]: "select_weight xs s = (let
|
|
89 |
(k, s') = range (foldr (op + \<circ> index_of_nat \<circ> fst) xs 0) s
|
|
90 |
in (pick xs (nat_of_index k), s'))"
|
|
91 |
|
|
92 |
(*lemma
|
22528
|
93 |
"select (x#xs) s = select_weight (map (Pair 1) (x#xs)) s"
|
|
94 |
proof (induct xs)
|
26038
|
95 |
case Nil show ?case apply (auto simp add: Let_def split_def)
|
22528
|
96 |
next
|
|
97 |
have map_fst_Pair: "!!xs y. map fst (map (Pair y) xs) = replicate (length xs) y"
|
|
98 |
proof -
|
|
99 |
fix xs
|
|
100 |
fix y
|
|
101 |
show "map fst (map (Pair y) xs) = replicate (length xs) y"
|
|
102 |
by (induct xs) simp_all
|
|
103 |
qed
|
|
104 |
have pick_nth: "!!xs n. n < length xs \<Longrightarrow> pick (map (Pair 1) xs) n = nth xs n"
|
|
105 |
proof -
|
|
106 |
fix xs
|
|
107 |
fix n
|
|
108 |
assume "n < length xs"
|
|
109 |
then show "pick (map (Pair 1) xs) n = nth xs n"
|
|
110 |
proof (induct xs arbitrary: n)
|
|
111 |
case Nil then show ?case by simp
|
|
112 |
next
|
|
113 |
case (Cons x xs) show ?case
|
|
114 |
proof (cases n)
|
|
115 |
case 0 then show ?thesis by simp
|
|
116 |
next
|
|
117 |
case (Suc _)
|
|
118 |
from Cons have "n < length (x # xs)" by auto
|
|
119 |
then have "n < Suc (length xs)" by simp
|
|
120 |
with Suc have "n - 1 < Suc (length xs) - 1" by auto
|
|
121 |
with Cons have "pick (map (Pair (1\<Colon>nat)) xs) (n - 1) = xs ! (n - 1)" by auto
|
|
122 |
with Suc show ?thesis by auto
|
|
123 |
qed
|
|
124 |
qed
|
|
125 |
qed
|
|
126 |
have sum_length: "!!xs. foldl (op +) 0 (map fst (map (Pair 1) xs)) = length xs"
|
|
127 |
proof -
|
|
128 |
have replicate_append:
|
|
129 |
"!!x xs y. replicate (length (x # xs)) y = replicate (length xs) y @ [y]"
|
|
130 |
by (simp add: replicate_app_Cons_same)
|
|
131 |
fix xs
|
|
132 |
show "foldl (op +) 0 (map fst (map (Pair 1) xs)) = length xs"
|
|
133 |
unfolding map_fst_Pair proof (induct xs)
|
|
134 |
case Nil show ?case by simp
|
|
135 |
next
|
|
136 |
case (Cons x xs) then show ?case unfolding replicate_append by simp
|
|
137 |
qed
|
|
138 |
qed
|
|
139 |
have pick_nth_random:
|
|
140 |
"!!x xs s. pick (map (Pair 1) (x#xs)) (fst (random (length (x#xs)) s)) = nth (x#xs) (fst (random (length (x#xs)) s))"
|
|
141 |
proof -
|
|
142 |
fix s
|
|
143 |
fix x
|
|
144 |
fix xs
|
|
145 |
have bound: "fst (random (length (x#xs)) s) < length (x#xs)" by (rule random_bound) simp
|
|
146 |
from pick_nth [OF bound] show
|
|
147 |
"pick (map (Pair 1) (x#xs)) (fst (random (length (x#xs)) s)) = nth (x#xs) (fst (random (length (x#xs)) s))" .
|
|
148 |
qed
|
|
149 |
have pick_nth_random_do:
|
|
150 |
"!!x xs s. (do n \<leftarrow> random (length (x#xs)); return (pick (map (Pair 1) (x#xs)) n) done) s =
|
|
151 |
(do n \<leftarrow> random (length (x#xs)); return (nth (x#xs) n) done) s"
|
|
152 |
unfolding monad_collapse split_def unfolding pick_nth_random ..
|
|
153 |
case (Cons x xs) then show ?case
|
|
154 |
unfolding select_weight_def sum_length pick_nth_random_do
|
|
155 |
by simp
|
26038
|
156 |
qed*)
|
22528
|
157 |
|
26038
|
158 |
text {* The @{text ML} interface *}
|
22528
|
159 |
|
|
160 |
ML {*
|
26038
|
161 |
structure Quickcheck =
|
22528
|
162 |
struct
|
|
163 |
|
26038
|
164 |
type seed = int * int;
|
22528
|
165 |
|
|
166 |
local
|
26038
|
167 |
|
|
168 |
val seed = ref (0, 0);
|
|
169 |
|
|
170 |
fun init () =
|
|
171 |
let
|
|
172 |
val now = Time.toNanoseconds (Time.now ());
|
|
173 |
val (q, s1) = IntInf.divMod (now, 2147483562);
|
|
174 |
val s2 = q mod 2147483398;
|
|
175 |
in seed := (s1 + 1, s2 + 1) end;
|
|
176 |
|
22528
|
177 |
in
|
26038
|
178 |
|
|
179 |
val seed = seed; (* FIXME *)
|
|
180 |
|
|
181 |
fun run f =
|
|
182 |
let
|
|
183 |
val (x, seed') = f (!seed);
|
|
184 |
val _ = seed := seed'
|
|
185 |
val _ = if fst (! seed) = 0 orelse snd (! seed) = 0 then
|
|
186 |
(warning "broken random seed"; init ())
|
|
187 |
else ()
|
|
188 |
in x end;
|
|
189 |
|
22528
|
190 |
end;
|
|
191 |
|
|
192 |
end;
|
|
193 |
*}
|
|
194 |
|
26038
|
195 |
|
|
196 |
subsection {* The @{text random} class *}
|
|
197 |
|
|
198 |
class random = type +
|
|
199 |
fixes random :: "index \<Rightarrow> seed \<Rightarrow> 'a \<times> seed"
|
|
200 |
|
|
201 |
-- {* FIXME dummy implementations *}
|
|
202 |
|
|
203 |
instantiation nat :: random
|
|
204 |
begin
|
|
205 |
|
|
206 |
definition
|
|
207 |
"random k = apfst nat_of_index \<circ> range k"
|
|
208 |
|
|
209 |
instance ..
|
|
210 |
|
|
211 |
end
|
|
212 |
|
|
213 |
instantiation bool :: random
|
|
214 |
begin
|
|
215 |
|
|
216 |
definition
|
|
217 |
"random _ = apfst (op = 0) \<circ> range 2"
|
|
218 |
|
|
219 |
instance ..
|
|
220 |
|
|
221 |
end
|
24226
|
222 |
|
26038
|
223 |
instantiation unit :: random
|
|
224 |
begin
|
|
225 |
|
|
226 |
definition
|
|
227 |
"random _ = Pair ()"
|
|
228 |
|
|
229 |
instance ..
|
|
230 |
|
|
231 |
end
|
|
232 |
|
|
233 |
instantiation "+" :: (random, random) random
|
|
234 |
begin
|
|
235 |
|
|
236 |
definition
|
|
237 |
"random n = (do
|
|
238 |
k \<leftarrow> next;
|
|
239 |
let l = k div 2;
|
|
240 |
(if k mod 2 = 0 then do
|
|
241 |
x \<leftarrow> random l;
|
|
242 |
return (Inl x)
|
|
243 |
done else do
|
|
244 |
x \<leftarrow> random l;
|
|
245 |
return (Inr x)
|
|
246 |
done)
|
|
247 |
done)"
|
|
248 |
|
|
249 |
instance ..
|
|
250 |
|
|
251 |
end
|
22528
|
252 |
|
26038
|
253 |
instantiation "*" :: (random, random) random
|
|
254 |
begin
|
|
255 |
|
|
256 |
definition
|
|
257 |
"random n = (do
|
|
258 |
x \<leftarrow> random n;
|
|
259 |
y \<leftarrow> random n;
|
|
260 |
return (x, y)
|
|
261 |
done)"
|
|
262 |
|
|
263 |
instance ..
|
|
264 |
|
|
265 |
end
|
|
266 |
|
|
267 |
instantiation int :: random
|
|
268 |
begin
|
|
269 |
|
|
270 |
definition
|
|
271 |
"random n = (do
|
|
272 |
(b, m) \<leftarrow> random n;
|
|
273 |
return (if b then int m else - int m)
|
|
274 |
done)"
|
|
275 |
|
|
276 |
instance ..
|
|
277 |
|
|
278 |
end
|
|
279 |
|
|
280 |
instantiation list :: (random) random
|
|
281 |
begin
|
22528
|
282 |
|
26038
|
283 |
primrec
|
|
284 |
random_list_aux
|
|
285 |
where
|
|
286 |
"random_list_aux 0 = Pair []"
|
|
287 |
| "random_list_aux (Suc n) = (do
|
|
288 |
x \<leftarrow> random (index_of_nat (Suc n));
|
|
289 |
xs \<leftarrow> random_list_aux n;
|
|
290 |
return (x#xs)
|
|
291 |
done)"
|
|
292 |
|
|
293 |
definition
|
|
294 |
[code func del]: "random n = random_list_aux (nat_of_index n)"
|
|
295 |
|
|
296 |
lemma [code func]:
|
|
297 |
"random n = (if n = 0 then return ([]::'a list)
|
|
298 |
else do
|
|
299 |
x \<leftarrow> random n;
|
|
300 |
xs \<leftarrow> random (n - 1);
|
|
301 |
return (x#xs)
|
|
302 |
done)"
|
|
303 |
unfolding random_list_def
|
|
304 |
by (cases "nat_of_index n", auto)
|
|
305 |
(cases n, auto)+
|
|
306 |
|
|
307 |
(*fun
|
|
308 |
random_list
|
|
309 |
where
|
|
310 |
"random_list n = (if n = 0 then (\<lambda>_. ([]::'a list))
|
|
311 |
else random n \<guillemotright>=\<^isub>R (\<lambda>x::'a. random_list (n - 1) \<guillemotright>=\<^isub>R (\<lambda>(xs::'a list) _. x#xs)))"*)
|
|
312 |
|
|
313 |
instance ..
|
22528
|
314 |
|
|
315 |
end
|
26038
|
316 |
|
|
317 |
code_reserved SML Quickcheck
|
|
318 |
|
|
319 |
|
|
320 |
subsection {* Quickcheck generator *}
|
|
321 |
|
|
322 |
ML {*
|
|
323 |
structure Quickcheck =
|
|
324 |
struct
|
|
325 |
|
|
326 |
open Quickcheck;
|
|
327 |
|
|
328 |
val eval_ref : (unit -> int -> int * int -> term list option * (int * int)) option ref = ref NONE;
|
|
329 |
|
|
330 |
fun mk_generator_expr prop tys =
|
|
331 |
let
|
|
332 |
val bounds = map_index (fn (i, ty) => (i, ty)) tys;
|
|
333 |
val result = list_comb (prop, map (fn (i, _) => Bound (length tys - i - 1)) bounds);
|
|
334 |
val terms = map (fn (i, ty) => Const (@{const_name Eval.term_of}, ty --> @{typ term}) $ Bound (length tys - i - 1)) bounds;
|
|
335 |
val check = @{term "If \<Colon> bool \<Rightarrow> term list option \<Rightarrow> term list option \<Rightarrow> term list option"}
|
|
336 |
$ result $ @{term "None \<Colon> term list option"} $ (@{term "Some \<Colon> term list \<Rightarrow> term list option "} $ HOLogic.mk_list @{typ term} terms);
|
|
337 |
val return = @{term "Pair \<Colon> term list option \<Rightarrow> seed \<Rightarrow> term list option \<times> seed"};
|
|
338 |
fun mk_bindtyp ty = @{typ seed} --> HOLogic.mk_prodT (ty, @{typ seed});
|
|
339 |
fun mk_bindclause (i, ty) t = Const (@{const_name mbind}, mk_bindtyp ty
|
|
340 |
--> (ty --> mk_bindtyp @{typ "term list option"}) --> mk_bindtyp @{typ "term list option"})
|
|
341 |
$ (Const (@{const_name random}, @{typ index} --> mk_bindtyp ty)
|
|
342 |
$ Bound i) $ Abs ("a", ty, t);
|
|
343 |
val t = fold_rev mk_bindclause bounds (return $ check);
|
|
344 |
in Abs ("n", @{typ index}, t) end;
|
|
345 |
|
|
346 |
fun compile_generator_expr thy prop tys =
|
|
347 |
let
|
|
348 |
val f = CodePackage.eval_term ("Quickcheck.eval_ref", eval_ref) thy
|
|
349 |
(mk_generator_expr prop tys) [];
|
|
350 |
in f #> run #> (Option.map o map) (Code.postprocess_term thy) end;
|
|
351 |
|
|
352 |
end
|
|
353 |
*}
|
|
354 |
|
|
355 |
ML {* val f = Quickcheck.compile_generator_expr @{theory}
|
|
356 |
@{term "\<lambda>(n::nat) (m::nat) (q::nat). n = m + q + 1"} [@{typ nat}, @{typ nat}, @{typ nat}] *}
|
|
357 |
|
|
358 |
ML {* f 5 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
|
|
359 |
ML {* f 5 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
|
|
360 |
ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
|
|
361 |
ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
|
|
362 |
ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
|
|
363 |
ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
|
|
364 |
ML {* f 25 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
|
|
365 |
ML {* f 1 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
|
|
366 |
ML {* f 1 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
|
|
367 |
ML {* f 2 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
|
|
368 |
ML {* f 2 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
|
|
369 |
|
|
370 |
ML {* val f = Quickcheck.compile_generator_expr @{theory}
|
|
371 |
@{term "\<lambda>(n::int) (m::int) (q::int). n = m + q + 1"} [@{typ int}, @{typ int}, @{typ int}] *}
|
|
372 |
|
|
373 |
ML {* f 5 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
|
|
374 |
ML {* f 5 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
|
|
375 |
ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
|
|
376 |
ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
|
|
377 |
ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
|
|
378 |
ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
|
|
379 |
ML {* f 25 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
|
|
380 |
ML {* f 1 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
|
|
381 |
ML {* f 1 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
|
|
382 |
ML {* f 2 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
|
|
383 |
ML {* f 2 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
|
|
384 |
|
|
385 |
|
|
386 |
subsection {* Incremental function generator *}
|
|
387 |
|
|
388 |
ML {*
|
|
389 |
structure Quickcheck =
|
|
390 |
struct
|
|
391 |
|
|
392 |
open Quickcheck;
|
|
393 |
|
|
394 |
fun random_fun (eq : 'a -> 'a -> bool)
|
|
395 |
(random : seed -> 'b * seed)
|
|
396 |
(random_split : seed -> seed * seed)
|
|
397 |
(seed : seed) =
|
|
398 |
let
|
|
399 |
val (seed', seed'') = random_split seed;
|
|
400 |
val state = ref (seed', []);
|
|
401 |
fun random_fun' x =
|
|
402 |
let
|
|
403 |
val (seed, fun_map) = ! state;
|
|
404 |
in case AList.lookup (uncurry eq) fun_map x
|
|
405 |
of SOME y => y
|
|
406 |
| NONE => let
|
|
407 |
val (y, seed') = random seed;
|
|
408 |
val _ = state := (seed', (x, y) :: fun_map);
|
|
409 |
in y end
|
|
410 |
end;
|
|
411 |
in (random_fun', seed'') end;
|
|
412 |
|
|
413 |
end
|
|
414 |
*}
|
|
415 |
|
|
416 |
axiomatization
|
|
417 |
random_fun_aux :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> (seed \<Rightarrow> 'b \<times> seed)
|
|
418 |
\<Rightarrow> (seed \<Rightarrow> seed \<times> seed) \<Rightarrow> seed \<Rightarrow> ('a \<Rightarrow> 'b) \<times> seed"
|
|
419 |
|
|
420 |
code_const random_fun_aux (SML "Quickcheck.random'_fun")
|
|
421 |
|
|
422 |
instantiation "fun" :: (term_of, term_of) term_of
|
|
423 |
begin
|
|
424 |
|
|
425 |
instance ..
|
|
426 |
|
|
427 |
end
|
|
428 |
|
|
429 |
code_const "Eval.term_of :: ('a\<Colon>term_of \<Rightarrow> 'b\<Colon>term_of) \<Rightarrow> _"
|
|
430 |
(SML "(fn '_ => Const (\"arbitrary\", dummyT))")
|
|
431 |
|
|
432 |
instantiation "fun" :: (eq, random) random
|
|
433 |
begin
|
|
434 |
|
|
435 |
definition
|
|
436 |
"random n = random_fun_aux (op =) (random n) split_seed"
|
|
437 |
|
|
438 |
instance ..
|
|
439 |
|
|
440 |
end
|
|
441 |
|
|
442 |
ML {* val f = Quickcheck.compile_generator_expr @{theory}
|
|
443 |
@{term "\<lambda>f k. int (f k) = k"} [@{typ "int \<Rightarrow> nat"}, @{typ int}] *}
|
|
444 |
|
|
445 |
ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
|
|
446 |
ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
|
|
447 |
ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
|
|
448 |
ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
|
|
449 |
ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
|
|
450 |
ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
|
|
451 |
|
|
452 |
end
|