src/Tools/quickcheck.ML

   val map_test_params : (typ list * expectation -> typ list * expectation)
     -> Context.generic -> Context.generic
   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
      {counterexample : (string * term) list option,
       evaluation_terms : (term * term) list option,
       timings : (string * int) list,
       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:
     Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list  
       -> result list

     (merge (op =) (default_type1, default_type2), merge_expectation (expect1, expect2));
 
 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));
 );
 
 val test_params_of = snd o Data.get o Context.Proof;
 

 
 val expect = snd o dest_test_params o test_params_of
 
 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 =);
 
 val add_batch_validator = Data.map o apfst o apsnd o apsnd o AList.update (op =);
 

         | SOME tester => SOME tester
       end
   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 =
   let

     val check_goals = case some_locale
      of NONE => [(proto_goal, eval_terms)]
       | SOME locale =>
         map (fn (_, phi) => (Morphism.term phi proto_goal, map (Morphism.term phi) eval_terms))
           (Locale.registrations_of (Context.Theory thy) (*FIXME*) locale);
-  in
-    test_goal_terms lthy (time_limit, is_interactive) insts check_goals
+    val test_goals = the_default test_goal_terms (lookup_tester lthy (Config.get lthy tester))
+  in
+    test_goals lthy (time_limit, is_interactive) insts check_goals
   end
 
 (* pretty printing *)
 
 fun tool_name auto = (if auto then "Auto " else "") ^ "Quickcheck"

 fun read_expectation "no_expectation" = No_Expectation
   | read_expectation "no_counterexample" = No_Counterexample
   | 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
     Config.put_generic tester name genctxt
   else