# HG changeset patch
# User bulwahn
# Date 1322774075 -3600
# Node ID 1f5fc44254d73c8d4efed8edfc313f19f04a1880
# Parent  75691bcc2c0f2bf367fd4c90502480f0f283b65d
the simple exhaustive compilation also indicates if counterexample is potentially spurious;

diff -r 75691bcc2c0f -r 1f5fc44254d7 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
@@ -16,7 +16,7 @@
 subsection {* exhaustive generator type classes *}
 
 class exhaustive = term_of +
-  fixes exhaustive :: "('a \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
+  fixes exhaustive :: "('a \<Rightarrow> (bool * term list) option) \<Rightarrow> code_numeral \<Rightarrow> (bool * term list) option"
   
 class full_exhaustive = term_of +
   fixes full_exhaustive :: "('a * (unit => term) \<Rightarrow> (bool * term list) option) \<Rightarrow> code_numeral \<Rightarrow> (bool * term list) option"
@@ -42,7 +42,7 @@
 instantiation code_numeral :: exhaustive
 begin
 
-function exhaustive_code_numeral' :: "(code_numeral => term list option) => code_numeral => code_numeral => term list option"
+function exhaustive_code_numeral' :: "(code_numeral => (bool * term list) option) => code_numeral => code_numeral => (bool * term list) option"
   where "exhaustive_code_numeral' f d i =
     (if d < i then None
     else (f i orelse exhaustive_code_numeral' f d (i + 1)))"
@@ -78,7 +78,7 @@
 instantiation int :: exhaustive
 begin
 
-function exhaustive' :: "(int => term list option) => int => int => term list option"
+function exhaustive' :: "(int => (bool * term list) option) => int => int => (bool * term list) option"
   where "exhaustive' f d i = (if d < i then None else (f i orelse exhaustive' f d (i + 1)))"
 by pat_completeness auto
 
@@ -136,14 +136,14 @@
 instantiation "fun" :: ("{equal, exhaustive}", exhaustive) exhaustive
 begin
 
-fun exhaustive_fun' :: "(('a => 'b) => term list option) => code_numeral => code_numeral => term list option"
+fun exhaustive_fun' :: "(('a => 'b) => (bool * term list) option) => code_numeral => code_numeral => (bool * term list) option"
 where
   "exhaustive_fun' f i d = (exhaustive (%b. f (%_. b)) d)
    orelse (if i > 1 then
      exhaustive_fun' (%g. exhaustive (%a. exhaustive (%b.
        f (g(a := b))) d) d) (i - 1) d else None)"
 
-definition exhaustive_fun :: "(('a => 'b) => term list option) => code_numeral => term list option"
+definition exhaustive_fun :: "(('a => 'b) => (bool * term list) option) => code_numeral => (bool * term list) option"
 where
   "exhaustive_fun f d = exhaustive_fun' f d d" 
 
diff -r 75691bcc2c0f -r 1f5fc44254d7 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
@@ -96,8 +96,7 @@
 fun fast_exhaustiveT T = (T --> @{typ unit})
   --> @{typ code_numeral} --> @{typ unit}
 
-fun exhaustiveT T = (T --> @{typ "Code_Evaluation.term list option"})
-  --> @{typ code_numeral} --> @{typ "Code_Evaluation.term list option"}
+fun exhaustiveT T = (T --> resultT) --> @{typ code_numeral} --> resultT
 
 fun bounded_forallT T = (T --> @{typ bool}) --> @{typ code_numeral} --> @{typ bool}
 
@@ -154,13 +153,13 @@
 
 fun mk_equations functerms =
   let
-    fun test_function T = Free ("f", T --> @{typ "term list option"})
+    fun test_function T = Free ("f", T --> resultT)
     val mk_call = gen_mk_call (fn T =>
       Const (@{const_name "Quickcheck_Exhaustive.exhaustive_class.exhaustive"}, exhaustiveT T))
     val mk_aux_call = gen_mk_aux_call functerms
     val mk_consexpr = gen_mk_consexpr test_function functerms
     fun mk_rhs exprs =
-      mk_if (size_ge_zero, foldr1 mk_none_continuation exprs, @{term "None :: term list option"})
+      mk_if (size_ge_zero, foldr1 mk_none_continuation exprs, Const (@{const_name "None"}, resultT))
   in
     mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms)
   end
@@ -333,6 +332,9 @@
 fun mk_safe_term t = @{term "Quickcheck_Exhaustive.catch_match' :: term => term => term"}
       $ (HOLogic.mk_term_of (fastype_of t) t) $ mk_unknown_term (fastype_of t)    
 
+fun mk_return t genuine = @{term "Some :: bool * term list => (bool * term list) option"} $
+  (HOLogic.pair_const @{typ bool} @{typ "term list"} $ Quickcheck_Common.reflect_bool genuine $ t)
+
 fun mk_generator_expr ctxt (t, eval_terms) =
   let
     val thy = Proof_Context.theory_of ctxt
@@ -342,12 +344,12 @@
     fun lookup v = the (AList.lookup (op =) (names ~~ frees) v)
     val ([depth_name], ctxt'') = Variable.variant_fixes ["depth"] ctxt'
     val depth = Free (depth_name, @{typ code_numeral})
-    fun return _ = @{term "Some :: term list => term list option"} $ (HOLogic.mk_list @{typ "term"}
+    val return = mk_return (HOLogic.mk_list @{typ "term"}
         (map (fn t => HOLogic.mk_term_of (fastype_of t) t) frees @ map mk_safe_term eval_terms))
     fun mk_exhaustive_closure (free as Free (_, T)) t =
       Const (@{const_name "Quickcheck_Exhaustive.exhaustive_class.exhaustive"}, exhaustiveT T)
         $ lambda free t $ depth
-    val none_t = @{term "None :: 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
@@ -363,10 +365,8 @@
     val depth = Free (depth_name, @{typ code_numeral})
     val term_vars = map (fn n => Free (n, @{typ "unit => term"})) term_names
     fun lookup v = the (AList.lookup (op =) (names ~~ (frees ~~ term_vars)) v)
-    fun return genuine = @{term "Some :: bool * term list => (bool * term list) option"} $
-      (HOLogic.pair_const @{typ bool} @{typ "term list"} $ Quickcheck_Common.reflect_bool genuine $
-        (HOLogic.mk_list @{typ term}
-          (map (fn v => v $ @{term "()"}) term_vars @ map mk_safe_term eval_terms)))
+    val return = mk_return (HOLogic.mk_list @{typ term}
+          (map (fn v => v $ @{term "()"}) term_vars @ map mk_safe_term eval_terms))
     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)
diff -r 75691bcc2c0f -r 1f5fc44254d7 src/HOL/Tools/Quickcheck/quickcheck_common.ML
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Thu Dec 01 22:14:35 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Thu Dec 01 22:14:35 2011 +0100
@@ -274,7 +274,7 @@
   @{term "Quickcheck.catch_match :: (bool * term list) option => (bool * term list) option => (bool * term list) option"}
     $ (@{term "If :: bool => (bool * term list) option => (bool * term list) option => (bool * term list) option"}
       $ cond $ then_t $ else_t true)
-    $ (if Config.get ctxt Quickcheck.potential then else_t false else @{term "None :: term list option"});  
+    $ (if Config.get ctxt Quickcheck.potential then else_t false else @{term "None :: (bool * term list) option"});
 
 fun collect_results f [] results = results
   | collect_results f (t :: ts) results =