changing the exhaustive generator signatures;
replacing the hard-wired result type by its own identifier
--- a/src/HOL/Quickcheck_Exhaustive.thy Thu Dec 01 22:14:35 2011 +0100
+++ b/src/HOL/Quickcheck_Exhaustive.thy Thu Dec 01 22:14:35 2011 +0100
@@ -19,12 +19,12 @@
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"
+ fixes full_exhaustive :: "('a * (unit => term) \<Rightarrow> (bool * term list) option) \<Rightarrow> code_numeral \<Rightarrow> (bool * 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"
+function full_exhaustive_code_numeral' :: "(code_numeral * (unit => term) => (bool * term list) option) => code_numeral => code_numeral => (bool * 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)))"
@@ -94,7 +94,7 @@
instantiation int :: full_exhaustive
begin
-function full_exhaustive' :: "(int * (unit => term) => term list option) => int => int => term list option"
+function full_exhaustive' :: "(int * (unit => term) => (bool * term list) option) => int => int => (bool * 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
@@ -154,7 +154,7 @@
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"
+fun full_exhaustive_fun' :: "(('a => 'b) * (unit => term) => (bool * term list) option) => code_numeral => code_numeral => (bool * 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
@@ -168,7 +168,7 @@
(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 full_exhaustive_fun :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => term list option"
+definition full_exhaustive_fun :: "(('a => 'b) * (unit => term) => (bool * term list) option) => code_numeral => (bool * term list) option"
where
"full_exhaustive_fun f d = full_exhaustive_fun' f d d"
@@ -179,10 +179,10 @@
subsubsection {* A smarter enumeration scheme for functions over finite datatypes *}
class check_all = enum + term_of +
- fixes check_all :: "('a * (unit \<Rightarrow> term) \<Rightarrow> term list option) \<Rightarrow> term list option"
+ fixes check_all :: "('a * (unit \<Rightarrow> term) \<Rightarrow> (bool * term list) option) \<Rightarrow> (bool * term list) option"
fixes enum_term_of :: "'a itself \<Rightarrow> unit \<Rightarrow> term list"
-fun check_all_n_lists :: "(('a :: check_all) list * (unit \<Rightarrow> term list) \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
+fun check_all_n_lists :: "(('a :: check_all) list * (unit \<Rightarrow> term list) \<Rightarrow> (bool * term list) option) \<Rightarrow> code_numeral \<Rightarrow> (bool * term list) option"
where
"check_all_n_lists f n =
(if n = 0 then f ([], (%_. [])) else check_all (%(x, xt). check_all_n_lists (%(xs, xst). f ((x # xs), (%_. (xt () # xst ())))) (n - 1)))"
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Thu Dec 01 22:14:35 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Thu Dec 01 22:14:35 2011 +0100
@@ -86,6 +86,8 @@
exception Counterexample of term list
+val resultT = @{typ "(bool * term list) option"};
+
val exhaustiveN = "exhaustive";
val full_exhaustiveN = "full_exhaustive";
val fast_exhaustiveN = "fast_exhaustive";
@@ -99,11 +101,9 @@
fun bounded_forallT T = (T --> @{typ bool}) --> @{typ code_numeral} --> @{typ bool}
-fun full_exhaustiveT T = (termifyT T --> @{typ "(bool * Code_Evaluation.term list) option"})
- --> @{typ code_numeral} --> @{typ "(bool * Code_Evaluation.term list) option"}
+fun full_exhaustiveT T = (termifyT T --> resultT) --> @{typ code_numeral} --> resultT
-fun check_allT T = (termifyT T --> @{typ "Code_Evaluation.term list option"})
- --> @{typ "Code_Evaluation.term list option"}
+fun check_allT T = (termifyT T --> resultT) --> resultT
fun mk_equation_terms generics (descr, vs, Ts) =
let
@@ -181,7 +181,8 @@
fun mk_full_equations functerms =
let
- fun test_function T = Free ("f", termifyT T --> @{typ "(bool * term list) option"})
+ fun test_function T = Free ("f", termifyT T --> resultT)
+ fun split_const T = HOLogic.split_const (T, @{typ "unit => Code_Evaluation.term"}, resultT)
fun mk_call T =
let
val full_exhaustive =
@@ -189,9 +190,7 @@
full_exhaustiveT T)
in
(T, fn t => full_exhaustive $
- (HOLogic.split_const (T, @{typ "unit => Code_Evaluation.term"},
- @{typ "(bool * Code_Evaluation.term list) option"})
- $ absdummy T (absdummy @{typ "unit => Code_Evaluation.term"} t)) $ size_pred)
+ (split_const T $ absdummy T (absdummy @{typ "unit => Code_Evaluation.term"} t)) $ size_pred)
end
fun mk_aux_call fTs (k, _) (tyco, Ts) =
let
@@ -199,9 +198,7 @@
val _ = if not (null fTs) then raise FUNCTION_TYPE else ()
in
(T, fn t => nth functerms k $
- (HOLogic.split_const (T, @{typ "unit => Code_Evaluation.term"},
- @{typ "(bool * Code_Evaluation.term list) option"})
- $ absdummy T (absdummy @{typ "unit => Code_Evaluation.term"} t)) $ size_pred)
+ (split_const T $ absdummy T (absdummy @{typ "unit => Code_Evaluation.term"} t)) $ size_pred)
end
fun mk_consexpr simpleT (c, xs) =
let
@@ -219,7 +216,7 @@
in fold_rev (fn f => fn t => f t) fns start_term end
fun mk_rhs exprs =
mk_if (size_ge_zero, foldr1 mk_none_continuation exprs,
- @{term "None :: (bool * term list) option"})
+ Const (@{const_name "None"}, resultT))
in
mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms)
end
@@ -373,21 +370,21 @@
fun mk_exhaustive_closure (free as Free (_, T), term_var) t =
if Sign.of_sort thy (T, @{sort enum}) then
Const (@{const_name "Quickcheck_Exhaustive.check_all_class.check_all"}, check_allT T)
- $ (HOLogic.split_const (T, @{typ "unit => term"}, @{typ "term list option"})
+ $ (HOLogic.split_const (T, @{typ "unit => term"}, resultT)
$ lambda free (lambda term_var t))
else
Const (@{const_name "Quickcheck_Exhaustive.full_exhaustive_class.full_exhaustive"}, full_exhaustiveT T)
- $ (HOLogic.split_const (T, @{typ "unit => term"}, @{typ "(bool * term list) option"})
+ $ (HOLogic.split_const (T, @{typ "unit => term"}, resultT)
$ lambda free (lambda term_var t)) $ depth
- val none_t = @{term "None :: (bool * term list) option"}
+ val none_t = Const (@{const_name "None"}, resultT)
val mk_if = Quickcheck_Common.mk_safe_if ctxt
val mk_test_term = mk_test_term lookup mk_exhaustive_closure mk_if none_t return ctxt
in lambda depth (mk_test_term t) end
fun mk_parametric_generator_expr mk_generator_expr =
Quickcheck_Common.gen_mk_parametric_generator_expr
- ((mk_generator_expr, absdummy @{typ "code_numeral"} @{term "None :: (bool * term list) option"}),
- @{typ "code_numeral => (bool * term list) option"})
+ ((mk_generator_expr, absdummy @{typ "code_numeral"} (Const (@{const_name "None"}, resultT))),
+ @{typ "code_numeral"} --> resultT)
fun mk_validator_expr ctxt t =
let