# HG changeset patch
# User bulwahn
# Date 1301471056 -7200
# Node ID 234ec7011e5d463b3b41649e66a3bae7dc5cdff0
# Parent  9bcecd429f7764432210eede13c2aceba98d774b
generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities

diff -r 9bcecd429f77 -r 234ec7011e5d src/HOL/Library/SML_Quickcheck.thy
--- a/src/HOL/Library/SML_Quickcheck.thy	Tue Mar 29 23:46:46 2011 +0200
+++ b/src/HOL/Library/SML_Quickcheck.thy	Wed Mar 30 09:44:16 2011 +0200
@@ -8,7 +8,7 @@
 setup {*
   Inductive_Codegen.quickcheck_setup #>
   Context.theory_map (Quickcheck.add_generator ("SML",
-    fn ctxt => fn (t, eval_terms) =>
+    fn ctxt => fn [(t, eval_terms)] =>
       let
         val test_fun = Codegen.test_term ctxt t 
         val iterations = Config.get ctxt Quickcheck.iterations
@@ -21,7 +21,7 @@
             in
               case result of NONE => iterate size (j - 1) | SOME q => SOME q
             end
-     in fn size => (iterate size iterations, NONE) end))
+     in fn [size] => (iterate size iterations, NONE) end))
 *}
 
 end
diff -r 9bcecd429f77 -r 234ec7011e5d src/HOL/Quickcheck.thy
--- a/src/HOL/Quickcheck.thy	Tue Mar 29 23:46:46 2011 +0200
+++ b/src/HOL/Quickcheck.thy	Wed Mar 30 09:44:16 2011 +0200
@@ -209,5 +209,12 @@
 hide_type (open) randompred
 hide_const (open) random collapse beyond random_fun_aux random_fun_lift
   iter' iter empty single bind union if_randompred iterate_upto not_randompred Random map
+declare [[quickcheck_timing]]
+lemma
+  "rev xs = xs"
+quickcheck[tester = random, finite_types = true, report = false]
+
+quickcheck[tester = random, finite_types = false, report = false]
+oops
 
 end
diff -r 9bcecd429f77 -r 234ec7011e5d src/HOL/Tools/Predicate_Compile/code_prolog.ML
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Tue Mar 29 23:46:46 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Wed Mar 30 09:44:16 2011 +0200
@@ -39,7 +39,7 @@
   val write_program : logic_program -> string
   val run : (Time.time * prolog_system) -> logic_program -> (string * prol_term list) -> string list -> int option -> prol_term list list
   
-  val quickcheck : Proof.context -> term * term list -> int -> term list option * Quickcheck.report option
+  val quickcheck : Proof.context -> (term * term list) list -> int list -> term list option * Quickcheck.report option
 
   val trace : bool Unsynchronized.ref
   
@@ -1009,7 +1009,7 @@
 
 (* FIXME: a small clone of Predicate_Compile_Quickcheck - maybe refactor out commons *)
 
-fun quickcheck ctxt (t, []) size =
+fun quickcheck ctxt [(t, [])] [_, size] =
   let
     val t' = list_abs_free (Term.add_frees t [], t)
     val options = code_options_of (ProofContext.theory_of ctxt)
diff -r 9bcecd429f77 -r 234ec7011e5d src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Tue Mar 29 23:46:46 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Wed Mar 30 09:44:16 2011 +0200
@@ -22,7 +22,7 @@
   val tracing : bool Unsynchronized.ref;
   val quiet : bool Unsynchronized.ref;
   val quickcheck_compile_term : Predicate_Compile_Aux.compilation -> bool -> bool -> int ->
-    Proof.context -> term * term list -> int -> term list option * Quickcheck.report option;
+    Proof.context -> (term * term list) list -> int list -> term list option * Quickcheck.report option;
 (*  val test_term : Proof.context -> bool -> int -> int -> int -> int -> term -> *)
   val nrandom : int Unsynchronized.ref;
   val debug : bool Unsynchronized.ref;
@@ -215,7 +215,7 @@
   let val ({cpu, ...}, result) = Timing.timing e ()
   in (result, (description, Time.toMilliseconds cpu)) end
 
