1 (* Author: Florian Haftmann, TU Muenchen *) |
|
2 |
|
3 header {* A simple counterexample generator *} |
|
4 |
|
5 theory Quickcheck |
|
6 imports Random Code_Eval Map |
|
7 begin |
|
8 |
|
9 subsection {* The @{text random} class *} |
|
10 |
|
11 class random = typerep + |
|
12 fixes random :: "index \<Rightarrow> seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> seed" |
|
13 |
|
14 text {* Type @{typ "'a itself"} *} |
|
15 |
|
16 instantiation itself :: ("{type, typerep}") random |
|
17 begin |
|
18 |
|
19 definition |
|
20 "random _ = return (TYPE('a), \<lambda>u. Code_Eval.Const (STR ''TYPE'') TYPEREP('a))" |
|
21 |
|
22 instance .. |
|
23 |
|
24 end |
|
25 |
|
26 text {* Type @{typ "'a \<Rightarrow> 'b"} *} |
|
27 |
|
28 ML {* |
|
29 structure Random_Engine = |
|
30 struct |
|
31 |
|
32 open Random_Engine; |
|
33 |
|
34 fun random_fun (T1 : typ) (T2 : typ) (eq : 'a -> 'a -> bool) (term_of : 'a -> term) |
|
35 (random : Random_Engine.seed -> ('b * (unit -> term)) * Random_Engine.seed) |
|
36 (random_split : Random_Engine.seed -> Random_Engine.seed * Random_Engine.seed) |
|
37 (seed : Random_Engine.seed) = |
|
38 let |
|
39 val (seed', seed'') = random_split seed; |
|
40 val state = ref (seed', [], Const (@{const_name undefined}, T1 --> T2)); |
|
41 val fun_upd = Const (@{const_name fun_upd}, |
|
42 (T1 --> T2) --> T1 --> T2 --> T1 --> T2); |
|
43 fun random_fun' x = |
|
44 let |
|
45 val (seed, fun_map, f_t) = ! state; |
|
46 in case AList.lookup (uncurry eq) fun_map x |
|
47 of SOME y => y |
|
48 | NONE => let |
|
49 val t1 = term_of x; |
|
50 val ((y, t2), seed') = random seed; |
|
51 val fun_map' = (x, y) :: fun_map; |
|
52 val f_t' = fun_upd $ f_t $ t1 $ t2 (); |
|
53 val _ = state := (seed', fun_map', f_t'); |
|
54 in y end |
|
55 end; |
|
56 fun term_fun' () = #3 (! state); |
|
57 in ((random_fun', term_fun'), seed'') end; |
|
58 |
|
59 end |
|
60 *} |
|
61 |
|
62 axiomatization |
|
63 random_fun_aux :: "typerep \<Rightarrow> typerep \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> term) |
|
64 \<Rightarrow> (seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> seed) \<Rightarrow> (seed \<Rightarrow> seed \<times> seed) |
|
65 \<Rightarrow> seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> seed" |
|
66 |
|
67 code_const random_fun_aux (SML "Random'_Engine.random'_fun") |
|
68 |
|
69 instantiation "fun" :: ("{eq, term_of}", "{type, random}") random |
|
70 begin |
|
71 |
|
72 definition random_fun :: "index \<Rightarrow> seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> seed" where |
|
73 "random n = random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Eval.term_of (random n) split_seed" |
|
74 |
|
75 instance .. |
|
76 |
|
77 end |
|
78 |
|
79 code_reserved SML Random_Engine |
|
80 |
|
81 text {* Datatypes *} |
|
82 |
|
83 definition |
|
84 collapse :: "('a \<Rightarrow> ('a \<Rightarrow> 'b \<times> 'a) \<times> 'a) \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where |
|
85 "collapse f = (do g \<leftarrow> f; g done)" |
|
86 |
|
87 ML {* |
|
88 structure StateMonad = |
|
89 struct |
|
90 |
|
91 fun liftT T sT = sT --> HOLogic.mk_prodT (T, sT); |
|
92 fun liftT' sT = sT --> sT; |
|
93 |
|
94 fun return T sT x = Const (@{const_name return}, T --> liftT T sT) $ x; |
|
95 |
|
96 fun scomp T1 T2 sT f g = Const (@{const_name scomp}, |
|
97 liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g; |
|
98 |
|
99 end; |
|
100 *} |
|
101 |
|
102 lemma random'_if: |
|
103 fixes random' :: "index \<Rightarrow> index \<Rightarrow> seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> seed" |
|
104 assumes "random' 0 j = (\<lambda>s. undefined)" |
|
105 and "\<And>i. random' (Suc_index i) j = rhs2 i" |
|
106 shows "random' i j s = (if i = 0 then undefined else rhs2 (i - 1) s)" |
|
107 by (cases i rule: index.exhaust) (insert assms, simp_all) |
|
108 |
|
109 setup {* |
|
110 let |
|
111 exception REC of string; |
|
112 exception TYP of string; |
|
113 fun mk_collapse thy ty = Sign.mk_const thy |
|
114 (@{const_name collapse}, [@{typ seed}, ty]); |
|
115 fun term_ty ty = HOLogic.mk_prodT (ty, @{typ "unit \<Rightarrow> term"}); |
|
116 fun mk_split thy ty ty' = Sign.mk_const thy |
|
117 (@{const_name split}, [ty, @{typ "unit \<Rightarrow> term"}, StateMonad.liftT (term_ty ty') @{typ seed}]); |
|
118 fun mk_scomp_split thy ty ty' t t' = |
|
119 StateMonad.scomp (term_ty ty) (term_ty ty') @{typ seed} t |
|
120 (mk_split thy ty ty' $ Abs ("", ty, Abs ("", @{typ "unit \<Rightarrow> term"}, t'))) |
|
121 fun mk_cons thy this_ty (c, args) = |
|
122 let |
|
123 val tys = map (fst o fst) args; |
|
124 val c_ty = tys ---> this_ty; |
|
125 val c = Const (c, tys ---> this_ty); |
|
126 val t_indices = map (curry ( op * ) 2) (length tys - 1 downto 0); |
|
127 val c_indices = map (curry ( op + ) 1) t_indices; |
|
128 val c_t = list_comb (c, map Bound c_indices); |
|
129 val t_t = Abs ("", @{typ unit}, Eval.mk_term Free Typerep.typerep |
|
130 (list_comb (c, map (fn k => Bound (k + 1)) t_indices)) |
|
131 |> map_aterms (fn t as Bound _ => t $ @{term "()"} | t => t)); |
|
132 val return = StateMonad.return (term_ty this_ty) @{typ seed} |
|
133 (HOLogic.mk_prod (c_t, t_t)); |
|
134 val t = fold_rev (fn ((ty, _), random) => |
|
135 mk_scomp_split thy ty this_ty random) |
|
136 args return; |
|
137 val is_rec = exists (snd o fst) args; |
|
138 in (is_rec, t) end; |
|
139 fun mk_conss thy ty [] = NONE |
|
140 | mk_conss thy ty [(_, t)] = SOME t |
|
141 | mk_conss thy ty ts = SOME (mk_collapse thy (term_ty ty) $ |
|
142 (Sign.mk_const thy (@{const_name select}, [StateMonad.liftT (term_ty ty) @{typ seed}]) $ |
|
143 HOLogic.mk_list (StateMonad.liftT (term_ty ty) @{typ seed}) (map snd ts))); |
|
144 fun mk_clauses thy ty (tyco, (ts_rec, ts_atom)) = |
|
145 let |
|
146 val SOME t_atom = mk_conss thy ty ts_atom; |
|
147 in case mk_conss thy ty ts_rec |
|
148 of SOME t_rec => mk_collapse thy (term_ty ty) $ |
|
149 (Sign.mk_const thy (@{const_name select_default}, [StateMonad.liftT (term_ty ty) @{typ seed}]) $ |
|
150 @{term "i\<Colon>index"} $ t_rec $ t_atom) |
|
151 | NONE => t_atom |
|
152 end; |
|
153 fun mk_random_eqs thy vs tycos = |
|
154 let |
|
155 val this_ty = Type (hd tycos, map TFree vs); |
|
156 val this_ty' = StateMonad.liftT (term_ty this_ty) @{typ seed}; |
|
157 val random_name = NameSpace.base @{const_name random}; |
|
158 val random'_name = random_name ^ "_" ^ Class.type_name (hd tycos) ^ "'"; |
|
159 fun random ty = Sign.mk_const thy (@{const_name random}, [ty]); |
|
160 val random' = Free (random'_name, |
|
161 @{typ index} --> @{typ index} --> this_ty'); |
|
162 fun atom ty = if Sign.of_sort thy (ty, @{sort random}) |
|
163 then ((ty, false), random ty $ @{term "j\<Colon>index"}) |
|
164 else raise TYP |
|
165 ("Will not generate random elements for type(s) " ^ quote (hd tycos)); |
|
166 fun dtyp tyco = ((this_ty, true), random' $ @{term "i\<Colon>index"} $ @{term "j\<Colon>index"}); |
|
167 fun rtyp tyco tys = raise REC |
|
168 ("Will not generate random elements for mutual recursive type " ^ quote (hd tycos)); |
|
169 val rhss = DatatypePackage.construction_interpretation thy |
|
170 { atom = atom, dtyp = dtyp, rtyp = rtyp } vs tycos |
|
171 |> (map o apsnd o map) (mk_cons thy this_ty) |
|
172 |> (map o apsnd) (List.partition fst) |
|
173 |> map (mk_clauses thy this_ty) |
|
174 val eqss = map ((apsnd o map) (HOLogic.mk_Trueprop o HOLogic.mk_eq) o (fn rhs => ((this_ty, random'), [ |
|
175 (random' $ @{term "0\<Colon>index"} $ @{term "j\<Colon>index"}, Abs ("s", @{typ seed}, |
|
176 Const (@{const_name undefined}, HOLogic.mk_prodT (term_ty this_ty, @{typ seed})))), |
|
177 (random' $ @{term "Suc_index i"} $ @{term "j\<Colon>index"}, rhs) |
|
178 ]))) rhss; |
|
179 in eqss end; |
|
180 fun random_inst [tyco] thy = |
|
181 let |
|
182 val (raw_vs, _) = DatatypePackage.the_datatype_spec thy tyco; |
|
183 val vs = (map o apsnd) |
|
184 (curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort random}) raw_vs; |
|
185 val ((this_ty, random'), eqs') = singleton (mk_random_eqs thy vs) tyco; |
|
186 val eq = (HOLogic.mk_Trueprop o HOLogic.mk_eq) |
|
187 (Sign.mk_const thy (@{const_name random}, [this_ty]) $ @{term "i\<Colon>index"}, |
|
188 random' $ @{term "i\<Colon>index"} $ @{term "i\<Colon>index"}) |
|
189 val del_func = Attrib.internal (fn _ => Thm.declaration_attribute |
|
190 (fn thm => Context.mapping (Code.del_eqn thm) I)); |
|
191 fun add_code simps lthy = |
|
192 let |
|
193 val thy = ProofContext.theory_of lthy; |
|
194 val thm = @{thm random'_if} |
|
195 |> Drule.instantiate' [SOME (Thm.ctyp_of thy this_ty)] [SOME (Thm.cterm_of thy random')] |
|
196 |> (fn thm => thm OF simps) |
|
197 |> singleton (ProofContext.export lthy (ProofContext.init thy)); |
|
198 val c = (fst o dest_Const o fst o strip_comb o fst |
|
199 o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of) thm; |
|
200 in |
|
201 lthy |
|
202 |> LocalTheory.theory (Code.del_eqns c |
|
203 #> PureThy.add_thm ((Binding.name (fst (dest_Free random') ^ "_code"), thm), [Thm.kind_internal]) |
|
204 #-> Code.add_eqn) |
|
205 end; |
|
206 in |
|
207 thy |
|
208 |> TheoryTarget.instantiation ([tyco], vs, @{sort random}) |
|
209 |> PrimrecPackage.add_primrec |
|
210 [(Binding.name (fst (dest_Free random')), SOME (snd (dest_Free random')), NoSyn)] |
|
211 (map (fn eq => ((Binding.empty, [del_func]), eq)) eqs') |
|
212 |-> add_code |
|
213 |> `(fn lthy => Syntax.check_term lthy eq) |
|
214 |-> (fn eq => Specification.definition (NONE, (Attrib.empty_binding, eq))) |
|
215 |> snd |
|
216 |> Class.prove_instantiation_instance (K (Class.intro_classes_tac [])) |
|
217 |> LocalTheory.exit_global |
|
218 end |
|
219 | random_inst tycos thy = raise REC |
|
220 ("Will not generate random elements for mutual recursive type(s) " ^ commas (map quote tycos)); |
|
221 fun add_random_inst tycos thy = random_inst tycos thy |
|
222 handle REC msg => (warning msg; thy) |
|
223 | TYP msg => (warning msg; thy) |
|
224 in DatatypePackage.interpretation add_random_inst end |
|
225 *} |
|
226 |
|
227 text {* Type @{typ int} *} |
|
228 |
|
229 instantiation int :: random |
|
230 begin |
|
231 |
|
232 definition |
|
233 "random n = (do |
|
234 (b, _) \<leftarrow> random n; |
|
235 (m, t) \<leftarrow> random n; |
|
236 return (if b then (int m, \<lambda>u. Code_Eval.App (Code_Eval.Const (STR ''Int.int'') TYPEREP(nat \<Rightarrow> int)) (t ())) |
|
237 else (- int m, \<lambda>u. Code_Eval.App (Code_Eval.Const (STR ''HOL.uminus_class.uminus'') TYPEREP(int \<Rightarrow> int)) |
|
238 (Code_Eval.App (Code_Eval.Const (STR ''Int.int'') TYPEREP(nat \<Rightarrow> int)) (t ())))) |
|
239 done)" |
|
240 |
|
241 instance .. |
|
242 |
|
243 end |
|
244 |
|
245 |
|
246 subsection {* Quickcheck generator *} |
|
247 |
|
248 ML {* |
|
249 structure Quickcheck = |
|
250 struct |
|
251 |
|
252 open Quickcheck; |
|
253 |
|
254 val eval_ref : (unit -> int -> int * int -> term list option * (int * int)) option ref = ref NONE; |
|
255 |
|
256 fun mk_generator_expr thy prop tys = |
|
257 let |
|
258 val bound_max = length tys - 1; |
|
259 val bounds = map_index (fn (i, ty) => |
|
260 (2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) tys; |
|
261 val result = list_comb (prop, map (fn (i, _, _, _) => Bound i) bounds); |
|
262 val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds); |
|
263 val check = @{term "If \<Colon> bool \<Rightarrow> term list option \<Rightarrow> term list option \<Rightarrow> term list option"} |
|
264 $ result $ @{term "None \<Colon> term list option"} $ (@{term "Some \<Colon> term list \<Rightarrow> term list option "} $ terms); |
|
265 val return = @{term "Pair \<Colon> term list option \<Rightarrow> seed \<Rightarrow> term list option \<times> seed"}; |
|
266 fun mk_termtyp ty = HOLogic.mk_prodT (ty, @{typ "unit \<Rightarrow> term"}); |
|
267 fun mk_split ty = Sign.mk_const thy |
|
268 (@{const_name split}, [ty, @{typ "unit \<Rightarrow> term"}, StateMonad.liftT @{typ "term list option"} @{typ seed}]); |
|
269 fun mk_scomp_split ty t t' = |
|
270 StateMonad.scomp (mk_termtyp ty) @{typ "term list option"} @{typ seed} t (*FIXME*) |
|
271 (mk_split ty $ Abs ("", ty, Abs ("", @{typ "unit \<Rightarrow> term"}, t'))); |
|
272 fun mk_bindclause (_, _, i, ty) = mk_scomp_split ty |
|
273 (Sign.mk_const thy (@{const_name random}, [ty]) $ Bound i) |
|
274 val t = fold_rev mk_bindclause bounds (return $ check); |
|
275 in Abs ("n", @{typ index}, t) end; |
|
276 |
|
277 fun compile_generator_expr thy t = |
|
278 let |
|
279 val tys = (map snd o fst o strip_abs) t; |
|
280 val t' = mk_generator_expr thy t tys; |
|
281 val f = Code_ML.eval_term ("Quickcheck.eval_ref", eval_ref) thy t' []; |
|
282 in f #> Random_Engine.run #> (Option.map o map) (Code.postprocess_term thy) end; |
|
283 |
|
284 end |
|
285 *} |
|
286 |
|
287 setup {* |
|
288 Quickcheck.add_generator ("code", Quickcheck.compile_generator_expr o ProofContext.theory_of) |
|
289 *} |
|
290 |
|
291 subsection {* Examples *} |
|
292 |
|
293 theorem "map g (map f xs) = map (g o f) xs" |
|
294 quickcheck [generator = code] |
|
295 by (induct xs) simp_all |
|
296 |
|
297 theorem "map g (map f xs) = map (f o g) xs" |
|
298 quickcheck [generator = code] |
|
299 oops |
|
300 |
|
301 theorem "rev (xs @ ys) = rev ys @ rev xs" |
|
302 quickcheck [generator = code] |
|
303 by simp |
|
304 |
|
305 theorem "rev (xs @ ys) = rev xs @ rev ys" |
|
306 quickcheck [generator = code] |
|
307 oops |
|
308 |
|
309 theorem "rev (rev xs) = xs" |
|
310 quickcheck [generator = code] |
|
311 by simp |
|
312 |
|
313 theorem "rev xs = xs" |
|
314 quickcheck [generator = code] |
|
315 oops |
|
316 |
|
317 primrec app :: "('a \<Rightarrow> 'a) list \<Rightarrow> 'a \<Rightarrow> 'a" where |
|
318 "app [] x = x" |
|
319 | "app (f # fs) x = app fs (f x)" |
|
320 |
|
321 lemma "app (fs @ gs) x = app gs (app fs x)" |
|
322 quickcheck [generator = code] |
|
323 by (induct fs arbitrary: x) simp_all |
|
324 |
|
325 lemma "app (fs @ gs) x = app fs (app gs x)" |
|
326 quickcheck [generator = code] |
|
327 oops |
|
328 |
|
329 primrec occurs :: "'a \<Rightarrow> 'a list \<Rightarrow> nat" where |
|
330 "occurs a [] = 0" |
|
331 | "occurs a (x#xs) = (if (x=a) then Suc(occurs a xs) else occurs a xs)" |
|
332 |
|
333 primrec del1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where |
|
334 "del1 a [] = []" |
|
335 | "del1 a (x#xs) = (if (x=a) then xs else (x#del1 a xs))" |
|
336 |
|
337 lemma "Suc (occurs a (del1 a xs)) = occurs a xs" |
|
338 -- {* Wrong. Precondition needed.*} |
|
339 quickcheck [generator = code] |
|
340 oops |
|
341 |
|
342 lemma "xs ~= [] \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs" |
|
343 quickcheck [generator = code] |
|
344 -- {* Also wrong.*} |
|
345 oops |
|
346 |
|
347 lemma "0 < occurs a xs \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs" |
|
348 quickcheck [generator = code] |
|
349 by (induct xs) auto |
|
350 |
|
351 primrec replace :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where |
|
352 "replace a b [] = []" |
|
353 | "replace a b (x#xs) = (if (x=a) then (b#(replace a b xs)) |
|
354 else (x#(replace a b xs)))" |
|
355 |
|
356 lemma "occurs a xs = occurs b (replace a b xs)" |
|
357 quickcheck [generator = code] |
|
358 -- {* Wrong. Precondition needed.*} |
|
359 oops |
|
360 |
|
361 lemma "occurs b xs = 0 \<or> a=b \<longrightarrow> occurs a xs = occurs b (replace a b xs)" |
|
362 quickcheck [generator = code] |
|
363 by (induct xs) simp_all |
|
364 |
|
365 |
|
366 subsection {* Trees *} |
|
367 |
|
368 datatype 'a tree = Twig | Leaf 'a | Branch "'a tree" "'a tree" |
|
369 |
|
370 primrec leaves :: "'a tree \<Rightarrow> 'a list" where |
|
371 "leaves Twig = []" |
|
372 | "leaves (Leaf a) = [a]" |
|
373 | "leaves (Branch l r) = (leaves l) @ (leaves r)" |
|
374 |
|
375 primrec plant :: "'a list \<Rightarrow> 'a tree" where |
|
376 "plant [] = Twig " |
|
377 | "plant (x#xs) = Branch (Leaf x) (plant xs)" |
|
378 |
|
379 primrec mirror :: "'a tree \<Rightarrow> 'a tree" where |
|
380 "mirror (Twig) = Twig " |
|
381 | "mirror (Leaf a) = Leaf a " |
|
382 | "mirror (Branch l r) = Branch (mirror r) (mirror l)" |
|
383 |
|
384 theorem "plant (rev (leaves xt)) = mirror xt" |
|
385 quickcheck [generator = code] |
|
386 --{* Wrong! *} |
|
387 oops |
|
388 |
|
389 theorem "plant (leaves xt @ leaves yt) = Branch xt yt" |
|
390 quickcheck [generator = code] |
|
391 --{* Wrong! *} |
|
392 oops |
|
393 |
|
394 datatype 'a ntree = Tip "'a" | Node "'a" "'a ntree" "'a ntree" |
|
395 |
|
396 primrec inOrder :: "'a ntree \<Rightarrow> 'a list" where |
|
397 "inOrder (Tip a)= [a]" |
|
398 | "inOrder (Node f x y) = (inOrder x)@[f]@(inOrder y)" |
|
399 |
|
400 primrec root :: "'a ntree \<Rightarrow> 'a" where |
|
401 "root (Tip a) = a" |
|
402 | "root (Node f x y) = f" |
|
403 |
|
404 theorem "hd (inOrder xt) = root xt" |
|
405 quickcheck [generator = code] |
|
406 --{* Wrong! *} |
|
407 oops |
|
408 |
|
409 lemma "int (f k) = k" |
|
410 quickcheck [generator = code] |
|
411 oops |
|
412 |
|
413 end |
|