changing the exhaustive generator signatures;
authorbulwahn
Thu Dec 01 22:14:35 2011 +0100 (2011-12-01)
changeset 4572263b42a7db003
parent 45721 d1fb55c2ed65
child 45723 75691bcc2c0f
changing the exhaustive generator signatures;
replacing the hard-wired result type by its own identifier
src/HOL/Quickcheck_Exhaustive.thy
src/HOL/Tools/Quickcheck/exhaustive_generators.ML
     1.1 --- a/src/HOL/Quickcheck_Exhaustive.thy	Thu Dec 01 22:14:35 2011 +0100
     1.2 +++ b/src/HOL/Quickcheck_Exhaustive.thy	Thu Dec 01 22:14:35 2011 +0100
     1.3 @@ -19,12 +19,12 @@
     1.4    fixes exhaustive :: "('a \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
     1.5    
     1.6  class full_exhaustive = term_of +
     1.7 -  fixes full_exhaustive :: "('a * (unit => term) \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
     1.8 +  fixes full_exhaustive :: "('a * (unit => term) \<Rightarrow> (bool * term list) option) \<Rightarrow> code_numeral \<Rightarrow> (bool * term list) option"
     1.9  
    1.10  instantiation code_numeral :: full_exhaustive
    1.11  begin
    1.12  
    1.13 -function full_exhaustive_code_numeral' :: "(code_numeral * (unit => term) => term list option) => code_numeral => code_numeral => term list option"
    1.14 +function full_exhaustive_code_numeral' :: "(code_numeral * (unit => term) => (bool * term list) option) => code_numeral => code_numeral => (bool * term list) option"
    1.15    where "full_exhaustive_code_numeral' f d i =
    1.16      (if d < i then None
    1.17      else (f (i, %_. Code_Evaluation.term_of i)) orelse (full_exhaustive_code_numeral' f d (i + 1)))"
    1.18 @@ -94,7 +94,7 @@
    1.19  instantiation int :: full_exhaustive
    1.20  begin
    1.21  
    1.22 -function full_exhaustive' :: "(int * (unit => term) => term list option) => int => int => term list option"
    1.23 +function full_exhaustive' :: "(int * (unit => term) => (bool * term list) option) => int => int => (bool * term list) option"
    1.24    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.25  by pat_completeness auto
    1.26  
    1.27 @@ -154,7 +154,7 @@
    1.28  instantiation "fun" :: ("{equal, full_exhaustive}", full_exhaustive) full_exhaustive
    1.29  begin
    1.30  
    1.31 -fun full_exhaustive_fun' :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => code_numeral => term list option"
    1.32 +fun full_exhaustive_fun' :: "(('a => 'b) * (unit => term) => (bool * term list) option) => code_numeral => code_numeral => (bool * term list) option"
    1.33  where
    1.34    "full_exhaustive_fun' f i d = (full_exhaustive (%(b, t). f (%_. b, %_. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a)) (t ()))) d)
    1.35     orelse (if i > 1 then
    1.36 @@ -168,7 +168,7 @@
    1.37                    (Code_Evaluation.Const (STR ''Fun.fun_upd'') (fun (fun A B) (fun A (fun B (fun A B)))))
    1.38                  (gt ())) (at ())) (bt ())))) d) d) (i - 1) d else None)"
    1.39  
    1.40 -definition full_exhaustive_fun :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => term list option"
    1.41 +definition full_exhaustive_fun :: "(('a => 'b) * (unit => term) => (bool * term list) option) => code_numeral => (bool * term list) option"
    1.42  where
    1.43    "full_exhaustive_fun f d = full_exhaustive_fun' f d d" 
    1.44  
    1.45 @@ -179,10 +179,10 @@
    1.46  subsubsection {* A smarter enumeration scheme for functions over finite datatypes *}
    1.47  
    1.48  class check_all = enum + term_of +
    1.49 -  fixes check_all :: "('a * (unit \<Rightarrow> term) \<Rightarrow> term list option) \<Rightarrow> term list option"
    1.50 +  fixes check_all :: "('a * (unit \<Rightarrow> term) \<Rightarrow> (bool * term list) option) \<Rightarrow> (bool * term list) option"
    1.51    fixes enum_term_of :: "'a itself \<Rightarrow> unit \<Rightarrow> term list"
    1.52    
    1.53 -fun check_all_n_lists :: "(('a :: check_all) list * (unit \<Rightarrow> term list) \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
    1.54 +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"
    1.55  where
    1.56    "check_all_n_lists f n =
    1.57       (if n = 0 then f ([], (%_. [])) else check_all (%(x, xt). check_all_n_lists (%(xs, xst). f ((x # xs), (%_. (xt () # xst ())))) (n - 1)))"
     2.1 --- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Thu Dec 01 22:14:35 2011 +0100
     2.2 +++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Thu Dec 01 22:14:35 2011 +0100
     2.3 @@ -86,6 +86,8 @@
     2.4  
     2.5  exception Counterexample of term list
     2.6  
     2.7 +val resultT =  @{typ "(bool * term list) option"};
     2.8 +
     2.9  val exhaustiveN = "exhaustive";
    2.10  val full_exhaustiveN = "full_exhaustive";
    2.11  val fast_exhaustiveN = "fast_exhaustive";
    2.12 @@ -99,11 +101,9 @@
    2.13  
    2.14  fun bounded_forallT T = (T --> @{typ bool}) --> @{typ code_numeral} --> @{typ bool}
    2.15  
    2.16 -fun full_exhaustiveT T = (termifyT T --> @{typ "(bool * Code_Evaluation.term list) option"})
    2.17 -  --> @{typ code_numeral} --> @{typ "(bool * Code_Evaluation.term list) option"}
    2.18 +fun full_exhaustiveT T = (termifyT T --> resultT) --> @{typ code_numeral} --> resultT
    2.19  
    2.20 -fun check_allT T = (termifyT T --> @{typ "Code_Evaluation.term list option"})
    2.21 -  --> @{typ "Code_Evaluation.term list option"}
    2.22 +fun check_allT T = (termifyT T --> resultT) --> resultT
    2.23  
    2.24  fun mk_equation_terms generics (descr, vs, Ts) =
    2.25    let
    2.26 @@ -181,7 +181,8 @@
    2.27    
    2.28  fun mk_full_equations functerms =
    2.29    let
    2.30 -    fun test_function T = Free ("f", termifyT T --> @{typ "(bool * term list) option"})
    2.31 +    fun test_function T = Free ("f", termifyT T --> resultT)
    2.32 +    fun split_const T = HOLogic.split_const (T, @{typ "unit => Code_Evaluation.term"}, resultT)
    2.33      fun mk_call T =
    2.34        let
    2.35          val full_exhaustive =
    2.36 @@ -189,9 +190,7 @@
    2.37              full_exhaustiveT T)
    2.38        in                                   
    2.39          (T, fn t => full_exhaustive $
    2.40 -          (HOLogic.split_const (T, @{typ "unit => Code_Evaluation.term"},
    2.41 -            @{typ "(bool * Code_Evaluation.term list) option"})
    2.42 -          $ absdummy T (absdummy @{typ "unit => Code_Evaluation.term"} t)) $ size_pred)
    2.43 +          (split_const T $ absdummy T (absdummy @{typ "unit => Code_Evaluation.term"} t)) $ size_pred)
    2.44        end
    2.45      fun mk_aux_call fTs (k, _) (tyco, Ts) =
    2.46        let
    2.47 @@ -199,9 +198,7 @@
    2.48          val _ = if not (null fTs) then raise FUNCTION_TYPE else ()
    2.49        in
    2.50          (T, fn t => nth functerms k $
    2.51 -          (HOLogic.split_const (T, @{typ "unit => Code_Evaluation.term"},
    2.52 -            @{typ "(bool * Code_Evaluation.term list) option"})
    2.53 -            $ absdummy T (absdummy @{typ "unit => Code_Evaluation.term"} t)) $ size_pred)
    2.54 +          (split_const T $ absdummy T (absdummy @{typ "unit => Code_Evaluation.term"} t)) $ size_pred)
    2.55        end
    2.56      fun mk_consexpr simpleT (c, xs) =
    2.57        let
    2.58 @@ -219,7 +216,7 @@
    2.59        in fold_rev (fn f => fn t => f t) fns start_term end
    2.60      fun mk_rhs exprs =
    2.61        mk_if (size_ge_zero, foldr1 mk_none_continuation exprs,
    2.62 -        @{term "None :: (bool * term list) option"})
    2.63 +        Const (@{const_name "None"}, resultT))
    2.64    in
    2.65      mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms)
    2.66    end
    2.67 @@ -373,21 +370,21 @@
    2.68      fun mk_exhaustive_closure (free as Free (_, T), term_var) t =
    2.69        if Sign.of_sort thy (T, @{sort enum}) then
    2.70          Const (@{const_name "Quickcheck_Exhaustive.check_all_class.check_all"}, check_allT T)
    2.71 -          $ (HOLogic.split_const (T, @{typ "unit => term"}, @{typ "term list option"}) 
    2.72 +          $ (HOLogic.split_const (T, @{typ "unit => term"}, resultT) 
    2.73              $ lambda free (lambda term_var t))
    2.74        else
    2.75          Const (@{const_name "Quickcheck_Exhaustive.full_exhaustive_class.full_exhaustive"}, full_exhaustiveT T)
    2.76 -          $ (HOLogic.split_const (T, @{typ "unit => term"}, @{typ "(bool * term list) option"})
    2.77 +          $ (HOLogic.split_const (T, @{typ "unit => term"}, resultT)
    2.78              $ lambda free (lambda term_var t)) $ depth
    2.79 -    val none_t = @{term "None :: (bool * term list) option"}
    2.80 +    val none_t = Const (@{const_name "None"}, resultT)
    2.81      val mk_if = Quickcheck_Common.mk_safe_if ctxt
    2.82      val mk_test_term = mk_test_term lookup mk_exhaustive_closure mk_if none_t return ctxt
    2.83    in lambda depth (mk_test_term t) end
    2.84  
    2.85  fun mk_parametric_generator_expr mk_generator_expr =
    2.86    Quickcheck_Common.gen_mk_parametric_generator_expr 
    2.87 -    ((mk_generator_expr, absdummy @{typ "code_numeral"} @{term "None :: (bool * term list) option"}),
    2.88 -      @{typ "code_numeral => (bool * term list) option"})
    2.89 +    ((mk_generator_expr, absdummy @{typ "code_numeral"} (Const (@{const_name "None"}, resultT))),
    2.90 +      @{typ "code_numeral"} --> resultT)
    2.91  
    2.92  fun mk_validator_expr ctxt t =
    2.93    let