-fun compile_term compilation options ctxt (t, eval_terms) =
+fun compile_term compilation options ctxt [(t, eval_terms)] =
   let
     val t' = list_abs_free (Term.add_frees t [], t)
     val thy = Theory.copy (ProofContext.theory_of ctxt)
@@ -353,7 +353,7 @@
   let
     val c = compile_term compilation options ctxt t
   in
-    fn size => (try_upto (!quiet) (c size (!nrandom)) depth, NONE)
+    fn [card, size] => (try_upto (!quiet) (c size (!nrandom)) depth, NONE)
   end
 
 fun quickcheck_compile_term compilation function_flattening fail_safe_function_flattening depth =
diff -r 9bcecd429f77 -r 234ec7011e5d src/HOL/Tools/Quickcheck/exhaustive_generators.ML
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Tue Mar 29 23:46:46 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Wed Mar 30 09:44:16 2011 +0200
@@ -7,10 +7,9 @@
 signature EXHAUSTIVE_GENERATORS =
 sig
   val compile_generator_expr:
-    Proof.context -> term * term list -> int -> term list option * Quickcheck.report option
-  val compile_generator_exprs:
-    Proof.context -> term list -> (int -> term list option) list
-  val put_counterexample: (unit -> int -> term list option)
+    Proof.context -> (term * term list) list -> int list -> term list option * Quickcheck.report option
+  val compile_generator_exprs: Proof.context -> term list -> (int -> term list option) list
+  val put_counterexample: (unit -> int -> int -> term list option)
     -> Proof.context -> Proof.context
   val put_counterexample_batch: (unit -> (int -> term list option) list)
     -> Proof.context -> Proof.context
@@ -264,11 +263,16 @@
       if Config.get ctxt smart_quantifier then mk_smart_test_term else mk_naive_test_term 
   in lambda depth (mk_test_term t) end
 
+val mk_parametric_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"})
+  
 (** generator compiliation **)
 
 structure Counterexample = Proof_Data
 (
-  type T = unit -> int -> term list option
+  type T = unit -> int -> int -> term list option
   (* FIXME avoid user error with non-user text *)
   fun init _ () = error "Counterexample"
 );
@@ -283,8 +287,8 @@
 val put_counterexample_batch = Counterexample_Batch.put;
 
 val target = "Quickcheck";
-
-fun compile_generator_expr ctxt (t, eval_terms) =
+(*
+fun compile_simple_generator_expr ctxt (t, eval_terms) =
   let
     val thy = ProofContext.theory_of ctxt
     val t' = mk_generator_expr ctxt (t, eval_terms);
@@ -292,11 +296,26 @@
       (Counterexample.get, put_counterexample, "Exhaustive_Generators.put_counterexample")
       thy (SOME target) (fn proc => fn g => g #> (Option.map o map) proc) t' [];
   in
-    fn size => rpair NONE (compile size |> 
+    fn [size] => rpair NONE (compile [size] |> 
       (if Config.get ctxt quickcheck_pretty then
         Option.map (map Quickcheck_Common.post_process_term) else I))
   end;
-
+*)
+  
+fun compile_generator_expr ctxt ts =
+  let
+    val thy = ProofContext.theory_of ctxt
+    val t' = mk_parametric_generator_expr ctxt ts;
+    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' [];
+  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))
+  end;
+ 
 fun compile_generator_exprs ctxt ts =
   let
     val thy = ProofContext.theory_of ctxt
@@ -310,7 +329,6 @@
     map (fn compile => fn size => compile size
       |> Option.map (map Quickcheck_Common.post_process_term)) compiles
   end;
-
   
 (** setup **)
 
diff -r 9bcecd429f77 -r 234ec7011e5d src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Tue Mar 29 23:46:46 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Wed Mar 30 09:44:16 2011 +0200
@@ -7,7 +7,7 @@
 signature NARROWING_GENERATORS =
 sig
   val compile_generator_expr:
-    Proof.context -> term * term list -> int -> term list option * Quickcheck.report option
+    Proof.context -> term * term list -> int list -> term list option * Quickcheck.report option
   val put_counterexample: (unit -> term list option) -> Proof.context -> Proof.context
   val finite_functions : bool Config.T
   val setup: theory -> theory
