src/Tools/quickcheck.ML

       -> Context.generic -> Context.generic
   val add_batch_validator:
     string * (Proof.context -> term list -> (int -> bool) list)
       -> Context.generic -> Context.generic
   (* basic operations *)
+  type compile_generator =
+    Proof.context -> (term * term list) list -> int list -> term list option * report option
   val limit : Time.time -> (bool * bool) -> (unit -> 'a) -> (unit -> 'a) -> unit -> 'a  
   val instantiate_goals: Proof.context -> (string * typ) list -> (term * term list) list
     -> (typ option * (term * term list)) list list
   val collect_results: ('a -> result) -> 'a list -> result list -> result list
-  val generator_test_goal_terms: Proof.context -> bool * bool -> (string * typ) list ->
-    (term * term list) list -> result list
+  val generator_test_goal_terms: compile_generator ->
+    Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list -> result list
   (* testing terms and proof states *)
-  val test_term: Proof.context -> bool * bool -> term * term list -> result
+  val test_term: compile_generator -> 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
+    Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list -> result list
   val quickcheck: (string * string list) list -> int -> Proof.state -> (string * term) list option
   (* testing a batch of terms *)
   val test_terms:
     Proof.context -> term list -> (string * term) list option list option * (string * int) list
   val validate_terms: Proof.context -> term list -> bool list option * (string * int) list

       in case Exn.get_res tester of
           NONE => SOME (Exn.release tester)
         | SOME tester => SOME tester
       end
   end
-
+(*
 val mk_tester =
   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 *)
+
+type compile_generator =
+  Proof.context -> (term * term list) list -> int list -> term list option * report option
 
 fun check_test_term t =
   let
     val _ = (null (Term.add_tvars t []) andalso null (Term.add_tfrees t [])) orelse
       error "Term to be tested contains type variables";

     handle TimeLimit.TimeOut =>
       if is_interactive then exc () else raise TimeLimit.TimeOut
   else
     f ()
 
-fun test_term ctxt (limit_time, is_interactive) (t, eval_terms) =
+fun test_term compile ctxt (limit_time, is_interactive) (t, eval_terms) =
   let
     fun message s = if Config.get ctxt quiet then () else Output.urgent_message s
     val _ = check_test_term t
     val names = Term.add_free_names t []
     val current_size = Unsynchronized.ref 0

         end;
   in
     limit (seconds (Config.get ctxt timeout)) (limit_time, is_interactive) (fn () =>
       let
         val (test_fun, comp_time) = cpu_time "quickcheck compilation"
-          (fn () => mk_tester ctxt [(t, eval_terms)]);
+          (fn () => compile ctxt [(t, eval_terms)]);
         val _ = add_timing comp_time current_result
-      in
-        case test_fun of NONE => !current_result
-          | SOME test_fun =>
-            let
-              val (response, exec_time) =
-                cpu_time "quickcheck execution" (fn () => with_size test_fun 1)
-              val _ = add_response names eval_terms response current_result
-              val _ = add_timing exec_time current_result
-            in
-              !current_result
-            end
-       end)
-     (fn () => (message (excipit ()); !current_result)) ()
+        val (response, exec_time) =
+          cpu_time "quickcheck execution" (fn () => with_size test_fun 1)
+        val _ = add_response names eval_terms response current_result
+        val _ = add_timing exec_time current_result
+      in !current_result end)
+    (fn () => (message (excipit ()); !current_result)) ()
   end;
 
 fun validate_terms ctxt ts =
   let
     val _ = map check_test_term ts

   end
 
 (* FIXME: this function shows that many assumptions are made upon the generation *)
 (* In the end there is probably no generic quickcheck interface left... *)
 
-fun test_term_with_increasing_cardinality ctxt (limit_time, is_interactive) ts =
+fun test_term_with_increasing_cardinality compile ctxt (limit_time, is_interactive) ts =
   let
     val thy = Proof_Context.theory_of ctxt
     fun message s = if Config.get ctxt quiet then () else Output.urgent_message s
     val (ts', eval_terms) = split_list ts
     val _ = map check_test_term ts'

         map_product pair (1 upto (length ts)) (1 upto (Config.get ctxt size))
         |> sort (fn ((c1, s1), (c2, s2)) => int_ord ((c1 + s1), (c2 + s2)))
   in
     limit (seconds (Config.get ctxt timeout)) (limit_time, is_interactive) (fn () =>
       let
-        val (test_fun, comp_time) = cpu_time "quickcheck compilation" (fn () => mk_tester ctxt ts)
-        val _ = add_timing comp_time current_result
-      in
-        case test_fun of
-          NONE => !current_result
-        | SOME test_fun =>
-          let
-            val _ = case get_first (test_card_size test_fun) enumeration_card_size of
-              SOME (card, ts) => add_response names (nth eval_terms (card - 1)) (SOME ts) current_result
-            | NONE => ()
-          in !current_result end
-      end)
+        val (test_fun, comp_time) = cpu_time "quickcheck compilation" (fn () => compile ctxt ts)
+        val _ = add_timing comp_time current_result     
+        val _ = case get_first (test_card_size test_fun) enumeration_card_size of
+          SOME (card, ts) => add_response names (nth eval_terms (card - 1)) (SOME ts) current_result
+        | NONE => ()
+      in !current_result end)
       (fn () => (message "Quickcheck ran out of time"; !current_result)) ()
   end
 
 fun get_finite_types ctxt =
   fst (chop (Config.get ctxt finite_type_size)

         (result :: results)
       else
         collect_results f ts (result :: results)
     end  
 
-fun generator_test_goal_terms ctxt (limit_time, is_interactive) insts goals =
+fun generator_test_goal_terms compile ctxt (limit_time, is_interactive) insts goals =
   let
     fun test_term' goal =
       case goal of
-        [(NONE, t)] => test_term ctxt (limit_time, is_interactive) t
-      | ts => test_term_with_increasing_cardinality ctxt (limit_time, is_interactive) (map snd ts)
+        [(NONE, t)] => test_term compile ctxt (limit_time, is_interactive) t
+      | ts => test_term_with_increasing_cardinality compile ctxt (limit_time, is_interactive) (map snd ts)
     val correct_inst_goals = instantiate_goals ctxt insts goals
   in
     if Config.get ctxt finite_types then
       collect_results test_term' correct_inst_goals []
     else
-      collect_results (test_term ctxt (limit_time, is_interactive))
+      collect_results (test_term compile ctxt (limit_time, is_interactive))
         (maps (map snd) correct_inst_goals) []
   end;
 
 fun test_goal_terms ctxt (limit_time, is_interactive) insts goals =
   case lookup_tester ctxt (Config.get ctxt tester) of