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