# HG changeset patch
# User bulwahn
# Date 1322774075 -3600
# Node ID d1fb55c2ed65223be094cd8832785d480ed8a809
# Parent  d8fbd3fa0375c30afc82395294800ffdb330cae5
quickcheck's compilation returns if it is genuine counterexample or a counterexample due to a match exception

diff -r d8fbd3fa0375 -r d1fb55c2ed65 src/HOL/Quickcheck.thy
--- a/src/HOL/Quickcheck.thy	Thu Dec 01 22:14:35 2011 +0100
+++ b/src/HOL/Quickcheck.thy	Thu Dec 01 22:14:35 2011 +0100
@@ -16,7 +16,7 @@
 
 subsection {* Catching Match exceptions *}
 
-definition catch_match :: "term list option => term list option => term list option"
+definition catch_match :: "(bool * term list) option => (bool * term list) option => (bool * term list) option"
 where
   [code del]: "catch_match t1 t2 = (SOME t. t = t1 \<or> t = t2)"
 
diff -r d8fbd3fa0375 -r d1fb55c2ed65 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
@@ -7,10 +7,10 @@
 signature EXHAUSTIVE_GENERATORS =
 sig
   val compile_generator_expr:
-    Proof.context -> (term * term list) list -> int list -> term list option * Quickcheck.report option
+    Proof.context -> (term * term list) list -> int list -> (bool * term list) option * Quickcheck.report option
   val compile_generator_exprs: Proof.context -> term list -> (int -> term list option) list
   val compile_validator_exprs: Proof.context -> term list -> (int -> bool) list
-  val put_counterexample: (unit -> int -> int -> term list option)
+  val put_counterexample: (unit -> int -> int -> (bool * term list) option)
     -> Proof.context -> Proof.context
   val put_counterexample_batch: (unit -> (int -> term list option) list)
     -> Proof.context -> Proof.context
@@ -72,7 +72,12 @@
 
 fun mk_unit_let (x, y) =
   Const (@{const_name "Let"}, @{typ "unit => (unit => unit) => unit"}) $ x $ absdummy @{typ unit} y
-  
+
+fun mk_if (b, t, e) =
+  let
+    val T = fastype_of t
+  in Const (@{const_name "HOL.If"}, @{typ bool} --> T --> T --> T) $ b $ t $ e end
+
 (* handling inductive datatypes *)
 
 (** constructing generator instances **)
@@ -94,8 +99,8 @@
 
 fun bounded_forallT T = (T --> @{typ bool}) --> @{typ code_numeral} --> @{typ bool}
 
-fun full_exhaustiveT T = (termifyT T --> @{typ "Code_Evaluation.term list option"})
-  --> @{typ code_numeral} --> @{typ "Code_Evaluation.term list option"}
+fun full_exhaustiveT T = (termifyT T --> @{typ "(bool * Code_Evaluation.term list) option"})
+  --> @{typ code_numeral} --> @{typ "(bool * Code_Evaluation.term list) option"}
 
 fun check_allT T = (termifyT T --> @{typ "Code_Evaluation.term list option"})
   --> @{typ "Code_Evaluation.term list option"}
@@ -155,8 +160,7 @@
     val mk_aux_call = gen_mk_aux_call functerms
     val mk_consexpr = gen_mk_consexpr test_function functerms
     fun mk_rhs exprs =
-      @{term "If :: bool => term list option => term list option => term list option"}
-          $ size_ge_zero $ (foldr1 mk_none_continuation exprs) $ @{term "None :: term list option"}
+      mk_if (size_ge_zero, foldr1 mk_none_continuation exprs, @{term "None :: term list option"})
   in
     mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms)
   end
@@ -170,23 +174,23 @@
     val mk_aux_call = gen_mk_aux_call functerms
     val mk_consexpr = gen_mk_consexpr test_function functerms
     fun mk_rhs exprs =
