--- a/src/HOL/Quickcheck_Exhaustive.thy Fri Apr 08 16:38:46 2011 +0200
+++ b/src/HOL/Quickcheck_Exhaustive.thy Fri Apr 08 17:13:49 2011 +0200
@@ -16,18 +16,39 @@
subsection {* exhaustive generator type classes *}
class exhaustive = term_of +
-fixes exhaustive :: "('a * (unit => term) \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
+ fixes exhaustive :: "('a \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
+
+class full_exhaustive = term_of +
+ fixes full_exhaustive :: "('a * (unit => term) \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
+
+instantiation code_numeral :: full_exhaustive
+begin
+
+function full_exhaustive_code_numeral' :: "(code_numeral * (unit => term) => term list option) => code_numeral => code_numeral => term list option"
+ where "full_exhaustive_code_numeral' f d i =
+ (if d < i then None
+ else (f (i, %_. Code_Evaluation.term_of i)) orelse (full_exhaustive_code_numeral' f d (i + 1)))"
+by pat_completeness auto
+
+termination
+ by (relation "measure (%(_, d, i). Code_Numeral.nat_of (d + 1 - i))") auto
+
+definition "full_exhaustive f d = full_exhaustive_code_numeral' f d 0"
+
+instance ..
+
+end
instantiation code_numeral :: exhaustive
begin
-function exhaustive_code_numeral' :: "(code_numeral * (unit => term) => term list option) => code_numeral => code_numeral => term list option"
+function exhaustive_code_numeral' :: "(code_numeral => term list option) => code_numeral => code_numeral => term list option"
where "exhaustive_code_numeral' f d i =
(if d < i then None
- else (f (i, %_. Code_Evaluation.term_of i)) orelse (exhaustive_code_numeral' f d (i + 1)))"
+ else (f i orelse exhaustive_code_numeral' f d (i + 1)))"
by pat_completeness auto
-termination
+termination
by (relation "measure (%(_, d, i). Code_Numeral.nat_of (d + 1 - i))") auto
definition "exhaustive f d = exhaustive_code_numeral' f d 0"
@@ -39,7 +60,16 @@
instantiation nat :: exhaustive
begin
-definition "exhaustive f d = exhaustive (%(x, xt). f (Code_Numeral.nat_of x, %_. Code_Evaluation.term_of (Code_Numeral.nat_of x))) d"
+definition "exhaustive f d = exhaustive (%x. f (Code_Numeral.nat_of x)) d"
+
+instance ..
+
+end
+
+instantiation nat :: full_exhaustive
+begin
+
+definition "full_exhaustive f d = full_exhaustive (%(x, xt). f (Code_Numeral.nat_of x, %_. Code_Evaluation.term_of (Code_Numeral.nat_of x))) d"
instance ..
@@ -48,8 +78,8 @@
instantiation int :: exhaustive
begin
-function exhaustive' :: "(int * (unit => term) => term list option) => int => int => term list option"
- where "exhaustive' f d i = (if d < i then None else (case f (i, %_. Code_Evaluation.term_of i) of Some t => Some t | None => exhaustive' f d (i + 1)))"
+function exhaustive' :: "(int => term list option) => int => int => term list option"
+ where "exhaustive' f d i = (if d < i then None else (f i orelse exhaustive' f d (i + 1)))"
by pat_completeness auto
termination
@@ -61,11 +91,37 @@
end
+instantiation int :: full_exhaustive
+begin
+
+function full_exhaustive' :: "(int * (unit => term) => term list option) => int => int => term list option"
+ where "full_exhaustive' f d i = (if d < i then None else (case f (i, %_. Code_Evaluation.term_of i) of Some t => Some t | None => full_exhaustive' f d (i + 1)))"
+by pat_completeness auto
+
+termination
+ by (relation "measure (%(_, d, i). nat (d + 1 - i))") auto
+
+definition "full_exhaustive f d = full_exhaustive' f (Code_Numeral.int_of d) (- (Code_Numeral.int_of d))"
+
+instance ..
+
+end
+
instantiation prod :: (exhaustive, exhaustive) exhaustive
begin
definition
- "exhaustive f d = exhaustive (%(x, t1). exhaustive (%(y, t2). f ((x, y),
+ "exhaustive f d = exhaustive (%x. exhaustive (%y. f ((x, y))) d) d"
+
+instance ..
+
+end
+
+instantiation prod :: (full_exhaustive, full_exhaustive) full_exhaustive
+begin
+
+definition
+ "full_exhaustive f d = full_exhaustive (%(x, t1). full_exhaustive (%(y, t2). f ((x, y),
%u. let T1 = (Typerep.typerep (TYPE('a)));
T2 = (Typerep.typerep (TYPE('b)))
in Code_Evaluation.App (Code_Evaluation.App (
@@ -80,11 +136,29 @@
instantiation "fun" :: ("{equal, exhaustive}", exhaustive) exhaustive
begin
-fun exhaustive_fun' :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => code_numeral => term list option"
+fun exhaustive_fun' :: "(('a => 'b) => term list option) => code_numeral => code_numeral => term list option"
+where
+ "exhaustive_fun' f i d = (exhaustive (%b. f (%_. b)) d)
+ orelse (if i > 1 then
+ exhaustive_fun' (%g. exhaustive (%a. exhaustive (%b.
+ f (g(a := b))) d) d) (i - 1) d else None)"
+
+definition exhaustive_fun :: "(('a => 'b) => term list option) => code_numeral => term list option"
where
- "exhaustive_fun' f i d = (exhaustive (%(b, t). f (%_. b, %_. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a)) (t ()))) d)
+ "exhaustive_fun f d = exhaustive_fun' f d d"
+
+instance ..
+
+end
+
+instantiation "fun" :: ("{equal, full_exhaustive}", full_exhaustive) full_exhaustive
+begin
+
+fun full_exhaustive_fun' :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => code_numeral => term list option"
+where
+ "full_exhaustive_fun' f i d = (full_exhaustive (%(b, t). f (%_. b, %_. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a)) (t ()))) d)
orelse (if i > 1 then
- exhaustive_fun' (%(g, gt). exhaustive (%(a, at). exhaustive (%(b, bt).
+ full_exhaustive_fun' (%(g, gt). full_exhaustive (%(a, at). full_exhaustive (%(b, bt).
f (g(a := b),
(%_. let A = (Typerep.typerep (TYPE('a)));
B = (Typerep.typerep (TYPE('b)));
@@ -94,9 +168,9 @@
(Code_Evaluation.Const (STR ''Fun.fun_upd'') (fun (fun A B) (fun A (fun B (fun A B)))))
(gt ())) (at ())) (bt ())))) d) d) (i - 1) d else None)"
-definition exhaustive_fun :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => term list option"
+definition full_exhaustive_fun :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => term list option"
where
- "exhaustive_fun f d = exhaustive_fun' f d d"
+ "full_exhaustive_fun f d = full_exhaustive_fun' f d d"
instance ..
@@ -351,6 +425,20 @@
class bounded_forall =
fixes bounded_forall :: "('a \<Rightarrow> bool) \<Rightarrow> code_numeral \<Rightarrow> bool"
+subsection {* Fast exhaustive combinators *}
+
+
+class fast_exhaustive = term_of +
+ fixes fast_exhaustive :: "('a \<Rightarrow> unit) \<Rightarrow> code_numeral \<Rightarrow> unit"
+
+consts throw_Counterexample :: "term list => unit"
+consts catch_Counterexample :: "unit => term list option"
+
+code_const throw_Counterexample
+ (Quickcheck "raise (Exhaustive'_Generators.Counterexample _)")
+code_const catch_Counterexample
+ (Quickcheck "(((_); NONE) handle Exhaustive'_Generators.Counterexample ts => SOME ts)")
+
subsection {* Defining combinators for any first-order data type *}
definition catch_match :: "term list option => term list option => term list option"
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Fri Apr 08 16:38:46 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Fri Apr 08 17:13:49 2011 +0200
@@ -15,6 +15,7 @@
val put_counterexample_batch: (unit -> (int -> term list option) list)
-> Proof.context -> Proof.context
val put_validator_batch: (unit -> (int -> bool) list) -> Proof.context -> Proof.context
+ exception Counterexample of term list
val smart_quantifier : bool Config.T
val quickcheck_pretty : bool Config.T
val setup: theory -> theory
@@ -23,11 +24,19 @@
structure Exhaustive_Generators : EXHAUSTIVE_GENERATORS =
struct
-(* dynamic options *)
+(* basics *)
+
+(** dynamic options **)
val (smart_quantifier, setup_smart_quantifier) =
Attrib.config_bool "quickcheck_smart_quantifier" (K true)
+val (fast, setup_fast) =
+ Attrib.config_bool "quickcheck_fast" (K false)
+
+val (full_support, setup_full_support) =
+ Attrib.config_bool "quickcheck_full_support" (K true)
+
val (quickcheck_pretty, setup_quickcheck_pretty) =
Attrib.config_bool "quickcheck_pretty" (K true)
@@ -51,9 +60,6 @@
end
| mk_sumcases _ f T = f T
-fun mk_undefined T = Const(@{const_name undefined}, T)
-
-
(** abstract syntax **)
fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => Code_Evaluation.term"});
@@ -61,7 +67,6 @@
val size = @{term "i :: code_numeral"}
val size_pred = @{term "(i :: code_numeral) - 1"}
val size_ge_zero = @{term "(i :: code_numeral) > 0"}
-fun test_function T = Free ("f", termifyT T --> @{typ "term list option"})
fun mk_none_continuation (x, y) =
let
@@ -70,26 +75,122 @@
Const (@{const_name "Quickcheck_Exhaustive.orelse"}, T --> T --> T) $ x $ y
end
-(** datatypes **)
+fun mk_unit_let (x, y) =
+ Const (@{const_name "Let"}, @{typ "unit => (unit => unit) => unit"}) $ x $ (absdummy (@{typ unit}, y))
+
+(* handling inductive datatypes *)
-(* constructing exhaustive generator instances on datatypes *)
+(** constructing generator instances **)
exception FUNCTION_TYPE;
+
+exception Counterexample of term list
+
val exhaustiveN = "exhaustive";
+val full_exhaustiveN = "full_exhaustive";
+val fast_exhaustiveN = "fast_exhaustive";
+val bounded_forallN = "bounded_forall";
-fun exhaustiveT T = (termifyT T --> @{typ "Code_Evaluation.term list option"})
+fun fast_exhaustiveT T = (T --> @{typ unit})
+ --> @{typ code_numeral} --> @{typ unit}
+
+fun exhaustiveT T = (T --> @{typ "Code_Evaluation.term list option"})
+ --> @{typ code_numeral} --> @{typ "Code_Evaluation.term list option"}
+
+fun bounded_forallT T = (T --> @{typ bool}) --> @{typ code_numeral} --> @{typ bool}
+
+fun full_exhaustiveT T = (termifyT T --> @{typ "Code_Evaluation.term list option"})
--> @{typ code_numeral} --> @{typ "Code_Evaluation.term list option"}
fun check_allT T = (termifyT T --> @{typ "Code_Evaluation.term list option"})
--> @{typ "Code_Evaluation.term list option"}
-fun mk_equations descr vs tycos exhaustives (Ts, Us) =
+fun mk_equation_terms generics (descr, vs, Ts) =
+ let
+ val (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, exhaustives) = generics
+ val rhss =
+ Datatype_Aux.interpret_construction descr vs
+ { atyp = mk_call, dtyp = mk_aux_call }
+ |> (map o apfst) Type
+ |> map (fn (T, cs) => map (mk_consexpr T) cs)
+ |> map mk_rhs
+ val lhss = map2 (fn t => fn T => t $ test_function T $ size) exhaustives Ts
+ in
+ map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhss ~~ rhss)
+ end
+
+fun gen_mk_call c T = (T, fn t => c T $ absdummy (T, t) $ size_pred)
+
+fun gen_mk_aux_call functerms fTs (k, _) (tyco, Ts) =
+ let
+ val T = Type (tyco, Ts)
+ val _ = if not (null fTs) then raise FUNCTION_TYPE else ()
+ in
+ (T, fn t => nth functerms k $ absdummy (T, t) $ size_pred)
+ end
+
+fun gen_mk_consexpr test_function functerms simpleT (c, xs) =
+ let
+ val (Ts, fns) = split_list xs
+ val constr = Const (c, Ts ---> simpleT)
+ val bounds = map Bound (((length xs) - 1) downto 0)
+ val term_bounds = map (fn x => Bound (2 * x)) (((length xs) - 1) downto 0)
+ val start_term = test_function simpleT $ list_comb (constr, bounds)
+ in fold_rev (fn f => fn t => f t) fns start_term end
+
+fun mk_fast_equations functerms =
let
+ fun test_function T = Free ("f", T --> @{typ "unit"})
+ val mk_call = gen_mk_call (fn T =>
+ Const (@{const_name "Quickcheck_Exhaustive.fast_exhaustive_class.fast_exhaustive"},
+ fast_exhaustiveT T))
+ val mk_aux_call = gen_mk_aux_call functerms
+ val mk_consexpr = gen_mk_consexpr test_function functerms
+ fun mk_rhs exprs = @{term "If :: bool => unit => unit => unit"}
+ $ size_ge_zero $ (foldr1 mk_unit_let exprs) $ @{term "()"}
+ in
+ mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms)
+ end
+
+fun mk_equations functerms =
+ let
+ fun test_function T = Free ("f", T --> @{typ "term list option"})
+ val mk_call = gen_mk_call (fn T =>
+ Const (@{const_name "Quickcheck_Exhaustive.exhaustive_class.exhaustive"}, exhaustiveT T))
+ val mk_aux_call = gen_mk_aux_call functerms
+ val mk_consexpr = gen_mk_consexpr test_function functerms
+ fun mk_rhs exprs =
+ @{term "If :: bool => term list option => term list option => term list option"}
+ $ size_ge_zero $ (foldr1 mk_none_continuation exprs) $ @{term "None :: term list option"}
+ in
+ mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms)
+ end
+
+fun mk_bounded_forall_equations functerms =
+ let
+ fun test_function T = Free ("P", T --> @{typ bool})
+ val mk_call = gen_mk_call (fn T =>
+ Const (@{const_name "Quickcheck_Exhaustive.bounded_forall_class.bounded_forall"},
+ bounded_forallT T))
+ val mk_aux_call = gen_mk_aux_call functerms
+ val mk_consexpr = gen_mk_consexpr test_function functerms
+ fun mk_rhs exprs =
+ @{term "If :: bool => bool => bool => bool"} $ size_ge_zero $
+ (foldr1 HOLogic.mk_conj exprs) $ @{term "True"}
+ in
+ mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms)
+ end
+
+fun mk_full_equations functerms =
+ let
+ fun test_function T = Free ("f", termifyT T --> @{typ "term list option"})
fun mk_call T =
let
- val exhaustive = Const (@{const_name "Quickcheck_Exhaustive.exhaustive_class.exhaustive"}, exhaustiveT T)
+ val full_exhaustive =
+ Const (@{const_name "Quickcheck_Exhaustive.full_exhaustive_class.full_exhaustive"},
+ full_exhaustiveT T)
in
- (T, (fn t => exhaustive $
+ (T, (fn t => full_exhaustive $
(HOLogic.split_const (T, @{typ "unit => Code_Evaluation.term"}, @{typ "Code_Evaluation.term list option"})
$ absdummy (T, absdummy (@{typ "unit => Code_Evaluation.term"}, t))) $ size_pred))
end
@@ -98,7 +199,7 @@
val T = Type (tyco, Ts)
val _ = if not (null fTs) then raise FUNCTION_TYPE else ()
in
- (T, (fn t => nth exhaustives k $
+ (T, (fn t => nth functerms k $
(HOLogic.split_const (T, @{typ "unit => Code_Evaluation.term"}, @{typ "Code_Evaluation.term list option"})
$ absdummy (T, absdummy (@{typ "unit => Code_Evaluation.term"}, t))) $ size_pred))
end
@@ -119,19 +220,11 @@
fun mk_rhs exprs =
@{term "If :: bool => term list option => term list option => term list option"}
$ size_ge_zero $ (foldr1 mk_none_continuation exprs) $ @{term "None :: term list option"}
- val rhss =
- Datatype_Aux.interpret_construction descr vs
- { atyp = mk_call, dtyp = mk_aux_call }
- |> (map o apfst) Type
- |> map (fn (T, cs) => map (mk_consexpr T) cs)
- |> map mk_rhs
- val lhss = map2 (fn t => fn T => t $ test_function T $ size) exhaustives (Ts @ Us);
- val eqs = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhss ~~ rhss)
in
- eqs
+ mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms)
end
-
-(* foundational definition with the function package *)
+
+(** foundational definition with the function package **)
val less_int_pred = @{lemma "i > 0 ==> Code_Numeral.nat_of ((i :: code_numeral) - 1) < Code_Numeral.nat_of i" by auto}
@@ -152,90 +245,87 @@
(HOL_basic_ss addsimps [@{thm in_measure}, @{thm o_def}, @{thm snd_conv},
@{thm nat_mono_iff}, less_int_pred] @ @{thms sum.cases}) 1))
-(* creating the instances *)
-
-fun instantiate_exhaustive_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
- let
- val _ = Datatype_Aux.message config "Creating exhaustive generators...";
- val exhaustivesN = map (prefix (exhaustiveN ^ "_")) (names @ auxnames);
- in
- thy
- |> Class.instantiation (tycos, vs, @{sort exhaustive})
- |> Quickcheck_Common.define_functions
- (fn exhaustives => mk_equations descr vs tycos exhaustives (Ts, Us), SOME termination_tac)
- prfx ["f", "i"] exhaustivesN (map exhaustiveT (Ts @ Us))
- |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
- end handle FUNCTION_TYPE =>
+(** instantiating generator classes **)
+
+val contains_recursive_type_under_function_types =
+ exists (fn (_, (_, _, cs)) => cs |> exists (snd #> exists (fn dT =>
+ (case Datatype_Aux.strip_dtyp dT of (_ :: _, Datatype.DtRec _) => true | _ => false))))
+
+fun instantiate_datatype (name, constprfx, sort, mk_equations, mk_T, argnames)
+ config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
+ if not (contains_recursive_type_under_function_types descr) then
+ let
+ val _ = Datatype_Aux.message config ("Creating " ^ name ^ "...")
+ val fullnames = map (prefix (constprfx ^ "_")) (names @ auxnames)
+ in
+ thy
+ |> Class.instantiation (tycos, vs, sort)
+ |> Quickcheck_Common.define_functions
+ (fn functerms => mk_equations functerms (descr, vs, Ts @ Us), NONE)
+ prfx argnames fullnames (map mk_T (Ts @ Us))
+ |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
+ end
+ else
(Datatype_Aux.message config
- "Creation of exhaustive generators failed because the datatype contains a function type";
+ ("Creation of " ^ name ^ " failed because the datatype is recursive under a function type");
thy)
-(* constructing bounded_forall instances on datatypes *)
+val instantiate_bounded_forall_datatype = instantiate_datatype
+ ("bounded universal quantifiers", bounded_forallN, @{sort bounded_forall},
+ mk_bounded_forall_equations, bounded_forallT, ["P", "i"]);
-val bounded_forallN = "bounded_forall";
+val instantiate_fast_exhaustive_datatype = instantiate_datatype
+ ("fast exhaustive generators", fast_exhaustiveN, @{sort fast_exhaustive},
+ mk_fast_equations, fast_exhaustiveT, ["f", "i"])
-fun bounded_forallT T = (T --> @{typ bool}) --> @{typ code_numeral} --> @{typ bool}
+val instantiate_exhaustive_datatype = instantiate_datatype
+ ("exhaustive generators", exhaustiveN, @{sort full_exhaustive}, mk_equations, exhaustiveT, ["f", "i"])
-fun mk_bounded_forall_equations descr vs tycos bounded_foralls (Ts, Us) =
+val instantiate_full_exhaustive_datatype = instantiate_datatype
+ ("full exhaustive generators", full_exhaustiveN, @{sort full_exhaustive},
+ mk_full_equations, full_exhaustiveT, ["f", "i"])
+
+(* building and compiling generator expressions *)
+
+fun mk_fast_generator_expr ctxt (t, eval_terms) =
let
- fun mk_call T =
- let
- val bounded_forall =
- Const (@{const_name "Quickcheck_Exhaustive.bounded_forall_class.bounded_forall"},
- bounded_forallT T)
- in
- (T, (fn t => bounded_forall $ absdummy (T, t) $ size_pred))
- end
- fun mk_aux_call fTs (k, _) (tyco, Ts) =
- let
- val T = Type (tyco, Ts)
- val _ = if not (null fTs) then raise FUNCTION_TYPE else ()
- in
- (T, (fn t => nth bounded_foralls k $ absdummy (T, t) $ size_pred))
- end
- fun mk_consexpr simpleT (c, xs) =
+ val thy = ProofContext.theory_of ctxt
+ val ctxt' = Variable.auto_fixes t ctxt
+ val names = Term.add_free_names t []
+ val frees = map Free (Term.add_frees t [])
+ val ([depth_name], ctxt'') = Variable.variant_fixes ["depth"] ctxt'
+ val depth = Free (depth_name, @{typ code_numeral})
+ val return = @{term "throw_Counterexample :: term list => unit"} $
+ (HOLogic.mk_list @{typ "term"}
+ (map (fn t => HOLogic.mk_term_of (fastype_of t) t) (frees @ eval_terms)))
+ fun mk_exhaustive_closure (free as Free (_, T)) t =
+ Const (@{const_name "Quickcheck_Exhaustive.fast_exhaustive_class.fast_exhaustive"}, fast_exhaustiveT T)
+ $ lambda free t $ depth
+ val none_t = @{term "()"}
+ fun mk_safe_if (cond, then_t, else_t) =
+ @{term "If :: bool => unit => unit => unit"} $ cond $ then_t $ else_t
+ fun lookup v = the (AList.lookup (op =) (names ~~ frees) v)
+ fun mk_naive_test_term t =
+ fold_rev mk_exhaustive_closure frees (mk_safe_if (t, none_t, return))
+ fun mk_smart_test_term' concl bound_vars assms =
let
- val (Ts, fns) = split_list xs
- val constr = Const (c, Ts ---> simpleT)
- val bounds = map Bound (((length xs) - 1) downto 0)
- val start_term = Free ("P", simpleT --> @{typ bool}) $ list_comb (constr, bounds)
- in fold_rev (fn f => fn t => f t) fns start_term end
- fun mk_rhs exprs =
- @{term "If :: bool => bool => bool => bool"} $ size_ge_zero $
- (foldr1 HOLogic.mk_conj exprs) $ @{term "True"}
- val rhss =
- Datatype_Aux.interpret_construction descr vs
- { atyp = mk_call, dtyp = mk_aux_call }
- |> (map o apfst) Type
- |> map (fn (T, cs) => map (mk_consexpr T) cs)
- |> map mk_rhs
- val lhss =
- map2 (fn t => fn T => t $ Free ("P", T --> @{typ bool}) $ size) bounded_foralls (Ts @ Us)
- val eqs = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhss ~~ rhss)
- in
- eqs
- end
-
-(* creating the bounded_forall instances *)
-
-fun instantiate_bounded_forall_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
- let
- val _ = Datatype_Aux.message config "Creating bounded universal quantifiers...";
- val bounded_forallsN = map (prefix (bounded_forallN ^ "_")) (names @ auxnames);
- in
- thy
- |> Class.instantiation (tycos, vs, @{sort bounded_forall})
- |> Quickcheck_Common.define_functions
- (fn bounded_foralls =>
- mk_bounded_forall_equations descr vs tycos bounded_foralls (Ts, Us), NONE)
- prfx ["P", "i"] bounded_forallsN (map bounded_forallT (Ts @ Us))
- |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
- end handle FUNCTION_TYPE =>
- (Datatype_Aux.message config
- "Creation of bounded universal quantifiers failed because the datatype contains a function type";
- thy)
-
-(** building and compiling generator expressions **)
+ fun vars_of t = subtract (op =) bound_vars (Term.add_free_names t [])
+ val (vars, check) =
+ case assms of [] => (vars_of concl, (concl, none_t, return))
+ | assm :: assms => (vars_of assm, (assm,
+ mk_smart_test_term' concl (union (op =) (vars_of assm) bound_vars) assms, none_t))
+ in
+ fold_rev mk_exhaustive_closure (map lookup vars) (mk_safe_if check)
+ end
+ fun mk_smart_test_term t =
+ let
+ val (assms, concl) = Quickcheck_Common.strip_imp t
+ in
+ mk_smart_test_term' concl [] assms
+ end
+ val mk_test_term =
+ if Config.get ctxt smart_quantifier then mk_smart_test_term else mk_naive_test_term
+ in lambda depth (@{term "catch_Counterexample :: unit => term list option"} $ mk_test_term t) end
fun mk_generator_expr ctxt (t, eval_terms) =
let
@@ -244,6 +334,48 @@
val names = Term.add_free_names t []
val frees = map Free (Term.add_frees t [])
val ([depth_name], ctxt'') = Variable.variant_fixes ["depth"] ctxt'
+ val depth = Free (depth_name, @{typ code_numeral})
+ val return = @{term "Some :: term list => term list option"} $
+ (HOLogic.mk_list @{typ "term"}
+ (map (fn t => HOLogic.mk_term_of (fastype_of t) t) (frees @ eval_terms)))
+ fun mk_exhaustive_closure (free as Free (_, T)) t =
+ Const (@{const_name "Quickcheck_Exhaustive.exhaustive_class.exhaustive"}, exhaustiveT T)
+ $ lambda free t $ depth
+ val none_t = @{term "None :: term list option"}
+ fun mk_safe_if (cond, then_t, else_t) =
+ @{term "Quickcheck_Exhaustive.catch_match :: term list option => term list option => term list option"} $
+ (@{term "If :: bool => term list option => term list option => term list option"}
+ $ cond $ then_t $ else_t) $ none_t;
+ fun lookup v = the (AList.lookup (op =) (names ~~ frees) v)
+ fun mk_naive_test_term t =
+ fold_rev mk_exhaustive_closure frees (mk_safe_if (t, none_t, return))
+ fun mk_smart_test_term' concl bound_vars assms =
+ let
+ fun vars_of t = subtract (op =) bound_vars (Term.add_free_names t [])
+ val (vars, check) =
+ case assms of [] => (vars_of concl, (concl, none_t, return))
+ | assm :: assms => (vars_of assm, (assm,
+ mk_smart_test_term' concl (union (op =) (vars_of assm) bound_vars) assms, none_t))
+ in
+ fold_rev mk_exhaustive_closure (map lookup vars) (mk_safe_if check)
+ end
+ fun mk_smart_test_term t =
+ let
+ val (assms, concl) = Quickcheck_Common.strip_imp t
+ in
+ mk_smart_test_term' concl [] assms
+ end
+ val mk_test_term =
+ if Config.get ctxt smart_quantifier then mk_smart_test_term else mk_naive_test_term
+ in lambda depth (mk_test_term t) end
+
+fun mk_full_generator_expr ctxt (t, eval_terms) =
+ let
+ val thy = ProofContext.theory_of ctxt
+ val ctxt' = Variable.auto_fixes t ctxt
+ val names = Term.add_free_names t []
+ val frees = map Free (Term.add_frees t [])
+ val ([depth_name], ctxt'') = Variable.variant_fixes ["depth"] ctxt'
val (term_names, ctxt''') = Variable.variant_fixes (map (prefix "t_") names) ctxt''
val depth = Free (depth_name, @{typ code_numeral})
val term_vars = map (fn n => Free (n, @{typ "unit => term"})) term_names
@@ -257,7 +389,7 @@
$ (HOLogic.split_const (T, @{typ "unit => term"}, @{typ "term list option"})
$ lambda free (lambda term_var t))
else
- Const (@{const_name "Quickcheck_Exhaustive.exhaustive_class.exhaustive"}, exhaustiveT T)
+ Const (@{const_name "Quickcheck_Exhaustive.full_exhaustive_class.full_exhaustive"}, full_exhaustiveT T)
$ (HOLogic.split_const (T, @{typ "unit => term"}, @{typ "term list option"})
$ lambda free (lambda term_var t)) $ depth
val none_t = @{term "None :: term list option"}
@@ -288,7 +420,7 @@
if Config.get ctxt smart_quantifier then mk_smart_test_term else mk_naive_test_term
in lambda depth (mk_test_term t) end
-val mk_parametric_generator_expr =
+fun mk_parametric_generator_expr mk_generator_expr =
Quickcheck_Common.gen_mk_parametric_generator_expr
((mk_generator_expr, absdummy (@{typ "code_numeral"}, @{term "None :: term list option"})),
@{typ "code_numeral => term list option"})
@@ -359,7 +491,10 @@
fun compile_generator_expr ctxt ts =
let
val thy = ProofContext.theory_of ctxt
- val t' = mk_parametric_generator_expr ctxt ts;
+ val mk_generator_expr =
+ if Config.get ctxt fast then mk_fast_generator_expr
+ else if Config.get ctxt full_support then mk_full_generator_expr else mk_generator_expr
+ val t' = mk_parametric_generator_expr mk_generator_expr ctxt ts;
val compile = Code_Runtime.dynamic_value_strict
(Counterexample.get, put_counterexample, "Exhaustive_Generators.put_counterexample")
thy (SOME target) (fn proc => fn g =>
@@ -394,14 +529,20 @@
thy (SOME target) (K I) (HOLogic.mk_list @{typ "code_numeral => bool"} ts') []
end;
-(** setup **)
+(* setup *)
val setup =
Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
+ (((@{sort typerep}, @{sort term_of}), @{sort full_exhaustive}), instantiate_full_exhaustive_datatype))
+(* #> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
(((@{sort typerep}, @{sort term_of}), @{sort exhaustive}), instantiate_exhaustive_datatype))
#> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
- (((@{sort type}, @{sort type}), @{sort bounded_forall}), instantiate_bounded_forall_datatype))
+ (((@{sort typerep}, @{sort term_of}), @{sort fast_exhaustive}), instantiate_fast_exhaustive_datatype))
+ #> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
+ (((@{sort type}, @{sort type}), @{sort bounded_forall}), instantiate_bounded_forall_datatype))*)
#> setup_smart_quantifier
+ #> setup_full_support
+ #> setup_fast
#> setup_quickcheck_pretty
#> Context.theory_map (Quickcheck.add_generator ("exhaustive", compile_generator_expr))
#> Context.theory_map (Quickcheck.add_batch_generator ("exhaustive", compile_generator_exprs))