@@ -212,7 +212,7 @@
     list_abs (names ~~ Ts', t'')
   end
 
-fun compile_generator_expr ctxt (t, eval_terms) size =
+fun compile_generator_expr ctxt (t, eval_terms) [size] =
   let
     val thy = ProofContext.theory_of ctxt
     val t' = list_abs_free (Term.add_frees t [], t)
@@ -221,7 +221,7 @@
       Const (@{const_name Quickcheck_Narrowing.ensure_testable}, fastype_of t --> fastype_of t) $ t
     val result = dynamic_value_strict
       (Counterexample.get, Counterexample.put, "Narrowing_Generators.put_counterexample")
-      thy (Option.map o map) (ensure_testable t'') [] size
+      thy (Option.map o map) (ensure_testable t'') []
   in
     (result, NONE)
   end;
diff -r 9bcecd429f77 -r 234ec7011e5d src/HOL/Tools/Quickcheck/quickcheck_common.ML
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Tue Mar 29 23:46:46 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Wed Mar 30 09:44:16 2011 +0200
@@ -12,6 +12,8 @@
     sort * (Datatype.config -> Datatype.descr -> (string * sort) list -> string list -> string ->
       string list * string list -> typ list * typ list -> theory -> theory)
     -> Datatype.config -> string list -> theory -> theory
+  val gen_mk_parametric_generator_expr :
+   (((Proof.context -> term * term list -> term) * term) * typ) -> Proof.context -> (term * term list) list -> term
   val post_process_term : term -> term
 end;
 
@@ -53,6 +55,18 @@
       | NONE => thy
   end;
   
+(** generic parametric compilation **)
+
+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) $
+        (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)
+  end
+
 (** post-processing of function terms **)
 
 fun dest_fun_upd (Const (@{const_name fun_upd}, _) $ t0 $ t1 $ t2) = (t0, (t1, t2))