-      @{term "If :: bool => bool => bool => bool"} $ size_ge_zero $
-        (foldr1 HOLogic.mk_conj exprs) $ @{term "True"}
+      mk_if (size_ge_zero, foldr1 HOLogic.mk_conj exprs, @{term "True"})
   in
     mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms)
   end
   
 fun mk_full_equations functerms =
   let
-    fun test_function T = Free ("f", termifyT T --> @{typ "term list option"})
+    fun test_function T = Free ("f", termifyT T --> @{typ "(bool * term list) option"})
     fun mk_call T =
       let
         val full_exhaustive =
           Const (@{const_name "Quickcheck_Exhaustive.full_exhaustive_class.full_exhaustive"},
             full_exhaustiveT T)
-      in
+      in                                   
         (T, fn t => full_exhaustive $
-          (HOLogic.split_const (T, @{typ "unit => Code_Evaluation.term"}, @{typ "Code_Evaluation.term list option"})
+          (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)
       end
     fun mk_aux_call fTs (k, _) (tyco, Ts) =
@@ -195,7 +199,8 @@
         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 "Code_Evaluation.term list option"})
+          (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)
       end
     fun mk_consexpr simpleT (c, xs) =
@@ -213,8 +218,8 @@
           $ (list_comb (constr, bounds)) $ absdummy @{typ unit} term)
       in fold_rev (fn f => fn t => f t) fns start_term end
     fun mk_rhs exprs =
-        @{term "If :: bool => term list option => term list option => term list option"}
-            $ size_ge_zero $ (foldr1 mk_none_continuation exprs) $ @{term "None :: term list option"}
+      mk_if (size_ge_zero, foldr1 mk_none_continuation exprs,
+        @{term "None :: (bool * term list) option"})
   in
     mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms)
   end
@@ -287,8 +292,9 @@
 fun mk_test_term lookup mk_closure mk_if none_t return ctxt =
   let
     fun mk_naive_test_term t =
-      fold_rev mk_closure (map lookup (Term.add_free_names t [])) (mk_if (t, none_t, return))
-    fun mk_smart_test_term' concl bound_vars assms =
+      fold_rev mk_closure (map lookup (Term.add_free_names t []))
+        (mk_if (t, none_t, return))
+    fun mk_smart_test_term' concl bound_vars assms genuine =
       let
         fun vars_of t = subtract (op =) bound_vars (Term.add_free_names t [])
         val (vars, check) =
@@ -299,7 +305,7 @@
         fold_rev mk_closure (map lookup vars) (mk_if check)
       end
     val mk_smart_test_term =
-      Quickcheck_Common.strip_imp #> (fn (assms, concl) => mk_smart_test_term' concl [] assms)
+      Quickcheck_Common.strip_imp #> (fn (assms, concl) => mk_smart_test_term' concl [] assms true)
   in
     if Config.get ctxt smart_quantifier then mk_smart_test_term else mk_naive_test_term 
   end
@@ -313,7 +319,7 @@
     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})
-    val return = @{term "throw_Counterexample :: term list => unit"} $
+    fun return _ = @{term "throw_Counterexample :: term list => unit"} $
       (HOLogic.mk_list @{typ "term"}
         (map (fn t => HOLogic.mk_term_of (fastype_of t) t) (frees @ eval_terms)))
     fun mk_exhaustive_closure (free as Free (_, T)) t =
@@ -321,8 +327,7 @@
         fast_exhaustiveT T)
         $ lambda free t $ depth
     val none_t = @{term "()"}
-    fun mk_safe_if (cond, then_t, else_t) =
-      @{term "If :: bool => unit => unit => unit"} $ cond $ then_t $ else_t
+    fun mk_safe_if (cond, then_t, else_t) = mk_if (cond, then_t, else_t true)
     val mk_test_term = mk_test_term lookup mk_exhaustive_closure mk_safe_if none_t return ctxt 
   in lambda depth (@{term "catch_Counterexample :: unit => term list option"} $ mk_test_term t) end
 
@@ -340,7 +345,7 @@
     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})
