src/HOL/Tools/Quickcheck/exhaustive_generators.ML
 changeset 62981 3a01f1f58630 parent 62979 1e527c40ae40 child 67149 e61557884799
equal inserted replaced
62980:fedbdfbaa07a 62981:3a01f1f58630
55 val size_pred = @{term "(i :: natural) - 1"}
55 val size_pred = @{term "(i :: natural) - 1"}
56 val size_ge_zero = @{term "(i :: natural) > 0"}
56 val size_ge_zero = @{term "(i :: natural) > 0"}
57
57
58 fun mk_none_continuation (x, y) =
58 fun mk_none_continuation (x, y) =
59   let val (T as Type (@{type_name option}, _)) = fastype_of x
59   let val (T as Type (@{type_name option}, _)) = fastype_of x
60   in Const (@{const_name Quickcheck_Exhaustive.orelse}, T --> T --> T) \$ x \$ y end
60   in Const (@{const_name orelse}, T --> T --> T) \$ x \$ y end
61
61
62 fun mk_if (b, t, e) =
62 fun mk_if (b, t, e) =
63   let val T = fastype_of t
63   let val T = fastype_of t
64   in Const (@{const_name If}, @{typ bool} --> T --> T --> T) \$ b \$ t \$ e end
64   in Const (@{const_name If}, @{typ bool} --> T --> T --> T) \$ b \$ t \$ e end
65
65
117   in fold_rev (fn f => fn t => f t) fns start_term end
117   in fold_rev (fn f => fn t => f t) fns start_term end
118
118
119 fun mk_equations functerms =
119 fun mk_equations functerms =
120   let
120   let
121     fun test_function T = Free ("f", T --> resultT)
121     fun test_function T = Free ("f", T --> resultT)
122     val mk_call = gen_mk_call (fn T =>
122     val mk_call = gen_mk_call (fn T => Const (@{const_name exhaustive}, exhaustiveT T))
123       Const (@{const_name Quickcheck_Exhaustive.exhaustive_class.exhaustive}, exhaustiveT T))

124     val mk_aux_call = gen_mk_aux_call functerms
123     val mk_aux_call = gen_mk_aux_call functerms
125     val mk_consexpr = gen_mk_consexpr test_function
124     val mk_consexpr = gen_mk_consexpr test_function
126     fun mk_rhs exprs =
125     fun mk_rhs exprs =
127       mk_if (size_ge_zero, foldr1 mk_none_continuation exprs, Const (@{const_name None}, resultT))
126       mk_if (size_ge_zero, foldr1 mk_none_continuation exprs, Const (@{const_name None}, resultT))
128   in mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms) end
127   in mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms) end
129
128
130 fun mk_bounded_forall_equations functerms =
129 fun mk_bounded_forall_equations functerms =
131   let
130   let
132     fun test_function T = Free ("P", T --> @{typ bool})
131     fun test_function T = Free ("P", T --> @{typ bool})
133     val mk_call = gen_mk_call (fn T =>
132     val mk_call = gen_mk_call (fn T => Const (@{const_name bounded_forall}, bounded_forallT T))
134       Const (@{const_name Quickcheck_Exhaustive.bounded_forall_class.bounded_forall},

135         bounded_forallT T))

136     val mk_aux_call = gen_mk_aux_call functerms
133     val mk_aux_call = gen_mk_aux_call functerms
137     val mk_consexpr = gen_mk_consexpr test_function
134     val mk_consexpr = gen_mk_consexpr test_function
138     fun mk_rhs exprs = mk_if (size_ge_zero, foldr1 HOLogic.mk_conj exprs, @{term True})
135     fun mk_rhs exprs = 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
136   in mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms) end
140
137
143     fun test_function T = Free ("f", termifyT T --> resultT)
140     fun test_function T = Free ("f", termifyT T --> resultT)
144     fun case_prod_const T =
141     fun case_prod_const T =
145       HOLogic.case_prod_const (T, @{typ "unit \<Rightarrow> Code_Evaluation.term"}, resultT)
142       HOLogic.case_prod_const (T, @{typ "unit \<Rightarrow> Code_Evaluation.term"}, resultT)
146     fun mk_call T =
143     fun mk_call T =
147       let
144       let
148         val full_exhaustive =
145         val full_exhaustive = Const (@{const_name full_exhaustive}, full_exhaustiveT T)
149           Const (@{const_name Quickcheck_Exhaustive.full_exhaustive_class.full_exhaustive},

150             full_exhaustiveT T)

