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 @@ -69,10 +69,6 @@
1.4 val size_pred = @{term "(i :: code_numeral) - 1"}
1.5 val size_ge_zero = @{term "(i :: code_numeral) > 0"}
1.6
1.7 -fun test_function T = Free ("f", T --> @{typ "term list option"})
1.8 -fun full_test_function T = Free ("f", termifyT T --> @{typ "term list option"})
1.9 -fun fast_test_function T = Free ("f", T --> @{typ "unit"})
1.10 -
1.11 fun mk_none_continuation (x, y) =
1.12 let
1.13 val (T as Type(@{type_name "option"}, [T'])) = fastype_of x
1.14 @@ -98,7 +94,6 @@
1.15 fun fast_exhaustiveT T = (T --> @{typ unit})
1.16 --> @{typ code_numeral} --> @{typ unit}
1.17
1.18 -
1.19 fun exhaustiveT T = (T --> @{typ "Code_Evaluation.term list option"})
1.20 --> @{typ code_numeral} --> @{typ "Code_Evaluation.term list option"}
1.21
1.22 @@ -108,13 +103,28 @@
1.23 fun check_allT T = (termifyT T --> @{typ "Code_Evaluation.term list option"})
1.24 --> @{typ "Code_Evaluation.term list option"}
1.25
1.26 +fun mk_equation_terms generics (descr, vs, Ts) =
1.27 + let
1.28 + val (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, exhaustives) = generics
1.29 + val rhss =
1.30 + Datatype_Aux.interpret_construction descr vs
1.31 + { atyp = mk_call, dtyp = mk_aux_call }
1.32 + |> (map o apfst) Type
1.33 + |> map (fn (T, cs) => map (mk_consexpr T) cs)
1.34 + |> map mk_rhs
1.35 + val lhss = map2 (fn t => fn T => t $ test_function T $ size) exhaustives Ts
1.36 + in
1.37 + map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhss ~~ rhss)
1.38 + end
1.39
1.40 -fun mk_fast_equations descr vs tycos fast_exhaustives (Ts, Us) =
1.41 +fun mk_fast_equations functerms =
1.42 let
1.43 + fun test_function T = Free ("f", T --> @{typ "unit"})
1.44 fun mk_call T =
1.45 let
1.46 val fast_exhaustive =
1.47 - Const (@{const_name "Quickcheck_Exhaustive.fast_exhaustive_class.fast_exhaustive"}, fast_exhaustiveT T)
1.48 + Const (@{const_name "Quickcheck_Exhaustive.fast_exhaustive_class.fast_exhaustive"},
1.49 + fast_exhaustiveT T)
1.50 in
1.51 (T, fn t => fast_exhaustive $ absdummy (T, t) $ size_pred)
1.52 end
1.53 @@ -123,7 +133,7 @@
1.54 val T = Type (tyco, Ts)
1.55 val _ = if not (null fTs) then raise FUNCTION_TYPE else ()
1.56 in
1.57 - (T, fn t => nth fast_exhaustives k $ absdummy (T, t) $ size_pred)
1.58 + (T, fn t => nth functerms k $ absdummy (T, t) $ size_pred)
1.59 end
1.60 fun mk_consexpr simpleT (c, xs) =
1.61 let
1.62 @@ -131,28 +141,21 @@
1.63 val constr = Const (c, Ts ---> simpleT)
1.64 val bounds = map Bound (((length xs) - 1) downto 0)
1.65 val term_bounds = map (fn x => Bound (2 * x)) (((length xs) - 1) downto 0)
1.66 - val start_term = fast_test_function simpleT $ list_comb (constr, bounds)
1.67 + val start_term = test_function simpleT $ list_comb (constr, bounds)
1.68 in fold_rev (fn f => fn t => f t) fns start_term end
1.69 - fun mk_rhs exprs =
1.70 - @{term "If :: bool => unit => unit => unit"}
1.71 - $ size_ge_zero $ (foldr1 mk_unit_let exprs) $ @{term "()"}
1.72 - val rhss =
1.73 - Datatype_Aux.interpret_construction descr vs
1.74 - { atyp = mk_call, dtyp = mk_aux_call }
1.75 - |> (map o apfst) Type
1.76 - |> map (fn (T, cs) => map (mk_consexpr T) cs)
1.77 - |> map mk_rhs
1.78 - val lhss = map2 (fn t => fn T => t $ fast_test_function T $ size) fast_exhaustives (Ts @ Us)
1.79 - val eqs = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhss ~~ rhss)
1.80 + fun mk_rhs exprs = @{term "If :: bool => unit => unit => unit"}
1.81 + $ size_ge_zero $ (foldr1 mk_unit_let exprs) $ @{term "()"}
1.82 in
1.83 - eqs
1.84 + mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms)
1.85 end
1.86 -
1.87 -fun mk_equations descr vs tycos exhaustives (Ts, Us) =
1.88 +
1.89 +fun mk_equations functerms =
1.90 let
1.91 + fun test_function T = Free ("f", T --> @{typ "term list option"})
1.92 fun mk_call T =
1.93 let
1.94 - val exhaustive = Const (@{const_name "Quickcheck_Exhaustive.exhaustive_class.exhaustive"}, exhaustiveT T)
1.95 + val exhaustive =
1.96 + Const (@{const_name "Quickcheck_Exhaustive.exhaustive_class.exhaustive"}, exhaustiveT T)
1.97 in
1.98 (T, fn t => exhaustive $ absdummy (T, t) $ size_pred)
1.99 end
1.100 @@ -161,7 +164,7 @@
1.101 val T = Type (tyco, Ts)
1.102 val _ = if not (null fTs) then raise FUNCTION_TYPE else ()
1.103 in
1.104 - (T, fn t => nth exhaustives k $ absdummy (T, t) $ size_pred)
1.105 + (T, fn t => nth functerms k $ absdummy (T, t) $ size_pred)
1.106 end
1.107 fun mk_consexpr simpleT (c, xs) =
1.108 let
1.109 @@ -174,23 +177,17 @@
1.110 fun mk_rhs exprs =
1.111 @{term "If :: bool => term list option => term list option => term list option"}
1.112 $ size_ge_zero $ (foldr1 mk_none_continuation exprs) $ @{term "None :: term list option"}
1.113 - val rhss =
1.114 - Datatype_Aux.interpret_construction descr vs
1.115 - { atyp = mk_call, dtyp = mk_aux_call }
1.116 - |> (map o apfst) Type
1.117 - |> map (fn (T, cs) => map (mk_consexpr T) cs)
1.118 - |> map mk_rhs
1.119 - val lhss = map2 (fn t => fn T => t $ test_function T $ size) exhaustives (Ts @ Us)
1.120 - val eqs = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhss ~~ rhss)
1.121 in
1.122 - eqs
1.123 + mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms)
1.124 end
1.125
1.126 -fun mk_full_equations descr vs tycos full_exhaustives (Ts, Us) =
1.127 +fun mk_full_equations functerms =
1.128 let
1.129 + fun test_function T = Free ("f", termifyT T --> @{typ "term list option"})
1.130 fun mk_call T =
1.131 let
1.132 - val full_exhaustive = Const (@{const_name "Quickcheck_Exhaustive.exhaustive_class.full_exhaustive"}, full_exhaustiveT T)
1.133 + val full_exhaustive =
1.134 + Const (@{const_name "Quickcheck_Exhaustive.exhaustive_class.full_exhaustive"}, full_exhaustiveT T)
1.135 in
1.136 (T, (fn t => full_exhaustive $
1.137 (HOLogic.split_const (T, @{typ "unit => Code_Evaluation.term"}, @{typ "Code_Evaluation.term list option"})
1.138 @@ -201,7 +198,7 @@
1.139 val T = Type (tyco, Ts)
1.140 val _ = if not (null fTs) then raise FUNCTION_TYPE else ()
1.141 in
1.142 - (T, (fn t => nth full_exhaustives k $
1.143 + (T, (fn t => nth functerms k $
1.144 (HOLogic.split_const (T, @{typ "unit => Code_Evaluation.term"}, @{typ "Code_Evaluation.term list option"})
1.145 $ absdummy (T, absdummy (@{typ "unit => Code_Evaluation.term"}, t))) $ size_pred))
1.146 end
1.147 @@ -215,25 +212,17 @@
1.148 val Eval_Const = Const ("Code_Evaluation.Const", HOLogic.literalT --> @{typ typerep} --> HOLogic.termT)
1.149 val term = fold (fn u => fn t => Eval_App $ t $ (u $ @{term "()"}))
1.150 bounds (Eval_Const $ HOLogic.mk_literal c $ HOLogic.mk_typerep (Ts ---> simpleT))
1.151 - val start_term = full_test_function simpleT $
1.152 + val start_term = test_function simpleT $
1.153 (HOLogic.pair_const simpleT @{typ "unit => Code_Evaluation.term"}
1.154 $ (list_comb (constr, bounds)) $ absdummy (@{typ unit}, term))
1.155 in fold_rev (fn f => fn t => f t) fns start_term end
1.156 fun mk_rhs exprs =
1.157 @{term "If :: bool => term list option => term list option => term list option"}
1.158 $ size_ge_zero $ (foldr1 mk_none_continuation exprs) $ @{term "None :: term list option"}
1.159 - val rhss =
1.160 - Datatype_Aux.interpret_construction descr vs
1.161 - { atyp = mk_call, dtyp = mk_aux_call }
1.162 - |> (map o apfst) Type
1.163 - |> map (fn (T, cs) => map (mk_consexpr T) cs)
1.164 - |> map mk_rhs
1.165 - val lhss = map2 (fn t => fn T => t $ full_test_function T $ size) full_exhaustives (Ts @ Us);
1.166 - val eqs = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhss ~~ rhss)
1.167 in
1.168 - eqs
1.169 + mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms)
1.170 end
1.171 -
1.172 +
1.173 (* foundational definition with the function package *)
1.174
1.175 val less_int_pred = @{lemma "i > 0 ==> Code_Numeral.nat_of ((i :: code_numeral) - 1) < Code_Numeral.nat_of i" by auto}
1.176 @@ -266,11 +255,10 @@
1.177 thy
1.178 |> Class.instantiation (tycos, vs, @{sort exhaustive})
1.179 |> Quickcheck_Common.define_functions
1.180 - (fn exhaustives => mk_equations descr vs tycos exhaustives (Ts, Us), SOME termination_tac)
1.181 + (fn functerms => mk_equations functerms (descr, vs, Ts @ Us), SOME termination_tac)
1.182 prfx ["f", "i"] exhaustivesN (map exhaustiveT (Ts @ Us))
1.183 |> Quickcheck_Common.define_functions
1.184 - (fn full_exhaustives => mk_full_equations descr vs tycos full_exhaustives (Ts, Us),
1.185 - SOME termination_tac)
1.186 + (fn functerms => mk_full_equations functerms (descr, vs, Ts @ Us), SOME termination_tac)
1.187 prfx ["f", "i"] full_exhaustivesN (map full_exhaustiveT (Ts @ Us))
1.188 |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
1.189 end handle FUNCTION_TYPE =>
1.190 @@ -286,7 +274,7 @@
1.191 thy
1.192 |> Class.instantiation (tycos, vs, @{sort fast_exhaustive})
1.193 |> Quickcheck_Common.define_functions
1.194 - (fn exhaustives => mk_fast_equations descr vs tycos exhaustives (Ts, Us), SOME termination_tac)
1.195 + (fn functerms => mk_fast_equations functerms (descr, vs, Ts @ Us), SOME termination_tac)
1.196 prfx ["f", "i"] fast_exhaustivesN (map fast_exhaustiveT (Ts @ Us))
1.197 |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
1.198 end handle FUNCTION_TYPE =>
1.199 @@ -300,8 +288,9 @@
1.200
1.201 fun bounded_forallT T = (T --> @{typ bool}) --> @{typ code_numeral} --> @{typ bool}
1.202
1.203 -fun mk_bounded_forall_equations descr vs tycos bounded_foralls (Ts, Us) =
1.204 +fun mk_bounded_forall_equations functerms =
1.205 let
1.206 + fun test_function T = Free ("P", T --> @{typ bool})
1.207 fun mk_call T =
1.208 let
1.209 val bounded_forall =
1.210 @@ -315,29 +304,20 @@
1.211 val T = Type (tyco, Ts)
1.212 val _ = if not (null fTs) then raise FUNCTION_TYPE else ()
1.213 in
1.214 - (T, (fn t => nth bounded_foralls k $ absdummy (T, t) $ size_pred))
1.215 + (T, (fn t => nth functerms k $ absdummy (T, t) $ size_pred))
1.216 end
1.217 fun mk_consexpr simpleT (c, xs) =
1.218 let
1.219 val (Ts, fns) = split_list xs
1.220 val constr = Const (c, Ts ---> simpleT)
1.221 val bounds = map Bound (((length xs) - 1) downto 0)
1.222 - val start_term = Free ("P", simpleT --> @{typ bool}) $ list_comb (constr, bounds)
1.223 + val start_term = test_function simpleT $ list_comb (constr, bounds)
1.224 in fold_rev (fn f => fn t => f t) fns start_term end
1.225 fun mk_rhs exprs =
1.226 @{term "If :: bool => bool => bool => bool"} $ size_ge_zero $
1.227 (foldr1 HOLogic.mk_conj exprs) $ @{term "True"}
1.228 - val rhss =
1.229 - Datatype_Aux.interpret_construction descr vs
1.230 - { atyp = mk_call, dtyp = mk_aux_call }
1.231 - |> (map o apfst) Type
1.232 - |> map (fn (T, cs) => map (mk_consexpr T) cs)
1.233 - |> map mk_rhs
1.234 - val lhss =
1.235 - map2 (fn t => fn T => t $ Free ("P", T --> @{typ bool}) $ size) bounded_foralls (Ts @ Us)
1.236 - val eqs = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhss ~~ rhss)
1.237 in
1.238 - eqs
1.239 + mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms)
1.240 end
1.241
1.242 (* creating the bounded_forall instances *)
1.243 @@ -350,8 +330,7 @@
1.244 thy
1.245 |> Class.instantiation (tycos, vs, @{sort bounded_forall})
1.246 |> Quickcheck_Common.define_functions
1.247 - (fn bounded_foralls =>
1.248 - mk_bounded_forall_equations descr vs tycos bounded_foralls (Ts, Us), NONE)
1.249 + (fn functerms => mk_bounded_forall_equations functerms (descr, vs, Ts @ Us), NONE)
1.250 prfx ["P", "i"] bounded_forallsN (map bounded_forallT (Ts @ Us))
1.251 |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
1.252 end handle FUNCTION_TYPE =>