# HG changeset patch
# User bulwahn
# Date 1322774075 -3600
# Node ID 63b42a7db003bacd66684a5866c8611de3f56c96
# Parent  d1fb55c2ed65223be094cd8832785d480ed8a809
changing the exhaustive generator signatures;
replacing the hard-wired result type by its own identifier

diff -r d1fb55c2ed65 -r 63b42a7db003 src/HOL/Quickcheck_Exhaustive.thy
--- 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)))"
diff -r d1fb55c2ed65 -r 63b42a7db003 src/HOL/Tools/Quickcheck/exhaustive_generators.ML
--- 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