-    val return = @{term "Some :: term list => term list option"} $ (HOLogic.mk_list @{typ "term"}
+    fun return _ = @{term "Some :: term list => term list option"} $ (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)
@@ -361,8 +366,10 @@
     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)
-    val return = @{term "Some :: term list => term list option"} $ (HOLogic.mk_list @{typ term}
-      (map (fn v => v $ @{term "()"}) term_vars @ map mk_safe_term eval_terms))
+    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)))
     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)
@@ -370,17 +377,17 @@
             $ 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 "term list option"})
+          $ (HOLogic.split_const (T, @{typ "unit => term"}, @{typ "(bool * term list) option"})
             $ lambda free (lambda term_var t)) $ depth
-    val none_t = @{term "None :: term list option"}
+    val none_t = @{term "None :: (bool * term list) option"}
     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 :: term list option"}),
-      @{typ "code_numeral => term list option"})
+    ((mk_generator_expr, absdummy @{typ "code_numeral"} @{term "None :: (bool * term list) option"}),
+      @{typ "code_numeral => (bool * term list) option"})
 
 fun mk_validator_expr ctxt t =
   let
@@ -395,9 +402,9 @@
     fun mk_bounded_forall (Free (s, T)) t =
       Const (@{const_name "Quickcheck_Exhaustive.bounded_forall_class.bounded_forall"}, bounded_forallT T)
         $ lambda (Free (s, T)) t $ depth
-    fun mk_if (cond, then_t, else_t) =
-      @{term "If :: bool => bool => bool => bool"} $ cond $ then_t $ else_t
-    val mk_test_term = mk_test_term lookup mk_bounded_forall mk_if @{term True} @{term False} ctxt
+    fun mk_safe_if (cond, then_t, else_t) = mk_if (cond, then_t, else_t true)
+    val mk_test_term =
+      mk_test_term lookup mk_bounded_forall mk_safe_if @{term True} (K @{term False}) ctxt
   in lambda depth (mk_test_term t) end
 
 
@@ -418,7 +425,7 @@
 
 structure Counterexample = Proof_Data
 (
-  type T = unit -> int -> int -> term list option
+  type T = unit -> int -> int -> (bool * term list) option
   (* FIXME avoid user error with non-user text *)
   fun init _ () = error "Counterexample"
 );
@@ -454,11 +461,11 @@
     val compile = Code_Runtime.dynamic_value_strict
       (Counterexample.get, put_counterexample, "Exhaustive_Generators.put_counterexample")
       thy (SOME target) (fn proc => fn g =>
-        fn card => fn size => g card size |> (Option.map o map) proc) t' []
+        fn card => fn size => g card size |> (Option.map o apsnd o map) proc) t' []
   in
     fn [card, size] => rpair NONE (compile card size |> 
       (if Config.get ctxt quickcheck_pretty then
-        Option.map (map Quickcheck_Common.post_process_term) else I))
+        Option.map (apsnd (map Quickcheck_Common.post_process_term)) else I))
   end;
 
 fun compile_generator_exprs ctxt ts =