diff -r 9bcecd429f77 -r 234ec7011e5d src/HOL/Tools/Quickcheck/random_generators.ML
--- a/src/HOL/Tools/Quickcheck/random_generators.ML	Tue Mar 29 23:46:46 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Wed Mar 30 09:44:16 2011 +0200
@@ -11,10 +11,10 @@
     -> (seed -> ('b * (unit -> term)) * seed) -> (seed -> seed * seed)
     -> seed -> (('a -> 'b) * (unit -> term)) * seed
   val compile_generator_expr:
-    Proof.context -> term * term list -> int -> term list option * Quickcheck.report option
-  val put_counterexample: (unit -> int -> seed -> term list option * seed)
+    Proof.context -> (term * term list) list -> int list -> term list option * Quickcheck.report option
+  val put_counterexample: (unit -> int -> int -> seed -> term list option * seed)
     -> Proof.context -> Proof.context
-  val put_counterexample_report: (unit -> int -> seed -> (term list option * (bool list * bool)) * seed)
+  val put_counterexample_report: (unit -> int -> int -> seed -> (term list option * (bool list * bool)) * seed)
     -> Proof.context -> Proof.context
   val setup: theory -> theory
 end;
@@ -272,7 +272,7 @@
 
 structure Counterexample = Proof_Data
 (
-  type T = unit -> int -> int * int -> term list option * (int * int)
+  type T = unit -> int -> int -> int * int -> term list option * (int * int)
   (* FIXME avoid user error with non-user text *)
   fun init _ () = error "Counterexample"
 );
@@ -280,7 +280,7 @@
 
 structure Counterexample_Report = Proof_Data
 (
-  type T = unit -> int -> seed -> (term list option * (bool list * bool)) * seed
+  type T = unit -> int -> int -> seed -> (term list option * (bool list * bool)) * seed
   (* FIXME avoid user error with non-user text *)
   fun init _ () = error "Counterexample_Report"
 );
@@ -288,8 +288,11 @@
 
 val target = "Quickcheck";
 
-fun mk_generator_expr thy prop Ts =
-  let
+fun mk_generator_expr ctxt (t, eval_terms) =
+  let  
+    val thy = ProofContext.theory_of ctxt
+    val prop = list_abs_free (Term.add_frees t [], t)
+    val Ts = (map snd o fst o strip_abs) prop
     val bound_max = length Ts - 1;
     val bounds = map_index (fn (i, ty) =>
       (2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) Ts;
@@ -311,9 +314,12 @@
       (Sign.mk_const thy (@{const_name Quickcheck.random}, [T]) $ Bound i);
   in Abs ("n", @{typ code_numeral}, fold_rev mk_bindclause bounds (return $ check)) end;
 
-fun mk_reporting_generator_expr thy prop Ts =
+fun mk_reporting_generator_expr ctxt (t, eval_terms) =
   let
-    val bound_max = length Ts - 1;
+    val thy = ProofContext.theory_of ctxt
+    val prop = list_abs_free (Term.add_frees t [], t)
+    val Ts = (map snd o fst o strip_abs) prop
+    val bound_max = length Ts - 1
     val bounds = map_index (fn (i, ty) =>
       (2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) Ts;
     fun strip_imp (Const(@{const_name HOL.implies},_) $ A $ B) = apfst (cons A) (strip_imp B)
@@ -354,6 +360,18 @@
     Abs ("n", @{typ code_numeral}, fold_rev mk_bindclause bounds (return $ check))
   end
 
+val mk_parametric_generator_expr = Quickcheck_Common.gen_mk_parametric_generator_expr 
+  ((mk_generator_expr, 
+    absdummy (@{typ code_numeral}, @{term "Pair None :: Random.seed => term list option * Random.seed"})),
+    @{typ "code_numeral => Random.seed => term list option * Random.seed"})
+
+val mk_parametric_reporting_generator_expr = Quickcheck_Common.gen_mk_parametric_generator_expr 
+  ((mk_reporting_generator_expr,
+    absdummy (@{typ code_numeral},
+      @{term "Pair (None, ([], False)) :: Random.seed => (term list option * (bool list * bool)) * Random.seed"})),
+    @{typ "code_numeral => Random.seed => (term list option * (bool list * bool)) * Random.seed"})
+    
+    
 (* single quickcheck report *)
 
 datatype single_report = Run of bool list * bool | MatchExc
@@ -375,52 +393,50 @@
 val empty_report = Quickcheck.Report { iterations = 0, raised_match_errors = 0,
   satisfied_assms = [], positive_concl_tests = 0 }
     
-fun compile_generator_expr ctxt (t, eval_terms) =
+fun compile_generator_expr ctxt ts =
   let
-    val t' = list_abs_free (Term.add_frees t [], t)
-    val Ts = (map snd o fst o strip_abs) t';
     val thy = ProofContext.theory_of ctxt
     val iterations = Config.get ctxt Quickcheck.iterations
   in
     if Config.get ctxt Quickcheck.report then
       let
-        val t'' = mk_reporting_generator_expr thy t' Ts;
+        val t' = mk_parametric_reporting_generator_expr ctxt ts;
         val compile = Code_Runtime.dynamic_value_strict
           (Counterexample_Report.get, put_counterexample_report, "Random_Generators.put_counterexample_report")
-          thy (SOME target) (fn proc => fn g => fn s => g s #>> (apfst o Option.map o map) proc) t'' [];
-        val single_tester = compile #> Random_Engine.run
-        fun iterate_and_collect size 0 report = (NONE, report)
-          | iterate_and_collect size j report =
+          thy (SOME target) (fn proc => fn g => fn c => fn s => g c s #>> (apfst o Option.map o map) proc) t' [];
+        fun single_tester c s = compile c s |> Random_Engine.run
+        fun iterate_and_collect (card, size) 0 report = (NONE, report)
+          | iterate_and_collect (card, size) j report =
             let
-              val (test_result, single_report) = apsnd Run (single_tester size) handle Match => 
+              val (test_result, single_report) = apsnd Run (single_tester card size) handle Match => 
                 (if Config.get ctxt Quickcheck.quiet then ()
                  else warning "Exception Match raised during quickcheck"; (NONE, MatchExc))
               val report = collect_single_report single_report report
             in
-              case test_result of NONE => iterate_and_collect size (j - 1) report
+              case test_result of NONE => iterate_and_collect (card, size) (j - 1) report
                 | SOME q => (SOME q, report)
             end
       in
-        fn size => apsnd SOME (iterate_and_collect size iterations empty_report)
+        fn [card, size] => apsnd SOME (iterate_and_collect (card, size) iterations empty_report)
       end
     else
       let
-        val t'' = mk_generator_expr thy t' Ts;
+        val t' = mk_parametric_generator_expr ctxt ts;
         val compile = Code_Runtime.dynamic_value_strict
           (Counterexample.get, put_counterexample, "Random_Generators.put_counterexample")
-          thy (SOME target) (fn proc => fn g => fn s => g s #>> (Option.map o map) proc) t'' [];
-        val single_tester = compile #> Random_Engine.run
-        fun iterate size 0 = NONE
-          | iterate size j =
+          thy (SOME target) (fn proc => fn g => fn c => fn s => g c s #>> (Option.map o map) proc) t' [];
+        fun single_tester c s = compile c s |> Random_Engine.run
+        fun iterate (card, size) 0 = NONE
+          | iterate (card, size) j =
             let
-              val result = single_tester size handle Match => 
+              val result = single_tester card size handle Match => 
                 (if Config.get ctxt Quickcheck.quiet then ()
                  else warning "Exception Match raised during quickcheck"; NONE)
             in
-              case result of NONE => iterate size (j - 1) | SOME q => SOME q
+              case result of NONE => iterate (card, size) (j - 1) | SOME q => SOME q
             end
       in
-        fn size => (rpair NONE (iterate size iterations))
+        fn [card, size] => (rpair NONE (iterate (card, size) iterations))
       end
   end;
 
diff -r 9bcecd429f77 -r 234ec7011e5d src/HOL/Tools/inductive_codegen.ML
--- a/src/HOL/Tools/inductive_codegen.ML	Tue Mar 29 23:46:46 2011 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML	Wed Mar 30 09:44:16 2011 +0200
@@ -9,7 +9,7 @@
   val add : string option -> int option -> attribute
   val test_fn : (int * int * int -> term list option) Unsynchronized.ref  (* FIXME *)
   val test_term:
-    Proof.context -> term * term list -> int -> term list option * Quickcheck.report option
+    Proof.context -> (term * term list) list -> int list -> term list option * Quickcheck.report option
   val setup : theory -> theory
   val quickcheck_setup : theory -> theory
 end;
@@ -808,7 +808,7 @@
 val (random_values, setup_random_values) = Attrib.config_int "ind_quickcheck_random" (K 5);
 val (size_offset, setup_size_offset) = Attrib.config_int "ind_quickcheck_size_offset" (K 0);
 
-fun test_term ctxt (t, []) =
+fun test_term ctxt [(t, [])] =
   let
     val t' = list_abs_free (Term.add_frees t [], t)
     val thy = ProofContext.theory_of ctxt;
@@ -852,11 +852,12 @@
     val bound = Config.get ctxt depth_bound;
     val start = Config.get ctxt depth_start;
     val offset = Config.get ctxt size_offset;
-    fun test k = (deepen bound (fn i =>
+    fun test [k] = (deepen bound (fn i =>
       (Output.urgent_message ("Search depth: " ^ string_of_int i);
        test_fn' (i, values, k+offset))) start, NONE);
   in test end
-  | test_term ctxt (t, _) = error "Option eval is not supported by tester SML_inductive";
+  | test_term ctxt [(t, _)] = error "Option eval is not supported by tester SML_inductive"
+  | test_term ctxt _ = error "Compilation of multiple instances is not supported by tester SML_inductive";
 
 val quickcheck_setup =
   setup_depth_bound #>
diff -r 9bcecd429f77 -r 234ec7011e5d src/HOL/ex/Quickcheck_Examples.thy
--- a/src/HOL/ex/Quickcheck_Examples.thy	Tue Mar 29 23:46:46 2011 +0200
+++ b/src/HOL/ex/Quickcheck_Examples.thy	Wed Mar 30 09:44:16 2011 +0200
@@ -50,9 +50,14 @@
   oops
 
 theorem "rev xs = xs"
-  quickcheck[random, expect = counterexample]
-  quickcheck[exhaustive, expect = counterexample]
-  oops
+  quickcheck[tester = random, finite_types = true, report = false, expect = counterexample]
+  quickcheck[tester = random, finite_types = false, report = false, expect = counterexample]
+  quickcheck[tester = random, finite_types = true, report = true, expect = counterexample]
+  quickcheck[tester = random, finite_types = false, report = true, expect = counterexample]
+  quickcheck[tester = exhaustive, finite_types = true, expect = counterexample]
+  quickcheck[tester = exhaustive, finite_types = false, expect = counterexample]
+oops
+
 
 text {* An example involving functions inside other data structures *}
 
diff -r 9bcecd429f77 -r 234ec7011e5d src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Tue Mar 29 23:46:46 2011 +0200
+++ b/src/Tools/quickcheck.ML	Wed Mar 30 09:44:16 2011 +0200
@@ -29,7 +29,7 @@
       satisfied_assms : int list, positive_concl_tests : int }
   (* registering generators *)
   val add_generator:
-    string * (Proof.context -> term * term list -> int -> term list option * report option)
+    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)
@@ -161,7 +161,7 @@
 structure Data = Generic_Data
 (
   type T =
-    ((string * (Proof.context -> term * term list -> int -> term list option * report option)) list
+    ((string * (Proof.context -> (term * term list) list -> int list -> term list option * report option)) list
       * (string * (Proof.context -> term list -> (int -> term list option) list)) list)
       * test_params;
   val empty = (([], []), Test_Params {default_type = [], expect = No_Expectation});
@@ -240,7 +240,7 @@
     fun excipit () =
       "Quickcheck ran out of time while testing at size " ^ string_of_int (!current_size)
     val (test_fun, comp_time) = cpu_time "quickcheck compilation"
-      (fn () => mk_tester ctxt (t, eval_terms));
+      (fn () => mk_tester ctxt [(t, eval_terms)]);
     val _ = add_timing comp_time current_result
     fun with_size test_fun k =
       if k > Config.get ctxt size then
@@ -250,7 +250,7 @@
           val _ = message ("Test data size: " ^ string_of_int k)
           val _ = current_size := k
           val ((result, report), timing) =
-            cpu_time ("size " ^ string_of_int k) (fn () => test_fun (k - 1))
+            cpu_time ("size " ^ string_of_int k) (fn () => test_fun [1, k - 1])
           val _ = add_timing timing current_result
           val _ = add_report k report current_result
         in
@@ -293,19 +293,18 @@
   let
     val thy = ProofContext.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
-    val names = Term.add_free_names (hd ts) []
-    val Ts = map snd (Term.add_frees (hd ts) [])
+    val (ts', eval_terms) = split_list ts
+    val _ = map check_test_term ts'
+    val names = Term.add_free_names (hd ts') []
+    val Ts = map snd (Term.add_frees (hd ts') [])
     val current_result = Unsynchronized.ref empty_result 
-    val (test_funs, comp_time) = cpu_time "quickcheck compilation"
-      (fn () => map (mk_tester ctxt) (ts ~~ eval_terms))
+    val (test_fun, comp_time) = cpu_time "quickcheck compilation" (fn () => mk_tester ctxt ts)
     val _ = add_timing comp_time current_result
     fun test_card_size (card, size) =
       (* FIXME: why decrement size by one? *)
       let
         val (ts, timing) = cpu_time ("size " ^ string_of_int size ^ " and card " ^ string_of_int card)
-          (fn () => fst (the (nth test_funs (card - 1)) (size - 1)))
+          (fn () => fst ((the test_fun) [card - 1, size - 1]))
         val _ = add_timing timing current_result
       in
         Option.map (pair card) ts
@@ -319,8 +318,9 @@
         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
-      if (forall is_none test_funs) then !current_result
-      else if (forall is_some test_funs) then
+      case test_fun of
+          NONE => !current_result
+        | SOME test_fun =>
         limit ctxt (limit_time, is_interactive) (fn () =>
           let
             val _ = case get_first test_card_size enumeration_card_size of
@@ -328,8 +328,6 @@
             | NONE => ()
           in !current_result end)
           (fn () => (message "Quickcheck ran out of time"; !current_result)) ()
-      else
-        error "Unexpectedly, testers of some cardinalities are executable but others are not"
     end
 
 fun get_finite_types ctxt =