151       in
146       in
152         (T,
147         (T,
153           fn t =>
148           fn t =>
154             full_exhaustive \$
149             full_exhaustive \$
155               (case_prod_const T \$ absdummy T (absdummy @{typ "unit \<Rightarrow> Code_Evaluation.term"} t)) \$
150               (case_prod_const T \$ absdummy T (absdummy @{typ "unit \<Rightarrow> Code_Evaluation.term"} t)) \$
332     fun return _ =
327     fun return _ =
333       @{term "throw_Counterexample :: term list \<Rightarrow> unit"} \$
328       @{term "throw_Counterexample :: term list \<Rightarrow> unit"} \$
334         (HOLogic.mk_list @{typ term}
329         (HOLogic.mk_list @{typ term}
335           (map (fn t => HOLogic.mk_term_of (fastype_of t) t) (frees @ eval_terms)))
330           (map (fn t => HOLogic.mk_term_of (fastype_of t) t) (frees @ eval_terms)))
336     fun mk_exhaustive_closure (free as Free (_, T)) t =
331     fun mk_exhaustive_closure (free as Free (_, T)) t =
337       Const (@{const_name Quickcheck_Exhaustive.fast_exhaustive_class.fast_exhaustive},
332       Const (@{const_name fast_exhaustive}, fast_exhaustiveT T) \$ lambda free t \$ depth
338         fast_exhaustiveT T) \$ lambda free t \$ depth

339     val none_t = @{term "()"}
333     val none_t = @{term "()"}
340     fun mk_safe_if (cond, then_t, else_t) genuine = mk_if (cond, then_t, else_t genuine)
334     fun mk_safe_if (cond, then_t, else_t) genuine = mk_if (cond, then_t, else_t genuine)
341     fun mk_let _ def v_opt t e = mk_let_expr (the_default def v_opt, t, e)
335     fun mk_let _ def v_opt t e = mk_let_expr (the_default def v_opt, t, e)
342     val mk_test_term =
336     val mk_test_term =
343       mk_test_term lookup mk_exhaustive_closure mk_safe_if mk_let none_t return ctxt
337       mk_test_term lookup mk_exhaustive_closure mk_safe_if mk_let none_t return ctxt
344   in lambda depth (@{term "catch_Counterexample :: unit => term list option"} \$ mk_test_term t) end
338   in lambda depth (@{term "catch_Counterexample :: unit => term list option"} \$ mk_test_term t) end
345
339
346 fun mk_unknown_term T =
340 fun mk_unknown_term T =
347   HOLogic.reflect_term (Const (@{const_name Quickcheck_Exhaustive.unknown}, T))
341   HOLogic.reflect_term (Const (@{const_name unknown}, T))
348
342
349 fun mk_safe_term t =
343 fun mk_safe_term t =
350   @{term "Quickcheck_Random.catch_match :: term \<Rightarrow> term \<Rightarrow> term"} \$
344   @{term "Quickcheck_Random.catch_match :: term \<Rightarrow> term \<Rightarrow> term"} \$
351     (HOLogic.mk_term_of (fastype_of t) t) \$ mk_unknown_term (fastype_of t)
345     (HOLogic.mk_term_of (fastype_of t) t) \$ mk_unknown_term (fastype_of t)
352
346
367     val genuine_only = Free (genuine_only_name, @{typ bool})
361     val genuine_only = Free (genuine_only_name, @{typ bool})
368     val return =
362     val return =
369       mk_return (HOLogic.mk_list @{typ term}
363       mk_return (HOLogic.mk_list @{typ term}
370         (map (fn t => HOLogic.mk_term_of (fastype_of t) t) frees @ map mk_safe_term eval_terms))
364         (map (fn t => HOLogic.mk_term_of (fastype_of t) t) frees @ map mk_safe_term eval_terms))
371     fun mk_exhaustive_closure (free as Free (_, T)) t =
365     fun mk_exhaustive_closure (free as Free (_, T)) t =
372       Const (@{const_name Quickcheck_Exhaustive.exhaustive_class.exhaustive}, exhaustiveT T) \$
366       Const (@{const_name exhaustive}, exhaustiveT T) \$ lambda free t \$ depth
373         lambda free t \$ depth

374     val none_t = Const (@{const_name None}, resultT)
367     val none_t = Const (@{const_name None}, resultT)
375     val mk_if = Quickcheck_Common.mk_safe_if genuine_only none_t
368     val mk_if = Quickcheck_Common.mk_safe_if genuine_only none_t
376     fun mk_let safe def v_opt t e =
369     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)
370       mk_safe_let_expr genuine_only none_t safe (the_default def v_opt, t, e)
378     val mk_test_term = mk_test_term lookup mk_exhaustive_closure mk_if mk_let none_t return ctxt
371     val mk_test_term = mk_test_term lookup mk_exhaustive_closure mk_if mk_let none_t return ctxt
395       mk_return
388       mk_return
396         (HOLogic.mk_list @{typ term}
389         (HOLogic.mk_list @{typ term}
397           (map (fn v => v \$ @{term "()"}) term_vars @ map mk_safe_term eval_terms))
390           (map (fn v => v \$ @{term "()"}) term_vars @ map mk_safe_term eval_terms))
398     fun mk_exhaustive_closure (free as Free (_, T), term_var) t =
391     fun mk_exhaustive_closure (free as Free (_, T), term_var) t =
399       if Sign.of_sort thy (T, @{sort check_all}) then
392       if Sign.of_sort thy (T, @{sort check_all}) then
400         Const (@{const_name Quickcheck_Exhaustive.check_all_class.check_all}, check_allT T) \$
393         Const (@{const_name check_all}, check_allT T) \$
401           (HOLogic.case_prod_const (T, @{typ "unit \<Rightarrow> term"}, resultT) \$
394           (HOLogic.case_prod_const (T, @{typ "unit \<Rightarrow> term"}, resultT) \$
402             lambda free (lambda term_var t))
395             lambda free (lambda term_var t))
403       else
396       else
404         Const (@{const_name Quickcheck_Exhaustive.full_exhaustive_class.full_exhaustive},
397         Const (@{const_name full_exhaustive}, full_exhaustiveT T) \$
405           full_exhaustiveT T) \$

406           (HOLogic.case_prod_const (T, @{typ "unit \<Rightarrow> term"}, resultT) \$
398           (HOLogic.case_prod_const (T, @{typ "unit \<Rightarrow> term"}, resultT) \$
407             lambda free (lambda term_var t)) \$ depth
399             lambda free (lambda term_var t)) \$ depth
408     val none_t = Const (@{const_name None}, resultT)
400     val none_t = Const (@{const_name None}, resultT)
409     val mk_if = Quickcheck_Common.mk_safe_if genuine_only none_t
401     val mk_if = Quickcheck_Common.mk_safe_if genuine_only none_t
410     fun mk_let safe _ (SOME (v, term_var)) t e =
402     fun mk_let safe _ (SOME (v, term_var)) t e =
428     val frees = map Free (Term.add_frees t [])
420     val frees = map Free (Term.add_frees t [])
429     fun lookup v = the (AList.lookup (op =) (names ~~ frees) v)
421     fun lookup v = the (AList.lookup (op =) (names ~~ frees) v)
430     val ([depth_name], _) = Variable.variant_fixes ["depth"] ctxt'
422     val ([depth_name], _) = Variable.variant_fixes ["depth"] ctxt'
431     val depth = Free (depth_name, @{typ natural})
423     val depth = Free (depth_name, @{typ natural})
432     fun mk_bounded_forall (Free (s, T)) t =
424     fun mk_bounded_forall (Free (s, T)) t =
433       Const (@{const_name Quickcheck_Exhaustive.bounded_forall_class.bounded_forall},
425       Const (@{const_name bounded_forall}, bounded_forallT T) \$ lambda (Free (s, T)) t \$ depth
434         bounded_forallT T) \$ lambda (Free (s, T)) t \$ depth

435     fun mk_safe_if (cond, then_t, else_t) genuine = mk_if (cond, then_t, else_t genuine)
426     fun mk_safe_if (cond, then_t, else_t) genuine = mk_if (cond, then_t, else_t genuine)
436     fun mk_let _ def v_opt t e = mk_let_expr (the_default def v_opt, t, e)
427     fun mk_let _ def v_opt t e = mk_let_expr (the_default def v_opt, t, e)
437     val mk_test_term =
428     val mk_test_term =
438       mk_test_term lookup mk_bounded_forall mk_safe_if mk_let @{term True} (K @{term False}) ctxt
429       mk_test_term lookup mk_bounded_forall mk_safe_if mk_let @{term True} (K @{term False}) ctxt
439   in lambda depth (mk_test_term t) end
430   in lambda depth (mk_test_term t) end