|
1 (* Title: HOL/Tools/smallvalue_generators.ML |
|
2 Author: Lukas Bulwahn, TU Muenchen |
|
3 |
|
4 Generators for small values for various types. |
|
5 *) |
|
6 |
|
7 signature SMALLVALUE_GENERATORS = |
|
8 sig |
|
9 val compile_generator_expr: |
|
10 Proof.context -> term -> int -> term list option * Quickcheck.report option |
|
11 val compile_generator_exprs: |
|
12 Proof.context -> term list -> (int -> term list option) list |
|
13 val put_counterexample: (unit -> int -> term list option) |
|
14 -> Proof.context -> Proof.context |
|
15 val put_counterexample_batch: (unit -> (int -> term list option) list) |
|
16 -> Proof.context -> Proof.context |
|
17 val smart_quantifier : bool Config.T; |
|
18 val quickcheck_pretty : bool Config.T; |
|
19 val setup: theory -> theory |
|
20 end; |
|
21 |
|
22 structure Smallvalue_Generators : SMALLVALUE_GENERATORS = |
|
23 struct |
|
24 |
|
25 (* static options *) |
|
26 |
|
27 val define_foundationally = false |
|
28 |
|
29 (* dynamic options *) |
|
30 |
|
31 val (smart_quantifier, setup_smart_quantifier) = |
|
32 Attrib.config_bool "quickcheck_smart_quantifier" (K true) |
|
33 |
|
34 val (quickcheck_pretty, setup_quickcheck_pretty) = |
|
35 Attrib.config_bool "quickcheck_pretty" (K true) |
|
36 |
|
37 (** general term functions **) |
|
38 |
|
39 fun mk_measure f = |
|
40 let |
|
41 val Type ("fun", [T, @{typ nat}]) = fastype_of f |
|
42 in |
|
43 Const (@{const_name Wellfounded.measure}, |
|
44 (T --> @{typ nat}) --> HOLogic.mk_prodT (T, T) --> @{typ bool}) |
|
45 $ f |
|
46 end |
|
47 |
|
48 fun mk_sumcases rT f (Type (@{type_name Sum_Type.sum}, [TL, TR])) = |
|
49 let |
|
50 val lt = mk_sumcases rT f TL |
|
51 val rt = mk_sumcases rT f TR |
|
52 in |
|
53 SumTree.mk_sumcase TL TR rT lt rt |
|
54 end |
|
55 | mk_sumcases _ f T = f T |
|
56 |
|
57 fun mk_undefined T = Const(@{const_name undefined}, T) |
|
58 |
|
59 |
|
60 (** abstract syntax **) |
|
61 |
|
62 fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => Code_Evaluation.term"}); |
|
63 |
|
64 val size = @{term "i :: code_numeral"} |
|
65 val size_pred = @{term "(i :: code_numeral) - 1"} |
|
66 val size_ge_zero = @{term "(i :: code_numeral) > 0"} |
|
67 fun test_function T = Free ("f", termifyT T --> @{typ "term list option"}) |
|
68 |
|
69 fun mk_none_continuation (x, y) = |
|
70 let |
|
71 val (T as Type(@{type_name "option"}, [T'])) = fastype_of x |
|
72 in |
|
73 Const (@{const_name "Smallcheck.orelse"}, T --> T --> T) |
|
74 $ x $ y |
|
75 end |
|
76 |
|
77 (** datatypes **) |
|
78 |
|
79 (* constructing smallvalue generator instances on datatypes *) |
|
80 |
|
81 exception FUNCTION_TYPE; |
|
82 |
|
83 val smallN = "small"; |
|
84 |
|
85 fun smallT T = (T --> @{typ "Code_Evaluation.term list option"}) --> @{typ code_numeral} |
|
86 --> @{typ "Code_Evaluation.term list option"} |
|
87 |
|
88 val full_smallN = "full_small"; |
|
89 |
|
90 fun full_smallT T = (termifyT T --> @{typ "Code_Evaluation.term list option"}) |
|
91 --> @{typ code_numeral} --> @{typ "Code_Evaluation.term list option"} |
|
92 |
|
93 fun check_allT T = (termifyT T --> @{typ "Code_Evaluation.term list option"}) |
|
94 --> @{typ "Code_Evaluation.term list option"} |
|
95 |
|
96 fun mk_equations thy descr vs tycos smalls (Ts, Us) = |
|
97 let |
|
98 fun mk_small_call T = |
|
99 let |
|
100 val small = Const (@{const_name "Smallcheck.full_small_class.full_small"}, full_smallT T) |
|
101 in |
|
102 (T, (fn t => small $ |
|
103 (HOLogic.split_const (T, @{typ "unit => Code_Evaluation.term"}, @{typ "Code_Evaluation.term list option"}) |
|
104 $ absdummy (T, absdummy (@{typ "unit => Code_Evaluation.term"}, t))) $ size_pred)) |
|
105 end |
|
106 fun mk_small_aux_call fTs (k, _) (tyco, Ts) = |
|
107 let |
|
108 val T = Type (tyco, Ts) |
|
109 val _ = if not (null fTs) then raise FUNCTION_TYPE else () |
|
110 val small = nth smalls k |
|
111 in |
|
112 (T, (fn t => small $ |
|
113 (HOLogic.split_const (T, @{typ "unit => Code_Evaluation.term"}, @{typ "Code_Evaluation.term list option"}) |
|
114 $ absdummy (T, absdummy (@{typ "unit => Code_Evaluation.term"}, t))) $ size_pred)) |
|
115 end |
|
116 fun mk_consexpr simpleT (c, xs) = |
|
117 let |
|
118 val (Ts, fns) = split_list xs |
|
119 val constr = Const (c, Ts ---> simpleT) |
|
120 val bounds = map (fn x => Bound (2 * x + 1)) (((length xs) - 1) downto 0) |
|
121 val term_bounds = map (fn x => Bound (2 * x)) (((length xs) - 1) downto 0) |
|
122 val Eval_App = Const ("Code_Evaluation.App", HOLogic.termT --> HOLogic.termT --> HOLogic.termT) |
|
123 val Eval_Const = Const ("Code_Evaluation.Const", HOLogic.literalT --> @{typ typerep} --> HOLogic.termT) |
|
124 val term = fold (fn u => fn t => Eval_App $ t $ (u $ @{term "()"})) |
|
125 bounds (Eval_Const $ HOLogic.mk_literal c $ HOLogic.mk_typerep (Ts ---> simpleT)) |
|
126 val start_term = test_function simpleT $ |
|
127 (HOLogic.pair_const simpleT @{typ "unit => Code_Evaluation.term"} |
|
128 $ (list_comb (constr, bounds)) $ absdummy (@{typ unit}, term)) |
|
129 in fold_rev (fn f => fn t => f t) fns start_term end |
|
130 fun mk_rhs exprs = |
|
131 @{term "If :: bool => term list option => term list option => term list option"} |
|
132 $ size_ge_zero $ (foldr1 mk_none_continuation exprs) $ @{term "None :: term list option"} |
|
133 val rhss = |
|
134 Datatype_Aux.interpret_construction descr vs |
|
135 { atyp = mk_small_call, dtyp = mk_small_aux_call } |
|
136 |> (map o apfst) Type |
|
137 |> map (fn (T, cs) => map (mk_consexpr T) cs) |
|
138 |> map mk_rhs |
|
139 val lhss = map2 (fn t => fn T => t $ test_function T $ size) smalls (Ts @ Us); |
|
140 val eqs = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhss ~~ rhss) |
|
141 in |
|
142 eqs |
|
143 end |
|
144 |
|
145 (* foundational definition with the function package *) |
|
146 |
|
147 val less_int_pred = @{lemma "i > 0 ==> Code_Numeral.nat_of ((i :: code_numeral) - 1) < Code_Numeral.nat_of i" by auto} |
|
148 |
|
149 fun mk_single_measure T = HOLogic.mk_comp (@{term "Code_Numeral.nat_of"}, |
|
150 Const (@{const_name "Product_Type.snd"}, T --> @{typ "code_numeral"})) |
|
151 |
|
152 fun mk_termination_measure T = |
|
153 let |
|
154 val T' = fst (HOLogic.dest_prodT (HOLogic.dest_setT T)) |
|
155 in |
|
156 mk_measure (mk_sumcases @{typ nat} mk_single_measure T') |
|
157 end |
|
158 |
|
159 fun termination_tac ctxt = |
|
160 Function_Relation.relation_tac ctxt mk_termination_measure 1 |
|
161 THEN rtac @{thm wf_measure} 1 |
|
162 THEN (REPEAT_DETERM (Simplifier.asm_full_simp_tac |
|
163 (HOL_basic_ss addsimps [@{thm in_measure}, @{thm o_def}, @{thm snd_conv}, |
|
164 @{thm nat_mono_iff}, less_int_pred] @ @{thms sum.cases}) 1)) |
|
165 |
|
166 fun pat_completeness_auto ctxt = |
|
167 Pat_Completeness.pat_completeness_tac ctxt 1 |
|
168 THEN auto_tac (clasimpset_of ctxt) |
|
169 |
|
170 |
|
171 (* creating the instances *) |
|
172 |
|
173 fun instantiate_smallvalue_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy = |
|
174 let |
|
175 val _ = Datatype_Aux.message config "Creating smallvalue generators ..."; |
|
176 val smallsN = map (prefix (full_smallN ^ "_")) (names @ auxnames); |
|
177 in |
|
178 thy |
|
179 |> Class.instantiation (tycos, vs, @{sort full_small}) |
|
180 |> (if define_foundationally then |
|
181 let |
|
182 val smalls = map2 (fn name => fn T => Free (name, full_smallT T)) smallsN (Ts @ Us) |
|
183 val eqs = mk_equations thy descr vs tycos smalls (Ts, Us) |
|
184 in |
|
185 Function.add_function |
|
186 (map (fn (name, T) => |
|
187 Syntax.no_syn (Binding.conceal (Binding.name name), SOME (full_smallT T))) |
|
188 (smallsN ~~ (Ts @ Us))) |
|
189 (map (pair (apfst Binding.conceal Attrib.empty_binding)) eqs) |
|
190 Function_Common.default_config pat_completeness_auto |
|
191 #> snd |
|
192 #> Local_Theory.restore |
|
193 #> (fn lthy => Function.prove_termination NONE (termination_tac lthy) lthy) |
|
194 #> snd |
|
195 end |
|
196 else |
|
197 fold_map (fn (name, T) => Local_Theory.define |
|
198 ((Binding.conceal (Binding.name name), NoSyn), |
|
199 (apfst Binding.conceal Attrib.empty_binding, mk_undefined (full_smallT T))) |
|
200 #> apfst fst) (smallsN ~~ (Ts @ Us)) |
|
201 #> (fn (smalls, lthy) => |
|
202 let |
|
203 val eqs_t = mk_equations thy descr vs tycos smalls (Ts, Us) |
|
204 val eqs = map (fn eq => Goal.prove lthy ["f", "i"] [] eq |
|
205 (fn _ => Skip_Proof.cheat_tac (ProofContext.theory_of lthy))) eqs_t |
|
206 in |
|
207 fold (fn (name, eq) => Local_Theory.note |
|
208 ((Binding.conceal (Binding.qualify true prfx |
|
209 (Binding.qualify true name (Binding.name "simps"))), |
|
210 Code.add_default_eqn_attrib :: map (Attrib.internal o K) |
|
211 [Simplifier.simp_add, Nitpick_Simps.add]), [eq]) #> snd) (smallsN ~~ eqs) lthy |
|
212 end)) |
|
213 |> Class.prove_instantiation_exit (K (Class.intro_classes_tac [])) |
|
214 end handle FUNCTION_TYPE => |
|
215 (Datatype_Aux.message config |
|
216 "Creation of smallvalue generators failed because the datatype contains a function type"; |
|
217 thy) |
|
218 |
|
219 (** building and compiling generator expressions **) |
|
220 |
|
221 structure Counterexample = Proof_Data |
|
222 ( |
|
223 type T = unit -> int -> term list option |
|
224 (* FIXME avoid user error with non-user text *) |
|
225 fun init _ () = error "Counterexample" |
|
226 ); |
|
227 val put_counterexample = Counterexample.put; |
|
228 |
|
229 structure Counterexample_Batch = Proof_Data |
|
230 ( |
|
231 type T = unit -> (int -> term list option) list |
|
232 (* FIXME avoid user error with non-user text *) |
|
233 fun init _ () = error "Counterexample" |
|
234 ); |
|
235 val put_counterexample_batch = Counterexample_Batch.put; |
|
236 |
|
237 val target = "Quickcheck"; |
|
238 |
|
239 fun mk_smart_generator_expr ctxt t = |
|
240 let |
|
241 val thy = ProofContext.theory_of ctxt |
|
242 val ((vnames, Ts), t') = apfst split_list (strip_abs t) |
|
243 val ([depth_name], ctxt') = Variable.variant_fixes ["depth"] ctxt |
|
244 val (names, ctxt'') = Variable.variant_fixes vnames ctxt' |
|
245 val (term_names, ctxt''') = Variable.variant_fixes (map (prefix "t_") vnames) ctxt'' |
|
246 val depth = Free (depth_name, @{typ code_numeral}) |
|
247 val frees = map2 (curry Free) names Ts |
|
248 val term_vars = map (fn n => Free (n, @{typ "unit => term"})) term_names |
|
249 fun strip_imp (Const(@{const_name HOL.implies},_) $ A $ B) = apfst (cons A) (strip_imp B) |
|
250 | strip_imp A = ([], A) |
|
251 val (assms, concl) = strip_imp (subst_bounds (rev frees, t')) |
|
252 val terms = HOLogic.mk_list @{typ term} (map (fn v => v $ @{term "()"}) term_vars) |
|
253 fun mk_small_closure (free as Free (_, T), term_var) t = |
|
254 if Sign.of_sort thy (T, @{sort enum}) then |
|
255 Const (@{const_name "Smallcheck.check_all_class.check_all"}, check_allT T) |
|
256 $ (HOLogic.split_const (T, @{typ "unit => term"}, @{typ "term list option"}) |
|
257 $ lambda free (lambda term_var t)) |
|
258 else |
|
259 Const (@{const_name "Smallcheck.full_small_class.full_small"}, full_smallT T) |
|
260 $ (HOLogic.split_const (T, @{typ "unit => term"}, @{typ "term list option"}) |
|
261 $ lambda free (lambda term_var t)) $ depth |
|
262 fun lookup v = the (AList.lookup (op =) (names ~~ (frees ~~ term_vars)) v) |
|
263 val none_t = @{term "None :: term list option"} |
|
264 fun mk_safe_if (cond, then_t, else_t) = |
|
265 @{term "Smallcheck.catch_match :: term list option => term list option => term list option"} $ |
|
266 (@{term "If :: bool => term list option => term list option => term list option"} |
|
267 $ cond $ then_t $ else_t) $ none_t; |
|
268 fun mk_test_term bound_vars assms = |
|
269 let |
|
270 fun vars_of t = subtract (op =) bound_vars (Term.add_free_names t []) |
|
271 val (vars, check) = |
|
272 case assms of [] => |
|
273 (vars_of concl, (concl, none_t, @{term "Some :: term list => term list option"} $ terms)) |
|
274 | assm :: assms => |
|
275 (vars_of assm, (assm, mk_test_term (union (op =) (vars_of assm) bound_vars) assms, none_t)) |
|
276 in |
|
277 fold_rev mk_small_closure (map lookup vars) (mk_safe_if check) |
|
278 end |
|
279 in lambda depth (mk_test_term [] assms) end |
|
280 |
|
281 fun mk_generator_expr ctxt t = |
|
282 let |
|
283 val Ts = (map snd o fst o strip_abs) t; |
|
284 val thy = ProofContext.theory_of ctxt |
|
285 val bound_max = length Ts - 1; |
|
286 val bounds = map_index (fn (i, ty) => |
|
287 (2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) Ts; |
|
288 val result = list_comb (t, map (fn (i, _, _, _) => Bound i) bounds); |
|
289 val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds); |
|
290 val check = |
|
291 @{term "Smallcheck.catch_match :: term list option => term list option => term list option"} $ |
|
292 (@{term "If :: bool => term list option => term list option => term list option"} |
|
293 $ result $ @{term "None :: term list option"} $ (@{term "Some :: term list => term list option"} $ terms)) |
|
294 $ @{term "None :: term list option"}; |
|
295 fun mk_small_closure (_, _, i, T) t = |
|
296 Const (@{const_name "Smallcheck.full_small_class.full_small"}, full_smallT T) |
|
297 $ (HOLogic.split_const (T, @{typ "unit => term"}, @{typ "term list option"}) |
|
298 $ absdummy (T, absdummy (@{typ "unit => term"}, t))) $ Bound i |
|
299 in Abs ("d", @{typ code_numeral}, fold_rev mk_small_closure bounds check) end |
|
300 |
|
301 (** post-processing of function terms **) |
|
302 |
|
303 fun dest_fun_upd (Const (@{const_name fun_upd}, _) $ t0 $ t1 $ t2) = (t0, (t1, t2)) |
|
304 | dest_fun_upd t = raise TERM ("dest_fun_upd", [t]) |
|
305 |
|
306 fun mk_fun_upd T1 T2 (t1, t2) t = |
|
307 Const (@{const_name fun_upd}, (T1 --> T2) --> T1 --> T2 --> T1 --> T2) $ t $ t1 $ t2 |
|
308 |
|
309 fun dest_fun_upds t = |
|
310 case try dest_fun_upd t of |
|
311 NONE => |
|
312 (case t of |
|
313 Abs (_, _, _) => ([], t) |
|
314 | _ => raise TERM ("dest_fun_upds", [t])) |
|
315 | SOME (t0, (t1, t2)) => apfst (cons (t1, t2)) (dest_fun_upds t0) |
|
316 |
|
317 fun make_fun_upds T1 T2 (tps, t) = fold_rev (mk_fun_upd T1 T2) tps t |
|
318 |
|
319 fun make_set T1 [] = Const (@{const_abbrev Set.empty}, T1 --> @{typ bool}) |
|
320 | make_set T1 ((_, @{const False}) :: tps) = make_set T1 tps |
|
321 | make_set T1 ((t1, @{const True}) :: tps) = |
|
322 Const (@{const_name insert}, T1 --> (T1 --> @{typ bool}) --> T1 --> @{typ bool}) |
|
323 $ t1 $ (make_set T1 tps) |
|
324 | make_set T1 ((_, t) :: tps) = raise TERM ("make_set", [t]) |
|
325 |
|
326 fun make_coset T [] = Const (@{const_abbrev UNIV}, T --> @{typ bool}) |
|
327 | make_coset T tps = |
|
328 let |
|
329 val U = T --> @{typ bool} |
|
330 fun invert @{const False} = @{const True} |
|
331 | invert @{const True} = @{const False} |
|
332 in |
|
333 Const (@{const_name "Groups.minus_class.minus"}, U --> U --> U) |
|
334 $ Const (@{const_abbrev UNIV}, U) $ make_set T (map (apsnd invert) tps) |
|
335 end |
|
336 |
|
337 fun make_map T1 T2 [] = Const (@{const_abbrev Map.empty}, T1 --> T2) |
|
338 | make_map T1 T2 ((_, Const (@{const_name None}, _)) :: tps) = make_map T1 T2 tps |
|
339 | make_map T1 T2 ((t1, t2) :: tps) = mk_fun_upd T1 T2 (t1, t2) (make_map T1 T2 tps) |
|
340 |
|
341 fun post_process_term t = |
|
342 let |
|
343 fun map_Abs f t = |
|
344 case t of Abs (x, T, t') => Abs (x, T, f t') | _ => raise TERM ("map_Abs", [t]) |
|
345 fun process_args t = case strip_comb t of |
|
346 (c as Const (_, _), ts) => list_comb (c, map post_process_term ts) |
|
347 in |
|
348 case fastype_of t of |
|
349 Type (@{type_name fun}, [T1, T2]) => |
|
350 (case try dest_fun_upds t of |
|
351 SOME (tps, t) => |
|
352 (map (pairself post_process_term) tps, map_Abs post_process_term t) |
|
353 |> (case T2 of |
|
354 @{typ bool} => |
|
355 (case t of |
|
356 Abs(_, _, @{const True}) => fst #> rev #> make_set T1 |
|
357 | Abs(_, _, @{const False}) => fst #> rev #> make_coset T1 |
|
358 | Abs(_, _, Const (@{const_name undefined}, _)) => fst #> rev #> make_set T1 |
|
359 | _ => raise TERM ("post_process_term", [t])) |
|
360 | Type (@{type_name option}, _) => |
|
361 (case t of |
|
362 Abs(_, _, Const(@{const_name None}, _)) => fst #> make_map T1 T2 |
|
363 | Abs(_, _, Const (@{const_name undefined}, _)) => fst #> make_map T1 T2 |
|
364 | _ => make_fun_upds T1 T2) |
|
365 | _ => make_fun_upds T1 T2) |
|
366 | NONE => process_args t) |
|
367 | _ => process_args t |
|
368 end |
|
369 |
|
370 (** generator compiliation **) |
|
371 |
|
372 fun compile_generator_expr ctxt t = |
|
373 let |
|
374 val thy = ProofContext.theory_of ctxt |
|
375 val t' = |
|
376 (if Config.get ctxt smart_quantifier then mk_smart_generator_expr else mk_generator_expr) |
|
377 ctxt t; |
|
378 val compile = Code_Runtime.dynamic_value_strict |
|
379 (Counterexample.get, put_counterexample, "Smallvalue_Generators.put_counterexample") |
|
380 thy (SOME target) (fn proc => fn g => g #> (Option.map o map) proc) t' []; |
|
381 in |
|
382 fn size => rpair NONE (compile size |> |
|
383 (if Config.get ctxt quickcheck_pretty then Option.map (map post_process_term) else I)) |
|
384 end; |
|
385 |
|
386 fun compile_generator_exprs ctxt ts = |
|
387 let |
|
388 val thy = ProofContext.theory_of ctxt |
|
389 val mk_generator_expr = |
|
390 if Config.get ctxt smart_quantifier then mk_smart_generator_expr else mk_generator_expr |
|
391 val ts' = map (mk_generator_expr ctxt) ts; |
|
392 val compiles = Code_Runtime.dynamic_value_strict |
|
393 (Counterexample_Batch.get, put_counterexample_batch, |
|
394 "Smallvalue_Generators.put_counterexample_batch") |
|
395 thy (SOME target) (fn proc => map (fn g => g #> (Option.map o map) proc)) |
|
396 (HOLogic.mk_list @{typ "code_numeral => term list option"} ts') []; |
|
397 in |
|
398 map (fn compile => fn size => compile size |> Option.map (map post_process_term)) compiles |
|
399 end; |
|
400 |
|
401 |
|
402 (** setup **) |
|
403 |
|
404 val setup = |
|
405 Datatype.interpretation |
|
406 (Quickcheck_Generators.ensure_sort_datatype (@{sort full_small}, instantiate_smallvalue_datatype)) |
|
407 #> setup_smart_quantifier |
|
408 #> setup_quickcheck_pretty |
|
409 #> Context.theory_map (Quickcheck.add_generator ("exhaustive", compile_generator_expr)) |
|
410 #> Context.theory_map (Quickcheck.add_batch_generator ("exhaustive", compile_generator_exprs)); |
|
411 |
|
412 end; |