@@ -485,7 +492,8 @@
       thy (SOME target) (K I) (HOLogic.mk_list @{typ "code_numeral => bool"} ts') []
   end;
 
-val test_goals = Quickcheck_Common.generator_test_goal_terms ("exhaustive", compile_generator_expr);
+val test_goals = Quickcheck_Common.generator_test_goal_terms ("exhaustive",
+  apfst (Option.map snd) ooo compile_generator_expr);
   
 (* setup *)
 
diff -r d8fbd3fa0375 -r d1fb55c2ed65 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
@@ -7,13 +7,14 @@
 signature QUICKCHECK_COMMON =
 sig
   val strip_imp : term -> (term list * term)
+  val reflect_bool : bool -> term
   val define_functions : ((term list -> term list) * (Proof.context -> tactic) option)
     -> string -> string list -> string list -> typ list -> Proof.context -> Proof.context 
   val perhaps_constrain: theory -> (typ * sort) list -> (string * sort) list
     -> (string * sort -> string * sort) option
   val instantiate_goals: Proof.context -> (string * typ) list -> (term * term list) list
     -> (typ option * (term * term list)) list list
-  val mk_safe_if : Proof.context -> (term * term * term) -> term
+  val mk_safe_if : Proof.context -> term * term * (bool -> term) -> term
   val collect_results : ('a -> Quickcheck.result) -> 'a list -> Quickcheck.result list -> Quickcheck.result list
   type compile_generator =
     Proof.context -> (term * term list) list -> int list -> term list option * Quickcheck.report option
@@ -45,6 +46,8 @@
 fun strip_imp (Const(@{const_name HOL.implies},_) $ A $ B) = apfst (cons A) (strip_imp B)
   | strip_imp A = ([], A)
 
+fun reflect_bool b = if b then @{term "True"} else @{term "False"}
+
 fun mk_undefined T = Const(@{const_name undefined}, T)
 
 (* testing functions: testing with increasing sizes (and cardinalities) *)
@@ -142,7 +145,6 @@
       [comp_time, exec_time])
   end
 
-
 fun test_term_with_cardinality (name, compile) ctxt catch_code_errors ts =
   let
     val thy = Proof_Context.theory_of ctxt
@@ -269,10 +271,10 @@
 (* compilation of testing functions *)
 
 fun mk_safe_if ctxt (cond, then_t, else_t) =
-  @{term "Quickcheck.catch_match :: term list option => term list option => term list option"}
-    $ (@{term "If :: bool => term list option => term list option => term list option"}
-      $ cond $ then_t $ else_t)
-    $ (if Config.get ctxt Quickcheck.potential then else_t else @{term "None :: term list option"});  
+  @{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"});  
 
 fun collect_results f [] results = results
   | collect_results f (t :: ts) results =
@@ -379,8 +381,8 @@
 fun gen_mk_parametric_generator_expr ((mk_generator_expr, out_of_bounds), T) ctxt ts =
   let
     val if_t = Const (@{const_name "If"}, @{typ bool} --> T --> T --> T)
-    fun mk_if (index, (t, eval_terms)) else_t =
-      if_t $ (HOLogic.eq_const @{typ code_numeral} $ Bound 0 $ HOLogic.mk_number @{typ code_numeral} index) $
+    fun mk_if (index, (t, eval_terms)) else_t = if_t $
+        (HOLogic.eq_const @{typ code_numeral} $ Bound 0 $ HOLogic.mk_number @{typ code_numeral} index) $
         (mk_generator_expr ctxt (t, eval_terms)) $ else_t
   in
     absdummy @{typ "code_numeral"} (fold_rev mk_if (1 upto (length ts) ~~ ts) out_of_bounds)
diff -r d8fbd3fa0375 -r d1fb55c2ed65 src/HOL/Tools/Quickcheck/random_generators.ML
--- a/src/HOL/Tools/Quickcheck/random_generators.ML	Thu Dec 01 22:14:35 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Thu Dec 01 22:14:35 2011 +0100
@@ -31,6 +31,7 @@
 val seed = @{term "s::Random.seed"};
 
 
+
 (** typ "'a => 'b" **)
 
 type seed = Random_Engine.seed;
@@ -298,7 +299,8 @@
     val result = list_comb (prop, map (fn (i, _, _, _) => Bound i) bounds);
     val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds);
     val check = Quickcheck_Common.mk_safe_if ctxt (result, @{term "None :: term list option"},
-      @{term "Some :: term list => term list option"} $ terms)
+      fn genuine => @{term "Some :: bool * term list => (bool * term list) option"} $
+        HOLogic.mk_prod (Quickcheck_Common.reflect_bool genuine, terms))
     val return = @{term "Pair :: term list option => Random.seed => term list option * Random.seed"};
     fun liftT T sT = sT --> HOLogic.mk_prodT (T, sT);
     fun mk_termtyp T = HOLogic.mk_prodT (T, @{typ "unit => term"});