1.1 --- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Fri Apr 08 16:31:14 2011 +0200
1.2 +++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Fri Apr 08 16:31:14 2011 +0200
1.3 @@ -24,7 +24,9 @@
1.4 structure Exhaustive_Generators : EXHAUSTIVE_GENERATORS =
1.5 struct
1.6
1.7 -(* dynamic options *)
1.8 +(* basics *)
1.9 +
1.10 +(** dynamic options **)
1.11
1.12 val (smart_quantifier, setup_smart_quantifier) =
1.13 Attrib.config_bool "quickcheck_smart_quantifier" (K true)
1.14 @@ -59,7 +61,6 @@
1.15 | mk_sumcases _ f T = f T
1.16
1.17 fun mk_undefined T = Const(@{const_name undefined}, T)
1.18 -
1.19
1.20 (** abstract syntax **)
1.21
1.22 @@ -79,9 +80,9 @@
1.23 fun mk_unit_let (x, y) =
1.24 Const (@{const_name "Let"}, @{typ "unit => (unit => unit) => unit"}) $ x $ (absdummy (@{typ unit}, y))
1.25
1.26 -(** datatypes **)
1.27 +(* handling inductive datatypes *)
1.28
1.29 -(* constructing exhaustive generator instances on datatypes *)
1.30 +(** constructing generator instances **)
1.31
1.32 exception FUNCTION_TYPE;
1.33
1.34 @@ -90,6 +91,7 @@
1.35 val exhaustiveN = "exhaustive";
1.36 val full_exhaustiveN = "full_exhaustive";
1.37 val fast_exhaustiveN = "fast_exhaustive";
1.38 +val bounded_forallN = "bounded_forall";
1.39
1.40 fun fast_exhaustiveT T = (T --> @{typ unit})
1.41 --> @{typ code_numeral} --> @{typ unit}
1.42 @@ -97,6 +99,8 @@
1.43 fun exhaustiveT T = (T --> @{typ "Code_Evaluation.term list option"})
1.44 --> @{typ code_numeral} --> @{typ "Code_Evaluation.term list option"}
1.45
1.46 +fun bounded_forallT T = (T --> @{typ bool}) --> @{typ code_numeral} --> @{typ bool}
1.47 +
1.48 fun full_exhaustiveT T = (termifyT T --> @{typ "Code_Evaluation.term list option"})
1.49 --> @{typ code_numeral} --> @{typ "Code_Evaluation.term list option"}
1.50
1.51 @@ -117,32 +121,33 @@
1.52 map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhss ~~ rhss)
1.53 end
1.54
1.55 +fun gen_mk_call c T = (T, fn t => c T $ absdummy (T, t) $ size_pred)
1.56 +
1.57 +fun gen_mk_aux_call functerms fTs (k, _) (tyco, Ts) =
1.58 + let
1.59 + val T = Type (tyco, Ts)
1.60 + val _ = if not (null fTs) then raise FUNCTION_TYPE else ()
1.61 + in
1.62 + (T, fn t => nth functerms k $ absdummy (T, t) $ size_pred)
1.63 + end
1.64 +
1.65 +fun gen_mk_consexpr test_function functerms simpleT (c, xs) =
1.66 + let
1.67 + val (Ts, fns) = split_list xs
1.68 + val constr = Const (c, Ts ---> simpleT)
1.69 + val bounds = map Bound (((length xs) - 1) downto 0)
1.70 + val term_bounds = map (fn x => Bound (2 * x)) (((length xs) - 1) downto 0)
1.71 + val start_term = test_function simpleT $ list_comb (constr, bounds)
1.72 + in fold_rev (fn f => fn t => f t) fns start_term end
1.73 +
1.74 fun mk_fast_equations functerms =
1.75 let
1.76 fun test_function T = Free ("f", T --> @{typ "unit"})
1.77 - fun mk_call T =
1.78 - let
1.79 - val fast_exhaustive =
1.80 - Const (@{const_name "Quickcheck_Exhaustive.fast_exhaustive_class.fast_exhaustive"},
1.81 - fast_exhaustiveT T)
1.82 - in
1.83 - (T, fn t => fast_exhaustive $ absdummy (T, t) $ size_pred)
1.84 - end
1.85 - fun mk_aux_call fTs (k, _) (tyco, Ts) =
1.86 - let
1.87 - val T = Type (tyco, Ts)
1.88 - val _ = if not (null fTs) then raise FUNCTION_TYPE else ()
1.89 - in
1.90 - (T, fn t => nth functerms k $ absdummy (T, t) $ size_pred)
1.91 - end
1.92 - fun mk_consexpr simpleT (c, xs) =
1.93 - let
1.94 - val (Ts, fns) = split_list xs
1.95 - val constr = Const (c, Ts ---> simpleT)
1.96 - val bounds = map Bound (((length xs) - 1) downto 0)
1.97 - val term_bounds = map (fn x => Bound (2 * x)) (((length xs) - 1) downto 0)
1.98 - val start_term = test_function simpleT $ list_comb (constr, bounds)
1.99 - in fold_rev (fn f => fn t => f t) fns start_term end
1.100 + val mk_call = gen_mk_call (fn T =>
1.101 + Const (@{const_name "Quickcheck_Exhaustive.fast_exhaustive_class.fast_exhaustive"},
1.102 + fast_exhaustiveT T))
1.103 + val mk_aux_call = gen_mk_aux_call functerms
1.104 + val mk_consexpr = gen_mk_consexpr test_function functerms
1.105 fun mk_rhs exprs = @{term "If :: bool => unit => unit => unit"}
1.106 $ size_ge_zero $ (foldr1 mk_unit_let exprs) $ @{term "()"}
1.107 in
1.108 @@ -152,42 +157,40 @@
1.109 fun mk_equations functerms =
1.110 let
1.111 fun test_function T = Free ("f", T --> @{typ "term list option"})
1.112 - fun mk_call T =
1.113 - let
1.114 - val exhaustive =
1.115 - Const (@{const_name "Quickcheck_Exhaustive.exhaustive_class.exhaustive"}, exhaustiveT T)
1.116 - in
1.117 - (T, fn t => exhaustive $ absdummy (T, t) $ size_pred)
1.118 - end
1.119 - fun mk_aux_call fTs (k, _) (tyco, Ts) =
1.120 - let
1.121 - val T = Type (tyco, Ts)
1.122 - val _ = if not (null fTs) then raise FUNCTION_TYPE else ()
1.123 - in
1.124 - (T, fn t => nth functerms k $ absdummy (T, t) $ size_pred)
1.125 - end
1.126 - fun mk_consexpr simpleT (c, xs) =
1.127 - let
1.128 - val (Ts, fns) = split_list xs
1.129 - val constr = Const (c, Ts ---> simpleT)
1.130 - val bounds = map Bound (((length xs) - 1) downto 0)
1.131 - val term_bounds = map (fn x => Bound (2 * x)) (((length xs) - 1) downto 0)
1.132 - val start_term = test_function simpleT $ list_comb (constr, bounds)
1.133 - in fold_rev (fn f => fn t => f t) fns start_term end
1.134 + val mk_call = gen_mk_call (fn T =>
1.135 + Const (@{const_name "Quickcheck_Exhaustive.exhaustive_class.exhaustive"}, exhaustiveT T))
1.136 + val mk_aux_call = gen_mk_aux_call functerms
1.137 + val mk_consexpr = gen_mk_consexpr test_function functerms
1.138 fun mk_rhs exprs =
1.139 @{term "If :: bool => term list option => term list option => term list option"}
1.140 $ size_ge_zero $ (foldr1 mk_none_continuation exprs) $ @{term "None :: term list option"}
1.141 in
1.142 mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms)
1.143 end
1.144 -
1.145 +
1.146 +fun mk_bounded_forall_equations functerms =
1.147 + let
1.148 + fun test_function T = Free ("P", T --> @{typ bool})
1.149 + val mk_call = gen_mk_call (fn T =>
1.150 + Const (@{const_name "Quickcheck_Exhaustive.bounded_forall_class.bounded_forall"},
1.151 + bounded_forallT T))
1.152 + val mk_aux_call = gen_mk_aux_call functerms
1.153 + val mk_consexpr = gen_mk_consexpr test_function functerms
1.154 + fun mk_rhs exprs =
1.155 + @{term "If :: bool => bool => bool => bool"} $ size_ge_zero $
1.156 + (foldr1 HOLogic.mk_conj exprs) $ @{term "True"}
1.157 + in
1.158 + mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms)
1.159 + end
1.160 +
1.161 fun mk_full_equations functerms =
1.162 let
1.163 fun test_function T = Free ("f", termifyT T --> @{typ "term list option"})
1.164 fun mk_call T =
1.165 let
1.166 val full_exhaustive =
1.167 - Const (@{const_name "Quickcheck_Exhaustive.exhaustive_class.full_exhaustive"}, full_exhaustiveT T)
1.168 + Const (@{const_name "Quickcheck_Exhaustive.exhaustive_class.full_exhaustive"},
1.169 + full_exhaustiveT T)
1.170 in
1.171 (T, (fn t => full_exhaustive $
1.172 (HOLogic.split_const (T, @{typ "unit => Code_Evaluation.term"}, @{typ "Code_Evaluation.term list option"})
1.173 @@ -223,7 +226,7 @@
1.174 mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms)
1.175 end
1.176
1.177 -(* foundational definition with the function package *)
1.178 +(** foundational definition with the function package **)
1.179
1.180 val less_int_pred = @{lemma "i > 0 ==> Code_Numeral.nat_of ((i :: code_numeral) - 1) < Code_Numeral.nat_of i" by auto}
1.181
1.182 @@ -244,7 +247,7 @@
1.183 (HOL_basic_ss addsimps [@{thm in_measure}, @{thm o_def}, @{thm snd_conv},
1.184 @{thm nat_mono_iff}, less_int_pred] @ @{thms sum.cases}) 1))
1.185
1.186 -(* creating the instances *)
1.187 +(** instantiating generator classes **)
1.188
1.189 fun instantiate_exhaustive_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
1.190 let
1.191 @@ -281,46 +284,6 @@
1.192 (Datatype_Aux.message config
1.193 "Creation of exhaustive generators failed because the datatype contains a function type";
1.194 thy)
1.195 -
1.196 -(* constructing bounded_forall instances on datatypes *)
1.197 -
1.198 -val bounded_forallN = "bounded_forall";
1.199 -
1.200 -fun bounded_forallT T = (T --> @{typ bool}) --> @{typ code_numeral} --> @{typ bool}
1.201 -
1.202 -fun mk_bounded_forall_equations functerms =
1.203 - let
1.204 - fun test_function T = Free ("P", T --> @{typ bool})
1.205 - fun mk_call T =
1.206 - let
1.207 - val bounded_forall =
1.208 - Const (@{const_name "Quickcheck_Exhaustive.bounded_forall_class.bounded_forall"},
1.209 - bounded_forallT T)
1.210 - in
1.211 - (T, (fn t => bounded_forall $ absdummy (T, t) $ size_pred))
1.212 - end
1.213 - fun mk_aux_call fTs (k, _) (tyco, Ts) =
1.214 - let
1.215 - val T = Type (tyco, Ts)
1.216 - val _ = if not (null fTs) then raise FUNCTION_TYPE else ()
1.217 - in
1.218 - (T, (fn t => nth functerms k $ absdummy (T, t) $ size_pred))
1.219 - end
1.220 - fun mk_consexpr simpleT (c, xs) =
1.221 - let
1.222 - val (Ts, fns) = split_list xs
1.223 - val constr = Const (c, Ts ---> simpleT)
1.224 - val bounds = map Bound (((length xs) - 1) downto 0)
1.225 - val start_term = test_function simpleT $ list_comb (constr, bounds)
1.226 - in fold_rev (fn f => fn t => f t) fns start_term end
1.227 - fun mk_rhs exprs =
1.228 - @{term "If :: bool => bool => bool => bool"} $ size_ge_zero $
1.229 - (foldr1 HOLogic.mk_conj exprs) $ @{term "True"}
1.230 - in
1.231 - mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms)
1.232 - end
1.233 -
1.234 -(* creating the bounded_forall instances *)
1.235
1.236 fun instantiate_bounded_forall_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
1.237 let
1.238 @@ -338,7 +301,7 @@
1.239 "Creation of bounded universal quantifiers failed because the datatype contains a function type";
1.240 thy)
1.241
1.242 -(** building and compiling generator expressions **)
1.243 +(* building and compiling generator expressions *)
1.244
1.245 fun mk_fast_generator_expr ctxt (t, eval_terms) =
1.246 let
1.247 @@ -582,7 +545,7 @@
1.248 thy (SOME target) (K I) (HOLogic.mk_list @{typ "code_numeral => bool"} ts') []
1.249 end;
1.250
1.251 -(** setup **)
1.252 +(* setup *)
1.253
1.254 val setup =
1.255 Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype