the simple exhaustive compilation also indicates if counterexample is potentially spurious;
authorbulwahn
Thu Dec 01 22:14:35 2011 +0100 (2011-12-01)
changeset 457241f5fc44254d7
parent 45723 75691bcc2c0f
child 45725 2987b29518aa
the simple exhaustive compilation also indicates if counterexample is potentially spurious;
src/HOL/Quickcheck_Exhaustive.thy
src/HOL/Tools/Quickcheck/exhaustive_generators.ML
src/HOL/Tools/Quickcheck/quickcheck_common.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 @@ -16,7 +16,7 @@
     1.4  subsection {* exhaustive generator type classes *}
     1.5  
     1.6  class exhaustive = term_of +
     1.7 -  fixes exhaustive :: "('a \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
     1.8 +  fixes exhaustive :: "('a \<Rightarrow> (bool * term list) option) \<Rightarrow> code_numeral \<Rightarrow> (bool * term list) option"
     1.9    
    1.10  class full_exhaustive = term_of +
    1.11    fixes full_exhaustive :: "('a * (unit => term) \<Rightarrow> (bool * term list) option) \<Rightarrow> code_numeral \<Rightarrow> (bool * term list) option"
    1.12 @@ -42,7 +42,7 @@
    1.13  instantiation code_numeral :: exhaustive
    1.14  begin
    1.15  
    1.16 -function exhaustive_code_numeral' :: "(code_numeral => term list option) => code_numeral => code_numeral => term list option"
    1.17 +function exhaustive_code_numeral' :: "(code_numeral => (bool * term list) option) => code_numeral => code_numeral => (bool * term list) option"
    1.18    where "exhaustive_code_numeral' f d i =
    1.19      (if d < i then None
    1.20      else (f i orelse exhaustive_code_numeral' f d (i + 1)))"
    1.21 @@ -78,7 +78,7 @@
    1.22  instantiation int :: exhaustive
    1.23  begin
    1.24  
    1.25 -function exhaustive' :: "(int => term list option) => int => int => term list option"
    1.26 +function exhaustive' :: "(int => (bool * term list) option) => int => int => (bool * term list) option"
    1.27    where "exhaustive' f d i = (if d < i then None else (f i orelse exhaustive' f d (i + 1)))"
    1.28  by pat_completeness auto
    1.29  
    1.30 @@ -136,14 +136,14 @@
    1.31  instantiation "fun" :: ("{equal, exhaustive}", exhaustive) exhaustive
    1.32  begin
    1.33  
    1.34 -fun exhaustive_fun' :: "(('a => 'b) => term list option) => code_numeral => code_numeral => term list option"
    1.35 +fun exhaustive_fun' :: "(('a => 'b) => (bool * term list) option) => code_numeral => code_numeral => (bool * term list) option"
    1.36  where
    1.37    "exhaustive_fun' f i d = (exhaustive (%b. f (%_. b)) d)
    1.38     orelse (if i > 1 then
    1.39       exhaustive_fun' (%g. exhaustive (%a. exhaustive (%b.
    1.40         f (g(a := b))) d) d) (i - 1) d else None)"
    1.41  
    1.42 -definition exhaustive_fun :: "(('a => 'b) => term list option) => code_numeral => term list option"
    1.43 +definition exhaustive_fun :: "(('a => 'b) => (bool * term list) option) => code_numeral => (bool * term list) option"
    1.44  where
    1.45    "exhaustive_fun f d = exhaustive_fun' f d d" 
    1.46  
     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 @@ -96,8 +96,7 @@
     2.4  fun fast_exhaustiveT T = (T --> @{typ unit})
     2.5    --> @{typ code_numeral} --> @{typ unit}
     2.6  
     2.7 -fun exhaustiveT T = (T --> @{typ "Code_Evaluation.term list option"})
     2.8 -  --> @{typ code_numeral} --> @{typ "Code_Evaluation.term list option"}
     2.9 +fun exhaustiveT T = (T --> resultT) --> @{typ code_numeral} --> resultT
    2.10  
    2.11  fun bounded_forallT T = (T --> @{typ bool}) --> @{typ code_numeral} --> @{typ bool}
    2.12  
    2.13 @@ -154,13 +153,13 @@
    2.14  
    2.15  fun mk_equations functerms =
    2.16    let
    2.17 -    fun test_function T = Free ("f", T --> @{typ "term list option"})
    2.18 +    fun test_function T = Free ("f", T --> resultT)
    2.19      val mk_call = gen_mk_call (fn T =>
    2.20        Const (@{const_name "Quickcheck_Exhaustive.exhaustive_class.exhaustive"}, exhaustiveT T))
    2.21      val mk_aux_call = gen_mk_aux_call functerms
    2.22      val mk_consexpr = gen_mk_consexpr test_function functerms
    2.23      fun mk_rhs exprs =
    2.24 -      mk_if (size_ge_zero, foldr1 mk_none_continuation exprs, @{term "None :: term list option"})
    2.25 +      mk_if (size_ge_zero, foldr1 mk_none_continuation exprs, Const (@{const_name "None"}, resultT))
    2.26    in
    2.27      mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms)
    2.28    end
    2.29 @@ -333,6 +332,9 @@
    2.30  fun mk_safe_term t = @{term "Quickcheck_Exhaustive.catch_match' :: term => term => term"}
    2.31        $ (HOLogic.mk_term_of (fastype_of t) t) $ mk_unknown_term (fastype_of t)    
    2.32  
    2.33 +fun mk_return t genuine = @{term "Some :: bool * term list => (bool * term list) option"} $
    2.34 +  (HOLogic.pair_const @{typ bool} @{typ "term list"} $ Quickcheck_Common.reflect_bool genuine $ t)
    2.35 +
    2.36  fun mk_generator_expr ctxt (t, eval_terms) =
    2.37    let
    2.38      val thy = Proof_Context.theory_of ctxt
    2.39 @@ -342,12 +344,12 @@
    2.40      fun lookup v = the (AList.lookup (op =) (names ~~ frees) v)
    2.41      val ([depth_name], ctxt'') = Variable.variant_fixes ["depth"] ctxt'
    2.42      val depth = Free (depth_name, @{typ code_numeral})
    2.43 -    fun return _ = @{term "Some :: term list => term list option"} $ (HOLogic.mk_list @{typ "term"}
    2.44 +    val return = mk_return (HOLogic.mk_list @{typ "term"}
    2.45          (map (fn t => HOLogic.mk_term_of (fastype_of t) t) frees @ map mk_safe_term eval_terms))
    2.46      fun mk_exhaustive_closure (free as Free (_, T)) t =
    2.47        Const (@{const_name "Quickcheck_Exhaustive.exhaustive_class.exhaustive"}, exhaustiveT T)
    2.48          $ lambda free t $ depth
    2.49 -    val none_t = @{term "None :: term list option"}
    2.50 +    val none_t = Const (@{const_name "None"}, resultT)
    2.51      val mk_if = Quickcheck_Common.mk_safe_if ctxt
    2.52      val mk_test_term = mk_test_term lookup mk_exhaustive_closure mk_if none_t return ctxt
    2.53    in lambda depth (mk_test_term t) end
    2.54 @@ -363,10 +365,8 @@
    2.55      val depth = Free (depth_name, @{typ code_numeral})
    2.56      val term_vars = map (fn n => Free (n, @{typ "unit => term"})) term_names
    2.57      fun lookup v = the (AList.lookup (op =) (names ~~ (frees ~~ term_vars)) v)
    2.58 -    fun return genuine = @{term "Some :: bool * term list => (bool * term list) option"} $
    2.59 -      (HOLogic.pair_const @{typ bool} @{typ "term list"} $ Quickcheck_Common.reflect_bool genuine $
    2.60 -        (HOLogic.mk_list @{typ term}
    2.61 -          (map (fn v => v $ @{term "()"}) term_vars @ map mk_safe_term eval_terms)))
    2.62 +    val return = mk_return (HOLogic.mk_list @{typ term}
    2.63 +          (map (fn v => v $ @{term "()"}) term_vars @ map mk_safe_term eval_terms))
    2.64      fun mk_exhaustive_closure (free as Free (_, T), term_var) t =
    2.65        if Sign.of_sort thy (T, @{sort enum}) then
    2.66          Const (@{const_name "Quickcheck_Exhaustive.check_all_class.check_all"}, check_allT T)
     3.1 --- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Thu Dec 01 22:14:35 2011 +0100
     3.2 +++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Thu Dec 01 22:14:35 2011 +0100
     3.3 @@ -274,7 +274,7 @@
     3.4    @{term "Quickcheck.catch_match :: (bool * term list) option => (bool * term list) option => (bool * term list) option"}
     3.5      $ (@{term "If :: bool => (bool * term list) option => (bool * term list) option => (bool * term list) option"}
     3.6        $ cond $ then_t $ else_t true)
     3.7 -    $ (if Config.get ctxt Quickcheck.potential then else_t false else @{term "None :: term list option"});  
     3.8 +    $ (if Config.get ctxt Quickcheck.potential then else_t false else @{term "None :: (bool * term list) option"});
     3.9  
    3.10  fun collect_results f [] results = results
    3.11    | collect_results f (t :: ts) results =