1.1 --- a/src/HOL/Quickcheck_Exhaustive.thy Thu Apr 07 21:49:24 2011 +0200
1.2 +++ b/src/HOL/Quickcheck_Exhaustive.thy Fri Apr 08 16:31:14 2011 +0200
1.3 @@ -16,22 +16,35 @@
1.4 subsection {* exhaustive generator type classes *}
1.5
1.6 class exhaustive = term_of +
1.7 -fixes exhaustive :: "('a * (unit => term) \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
1.8 + fixes exhaustive :: "('a \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
1.9 + fixes full_exhaustive :: "('a * (unit => term) \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
1.10
1.11 instantiation code_numeral :: exhaustive
1.12 begin
1.13
1.14 -function exhaustive_code_numeral' :: "(code_numeral * (unit => term) => term list option) => code_numeral => code_numeral => term list option"
1.15 +function full_exhaustive_code_numeral' :: "(code_numeral * (unit => term) => term list option) => code_numeral => code_numeral => term list option"
1.16 + where "full_exhaustive_code_numeral' f d i =
1.17 + (if d < i then None
1.18 + else (f (i, %_. Code_Evaluation.term_of i)) orelse (full_exhaustive_code_numeral' f d (i + 1)))"
1.19 +by pat_completeness auto
1.20 +
1.21 +termination
1.22 + by (relation "measure (%(_, d, i). Code_Numeral.nat_of (d + 1 - i))") auto
1.23 +
1.24 +definition "full_exhaustive f d = full_exhaustive_code_numeral' f d 0"
1.25 +
1.26 +function exhaustive_code_numeral' :: "(code_numeral => term list option) => code_numeral => code_numeral => term list option"
1.27 where "exhaustive_code_numeral' f d i =
1.28 (if d < i then None
1.29 - else (f (i, %_. Code_Evaluation.term_of i)) orelse (exhaustive_code_numeral' f d (i + 1)))"
1.30 + else (f i orelse exhaustive_code_numeral' f d (i + 1)))"
1.31 by pat_completeness auto
1.32
1.33 -termination
1.34 +termination
1.35 by (relation "measure (%(_, d, i). Code_Numeral.nat_of (d + 1 - i))") auto
1.36
1.37 definition "exhaustive f d = exhaustive_code_numeral' f d 0"
1.38
1.39 +
1.40 instance ..
1.41
1.42 end
1.43 @@ -39,7 +52,9 @@
1.44 instantiation nat :: exhaustive
1.45 begin
1.46
1.47 -definition "exhaustive f d = exhaustive (%(x, xt). f (Code_Numeral.nat_of x, %_. Code_Evaluation.term_of (Code_Numeral.nat_of x))) d"
1.48 +definition "exhaustive f d = exhaustive (%x. f (Code_Numeral.nat_of x)) d"
1.49 +
1.50 +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"
1.51
1.52 instance ..
1.53
1.54 @@ -48,8 +63,8 @@
1.55 instantiation int :: exhaustive
1.56 begin
1.57
1.58 -function exhaustive' :: "(int * (unit => term) => term list option) => int => int => term list option"
1.59 - 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)))"
1.60 +function exhaustive' :: "(int => term list option) => int => int => term list option"
1.61 + where "exhaustive' f d i = (if d < i then None else (f i orelse exhaustive' f d (i + 1)))"
1.62 by pat_completeness auto
1.63
1.64 termination
1.65 @@ -57,6 +72,15 @@
1.66
1.67 definition "exhaustive f d = exhaustive' f (Code_Numeral.int_of d) (- (Code_Numeral.int_of d))"
1.68
1.69 +function full_exhaustive' :: "(int * (unit => term) => term list option) => int => int => term list option"
1.70 + 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)))"
1.71 +by pat_completeness auto
1.72 +
1.73 +termination
1.74 + by (relation "measure (%(_, d, i). nat (d + 1 - i))") auto
1.75 +
1.76 +definition "full_exhaustive f d = full_exhaustive' f (Code_Numeral.int_of d) (- (Code_Numeral.int_of d))"
1.77 +
1.78 instance ..
1.79
1.80 end
1.81 @@ -65,7 +89,10 @@
1.82 begin
1.83
1.84 definition
1.85 - "exhaustive f d = exhaustive (%(x, t1). exhaustive (%(y, t2). f ((x, y),
1.86 + "exhaustive f d = exhaustive (%x. exhaustive (%y. f ((x, y))) d) d"
1.87 +
1.88 +definition
1.89 + "full_exhaustive f d = full_exhaustive (%(x, t1). full_exhaustive (%(y, t2). f ((x, y),
1.90 %u. let T1 = (Typerep.typerep (TYPE('a)));
1.91 T2 = (Typerep.typerep (TYPE('b)))
1.92 in Code_Evaluation.App (Code_Evaluation.App (
1.93 @@ -80,11 +107,23 @@
1.94 instantiation "fun" :: ("{equal, exhaustive}", exhaustive) exhaustive
1.95 begin
1.96
1.97 -fun exhaustive_fun' :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => code_numeral => term list option"
1.98 +fun exhaustive_fun' :: "(('a => 'b) => term list option) => code_numeral => code_numeral => term list option"
1.99 where
1.100 - "exhaustive_fun' f i d = (exhaustive (%(b, t). f (%_. b, %_. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a)) (t ()))) d)
1.101 + "exhaustive_fun' f i d = (exhaustive (%b. f (%_. b)) d)
1.102 orelse (if i > 1 then
1.103 - exhaustive_fun' (%(g, gt). exhaustive (%(a, at). exhaustive (%(b, bt).
1.104 + exhaustive_fun' (%g. exhaustive (%a. exhaustive (%b.
1.105 + f (g(a := b))) d) d) (i - 1) d else None)"
1.106 +
1.107 +definition exhaustive_fun :: "(('a => 'b) => term list option) => code_numeral => term list option"
1.108 +where
1.109 + "exhaustive_fun f d = exhaustive_fun' f d d"
1.110 +
1.111 +
1.112 +fun full_exhaustive_fun' :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => code_numeral => term list option"
1.113 +where
1.114 + "full_exhaustive_fun' f i d = (full_exhaustive (%(b, t). f (%_. b, %_. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a)) (t ()))) d)
1.115 + orelse (if i > 1 then
1.116 + full_exhaustive_fun' (%(g, gt). full_exhaustive (%(a, at). full_exhaustive (%(b, bt).
1.117 f (g(a := b),
1.118 (%_. let A = (Typerep.typerep (TYPE('a)));
1.119 B = (Typerep.typerep (TYPE('b)));
1.120 @@ -94,9 +133,9 @@
1.121 (Code_Evaluation.Const (STR ''Fun.fun_upd'') (fun (fun A B) (fun A (fun B (fun A B)))))
1.122 (gt ())) (at ())) (bt ())))) d) d) (i - 1) d else None)"
1.123
1.124 -definition exhaustive_fun :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => term list option"
1.125 +definition full_exhaustive_fun :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => term list option"
1.126 where
1.127 - "exhaustive_fun f d = exhaustive_fun' f d d"
1.128 + "full_exhaustive_fun f d = full_exhaustive_fun' f d d"
1.129
1.130 instance ..
1.131
2.1 --- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Thu Apr 07 21:49:24 2011 +0200
2.2 +++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Fri Apr 08 16:31:14 2011 +0200
2.3 @@ -28,6 +28,9 @@
2.4 val (smart_quantifier, setup_smart_quantifier) =
2.5 Attrib.config_bool "quickcheck_smart_quantifier" (K true)
2.6
2.7 +val (full_support, setup_full_support) =
2.8 + Attrib.config_bool "quickcheck_full_support" (K true)
2.9 +
2.10 val (quickcheck_pretty, setup_quickcheck_pretty) =
2.11 Attrib.config_bool "quickcheck_pretty" (K true)
2.12
2.13 @@ -61,7 +64,9 @@
2.14 val size = @{term "i :: code_numeral"}
2.15 val size_pred = @{term "(i :: code_numeral) - 1"}
2.16 val size_ge_zero = @{term "(i :: code_numeral) > 0"}
2.17 -fun test_function T = Free ("f", termifyT T --> @{typ "term list option"})
2.18 +
2.19 +fun test_function T = Free ("f", T --> @{typ "term list option"})
2.20 +fun full_test_function T = Free ("f", termifyT T --> @{typ "term list option"})
2.21
2.22 fun mk_none_continuation (x, y) =
2.23 let
2.24 @@ -76,8 +81,12 @@
2.25
2.26 exception FUNCTION_TYPE;
2.27 val exhaustiveN = "exhaustive";
2.28 +val full_exhaustiveN = "full_exhaustive";
2.29
2.30 -fun exhaustiveT T = (termifyT T --> @{typ "Code_Evaluation.term list option"})
2.31 +fun exhaustiveT T = (T --> @{typ "Code_Evaluation.term list option"})
2.32 + --> @{typ code_numeral} --> @{typ "Code_Evaluation.term list option"}
2.33 +
2.34 +fun full_exhaustiveT T = (termifyT T --> @{typ "Code_Evaluation.term list option"})
2.35 --> @{typ code_numeral} --> @{typ "Code_Evaluation.term list option"}
2.36
2.37 fun check_allT T = (termifyT T --> @{typ "Code_Evaluation.term list option"})
2.38 @@ -89,7 +98,45 @@
2.39 let
2.40 val exhaustive = Const (@{const_name "Quickcheck_Exhaustive.exhaustive_class.exhaustive"}, exhaustiveT T)
2.41 in
2.42 - (T, (fn t => exhaustive $
2.43 + (T, fn t => exhaustive $ absdummy (T, t) $ size_pred)
2.44 + end
2.45 + fun mk_aux_call fTs (k, _) (tyco, Ts) =
2.46 + let
2.47 + val T = Type (tyco, Ts)
2.48 + val _ = if not (null fTs) then raise FUNCTION_TYPE else ()
2.49 + in
2.50 + (T, fn t => nth exhaustives k $ absdummy (T, t) $ size_pred)
2.51 + end
2.52 + fun mk_consexpr simpleT (c, xs) =
2.53 + let
2.54 + val (Ts, fns) = split_list xs
2.55 + val constr = Const (c, Ts ---> simpleT)
2.56 + val bounds = map Bound (((length xs) - 1) downto 0)
2.57 + val term_bounds = map (fn x => Bound (2 * x)) (((length xs) - 1) downto 0)
2.58 + val start_term = test_function simpleT $ list_comb (constr, bounds)
2.59 + in fold_rev (fn f => fn t => f t) fns start_term end
2.60 + fun mk_rhs exprs =
2.61 + @{term "If :: bool => term list option => term list option => term list option"}
2.62 + $ size_ge_zero $ (foldr1 mk_none_continuation exprs) $ @{term "None :: term list option"}
2.63 + val rhss =
2.64 + Datatype_Aux.interpret_construction descr vs
2.65 + { atyp = mk_call, dtyp = mk_aux_call }
2.66 + |> (map o apfst) Type
2.67 + |> map (fn (T, cs) => map (mk_consexpr T) cs)
2.68 + |> map mk_rhs
2.69 + val lhss = map2 (fn t => fn T => t $ test_function T $ size) exhaustives (Ts @ Us)
2.70 + val eqs = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhss ~~ rhss)
2.71 + in
2.72 + eqs
2.73 + end
2.74 +
2.75 +fun mk_full_equations descr vs tycos full_exhaustives (Ts, Us) =
2.76 + let
2.77 + fun mk_call T =
2.78 + let
2.79 + val full_exhaustive = Const (@{const_name "Quickcheck_Exhaustive.exhaustive_class.full_exhaustive"}, full_exhaustiveT T)
2.80 + in
2.81 + (T, (fn t => full_exhaustive $
2.82 (HOLogic.split_const (T, @{typ "unit => Code_Evaluation.term"}, @{typ "Code_Evaluation.term list option"})
2.83 $ absdummy (T, absdummy (@{typ "unit => Code_Evaluation.term"}, t))) $ size_pred))
2.84 end
2.85 @@ -98,7 +145,7 @@
2.86 val T = Type (tyco, Ts)
2.87 val _ = if not (null fTs) then raise FUNCTION_TYPE else ()
2.88 in
2.89 - (T, (fn t => nth exhaustives k $
2.90 + (T, (fn t => nth full_exhaustives k $
2.91 (HOLogic.split_const (T, @{typ "unit => Code_Evaluation.term"}, @{typ "Code_Evaluation.term list option"})
2.92 $ absdummy (T, absdummy (@{typ "unit => Code_Evaluation.term"}, t))) $ size_pred))
2.93 end
2.94 @@ -112,7 +159,7 @@
2.95 val Eval_Const = Const ("Code_Evaluation.Const", HOLogic.literalT --> @{typ typerep} --> HOLogic.termT)
2.96 val term = fold (fn u => fn t => Eval_App $ t $ (u $ @{term "()"}))
2.97 bounds (Eval_Const $ HOLogic.mk_literal c $ HOLogic.mk_typerep (Ts ---> simpleT))
2.98 - val start_term = test_function simpleT $
2.99 + val start_term = full_test_function simpleT $
2.100 (HOLogic.pair_const simpleT @{typ "unit => Code_Evaluation.term"}
2.101 $ (list_comb (constr, bounds)) $ absdummy (@{typ unit}, term))
2.102 in fold_rev (fn f => fn t => f t) fns start_term end
2.103 @@ -125,7 +172,7 @@
2.104 |> (map o apfst) Type
2.105 |> map (fn (T, cs) => map (mk_consexpr T) cs)
2.106 |> map mk_rhs
2.107 - val lhss = map2 (fn t => fn T => t $ test_function T $ size) exhaustives (Ts @ Us);
2.108 + val lhss = map2 (fn t => fn T => t $ full_test_function T $ size) full_exhaustives (Ts @ Us);
2.109 val eqs = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhss ~~ rhss)
2.110 in
2.111 eqs
2.112 @@ -157,13 +204,18 @@
2.113 fun instantiate_exhaustive_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
2.114 let
2.115 val _ = Datatype_Aux.message config "Creating exhaustive generators...";
2.116 - val exhaustivesN = map (prefix (exhaustiveN ^ "_")) (names @ auxnames);
2.117 + val exhaustivesN = map (prefix (exhaustiveN ^ "_")) (names @ auxnames)
2.118 + val full_exhaustivesN = map (prefix (full_exhaustiveN ^ "_")) (names @ auxnames)
2.119 in
2.120 thy
2.121 |> Class.instantiation (tycos, vs, @{sort exhaustive})
2.122 |> Quickcheck_Common.define_functions
2.123 (fn exhaustives => mk_equations descr vs tycos exhaustives (Ts, Us), SOME termination_tac)
2.124 prfx ["f", "i"] exhaustivesN (map exhaustiveT (Ts @ Us))
2.125 + |> Quickcheck_Common.define_functions
2.126 + (fn full_exhaustives => mk_full_equations descr vs tycos full_exhaustives (Ts, Us),
2.127 + SOME termination_tac)
2.128 + prfx ["f", "i"] full_exhaustivesN (map full_exhaustiveT (Ts @ Us))
2.129 |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
2.130 end handle FUNCTION_TYPE =>
2.131 (Datatype_Aux.message config
2.132 @@ -244,6 +296,48 @@
2.133 val names = Term.add_free_names t []
2.134 val frees = map Free (Term.add_frees t [])
2.135 val ([depth_name], ctxt'') = Variable.variant_fixes ["depth"] ctxt'
2.136 + val depth = Free (depth_name, @{typ code_numeral})
2.137 + val return = @{term "Some :: term list => term list option"} $
2.138 + (HOLogic.mk_list @{typ "term"}
2.139 + (map (fn t => HOLogic.mk_term_of (fastype_of t) t) (frees @ eval_terms)))
2.140 + fun mk_exhaustive_closure (free as Free (_, T)) t =
2.141 + Const (@{const_name "Quickcheck_Exhaustive.exhaustive_class.exhaustive"}, exhaustiveT T)
2.142 + $ lambda free t $ depth
2.143 + val none_t = @{term "None :: term list option"}
2.144 + fun mk_safe_if (cond, then_t, else_t) =
2.145 + @{term "Quickcheck_Exhaustive.catch_match :: term list option => term list option => term list option"} $
2.146 + (@{term "If :: bool => term list option => term list option => term list option"}
2.147 + $ cond $ then_t $ else_t) $ none_t;
2.148 + fun lookup v = the (AList.lookup (op =) (names ~~ frees) v)
2.149 + fun mk_naive_test_term t =
2.150 + fold_rev mk_exhaustive_closure frees (mk_safe_if (t, none_t, return))
2.151 + fun mk_smart_test_term' concl bound_vars assms =
2.152 + let
2.153 + fun vars_of t = subtract (op =) bound_vars (Term.add_free_names t [])
2.154 + val (vars, check) =
2.155 + case assms of [] => (vars_of concl, (concl, none_t, return))
2.156 + | assm :: assms => (vars_of assm, (assm,
2.157 + mk_smart_test_term' concl (union (op =) (vars_of assm) bound_vars) assms, none_t))
2.158 + in
2.159 + fold_rev mk_exhaustive_closure (map lookup vars) (mk_safe_if check)
2.160 + end
2.161 + fun mk_smart_test_term t =
2.162 + let
2.163 + val (assms, concl) = Quickcheck_Common.strip_imp t
2.164 + in
2.165 + mk_smart_test_term' concl [] assms
2.166 + end
2.167 + val mk_test_term =
2.168 + if Config.get ctxt smart_quantifier then mk_smart_test_term else mk_naive_test_term
2.169 + in lambda depth (mk_test_term t) end
2.170 +
2.171 +fun mk_full_generator_expr ctxt (t, eval_terms) =
2.172 + let
2.173 + val thy = ProofContext.theory_of ctxt
2.174 + val ctxt' = Variable.auto_fixes t ctxt
2.175 + val names = Term.add_free_names t []
2.176 + val frees = map Free (Term.add_frees t [])
2.177 + val ([depth_name], ctxt'') = Variable.variant_fixes ["depth"] ctxt'
2.178 val (term_names, ctxt''') = Variable.variant_fixes (map (prefix "t_") names) ctxt''
2.179 val depth = Free (depth_name, @{typ code_numeral})
2.180 val term_vars = map (fn n => Free (n, @{typ "unit => term"})) term_names
2.181 @@ -288,7 +382,7 @@
2.182 if Config.get ctxt smart_quantifier then mk_smart_test_term else mk_naive_test_term
2.183 in lambda depth (mk_test_term t) end
2.184
2.185 -val mk_parametric_generator_expr =
2.186 +fun mk_parametric_generator_expr mk_generator_expr =
2.187 Quickcheck_Common.gen_mk_parametric_generator_expr
2.188 ((mk_generator_expr, absdummy (@{typ "code_numeral"}, @{term "None :: term list option"})),
2.189 @{typ "code_numeral => term list option"})
2.190 @@ -359,7 +453,9 @@
2.191 fun compile_generator_expr ctxt ts =
2.192 let
2.193 val thy = ProofContext.theory_of ctxt
2.194 - val t' = mk_parametric_generator_expr ctxt ts;
2.195 + val mk_generator_expr =
2.196 + if Config.get ctxt full_support then mk_full_generator_expr else mk_generator_expr
2.197 + val t' = mk_parametric_generator_expr mk_generator_expr ctxt ts;
2.198 val compile = Code_Runtime.dynamic_value_strict
2.199 (Counterexample.get, put_counterexample, "Exhaustive_Generators.put_counterexample")
2.200 thy (SOME target) (fn proc => fn g =>
2.201 @@ -402,6 +498,7 @@
2.202 #> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
2.203 (((@{sort type}, @{sort type}), @{sort bounded_forall}), instantiate_bounded_forall_datatype))
2.204 #> setup_smart_quantifier
2.205 + #> setup_full_support
2.206 #> setup_quickcheck_pretty
2.207 #> Context.theory_map (Quickcheck.add_generator ("exhaustive", compile_generator_expr))
2.208 #> Context.theory_map (Quickcheck.add_batch_generator ("exhaustive", compile_generator_exprs))