src/Tools/quickcheck.ML

--- a/src/Tools/quickcheck.ML	Tue May 31 11:21:47 2011 +0200
+++ b/src/Tools/quickcheck.ML	Tue May 31 15:45:24 2011 +0200
@@ -31,16 +31,6 @@
   datatype report = Report of
     { iterations : int, raised_match_errors : int,
       satisfied_assms : int list, positive_concl_tests : int }
-  (* registering generators *)
-  val add_generator:
-    string * (Proof.context -> (term * term list) list -> int list -> term list option * report option)
-      -> Context.generic -> Context.generic
-  val add_batch_generator:
-    string * (Proof.context -> term list -> (int -> term list option) list)
-      -> Context.generic -> Context.generic
-  val add_batch_validator:
-    string * (Proof.context -> term list -> (int -> bool) list)
-      -> Context.generic -> Context.generic
   (* quickcheck's result *)
   datatype result =
     Result of
@@ -50,6 +40,19 @@
       reports : (int * report) list}
   val counterexample_of : result -> (string * term) list option
   val timings_of : result -> (string * int) list
+  (* registering generators *)
+  val add_generator:
+    string * (Proof.context -> (term * term list) list -> int list -> term list option * report option)
+      -> Context.generic -> Context.generic
+  val add_tester:
+    string * (Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list -> result list)
+      -> Context.generic -> Context.generic
+  val add_batch_generator:
+    string * (Proof.context -> term list -> (int -> term list option) list)
+      -> Context.generic -> Context.generic
+  val add_batch_validator:
+    string * (Proof.context -> term list -> (int -> bool) list)
+      -> Context.generic -> Context.generic
   (* testing terms and proof states *)
   val test_term: Proof.context -> bool * bool -> term * term list -> result
   val test_goal_terms:
@@ -174,17 +177,19 @@
 structure Data = Generic_Data
 (
   type T =
-    ((string * (Proof.context -> (term * term list) list -> int list -> term list option * report option)) list
+    (((string * (Proof.context -> (term * term list) list -> int list -> term list option * report option)) list
+      * (string * (Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list -> result list)) list)
       * ((string * (Proof.context -> term list -> (int -> term list option) list)) list
       * ((string * (Proof.context -> term list -> (int -> bool) list)) list)))
       * test_params;
-  val empty = (([], ([], [])), Test_Params {default_type = [], expect = No_Expectation});
+  val empty = ((([], []), ([], [])), Test_Params {default_type = [], expect = No_Expectation});
   val extend = I;
-  fun merge (((generators1, (batch_generators1, batch_validators1)), params1),
-    ((generators2, (batch_generators2, batch_validators2)), params2)) : T =
-    ((AList.merge (op =) (K true) (generators1, generators2),
-     (AList.merge (op =) (K true) (batch_generators1, batch_generators2),
-      AList.merge (op =) (K true) (batch_validators1, batch_validators2))),
+  fun merge ((((generators1, testers1), (batch_generators1, batch_validators1)), params1),
+    (((generators2, testers2), (batch_generators2, batch_validators2)), params2)) : T =
+    (((AList.merge (op =) (K true) (generators1, generators2),
+       AList.merge (op =) (K true) (testers1, testers2)),
+      (AList.merge (op =) (K true) (batch_generators1, batch_generators2),
+       AList.merge (op =) (K true) (batch_validators1, batch_validators2))),
       merge_test_params (params1, params2));
 );
 
@@ -196,7 +201,9 @@
 
 val map_test_params = Data.map o apsnd o map_test_params'
 
-val add_generator = Data.map o apfst o apfst o AList.update (op =);
+val add_generator = Data.map o apfst o apfst o apfst o AList.update (op =);
+
+val add_tester = Data.map o apfst o apfst o apsnd o AList.update (op =);
 
 val add_batch_generator = Data.map o apfst o apsnd o apfst o AList.update (op =);
 
@@ -223,12 +230,15 @@
   end
 
 val mk_tester =
-  gen_mk_tester (fn ctxt => AList.lookup (op =) ((fst o fst o Data.get o Context.Proof) ctxt))
+  gen_mk_tester (fn ctxt => AList.lookup (op =) ((fst o fst o fst o Data.get o Context.Proof) ctxt))
 val mk_batch_tester =
   gen_mk_tester (fn ctxt => AList.lookup (op =) ((fst o snd o fst o Data.get o Context.Proof) ctxt))
 val mk_batch_validator =
   gen_mk_tester (fn ctxt => AList.lookup (op =) ((snd o snd o fst o Data.get o Context.Proof) ctxt))
 
+  
+fun lookup_tester ctxt = AList.lookup (op =) ((snd o fst o fst o Data.get o Context.Proof) ctxt)
+
 (* testing propositions *)
 
 fun check_test_term t =
@@ -470,8 +480,9 @@
       | SOME locale =>
         map (fn (_, phi) => (Morphism.term phi proto_goal, map (Morphism.term phi) eval_terms))
           (Locale.registrations_of (Context.Theory thy) (*FIXME*) locale);
+    val test_goals = the_default test_goal_terms (lookup_tester lthy (Config.get lthy tester))
   in
-    test_goal_terms lthy (time_limit, is_interactive) insts check_goals
+    test_goals lthy (time_limit, is_interactive) insts check_goals
   end
 
 (* pretty printing *)
@@ -544,7 +555,7 @@
   | read_expectation "counterexample" = Counterexample
   | read_expectation s = error ("Not an expectation value: " ^ s)
 
-fun valid_tester_name genctxt = AList.defined (op =) (fst (fst (Data.get genctxt)))
+fun valid_tester_name genctxt = AList.defined (op =) (fst (fst (fst (Data.get genctxt))))
 
 fun parse_tester name genctxt =
   if valid_tester_name genctxt name then