# HG changeset patch
# User bulwahn
# Date 1322774075 -3600
# Node ID 8979b2463fc8938054e9ee7e58bf2b39912309dd
# Parent  b4e7b9968e60dfefa1363b9f857edb98faf20827
quickcheck random can also find potential counterexamples;
moved catch_match definition;
split quickcheck setup;

diff -r b4e7b9968e60 -r 8979b2463fc8 src/HOL/Quickcheck.thy
--- a/src/HOL/Quickcheck.thy	Thu Dec 01 20:54:48 2011 +0100
+++ b/src/HOL/Quickcheck.thy	Thu Dec 01 22:14:35 2011 +0100
@@ -5,13 +5,23 @@
 theory Quickcheck
 imports Random Code_Evaluation Enum
 uses
-  "Tools/Quickcheck/quickcheck_common.ML"
+  ("Tools/Quickcheck/quickcheck_common.ML")
   ("Tools/Quickcheck/random_generators.ML")
 begin
 
 notation fcomp (infixl "\<circ>>" 60)
 notation scomp (infixl "\<circ>\<rightarrow>" 60)
 
+setup {* Code_Target.extend_target ("Quickcheck", (Code_Runtime.target, K I)) *}
+
+subsection {* Catching Match exceptions *}
+
+definition catch_match :: "term list option => term list option => term list option"
+where
+  [code del]: "catch_match t1 t2 = (SOME t. t = t1 \<or> t = t2)"
+
+code_const catch_match 
+  (Quickcheck "(_) handle Match => _")
 
 subsection {* The @{text random} class *}
 
@@ -128,6 +138,9 @@
   shows "random_aux k = rhs k"
   using assms by (rule code_numeral.induct)
 
+subsection {* Deriving random generators for datatypes *}
+
+use "Tools/Quickcheck/quickcheck_common.ML" 
 use "Tools/Quickcheck/random_generators.ML"
 setup Random_Generators.setup
 
diff -r b4e7b9968e60 -r 8979b2463fc8 src/HOL/Quickcheck_Exhaustive.thy
--- a/src/HOL/Quickcheck_Exhaustive.thy	Thu Dec 01 20:54:48 2011 +0100
+++ b/src/HOL/Quickcheck_Exhaustive.thy	Thu Dec 01 22:14:35 2011 +0100
@@ -523,13 +523,6 @@
 
 subsection {* Defining combinators for any first-order data type *}
 
-definition catch_match :: "term list option => term list option => term list option"
-where
-  [code del]: "catch_match t1 t2 = (SOME t. t = t1 \<or> t = t2)"
-
-code_const catch_match 
-  (Quickcheck "(_) handle Match => _")
-
 definition catch_match' :: "term => term => term"
 where
   [code del]: "catch_match' t1 t2 = (SOME t. t = t1 \<or> t = t2)"
diff -r b4e7b9968e60 -r 8979b2463fc8 src/HOL/Tools/Quickcheck/exhaustive_generators.ML
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Thu Dec 01 20:54:48 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Thu Dec 01 22:14:35 2011 +0100
@@ -328,12 +328,6 @@
 
 fun mk_unknown_term T = HOLogic.reflect_term (Const ("Quickcheck_Exhaustive.unknown", T))
 
-fun mk_safe_if ctxt (cond, then_t, else_t) =
-  @{term "Quickcheck_Exhaustive.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"});  
-
 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)    
 
@@ -352,7 +346,8 @@
       Const (@{const_name "Quickcheck_Exhaustive.exhaustive_class.exhaustive"}, exhaustiveT T)
         $ lambda free t $ depth
     val none_t = @{term "None :: term list option"}
-    val mk_test_term = mk_test_term lookup mk_exhaustive_closure (mk_safe_if ctxt) none_t return ctxt
+    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_full_generator_expr ctxt (t, eval_terms) =
@@ -378,7 +373,8 @@
           $ (HOLogic.split_const (T, @{typ "unit => term"}, @{typ "term list option"})
             $ lambda free (lambda term_var t)) $ depth
     val none_t = @{term "None :: term list option"}
-    val mk_test_term = mk_test_term lookup mk_exhaustive_closure (mk_safe_if ctxt) none_t return ctxt
+    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 =
diff -r b4e7b9968e60 -r 8979b2463fc8 src/HOL/Tools/Quickcheck/quickcheck_common.ML
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Thu Dec 01 20:54:48 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Thu Dec 01 22:14:35 2011 +0100
@@ -13,6 +13,7 @@
     -> (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 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
@@ -265,6 +266,14 @@
     correct_inst_goals
   end
 
+(* 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"});  
+
 fun collect_results f [] results = results
   | collect_results f (t :: ts) results =
     let
diff -r b4e7b9968e60 -r 8979b2463fc8 src/HOL/Tools/Quickcheck/random_generators.ML
--- a/src/HOL/Tools/Quickcheck/random_generators.ML	Thu Dec 01 20:54:48 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Thu Dec 01 22:14:35 2011 +0100
@@ -297,8 +297,8 @@
       (2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) Ts;
     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 = @{term "If :: bool => term list option => term list option => term list option"}
-      $ result $ @{term "None :: term list option"} $ (@{term "Some :: term list => term list option"} $ terms);
+    val check = Quickcheck_Common.mk_safe_if ctxt (result, @{term "None :: term list option"},
+      @{term "Some :: term list => term list option"} $ 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"});
@@ -446,7 +446,6 @@
 val setup =
   Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
     (((@{sort typerep}, @{sort term_of}), @{sort random}), instantiate_random_datatype))
-  #> Code_Target.extend_target (target, (Code_Runtime.target, K I))
   #> Context.theory_map (Quickcheck.add_tester ("random", (active, test_goals)));
 
 end;