124 |
118 |
125 fun mk_equations functerms = |
119 fun mk_equations functerms = |
126 let |
120 let |
127 fun test_function T = Free ("f", T --> resultT) |
121 fun test_function T = Free ("f", T --> resultT) |
128 val mk_call = gen_mk_call (fn T => |
122 val mk_call = gen_mk_call (fn T => |
129 Const (@{const_name "Quickcheck_Exhaustive.exhaustive_class.exhaustive"}, exhaustiveT T)) |
123 Const (@{const_name Quickcheck_Exhaustive.exhaustive_class.exhaustive}, exhaustiveT T)) |
130 val mk_aux_call = gen_mk_aux_call functerms |
124 val mk_aux_call = gen_mk_aux_call functerms |
131 val mk_consexpr = gen_mk_consexpr test_function |
125 val mk_consexpr = gen_mk_consexpr test_function |
132 fun mk_rhs exprs = |
126 fun mk_rhs exprs = |
133 mk_if (size_ge_zero, foldr1 mk_none_continuation exprs, Const (@{const_name "None"}, resultT)) |
127 mk_if (size_ge_zero, foldr1 mk_none_continuation exprs, Const (@{const_name None}, resultT)) |
134 in |
128 in mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms) end |
135 mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms) |
|
136 end |
|
137 |
129 |
138 fun mk_bounded_forall_equations functerms = |
130 fun mk_bounded_forall_equations functerms = |
139 let |
131 let |
140 fun test_function T = Free ("P", T --> @{typ bool}) |
132 fun test_function T = Free ("P", T --> @{typ bool}) |
141 val mk_call = gen_mk_call (fn T => |
133 val mk_call = gen_mk_call (fn T => |
142 Const (@{const_name "Quickcheck_Exhaustive.bounded_forall_class.bounded_forall"}, |
134 Const (@{const_name Quickcheck_Exhaustive.bounded_forall_class.bounded_forall}, |
143 bounded_forallT T)) |
135 bounded_forallT T)) |
144 val mk_aux_call = gen_mk_aux_call functerms |
136 val mk_aux_call = gen_mk_aux_call functerms |
145 val mk_consexpr = gen_mk_consexpr test_function |
137 val mk_consexpr = gen_mk_consexpr test_function |
146 fun mk_rhs exprs = |
138 fun mk_rhs exprs = mk_if (size_ge_zero, foldr1 HOLogic.mk_conj exprs, @{term True}) |
147 mk_if (size_ge_zero, foldr1 HOLogic.mk_conj exprs, @{term "True"}) |
139 in mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms) end |
148 in |
140 |
149 mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms) |
|
150 end |
|
151 |
|
152 fun mk_full_equations functerms = |
141 fun mk_full_equations functerms = |
153 let |
142 let |
154 fun test_function T = Free ("f", termifyT T --> resultT) |
143 fun test_function T = Free ("f", termifyT T --> resultT) |
155 fun case_prod_const T = HOLogic.case_prod_const (T, @{typ "unit => Code_Evaluation.term"}, resultT) |
144 fun case_prod_const T = |
|
145 HOLogic.case_prod_const (T, @{typ "unit \<Rightarrow> Code_Evaluation.term"}, resultT) |
156 fun mk_call T = |
146 fun mk_call T = |
157 let |
147 let |
158 val full_exhaustive = |
148 val full_exhaustive = |
159 Const (@{const_name "Quickcheck_Exhaustive.full_exhaustive_class.full_exhaustive"}, |
149 Const (@{const_name Quickcheck_Exhaustive.full_exhaustive_class.full_exhaustive}, |
160 full_exhaustiveT T) |
150 full_exhaustiveT T) |
161 in |
151 in |
162 (T, fn t => full_exhaustive $ |
152 (T, |
163 (case_prod_const T $ absdummy T (absdummy @{typ "unit => Code_Evaluation.term"} t)) $ size_pred) |
153 fn t => |
|
154 full_exhaustive $ |
|
155 (case_prod_const T $ absdummy T (absdummy @{typ "unit \<Rightarrow> Code_Evaluation.term"} t)) $ |
|
156 size_pred) |
164 end |
157 end |
165 fun mk_aux_call fTs (k, _) (tyco, Ts) = |
158 fun mk_aux_call fTs (k, _) (tyco, Ts) = |
166 let |
159 let |
167 val T = Type (tyco, Ts) |
160 val T = Type (tyco, Ts) |
168 val _ = if not (null fTs) then raise FUNCTION_TYPE else () |
161 val _ = if not (null fTs) then raise FUNCTION_TYPE else () |
169 in |
162 in |
170 (T, fn t => nth functerms k $ |
163 (T, |
171 (case_prod_const T $ absdummy T (absdummy @{typ "unit => Code_Evaluation.term"} t)) $ size_pred) |
164 fn t => |
|
165 nth functerms k $ |
|
166 (case_prod_const T $ absdummy T (absdummy @{typ "unit \<Rightarrow> Code_Evaluation.term"} t)) $ |
|
167 size_pred) |
172 end |
168 end |
173 fun mk_consexpr simpleT (c, xs) = |
169 fun mk_consexpr simpleT (c, xs) = |
174 let |
170 let |
175 val (Ts, fns) = split_list xs |
171 val (Ts, fns) = split_list xs |
176 val constr = Const (c, Ts ---> simpleT) |
172 val constr = Const (c, Ts ---> simpleT) |
177 val bounds = map (fn x => Bound (2 * x + 1)) (((length xs) - 1) downto 0) |
173 val bounds = map (fn x => Bound (2 * x + 1)) (((length xs) - 1) downto 0) |
178 val Eval_App = |
174 val Eval_App = |
179 Const (@{const_name Code_Evaluation.App}, HOLogic.termT --> HOLogic.termT --> HOLogic.termT) |
175 Const (@{const_name Code_Evaluation.App}, |
|
176 HOLogic.termT --> HOLogic.termT --> HOLogic.termT) |
180 val Eval_Const = |
177 val Eval_Const = |
181 Const (@{const_name Code_Evaluation.Const}, HOLogic.literalT --> @{typ typerep} --> HOLogic.termT) |
178 Const (@{const_name Code_Evaluation.Const}, |
182 val term = fold (fn u => fn t => Eval_App $ t $ (u $ @{term "()"})) |
179 HOLogic.literalT --> @{typ typerep} --> HOLogic.termT) |
183 bounds (Eval_Const $ HOLogic.mk_literal c $ HOLogic.mk_typerep (Ts ---> simpleT)) |
180 val term = |
184 val start_term = test_function simpleT $ |
181 fold (fn u => fn t => Eval_App $ t $ (u $ @{term "()"})) |
185 (HOLogic.pair_const simpleT @{typ "unit => Code_Evaluation.term"} |
182 bounds (Eval_Const $ HOLogic.mk_literal c $ HOLogic.mk_typerep (Ts ---> simpleT)) |
186 $ (list_comb (constr, bounds)) $ absdummy @{typ unit} term) |
183 val start_term = |
|
184 test_function simpleT $ |
|
185 (HOLogic.pair_const simpleT @{typ "unit \<Rightarrow> Code_Evaluation.term"} $ |
|
186 (list_comb (constr, bounds)) $ absdummy @{typ unit} term) |
187 in fold_rev (fn f => fn t => f t) fns start_term end |
187 in fold_rev (fn f => fn t => f t) fns start_term end |
188 fun mk_rhs exprs = |
188 fun mk_rhs exprs = |
189 mk_if (size_ge_zero, foldr1 mk_none_continuation exprs, |
189 mk_if (size_ge_zero, foldr1 mk_none_continuation exprs, Const (@{const_name None}, resultT)) |
190 Const (@{const_name "None"}, resultT)) |
190 in mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms) end |
191 in |
191 |
192 mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms) |
|
193 end |
|
194 |
|
195 |
192 |
196 (** instantiating generator classes **) |
193 (** instantiating generator classes **) |
197 |
194 |
198 fun contains_recursive_type_under_function_types xs = |
195 fun contains_recursive_type_under_function_types xs = |
199 exists (fn (_, (_, _, cs)) => cs |> exists (snd #> exists (fn dT => |
196 exists (fn (_, (_, _, cs)) => cs |> exists (snd #> exists (fn dT => |
200 (case Old_Datatype_Aux.strip_dtyp dT of (_ :: _, Old_Datatype_Aux.DtRec _) => true | _ => false)))) xs |
197 (case Old_Datatype_Aux.strip_dtyp dT of (_ :: _, Old_Datatype_Aux.DtRec _) => true | _ => false)))) xs |
201 |
198 |
202 fun instantiate_datatype (name, constprfx, sort, mk_equations, mk_T, argnames) |
199 fun instantiate_datatype (name, constprfx, sort, mk_equations, mk_T, argnames) |
203 config descr vs tycos prfx (names, auxnames) (Ts, Us) thy = |
200 config descr vs tycos prfx (names, auxnames) (Ts, Us) thy = |
204 if not (contains_recursive_type_under_function_types descr) then |
201 if not (contains_recursive_type_under_function_types descr) then |
205 let |
202 let |
206 val _ = Old_Datatype_Aux.message config ("Creating " ^ name ^ "...") |
203 val _ = Old_Datatype_Aux.message config ("Creating " ^ name ^ "...") |
216 else |
213 else |
217 (Old_Datatype_Aux.message config |
214 (Old_Datatype_Aux.message config |
218 ("Creation of " ^ name ^ " failed because the datatype is recursive under a function type"); |
215 ("Creation of " ^ name ^ " failed because the datatype is recursive under a function type"); |
219 thy) |
216 thy) |
220 |
217 |
221 val instantiate_bounded_forall_datatype = instantiate_datatype |
218 val instantiate_bounded_forall_datatype = |
222 ("bounded universal quantifiers", bounded_forallN, @{sort bounded_forall}, |
219 instantiate_datatype |
223 mk_bounded_forall_equations, bounded_forallT, ["P", "i"]); |
220 ("bounded universal quantifiers", bounded_forallN, @{sort bounded_forall}, |
224 |
221 mk_bounded_forall_equations, bounded_forallT, ["P", "i"]) |
225 val instantiate_exhaustive_datatype = instantiate_datatype |
222 |
226 ("exhaustive generators", exhaustiveN, @{sort exhaustive}, |
223 val instantiate_exhaustive_datatype = |
227 mk_equations, exhaustiveT, ["f", "i"]) |
224 instantiate_datatype |
228 |
225 ("exhaustive generators", exhaustiveN, @{sort exhaustive}, |
229 val instantiate_full_exhaustive_datatype = instantiate_datatype |
226 mk_equations, exhaustiveT, ["f", "i"]) |
230 ("full exhaustive generators", full_exhaustiveN, @{sort full_exhaustive}, |
227 |
231 mk_full_equations, full_exhaustiveT, ["f", "i"]) |
228 val instantiate_full_exhaustive_datatype = |
|
229 instantiate_datatype |
|
230 ("full exhaustive generators", full_exhaustiveN, @{sort full_exhaustive}, |
|
231 mk_full_equations, full_exhaustiveT, ["f", "i"]) |
|
232 |
232 |
233 |
233 (* building and compiling generator expressions *) |
234 (* building and compiling generator expressions *) |
234 |
235 |
235 fun mk_let_expr (x, t, e) genuine = |
236 fun mk_let_expr (x, t, e) genuine = |
|
237 let val (T1, T2) = (fastype_of x, fastype_of (e genuine)) |
|
238 in Const (@{const_name Let}, T1 --> (T1 --> T2) --> T2) $ t $ lambda x (e genuine) end |
|
239 |
|
240 fun mk_safe_let_expr genuine_only none safe (x, t, e) genuine = |
236 let |
241 let |
237 val (T1, T2) = (fastype_of x, fastype_of (e genuine)) |
242 val (T1, T2) = (fastype_of x, fastype_of (e genuine)) |
238 in |
243 val if_t = Const (@{const_name If}, @{typ bool} --> T2 --> T2 --> T2) |
239 Const (@{const_name Let}, T1 --> (T1 --> T2) --> T2) $ t $ lambda x (e genuine) |
|
240 end |
|
241 |
|
242 fun mk_safe_let_expr genuine_only none safe (x, t, e) genuine = |
|
243 let |
|
244 val (T1, T2) = (fastype_of x, fastype_of (e genuine)) |
|
245 val if_t = Const (@{const_name "If"}, @{typ bool} --> T2 --> T2 --> T2) |
|
246 in |
244 in |
247 Const (@{const_name "Quickcheck_Random.catch_match"}, T2 --> T2 --> T2) $ |
245 Const (@{const_name Quickcheck_Random.catch_match}, T2 --> T2 --> T2) $ |
248 (Const (@{const_name Let}, T1 --> (T1 --> T2) --> T2) $ t $ lambda x (e genuine)) $ |
246 (Const (@{const_name Let}, T1 --> (T1 --> T2) --> T2) $ t $ lambda x (e genuine)) $ |
249 (if_t $ genuine_only $ none $ safe false) |
247 (if_t $ genuine_only $ none $ safe false) |
250 end |
248 end |
251 |
249 |
252 fun mk_test_term lookup mk_closure mk_if mk_let none_t return ctxt = |
250 fun mk_test_term lookup mk_closure mk_if mk_let none_t return ctxt = |
253 let |
251 let |
254 val cnstrs = flat (maps |
252 val cnstrs = |
255 (map (fn (_, (Tname, _, cs)) => map (apsnd (rpair Tname o length)) cs) o #descr o snd) |
253 flat (maps |
256 (Symtab.dest (BNF_LFP_Compat.get_all (Proof_Context.theory_of ctxt) |
254 (map (fn (_, (Tname, _, cs)) => map (apsnd (rpair Tname o length)) cs) o #descr o snd) |
257 Quickcheck_Common.compat_prefs))) |
255 (Symtab.dest |
258 fun is_constrt (Const (s, T), ts) = (case (AList.lookup (op =) cnstrs s, body_type T) of |
256 (BNF_LFP_Compat.get_all (Proof_Context.theory_of ctxt) Quickcheck_Common.compat_prefs))) |
259 (SOME (i, Tname), Type (Tname', _)) => length ts = i andalso Tname = Tname' |
257 fun is_constrt (Const (s, T), ts) = |
260 | _ => false) |
258 (case (AList.lookup (op =) cnstrs s, body_type T) of |
|
259 (SOME (i, Tname), Type (Tname', _)) => length ts = i andalso Tname = Tname' |
|
260 | _ => false) |
261 | is_constrt _ = false |
261 | is_constrt _ = false |
262 fun mk_naive_test_term t = |
262 fun mk_naive_test_term t = |
263 fold_rev mk_closure (map lookup (Term.add_free_names t [])) |
263 fold_rev mk_closure (map lookup (Term.add_free_names t [])) (mk_if (t, none_t, return) true) |
264 (mk_if (t, none_t, return) true) |
|
265 fun mk_test (vars, check) = fold_rev mk_closure (map lookup vars) check |
264 fun mk_test (vars, check) = fold_rev mk_closure (map lookup vars) check |
266 fun mk_smart_test_term' concl bound_vars assms genuine = |
265 fun mk_smart_test_term' concl bound_vars assms genuine = |
267 let |
266 let |
268 fun vars_of t = subtract (op =) bound_vars (Term.add_free_names t []) |
267 fun vars_of t = subtract (op =) bound_vars (Term.add_free_names t []) |
269 fun mk_equality_term (lhs, f as Free (x, _)) c (assm, assms) = |
268 fun mk_equality_term (lhs, f as Free (x, _)) c (assm, assms) = |
270 if member (op =) (Term.add_free_names lhs bound_vars) x then |
269 if member (op =) (Term.add_free_names lhs bound_vars) x then |
271 c (assm, assms) |
270 c (assm, assms) |
272 else |
271 else |
273 (let |
272 let |
274 val rec_call = mk_smart_test_term' concl (union (op =) (vars_of assm) bound_vars) assms |
273 val rec_call = mk_smart_test_term' concl (union (op =) (vars_of assm) bound_vars) assms |
275 fun safe genuine = |
274 fun safe genuine = |
276 the_default I (Option.map mk_closure (try lookup x)) (rec_call genuine) |
275 the_default I (Option.map mk_closure (try lookup x)) (rec_call genuine) |
277 in |
276 in |
278 mk_test (remove (op =) x (vars_of assm), |
277 mk_test (remove (op =) x (vars_of assm), |
279 mk_let safe f (try lookup x) lhs |
278 mk_let safe f (try lookup x) lhs |
280 (mk_smart_test_term' concl (union (op =) (vars_of assm) bound_vars) assms) genuine) |
279 (mk_smart_test_term' concl (union (op =) (vars_of assm) bound_vars) assms) genuine) |
281 |
280 |
282 end) |
281 end |
283 | mk_equality_term (lhs, t) c (assm, assms) = |
282 | mk_equality_term (lhs, t) c (assm, assms) = |
284 if is_constrt (strip_comb t) then |
283 if is_constrt (strip_comb t) then |
285 let |
284 let |
286 val (constr, args) = strip_comb t |
285 val (constr, args) = strip_comb t |
287 val T = fastype_of t |
286 val T = fastype_of t |
288 val vars = map Free (Variable.variant_frees ctxt (concl :: assms) |
287 val vars = |
289 (map (fn t => ("x", fastype_of t)) args)) |
288 map Free |
290 val varnames = map (fst o dest_Free) vars |
289 (Variable.variant_frees ctxt (concl :: assms) |
291 val dummy_var = Free (singleton |
290 (map (fn t => ("x", fastype_of t)) args)) |
292 (Variable.variant_frees ctxt (concl :: assms @ vars)) ("dummy", T)) |
291 val varnames = map (fst o dest_Free) vars |
293 val new_assms = map HOLogic.mk_eq (vars ~~ args) |
292 val dummy_var = |
294 val bound_vars' = union (op =) (vars_of lhs) (union (op =) varnames bound_vars) |
293 Free (singleton |
295 val cont_t = mk_smart_test_term' concl bound_vars' (new_assms @ assms) genuine |
294 (Variable.variant_frees ctxt (concl :: assms @ vars)) ("dummy", T)) |
296 in |
295 val new_assms = map HOLogic.mk_eq (vars ~~ args) |
297 mk_test (vars_of lhs, |
296 val bound_vars' = union (op =) (vars_of lhs) (union (op =) varnames bound_vars) |
298 Case_Translation.make_case ctxt Case_Translation.Quiet Name.context lhs |
297 val cont_t = mk_smart_test_term' concl bound_vars' (new_assms @ assms) genuine |
299 [(list_comb (constr, vars), cont_t), (dummy_var, none_t)]) |
298 in |
300 end |
299 mk_test (vars_of lhs, |
301 else c (assm, assms) |
300 Case_Translation.make_case ctxt Case_Translation.Quiet Name.context lhs |
|
301 [(list_comb (constr, vars), cont_t), (dummy_var, none_t)]) |
|
302 end |
|
303 else c (assm, assms) |
302 fun default (assm, assms) = |
304 fun default (assm, assms) = |
303 mk_test (vars_of assm, |
305 mk_test |
304 mk_if (HOLogic.mk_not assm, none_t, |
306 (vars_of assm, |
305 mk_smart_test_term' concl (union (op =) (vars_of assm) bound_vars) assms) genuine) |
307 mk_if (HOLogic.mk_not assm, none_t, |
|
308 mk_smart_test_term' concl (union (op =) (vars_of assm) bound_vars) assms) genuine) |
306 in |
309 in |
307 case assms of [] => mk_test (vars_of concl, mk_if (concl, none_t, return) genuine) |
310 (case assms of |
308 | assm :: assms => |
311 [] => mk_test (vars_of concl, mk_if (concl, none_t, return) genuine) |
|
312 | assm :: assms => |
309 if Config.get ctxt optimise_equality then |
313 if Config.get ctxt optimise_equality then |
310 (case try HOLogic.dest_eq assm of |
314 (case try HOLogic.dest_eq assm of |
311 SOME (lhs, rhs) => |
315 SOME (lhs, rhs) => |
312 mk_equality_term (lhs, rhs) (mk_equality_term (rhs, lhs) default) (assm, assms) |
316 mk_equality_term (lhs, rhs) (mk_equality_term (rhs, lhs) default) (assm, assms) |
313 | NONE => default (assm, assms)) |
317 | NONE => default (assm, assms)) |
314 else default (assm, assms) |
318 else default (assm, assms)) |
315 end |
319 end |
316 val mk_smart_test_term = |
320 val mk_smart_test_term = |
317 Quickcheck_Common.strip_imp #> (fn (assms, concl) => mk_smart_test_term' concl [] assms true) |
321 Quickcheck_Common.strip_imp #> (fn (assms, concl) => mk_smart_test_term' concl [] assms true) |
318 in |
322 in if Config.get ctxt smart_quantifier then mk_smart_test_term else mk_naive_test_term end |
319 if Config.get ctxt smart_quantifier then mk_smart_test_term else mk_naive_test_term |
|
320 end |
|
321 |
323 |
322 fun mk_fast_generator_expr ctxt (t, eval_terms) = |
324 fun mk_fast_generator_expr ctxt (t, eval_terms) = |
323 let |
325 let |
324 val ctxt' = Variable.auto_fixes t ctxt |
326 val ctxt' = Variable.auto_fixes t ctxt |
325 val names = Term.add_free_names t [] |
327 val names = Term.add_free_names t [] |
326 val frees = map Free (Term.add_frees t []) |
328 val frees = map Free (Term.add_frees t []) |
327 fun lookup v = the (AList.lookup (op =) (names ~~ frees) v) |
329 fun lookup v = the (AList.lookup (op =) (names ~~ frees) v) |
328 val ([depth_name], _) = Variable.variant_fixes ["depth"] ctxt' |
330 val ([depth_name], _) = Variable.variant_fixes ["depth"] ctxt' |
329 val depth = Free (depth_name, @{typ natural}) |
331 val depth = Free (depth_name, @{typ natural}) |
330 fun return _ = @{term "throw_Counterexample :: term list => unit"} $ |
332 fun return _ = |
331 (HOLogic.mk_list @{typ "term"} |
333 @{term "throw_Counterexample :: term list \<Rightarrow> unit"} $ |
332 (map (fn t => HOLogic.mk_term_of (fastype_of t) t) (frees @ eval_terms))) |
334 (HOLogic.mk_list @{typ term} |
|
335 (map (fn t => HOLogic.mk_term_of (fastype_of t) t) (frees @ eval_terms))) |
333 fun mk_exhaustive_closure (free as Free (_, T)) t = |
336 fun mk_exhaustive_closure (free as Free (_, T)) t = |
334 Const (@{const_name "Quickcheck_Exhaustive.fast_exhaustive_class.fast_exhaustive"}, |
337 Const (@{const_name Quickcheck_Exhaustive.fast_exhaustive_class.fast_exhaustive}, |
335 fast_exhaustiveT T) |
338 fast_exhaustiveT T) $ lambda free t $ depth |
336 $ lambda free t $ depth |
|
337 val none_t = @{term "()"} |
339 val none_t = @{term "()"} |
338 fun mk_safe_if (cond, then_t, else_t) genuine = mk_if (cond, then_t, else_t genuine) |
340 fun mk_safe_if (cond, then_t, else_t) genuine = mk_if (cond, then_t, else_t genuine) |
339 fun mk_let _ def v_opt t e = mk_let_expr (the_default def v_opt, t, e) |
341 fun mk_let _ def v_opt t e = mk_let_expr (the_default def v_opt, t, e) |
340 val mk_test_term = mk_test_term lookup mk_exhaustive_closure mk_safe_if mk_let none_t return ctxt |
342 val mk_test_term = |
|
343 mk_test_term lookup mk_exhaustive_closure mk_safe_if mk_let none_t return ctxt |
341 in lambda depth (@{term "catch_Counterexample :: unit => term list option"} $ mk_test_term t) end |
344 in lambda depth (@{term "catch_Counterexample :: unit => term list option"} $ mk_test_term t) end |
342 |
345 |
343 fun mk_unknown_term T = HOLogic.reflect_term (Const (@{const_name Quickcheck_Exhaustive.unknown}, T)) |
346 fun mk_unknown_term T = |
344 |
347 HOLogic.reflect_term (Const (@{const_name Quickcheck_Exhaustive.unknown}, T)) |
345 fun mk_safe_term t = @{term "Quickcheck_Random.catch_match :: term => term => term"} |
348 |
346 $ (HOLogic.mk_term_of (fastype_of t) t) $ mk_unknown_term (fastype_of t) |
349 fun mk_safe_term t = |
347 |
350 @{term "Quickcheck_Random.catch_match :: term \<Rightarrow> term \<Rightarrow> term"} $ |
348 fun mk_return t genuine = @{term "Some :: bool * term list => (bool * term list) option"} $ |
351 (HOLogic.mk_term_of (fastype_of t) t) $ mk_unknown_term (fastype_of t) |
349 (HOLogic.pair_const @{typ bool} @{typ "term list"} $ Quickcheck_Common.reflect_bool genuine $ t) |
352 |
|
353 fun mk_return t genuine = |
|
354 @{term "Some :: bool \<times> term list \<Rightarrow> (bool \<times> term list) option"} $ |
|
355 (HOLogic.pair_const @{typ bool} @{typ "term list"} $ |
|
356 Quickcheck_Common.reflect_bool genuine $ t) |
350 |
357 |
351 fun mk_generator_expr ctxt (t, eval_terms) = |
358 fun mk_generator_expr ctxt (t, eval_terms) = |
352 let |
359 let |
353 val ctxt' = Variable.auto_fixes t ctxt |
360 val ctxt' = Variable.auto_fixes t ctxt |
354 val names = Term.add_free_names t [] |
361 val names = Term.add_free_names t [] |
355 val frees = map Free (Term.add_frees t []) |
362 val frees = map Free (Term.add_frees t []) |
356 fun lookup v = the (AList.lookup (op =) (names ~~ frees) v) |
363 fun lookup v = the (AList.lookup (op =) (names ~~ frees) v) |
357 val ([depth_name, genuine_only_name], _) = |
364 val ([depth_name, genuine_only_name], _) = |
358 Variable.variant_fixes ["depth", "genuine_only"] ctxt' |
365 Variable.variant_fixes ["depth", "genuine_only"] ctxt' |
359 val depth = Free (depth_name, @{typ natural}) |
366 val depth = Free (depth_name, @{typ natural}) |
360 val genuine_only = Free (genuine_only_name, @{typ bool}) |
367 val genuine_only = Free (genuine_only_name, @{typ bool}) |
361 val return = mk_return (HOLogic.mk_list @{typ "term"} |
368 val return = |
|
369 mk_return (HOLogic.mk_list @{typ term} |
362 (map (fn t => HOLogic.mk_term_of (fastype_of t) t) frees @ map mk_safe_term eval_terms)) |
370 (map (fn t => HOLogic.mk_term_of (fastype_of t) t) frees @ map mk_safe_term eval_terms)) |
363 fun mk_exhaustive_closure (free as Free (_, T)) t = |
371 fun mk_exhaustive_closure (free as Free (_, T)) t = |
364 Const (@{const_name "Quickcheck_Exhaustive.exhaustive_class.exhaustive"}, exhaustiveT T) |
372 Const (@{const_name Quickcheck_Exhaustive.exhaustive_class.exhaustive}, exhaustiveT T) $ |
365 $ lambda free t $ depth |
373 lambda free t $ depth |
366 val none_t = Const (@{const_name "None"}, resultT) |
374 val none_t = Const (@{const_name None}, resultT) |
367 val mk_if = Quickcheck_Common.mk_safe_if genuine_only none_t |
375 val mk_if = Quickcheck_Common.mk_safe_if genuine_only none_t |
368 fun mk_let safe def v_opt t e = mk_safe_let_expr genuine_only none_t safe (the_default def v_opt, t, e) |
376 fun mk_let safe def v_opt t e = |
|
377 mk_safe_let_expr genuine_only none_t safe (the_default def v_opt, t, e) |
369 val mk_test_term = mk_test_term lookup mk_exhaustive_closure mk_if mk_let none_t return ctxt |
378 val mk_test_term = mk_test_term lookup mk_exhaustive_closure mk_if mk_let none_t return ctxt |
370 in lambda genuine_only (lambda depth (mk_test_term t)) end |
379 in lambda genuine_only (lambda depth (mk_test_term t)) end |
371 |
380 |
372 fun mk_full_generator_expr ctxt (t, eval_terms) = |
381 fun mk_full_generator_expr ctxt (t, eval_terms) = |
373 let |
382 let |
377 val frees = map Free (Term.add_frees t []) |
386 val frees = map Free (Term.add_frees t []) |
378 val ([depth_name, genuine_only_name], ctxt'') = |
387 val ([depth_name, genuine_only_name], ctxt'') = |
379 Variable.variant_fixes ["depth", "genuine_only"] ctxt' |
388 Variable.variant_fixes ["depth", "genuine_only"] ctxt' |
380 val (term_names, _) = Variable.variant_fixes (map (prefix "t_") names) ctxt'' |
389 val (term_names, _) = Variable.variant_fixes (map (prefix "t_") names) ctxt'' |
381 val depth = Free (depth_name, @{typ natural}) |
390 val depth = Free (depth_name, @{typ natural}) |
382 val genuine_only = Free (genuine_only_name, @{typ bool}) |
391 val genuine_only = Free (genuine_only_name, @{typ bool}) |
383 val term_vars = map (fn n => Free (n, @{typ "unit => term"})) term_names |
392 val term_vars = map (fn n => Free (n, @{typ "unit \<Rightarrow> term"})) term_names |
384 fun lookup v = the (AList.lookup (op =) (names ~~ (frees ~~ term_vars)) v) |
393 fun lookup v = the (AList.lookup (op =) (names ~~ (frees ~~ term_vars)) v) |
385 val return = mk_return (HOLogic.mk_list @{typ term} |
394 val return = |
|
395 mk_return |
|
396 (HOLogic.mk_list @{typ term} |
386 (map (fn v => v $ @{term "()"}) term_vars @ map mk_safe_term eval_terms)) |
397 (map (fn v => v $ @{term "()"}) term_vars @ map mk_safe_term eval_terms)) |
387 fun mk_exhaustive_closure (free as Free (_, T), term_var) t = |
398 fun mk_exhaustive_closure (free as Free (_, T), term_var) t = |
388 if Sign.of_sort thy (T, @{sort check_all}) then |
399 if Sign.of_sort thy (T, @{sort check_all}) then |
389 Const (@{const_name "Quickcheck_Exhaustive.check_all_class.check_all"}, check_allT T) |
400 Const (@{const_name Quickcheck_Exhaustive.check_all_class.check_all}, check_allT T) $ |
390 $ (HOLogic.case_prod_const (T, @{typ "unit => term"}, resultT) |
401 (HOLogic.case_prod_const (T, @{typ "unit \<Rightarrow> term"}, resultT) $ |
391 $ lambda free (lambda term_var t)) |
402 lambda free (lambda term_var t)) |
392 else |
403 else |
393 Const (@{const_name "Quickcheck_Exhaustive.full_exhaustive_class.full_exhaustive"}, full_exhaustiveT T) |
404 Const (@{const_name Quickcheck_Exhaustive.full_exhaustive_class.full_exhaustive}, |
394 $ (HOLogic.case_prod_const (T, @{typ "unit => term"}, resultT) |
405 full_exhaustiveT T) $ |
395 $ lambda free (lambda term_var t)) $ depth |
406 (HOLogic.case_prod_const (T, @{typ "unit \<Rightarrow> term"}, resultT) $ |
396 val none_t = Const (@{const_name "None"}, resultT) |
407 lambda free (lambda term_var t)) $ depth |
|
408 val none_t = Const (@{const_name None}, resultT) |
397 val mk_if = Quickcheck_Common.mk_safe_if genuine_only none_t |
409 val mk_if = Quickcheck_Common.mk_safe_if genuine_only none_t |
398 fun mk_let safe _ (SOME (v, term_var)) t e = |
410 fun mk_let safe _ (SOME (v, term_var)) t e = |
399 mk_safe_let_expr genuine_only none_t safe (v, t, |
411 mk_safe_let_expr genuine_only none_t safe (v, t, |
400 e #> subst_free [(term_var, absdummy @{typ unit} (mk_safe_term t))]) |
412 e #> subst_free [(term_var, absdummy @{typ unit} (mk_safe_term t))]) |
401 | mk_let safe v NONE t e = mk_safe_let_expr genuine_only none_t safe (v, t, e) |
413 | mk_let safe v NONE t e = mk_safe_let_expr genuine_only none_t safe (v, t, e) |
402 val mk_test_term = mk_test_term lookup mk_exhaustive_closure mk_if mk_let none_t return ctxt |
414 val mk_test_term = mk_test_term lookup mk_exhaustive_closure mk_if mk_let none_t return ctxt |
403 in lambda genuine_only (lambda depth (mk_test_term t)) end |
415 in lambda genuine_only (lambda depth (mk_test_term t)) end |
404 |
416 |
405 fun mk_parametric_generator_expr mk_generator_expr = |
417 fun mk_parametric_generator_expr mk_generator_expr = |
406 Quickcheck_Common.gen_mk_parametric_generator_expr |
418 Quickcheck_Common.gen_mk_parametric_generator_expr |
407 ((mk_generator_expr, |
419 ((mk_generator_expr, |
408 absdummy @{typ bool} (absdummy @{typ natural} (Const (@{const_name "None"}, resultT)))), |
420 absdummy @{typ bool} (absdummy @{typ natural} (Const (@{const_name None}, resultT)))), |
409 @{typ bool} --> @{typ natural} --> resultT) |
421 @{typ bool} --> @{typ natural} --> resultT) |
410 |
422 |
411 fun mk_validator_expr ctxt t = |
423 fun mk_validator_expr ctxt t = |
412 let |
424 let |
413 fun bounded_forallT T = (T --> @{typ bool}) --> @{typ natural} --> @{typ bool} |
425 fun bounded_forallT T = (T --> @{typ bool}) --> @{typ natural} --> @{typ bool} |
416 val frees = map Free (Term.add_frees t []) |
428 val frees = map Free (Term.add_frees t []) |
417 fun lookup v = the (AList.lookup (op =) (names ~~ frees) v) |
429 fun lookup v = the (AList.lookup (op =) (names ~~ frees) v) |
418 val ([depth_name], _) = Variable.variant_fixes ["depth"] ctxt' |
430 val ([depth_name], _) = Variable.variant_fixes ["depth"] ctxt' |
419 val depth = Free (depth_name, @{typ natural}) |
431 val depth = Free (depth_name, @{typ natural}) |
420 fun mk_bounded_forall (Free (s, T)) t = |
432 fun mk_bounded_forall (Free (s, T)) t = |
421 Const (@{const_name "Quickcheck_Exhaustive.bounded_forall_class.bounded_forall"}, bounded_forallT T) |
433 Const (@{const_name Quickcheck_Exhaustive.bounded_forall_class.bounded_forall}, |
422 $ lambda (Free (s, T)) t $ depth |
434 bounded_forallT T) $ lambda (Free (s, T)) t $ depth |
423 fun mk_safe_if (cond, then_t, else_t) genuine = mk_if (cond, then_t, else_t genuine) |
435 fun mk_safe_if (cond, then_t, else_t) genuine = mk_if (cond, then_t, else_t genuine) |
424 fun mk_let _ def v_opt t e = mk_let_expr (the_default def v_opt, t, e) |
436 fun mk_let _ def v_opt t e = mk_let_expr (the_default def v_opt, t, e) |
425 val mk_test_term = |
437 val mk_test_term = |
426 mk_test_term lookup mk_bounded_forall mk_safe_if mk_let @{term True} (K @{term False}) ctxt |
438 mk_test_term lookup mk_bounded_forall mk_safe_if mk_let @{term True} (K @{term False}) ctxt |
427 in lambda depth (mk_test_term t) end |
439 in lambda depth (mk_test_term t) end |
428 |
440 |
429 |
441 fun mk_bounded_forall_generator_expr ctxt (t, eval_terms) = |
430 fun mk_bounded_forall_generator_expr ctxt (t, eval_terms) = |
|
431 let |
442 let |
432 val frees = Term.add_free_names t [] |
443 val frees = Term.add_free_names t [] |
433 val dummy_term = @{term "Code_Evaluation.Const (STR ''Pure.dummy_pattern'') |
444 val dummy_term = |
434 (Typerep.Typerep (STR ''dummy'') [])"} |
445 @{term "Code_Evaluation.Const (STR ''Pure.dummy_pattern'') (Typerep.Typerep (STR ''dummy'') [])"} |
435 val return = @{term "Some :: term list => term list option"} $ |
446 val return = |
436 (HOLogic.mk_list @{typ "term"} |
447 @{term "Some :: term list => term list option"} $ |
437 (replicate (length frees + length eval_terms) dummy_term)) |
448 (HOLogic.mk_list @{typ term} (replicate (length frees + length eval_terms) dummy_term)) |
438 val wrap = absdummy @{typ bool} |
449 val wrap = absdummy @{typ bool} |
439 (@{term "If :: bool => term list option => term list option => term list option"} $ |
450 (@{term "If :: bool \<Rightarrow> term list option \<Rightarrow> term list option \<Rightarrow> term list option"} $ |
440 Bound 0 $ @{term "None :: term list option"} $ return) |
451 Bound 0 $ @{term "None :: term list option"} $ return) |
441 in HOLogic.mk_comp (wrap, mk_validator_expr ctxt t) end |
452 in HOLogic.mk_comp (wrap, mk_validator_expr ctxt t) end |
442 |
453 |
443 |
454 |
444 (** generator compiliation **) |
455 (** generator compiliation **) |
445 |
456 |
446 structure Data = Proof_Data |
457 structure Data = Proof_Data |
447 ( |
458 ( |
448 type T = |
459 type T = |
449 (unit -> Code_Numeral.natural -> bool -> |
460 (unit -> Code_Numeral.natural -> bool -> Code_Numeral.natural -> (bool * term list) option) * |
450 Code_Numeral.natural -> (bool * term list) option) * |
|
451 (unit -> (Code_Numeral.natural -> term list option) list) * |
461 (unit -> (Code_Numeral.natural -> term list option) list) * |
452 (unit -> (Code_Numeral.natural -> bool) list); |
462 (unit -> (Code_Numeral.natural -> bool) list) |
453 val empty: T = |
463 val empty: T = |
454 (fn () => raise Fail "counterexample", |
464 (fn () => raise Fail "counterexample", |
455 fn () => raise Fail "counterexample_batch", |
465 fn () => raise Fail "counterexample_batch", |
456 fn () => raise Fail "validator_batch"); |
466 fn () => raise Fail "validator_batch") |
457 fun init _ = empty; |
467 fun init _ = empty |
458 ); |
468 ) |
459 |
469 |
460 val get_counterexample = #1 o Data.get; |
470 val get_counterexample = #1 o Data.get |
461 val get_counterexample_batch = #2 o Data.get; |
471 val get_counterexample_batch = #2 o Data.get |
462 val get_validator_batch = #3 o Data.get; |
472 val get_validator_batch = #3 o Data.get |
463 |
473 |
464 val put_counterexample = Data.map o @{apply 3(1)} o K; |
474 val put_counterexample = Data.map o @{apply 3(1)} o K |
465 val put_counterexample_batch = Data.map o @{apply 3(2)} o K; |
475 val put_counterexample_batch = Data.map o @{apply 3(2)} o K |
466 val put_validator_batch = Data.map o @{apply 3(3)} o K; |
476 val put_validator_batch = Data.map o @{apply 3(3)} o K |
467 |
477 |
468 val target = "Quickcheck"; |
478 val target = "Quickcheck" |
469 |
479 |
470 fun compile_generator_expr_raw ctxt ts = |
480 fun compile_generator_expr_raw ctxt ts = |
471 let |
481 let |
472 val mk_generator_expr = |
482 val mk_generator_expr = |
473 if Config.get ctxt fast then mk_fast_generator_expr |
483 if Config.get ctxt fast then mk_fast_generator_expr |
474 else if Config.get ctxt bounded_forall then mk_bounded_forall_generator_expr |
484 else if Config.get ctxt bounded_forall then mk_bounded_forall_generator_expr |
475 else if Config.get ctxt full_support then mk_full_generator_expr else mk_generator_expr |
485 else if Config.get ctxt full_support then mk_full_generator_expr else mk_generator_expr |
476 val t' = mk_parametric_generator_expr mk_generator_expr ctxt ts; |
486 val t' = mk_parametric_generator_expr mk_generator_expr ctxt ts |
477 val compile = Code_Runtime.dynamic_value_strict |
487 val compile = |
478 (get_counterexample, put_counterexample, "Exhaustive_Generators.put_counterexample") |
488 Code_Runtime.dynamic_value_strict |
479 ctxt (SOME target) (fn proc => fn g => |
489 (get_counterexample, put_counterexample, "Exhaustive_Generators.put_counterexample") |
480 fn card => fn genuine_only => fn size => g card genuine_only size |
490 ctxt (SOME target) |
|
491 (fn proc => fn g => fn card => fn genuine_only => fn size => |
|
492 g card genuine_only size |
481 |> (Option.map o apsnd o map) proc) t' [] |
493 |> (Option.map o apsnd o map) proc) t' [] |
482 in |
494 in |
483 fn genuine_only => fn [card, size] => rpair NONE (compile card genuine_only size |> |
495 fn genuine_only => fn [card, size] => |
484 (if Config.get ctxt quickcheck_pretty then |
496 rpair NONE (compile card genuine_only size |
485 Option.map (apsnd (map Quickcheck_Common.post_process_term)) else I)) |
497 |> (if Config.get ctxt quickcheck_pretty then |
486 end; |
498 Option.map (apsnd (map Quickcheck_Common.post_process_term)) else I)) |
|
499 end |
487 |
500 |
488 fun compile_generator_expr ctxt ts = |
501 fun compile_generator_expr ctxt ts = |
489 let |
502 let val compiled = compile_generator_expr_raw ctxt ts in |
490 val compiled = compile_generator_expr_raw ctxt ts; |
503 fn genuine_only => fn [card, size] => |
491 in fn genuine_only => fn [card, size] => |
504 compiled genuine_only |
492 compiled genuine_only [Code_Numeral.natural_of_integer card, Code_Numeral.natural_of_integer size] |
505 [Code_Numeral.natural_of_integer card, Code_Numeral.natural_of_integer size] |
493 end; |
506 end |
494 |
507 |
495 fun compile_generator_exprs_raw ctxt ts = |
508 fun compile_generator_exprs_raw ctxt ts = |
496 let |
509 let |
497 val ts' = map (fn t => mk_generator_expr ctxt (t, [])) ts; |
510 val ts' = map (fn t => mk_generator_expr ctxt (t, [])) ts |
498 val compiles = Code_Runtime.dynamic_value_strict |
511 val compiles = |
499 (get_counterexample_batch, put_counterexample_batch, |
512 Code_Runtime.dynamic_value_strict |
500 "Exhaustive_Generators.put_counterexample_batch") |
513 (get_counterexample_batch, put_counterexample_batch, |
501 ctxt (SOME target) (fn proc => map (fn g => g #> (Option.map o map) proc)) |
514 "Exhaustive_Generators.put_counterexample_batch") |
502 (HOLogic.mk_list @{typ "natural => term list option"} ts') [] |
515 ctxt (SOME target) (fn proc => map (fn g => g #> (Option.map o map) proc)) |
|
516 (HOLogic.mk_list @{typ "natural => term list option"} ts') [] |
503 in |
517 in |
504 map (fn compile => fn size => compile size |
518 map (fn compile => fn size => |
505 |> (Option.map o map) Quickcheck_Common.post_process_term) compiles |
519 compile size |> (Option.map o map) Quickcheck_Common.post_process_term) compiles |
506 end; |
520 end |
507 |
521 |
508 fun compile_generator_exprs ctxt ts = |
522 fun compile_generator_exprs ctxt ts = |
509 compile_generator_exprs_raw ctxt ts |
523 compile_generator_exprs_raw ctxt ts |
510 |> map (fn f => fn size => f (Code_Numeral.natural_of_integer size)); |
524 |> map (fn f => fn size => f (Code_Numeral.natural_of_integer size)) |
511 |
525 |
512 fun compile_validator_exprs_raw ctxt ts = |
526 fun compile_validator_exprs_raw ctxt ts = |
513 let |
527 let val ts' = map (mk_validator_expr ctxt) ts in |
514 val ts' = map (mk_validator_expr ctxt) ts |
|
515 in |
|
516 Code_Runtime.dynamic_value_strict |
528 Code_Runtime.dynamic_value_strict |
517 (get_validator_batch, put_validator_batch, "Exhaustive_Generators.put_validator_batch") |
529 (get_validator_batch, put_validator_batch, "Exhaustive_Generators.put_validator_batch") |
518 ctxt (SOME target) (K I) (HOLogic.mk_list @{typ "natural => bool"} ts') [] |
530 ctxt (SOME target) (K I) (HOLogic.mk_list @{typ "natural \<Rightarrow> bool"} ts') [] |
519 end; |
531 end |
520 |
532 |
521 fun compile_validator_exprs ctxt ts = |
533 fun compile_validator_exprs ctxt ts = |
522 compile_validator_exprs_raw ctxt ts |
534 compile_validator_exprs_raw ctxt ts |
523 |> map (fn f => fn size => f (Code_Numeral.natural_of_integer size)); |
535 |> map (fn f => fn size => f (Code_Numeral.natural_of_integer size)) |
524 |
536 |
525 fun size_matters_for thy Ts = not (forall (fn T => Sign.of_sort thy (T, @{sort check_all})) Ts) |
537 fun size_matters_for thy Ts = not (forall (fn T => Sign.of_sort thy (T, @{sort check_all})) Ts) |
526 |
538 |
527 val test_goals = |
539 val test_goals = |
528 Quickcheck_Common.generator_test_goal_terms ("exhaustive", (size_matters_for, compile_generator_expr)); |
540 Quickcheck_Common.generator_test_goal_terms |
529 |
541 ("exhaustive", (size_matters_for, compile_generator_expr)) |
|
542 |
|
543 |
530 (* setup *) |
544 (* setup *) |
531 |
545 |
532 val setup_exhaustive_datatype_interpretation = |
546 val setup_exhaustive_datatype_interpretation = |
533 Quickcheck_Common.datatype_interpretation @{plugin quickcheck_exhaustive} |
547 Quickcheck_Common.datatype_interpretation @{plugin quickcheck_exhaustive} |
534 (@{sort exhaustive}, instantiate_exhaustive_datatype) |
548 (@{sort exhaustive}, instantiate_exhaustive_datatype) |