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
authorbulwahn
Wed Mar 30 09:44:16 2011 +0200 (2011-03-30)
changeset 42159234ec7011e5d
parent 42158 9bcecd429f77
child 42160 43cba90b080f
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
src/HOL/Library/SML_Quickcheck.thy
src/HOL/Quickcheck.thy
src/HOL/Tools/Predicate_Compile/code_prolog.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
src/HOL/Tools/Quickcheck/exhaustive_generators.ML
src/HOL/Tools/Quickcheck/narrowing_generators.ML
src/HOL/Tools/Quickcheck/quickcheck_common.ML
src/HOL/Tools/Quickcheck/random_generators.ML
src/HOL/Tools/inductive_codegen.ML
src/HOL/ex/Quickcheck_Examples.thy
src/Tools/quickcheck.ML
     1.1 --- a/src/HOL/Library/SML_Quickcheck.thy	Tue Mar 29 23:46:46 2011 +0200
     1.2 +++ b/src/HOL/Library/SML_Quickcheck.thy	Wed Mar 30 09:44:16 2011 +0200
     1.3 @@ -8,7 +8,7 @@
     1.4  setup {*
     1.5    Inductive_Codegen.quickcheck_setup #>
     1.6    Context.theory_map (Quickcheck.add_generator ("SML",
     1.7 -    fn ctxt => fn (t, eval_terms) =>
     1.8 +    fn ctxt => fn [(t, eval_terms)] =>
     1.9        let
    1.10          val test_fun = Codegen.test_term ctxt t 
    1.11          val iterations = Config.get ctxt Quickcheck.iterations
    1.12 @@ -21,7 +21,7 @@
    1.13              in
    1.14                case result of NONE => iterate size (j - 1) | SOME q => SOME q
    1.15              end
    1.16 -     in fn size => (iterate size iterations, NONE) end))
    1.17 +     in fn [size] => (iterate size iterations, NONE) end))
    1.18  *}
    1.19  
    1.20  end
     2.1 --- a/src/HOL/Quickcheck.thy	Tue Mar 29 23:46:46 2011 +0200
     2.2 +++ b/src/HOL/Quickcheck.thy	Wed Mar 30 09:44:16 2011 +0200
     2.3 @@ -209,5 +209,12 @@
     2.4  hide_type (open) randompred
     2.5  hide_const (open) random collapse beyond random_fun_aux random_fun_lift
     2.6    iter' iter empty single bind union if_randompred iterate_upto not_randompred Random map
     2.7 +declare [[quickcheck_timing]]
     2.8 +lemma
     2.9 +  "rev xs = xs"
    2.10 +quickcheck[tester = random, finite_types = true, report = false]
    2.11 +
    2.12 +quickcheck[tester = random, finite_types = false, report = false]
    2.13 +oops
    2.14  
    2.15  end
     3.1 --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Tue Mar 29 23:46:46 2011 +0200
     3.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Wed Mar 30 09:44:16 2011 +0200
     3.3 @@ -39,7 +39,7 @@
     3.4    val write_program : logic_program -> string
     3.5    val run : (Time.time * prolog_system) -> logic_program -> (string * prol_term list) -> string list -> int option -> prol_term list list
     3.6    
     3.7 -  val quickcheck : Proof.context -> term * term list -> int -> term list option * Quickcheck.report option
     3.8 +  val quickcheck : Proof.context -> (term * term list) list -> int list -> term list option * Quickcheck.report option
     3.9  
    3.10    val trace : bool Unsynchronized.ref
    3.11    
    3.12 @@ -1009,7 +1009,7 @@
    3.13  
    3.14  (* FIXME: a small clone of Predicate_Compile_Quickcheck - maybe refactor out commons *)
    3.15  
    3.16 -fun quickcheck ctxt (t, []) size =
    3.17 +fun quickcheck ctxt [(t, [])] [_, size] =
    3.18    let
    3.19      val t' = list_abs_free (Term.add_frees t [], t)
    3.20      val options = code_options_of (ProofContext.theory_of ctxt)
     4.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Tue Mar 29 23:46:46 2011 +0200
     4.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Wed Mar 30 09:44:16 2011 +0200
     4.3 @@ -22,7 +22,7 @@
     4.4    val tracing : bool Unsynchronized.ref;
     4.5    val quiet : bool Unsynchronized.ref;
     4.6    val quickcheck_compile_term : Predicate_Compile_Aux.compilation -> bool -> bool -> int ->
     4.7 -    Proof.context -> term * term list -> int -> term list option * Quickcheck.report option;
     4.8 +    Proof.context -> (term * term list) list -> int list -> term list option * Quickcheck.report option;
     4.9  (*  val test_term : Proof.context -> bool -> int -> int -> int -> int -> term -> *)
    4.10    val nrandom : int Unsynchronized.ref;
    4.11    val debug : bool Unsynchronized.ref;
    4.12 @@ -215,7 +215,7 @@
    4.13    let val ({cpu, ...}, result) = Timing.timing e ()
    4.14    in (result, (description, Time.toMilliseconds cpu)) end
    4.15  
    4.16 -fun compile_term compilation options ctxt (t, eval_terms) =
    4.17 +fun compile_term compilation options ctxt [(t, eval_terms)] =
    4.18    let
    4.19      val t' = list_abs_free (Term.add_frees t [], t)
    4.20      val thy = Theory.copy (ProofContext.theory_of ctxt)
    4.21 @@ -353,7 +353,7 @@
    4.22    let
    4.23      val c = compile_term compilation options ctxt t
    4.24    in
    4.25 -    fn size => (try_upto (!quiet) (c size (!nrandom)) depth, NONE)
    4.26 +    fn [card, size] => (try_upto (!quiet) (c size (!nrandom)) depth, NONE)
    4.27    end
    4.28  
    4.29  fun quickcheck_compile_term compilation function_flattening fail_safe_function_flattening depth =
     5.1 --- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Tue Mar 29 23:46:46 2011 +0200
     5.2 +++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Wed Mar 30 09:44:16 2011 +0200
     5.3 @@ -7,10 +7,9 @@
     5.4  signature EXHAUSTIVE_GENERATORS =
     5.5  sig
     5.6    val compile_generator_expr:
     5.7 -    Proof.context -> term * term list -> int -> term list option * Quickcheck.report option
     5.8 -  val compile_generator_exprs:
     5.9 -    Proof.context -> term list -> (int -> term list option) list
    5.10 -  val put_counterexample: (unit -> int -> term list option)
    5.11 +    Proof.context -> (term * term list) list -> int list -> term list option * Quickcheck.report option
    5.12 +  val compile_generator_exprs: Proof.context -> term list -> (int -> term list option) list
    5.13 +  val put_counterexample: (unit -> int -> int -> term list option)
    5.14      -> Proof.context -> Proof.context
    5.15    val put_counterexample_batch: (unit -> (int -> term list option) list)
    5.16      -> Proof.context -> Proof.context
    5.17 @@ -264,11 +263,16 @@
    5.18        if Config.get ctxt smart_quantifier then mk_smart_test_term else mk_naive_test_term 
    5.19    in lambda depth (mk_test_term t) end
    5.20  
    5.21 +val mk_parametric_generator_expr =
    5.22 +  Quickcheck_Common.gen_mk_parametric_generator_expr 
    5.23 +    ((mk_generator_expr, absdummy (@{typ "code_numeral"}, @{term "None :: term list option"})),
    5.24 +      @{typ "code_numeral => term list option"})
    5.25 +  
    5.26  (** generator compiliation **)
    5.27  
    5.28  structure Counterexample = Proof_Data
    5.29  (
    5.30 -  type T = unit -> int -> term list option
    5.31 +  type T = unit -> int -> int -> term list option
    5.32    (* FIXME avoid user error with non-user text *)
    5.33    fun init _ () = error "Counterexample"
    5.34  );
    5.35 @@ -283,8 +287,8 @@
    5.36  val put_counterexample_batch = Counterexample_Batch.put;
    5.37  
    5.38  val target = "Quickcheck";
    5.39 -
    5.40 -fun compile_generator_expr ctxt (t, eval_terms) =
    5.41 +(*
    5.42 +fun compile_simple_generator_expr ctxt (t, eval_terms) =
    5.43    let
    5.44      val thy = ProofContext.theory_of ctxt
    5.45      val t' = mk_generator_expr ctxt (t, eval_terms);
    5.46 @@ -292,11 +296,26 @@
    5.47        (Counterexample.get, put_counterexample, "Exhaustive_Generators.put_counterexample")
    5.48        thy (SOME target) (fn proc => fn g => g #> (Option.map o map) proc) t' [];
    5.49    in
    5.50 -    fn size => rpair NONE (compile size |> 
    5.51 +    fn [size] => rpair NONE (compile [size] |> 
    5.52        (if Config.get ctxt quickcheck_pretty then
    5.53          Option.map (map Quickcheck_Common.post_process_term) else I))
    5.54    end;
    5.55 -
    5.56 +*)
    5.57 +  
    5.58 +fun compile_generator_expr ctxt ts =
    5.59 +  let
    5.60 +    val thy = ProofContext.theory_of ctxt
    5.61 +    val t' = mk_parametric_generator_expr ctxt ts;
    5.62 +    val compile = Code_Runtime.dynamic_value_strict
    5.63 +      (Counterexample.get, put_counterexample, "Exhaustive_Generators.put_counterexample")
    5.64 +      thy (SOME target) (fn proc => fn g =>
    5.65 +        fn card => fn size => g card size |> (Option.map o map) proc) t' [];
    5.66 +  in
    5.67 +    fn [card, size] => rpair NONE (compile card size |> 
    5.68 +      (if Config.get ctxt quickcheck_pretty then
    5.69 +        Option.map (map Quickcheck_Common.post_process_term) else I))
    5.70 +  end;
    5.71 + 
    5.72  fun compile_generator_exprs ctxt ts =
    5.73    let
    5.74      val thy = ProofContext.theory_of ctxt
    5.75 @@ -310,7 +329,6 @@
    5.76      map (fn compile => fn size => compile size
    5.77        |> Option.map (map Quickcheck_Common.post_process_term)) compiles
    5.78    end;
    5.79 -
    5.80    
    5.81  (** setup **)
    5.82  
     6.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Tue Mar 29 23:46:46 2011 +0200
     6.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Wed Mar 30 09:44:16 2011 +0200
     6.3 @@ -7,7 +7,7 @@
     6.4  signature NARROWING_GENERATORS =
     6.5  sig
     6.6    val compile_generator_expr:
     6.7 -    Proof.context -> term * term list -> int -> term list option * Quickcheck.report option
     6.8 +    Proof.context -> term * term list -> int list -> term list option * Quickcheck.report option
     6.9    val put_counterexample: (unit -> term list option) -> Proof.context -> Proof.context
    6.10    val finite_functions : bool Config.T
    6.11    val setup: theory -> theory
    6.12 @@ -212,7 +212,7 @@
    6.13      list_abs (names ~~ Ts', t'')
    6.14    end
    6.15  
    6.16 -fun compile_generator_expr ctxt (t, eval_terms) size =
    6.17 +fun compile_generator_expr ctxt (t, eval_terms) [size] =
    6.18    let
    6.19      val thy = ProofContext.theory_of ctxt
    6.20      val t' = list_abs_free (Term.add_frees t [], t)
    6.21 @@ -221,7 +221,7 @@
    6.22        Const (@{const_name Quickcheck_Narrowing.ensure_testable}, fastype_of t --> fastype_of t) $ t
    6.23      val result = dynamic_value_strict
    6.24        (Counterexample.get, Counterexample.put, "Narrowing_Generators.put_counterexample")
    6.25 -      thy (Option.map o map) (ensure_testable t'') [] size
    6.26 +      thy (Option.map o map) (ensure_testable t'') []
    6.27    in
    6.28      (result, NONE)
    6.29    end;
     7.1 --- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Tue Mar 29 23:46:46 2011 +0200
     7.2 +++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Wed Mar 30 09:44:16 2011 +0200
     7.3 @@ -12,6 +12,8 @@
     7.4      sort * (Datatype.config -> Datatype.descr -> (string * sort) list -> string list -> string ->
     7.5        string list * string list -> typ list * typ list -> theory -> theory)
     7.6      -> Datatype.config -> string list -> theory -> theory
     7.7 +  val gen_mk_parametric_generator_expr :
     7.8 +   (((Proof.context -> term * term list -> term) * term) * typ) -> Proof.context -> (term * term list) list -> term
     7.9    val post_process_term : term -> term
    7.10  end;
    7.11  
    7.12 @@ -53,6 +55,18 @@
    7.13        | NONE => thy
    7.14    end;
    7.15    
    7.16 +(** generic parametric compilation **)
    7.17 +
    7.18 +fun gen_mk_parametric_generator_expr ((mk_generator_expr, out_of_bounds), T) ctxt ts =
    7.19 +  let
    7.20 +    val if_t = Const (@{const_name "If"}, @{typ bool} --> T --> T --> T)
    7.21 +    fun mk_if (index, (t, eval_terms)) else_t =
    7.22 +      if_t $ (HOLogic.eq_const @{typ code_numeral} $ Bound 0 $ HOLogic.mk_number @{typ code_numeral} index) $
    7.23 +        (mk_generator_expr ctxt (t, eval_terms)) $ else_t
    7.24 +  in
    7.25 +    absdummy (@{typ "code_numeral"}, fold_rev mk_if (1 upto (length ts) ~~ ts) out_of_bounds)
    7.26 +  end
    7.27 +
    7.28  (** post-processing of function terms **)
    7.29  
    7.30  fun dest_fun_upd (Const (@{const_name fun_upd}, _) $ t0 $ t1 $ t2) = (t0, (t1, t2))
     8.1 --- a/src/HOL/Tools/Quickcheck/random_generators.ML	Tue Mar 29 23:46:46 2011 +0200
     8.2 +++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Wed Mar 30 09:44:16 2011 +0200
     8.3 @@ -11,10 +11,10 @@
     8.4      -> (seed -> ('b * (unit -> term)) * seed) -> (seed -> seed * seed)
     8.5      -> seed -> (('a -> 'b) * (unit -> term)) * seed
     8.6    val compile_generator_expr:
     8.7 -    Proof.context -> term * term list -> int -> term list option * Quickcheck.report option
     8.8 -  val put_counterexample: (unit -> int -> seed -> term list option * seed)
     8.9 +    Proof.context -> (term * term list) list -> int list -> term list option * Quickcheck.report option
    8.10 +  val put_counterexample: (unit -> int -> int -> seed -> term list option * seed)
    8.11      -> Proof.context -> Proof.context
    8.12 -  val put_counterexample_report: (unit -> int -> seed -> (term list option * (bool list * bool)) * seed)
    8.13 +  val put_counterexample_report: (unit -> int -> int -> seed -> (term list option * (bool list * bool)) * seed)
    8.14      -> Proof.context -> Proof.context
    8.15    val setup: theory -> theory
    8.16  end;
    8.17 @@ -272,7 +272,7 @@
    8.18  
    8.19  structure Counterexample = Proof_Data
    8.20  (
    8.21 -  type T = unit -> int -> int * int -> term list option * (int * int)
    8.22 +  type T = unit -> int -> int -> int * int -> term list option * (int * int)
    8.23    (* FIXME avoid user error with non-user text *)
    8.24    fun init _ () = error "Counterexample"
    8.25  );
    8.26 @@ -280,7 +280,7 @@
    8.27  
    8.28  structure Counterexample_Report = Proof_Data
    8.29  (
    8.30 -  type T = unit -> int -> seed -> (term list option * (bool list * bool)) * seed
    8.31 +  type T = unit -> int -> int -> seed -> (term list option * (bool list * bool)) * seed
    8.32    (* FIXME avoid user error with non-user text *)
    8.33    fun init _ () = error "Counterexample_Report"
    8.34  );
    8.35 @@ -288,8 +288,11 @@
    8.36  
    8.37  val target = "Quickcheck";
    8.38  
    8.39 -fun mk_generator_expr thy prop Ts =
    8.40 -  let
    8.41 +fun mk_generator_expr ctxt (t, eval_terms) =
    8.42 +  let  
    8.43 +    val thy = ProofContext.theory_of ctxt
    8.44 +    val prop = list_abs_free (Term.add_frees t [], t)
    8.45 +    val Ts = (map snd o fst o strip_abs) prop
    8.46      val bound_max = length Ts - 1;
    8.47      val bounds = map_index (fn (i, ty) =>
    8.48        (2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) Ts;
    8.49 @@ -311,9 +314,12 @@
    8.50        (Sign.mk_const thy (@{const_name Quickcheck.random}, [T]) $ Bound i);
    8.51    in Abs ("n", @{typ code_numeral}, fold_rev mk_bindclause bounds (return $ check)) end;
    8.52  
    8.53 -fun mk_reporting_generator_expr thy prop Ts =
    8.54 +fun mk_reporting_generator_expr ctxt (t, eval_terms) =
    8.55    let
    8.56 -    val bound_max = length Ts - 1;
    8.57 +    val thy = ProofContext.theory_of ctxt
    8.58 +    val prop = list_abs_free (Term.add_frees t [], t)
    8.59 +    val Ts = (map snd o fst o strip_abs) prop
    8.60 +    val bound_max = length Ts - 1
    8.61      val bounds = map_index (fn (i, ty) =>
    8.62        (2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) Ts;
    8.63      fun strip_imp (Const(@{const_name HOL.implies},_) $ A $ B) = apfst (cons A) (strip_imp B)
    8.64 @@ -354,6 +360,18 @@
    8.65      Abs ("n", @{typ code_numeral}, fold_rev mk_bindclause bounds (return $ check))
    8.66    end
    8.67  
    8.68 +val mk_parametric_generator_expr = Quickcheck_Common.gen_mk_parametric_generator_expr 
    8.69 +  ((mk_generator_expr, 
    8.70 +    absdummy (@{typ code_numeral}, @{term "Pair None :: Random.seed => term list option * Random.seed"})),
    8.71 +    @{typ "code_numeral => Random.seed => term list option * Random.seed"})
    8.72 +
    8.73 +val mk_parametric_reporting_generator_expr = Quickcheck_Common.gen_mk_parametric_generator_expr 
    8.74 +  ((mk_reporting_generator_expr,
    8.75 +    absdummy (@{typ code_numeral},
    8.76 +      @{term "Pair (None, ([], False)) :: Random.seed => (term list option * (bool list * bool)) * Random.seed"})),
    8.77 +    @{typ "code_numeral => Random.seed => (term list option * (bool list * bool)) * Random.seed"})
    8.78 +    
    8.79 +    
    8.80  (* single quickcheck report *)
    8.81  
    8.82  datatype single_report = Run of bool list * bool | MatchExc
    8.83 @@ -375,52 +393,50 @@
    8.84  val empty_report = Quickcheck.Report { iterations = 0, raised_match_errors = 0,
    8.85    satisfied_assms = [], positive_concl_tests = 0 }
    8.86      
    8.87 -fun compile_generator_expr ctxt (t, eval_terms) =
    8.88 +fun compile_generator_expr ctxt ts =
    8.89    let
    8.90 -    val t' = list_abs_free (Term.add_frees t [], t)
    8.91 -    val Ts = (map snd o fst o strip_abs) t';
    8.92      val thy = ProofContext.theory_of ctxt
    8.93      val iterations = Config.get ctxt Quickcheck.iterations
    8.94    in
    8.95      if Config.get ctxt Quickcheck.report then
    8.96        let
    8.97 -        val t'' = mk_reporting_generator_expr thy t' Ts;
    8.98 +        val t' = mk_parametric_reporting_generator_expr ctxt ts;
    8.99          val compile = Code_Runtime.dynamic_value_strict
   8.100            (Counterexample_Report.get, put_counterexample_report, "Random_Generators.put_counterexample_report")
   8.101 -          thy (SOME target) (fn proc => fn g => fn s => g s #>> (apfst o Option.map o map) proc) t'' [];
   8.102 -        val single_tester = compile #> Random_Engine.run
   8.103 -        fun iterate_and_collect size 0 report = (NONE, report)
   8.104 -          | iterate_and_collect size j report =
   8.105 +          thy (SOME target) (fn proc => fn g => fn c => fn s => g c s #>> (apfst o Option.map o map) proc) t' [];
   8.106 +        fun single_tester c s = compile c s |> Random_Engine.run
   8.107 +        fun iterate_and_collect (card, size) 0 report = (NONE, report)
   8.108 +          | iterate_and_collect (card, size) j report =
   8.109              let
   8.110 -              val (test_result, single_report) = apsnd Run (single_tester size) handle Match => 
   8.111 +              val (test_result, single_report) = apsnd Run (single_tester card size) handle Match => 
   8.112                  (if Config.get ctxt Quickcheck.quiet then ()
   8.113                   else warning "Exception Match raised during quickcheck"; (NONE, MatchExc))
   8.114                val report = collect_single_report single_report report
   8.115              in
   8.116 -              case test_result of NONE => iterate_and_collect size (j - 1) report
   8.117 +              case test_result of NONE => iterate_and_collect (card, size) (j - 1) report
   8.118                  | SOME q => (SOME q, report)
   8.119              end
   8.120        in
   8.121 -        fn size => apsnd SOME (iterate_and_collect size iterations empty_report)
   8.122 +        fn [card, size] => apsnd SOME (iterate_and_collect (card, size) iterations empty_report)
   8.123        end
   8.124      else
   8.125        let
   8.126 -        val t'' = mk_generator_expr thy t' Ts;
   8.127 +        val t' = mk_parametric_generator_expr ctxt ts;
   8.128          val compile = Code_Runtime.dynamic_value_strict
   8.129            (Counterexample.get, put_counterexample, "Random_Generators.put_counterexample")
   8.130 -          thy (SOME target) (fn proc => fn g => fn s => g s #>> (Option.map o map) proc) t'' [];
   8.131 -        val single_tester = compile #> Random_Engine.run
   8.132 -        fun iterate size 0 = NONE
   8.133 -          | iterate size j =
   8.134 +          thy (SOME target) (fn proc => fn g => fn c => fn s => g c s #>> (Option.map o map) proc) t' [];
   8.135 +        fun single_tester c s = compile c s |> Random_Engine.run
   8.136 +        fun iterate (card, size) 0 = NONE
   8.137 +          | iterate (card, size) j =
   8.138              let
   8.139 -              val result = single_tester size handle Match => 
   8.140 +              val result = single_tester card size handle Match => 
   8.141                  (if Config.get ctxt Quickcheck.quiet then ()
   8.142                   else warning "Exception Match raised during quickcheck"; NONE)
   8.143              in
   8.144 -              case result of NONE => iterate size (j - 1) | SOME q => SOME q
   8.145 +              case result of NONE => iterate (card, size) (j - 1) | SOME q => SOME q
   8.146              end
   8.147        in
   8.148 -        fn size => (rpair NONE (iterate size iterations))
   8.149 +        fn [card, size] => (rpair NONE (iterate (card, size) iterations))
   8.150        end
   8.151    end;
   8.152  
     9.1 --- a/src/HOL/Tools/inductive_codegen.ML	Tue Mar 29 23:46:46 2011 +0200
     9.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Wed Mar 30 09:44:16 2011 +0200
     9.3 @@ -9,7 +9,7 @@
     9.4    val add : string option -> int option -> attribute
     9.5    val test_fn : (int * int * int -> term list option) Unsynchronized.ref  (* FIXME *)
     9.6    val test_term:
     9.7 -    Proof.context -> term * term list -> int -> term list option * Quickcheck.report option
     9.8 +    Proof.context -> (term * term list) list -> int list -> term list option * Quickcheck.report option
     9.9    val setup : theory -> theory
    9.10    val quickcheck_setup : theory -> theory
    9.11  end;
    9.12 @@ -808,7 +808,7 @@
    9.13  val (random_values, setup_random_values) = Attrib.config_int "ind_quickcheck_random" (K 5);
    9.14  val (size_offset, setup_size_offset) = Attrib.config_int "ind_quickcheck_size_offset" (K 0);
    9.15  
    9.16 -fun test_term ctxt (t, []) =
    9.17 +fun test_term ctxt [(t, [])] =
    9.18    let
    9.19      val t' = list_abs_free (Term.add_frees t [], t)
    9.20      val thy = ProofContext.theory_of ctxt;
    9.21 @@ -852,11 +852,12 @@
    9.22      val bound = Config.get ctxt depth_bound;
    9.23      val start = Config.get ctxt depth_start;
    9.24      val offset = Config.get ctxt size_offset;
    9.25 -    fun test k = (deepen bound (fn i =>
    9.26 +    fun test [k] = (deepen bound (fn i =>
    9.27        (Output.urgent_message ("Search depth: " ^ string_of_int i);
    9.28         test_fn' (i, values, k+offset))) start, NONE);
    9.29    in test end
    9.30 -  | test_term ctxt (t, _) = error "Option eval is not supported by tester SML_inductive";
    9.31 +  | test_term ctxt [(t, _)] = error "Option eval is not supported by tester SML_inductive"
    9.32 +  | test_term ctxt _ = error "Compilation of multiple instances is not supported by tester SML_inductive";
    9.33  
    9.34  val quickcheck_setup =
    9.35    setup_depth_bound #>
    10.1 --- a/src/HOL/ex/Quickcheck_Examples.thy	Tue Mar 29 23:46:46 2011 +0200
    10.2 +++ b/src/HOL/ex/Quickcheck_Examples.thy	Wed Mar 30 09:44:16 2011 +0200
    10.3 @@ -50,9 +50,14 @@
    10.4    oops
    10.5  
    10.6  theorem "rev xs = xs"
    10.7 -  quickcheck[random, expect = counterexample]
    10.8 -  quickcheck[exhaustive, expect = counterexample]
    10.9 -  oops
   10.10 +  quickcheck[tester = random, finite_types = true, report = false, expect = counterexample]
   10.11 +  quickcheck[tester = random, finite_types = false, report = false, expect = counterexample]
   10.12 +  quickcheck[tester = random, finite_types = true, report = true, expect = counterexample]
   10.13 +  quickcheck[tester = random, finite_types = false, report = true, expect = counterexample]
   10.14 +  quickcheck[tester = exhaustive, finite_types = true, expect = counterexample]
   10.15 +  quickcheck[tester = exhaustive, finite_types = false, expect = counterexample]
   10.16 +oops
   10.17 +
   10.18  
   10.19  text {* An example involving functions inside other data structures *}
   10.20  
    11.1 --- a/src/Tools/quickcheck.ML	Tue Mar 29 23:46:46 2011 +0200
    11.2 +++ b/src/Tools/quickcheck.ML	Wed Mar 30 09:44:16 2011 +0200
    11.3 @@ -29,7 +29,7 @@
    11.4        satisfied_assms : int list, positive_concl_tests : int }
    11.5    (* registering generators *)
    11.6    val add_generator:
    11.7 -    string * (Proof.context -> term * term list -> int -> term list option * report option)
    11.8 +    string * (Proof.context -> (term * term list) list -> int list -> term list option * report option)
    11.9        -> Context.generic -> Context.generic
   11.10    val add_batch_generator:
   11.11      string * (Proof.context -> term list -> (int -> term list option) list)
   11.12 @@ -161,7 +161,7 @@
   11.13  structure Data = Generic_Data
   11.14  (
   11.15    type T =
   11.16 -    ((string * (Proof.context -> term * term list -> int -> term list option * report option)) list
   11.17 +    ((string * (Proof.context -> (term * term list) list -> int list -> term list option * report option)) list
   11.18        * (string * (Proof.context -> term list -> (int -> term list option) list)) list)
   11.19        * test_params;
   11.20    val empty = (([], []), Test_Params {default_type = [], expect = No_Expectation});
   11.21 @@ -240,7 +240,7 @@
   11.22      fun excipit () =
   11.23        "Quickcheck ran out of time while testing at size " ^ string_of_int (!current_size)
   11.24      val (test_fun, comp_time) = cpu_time "quickcheck compilation"
   11.25 -      (fn () => mk_tester ctxt (t, eval_terms));
   11.26 +      (fn () => mk_tester ctxt [(t, eval_terms)]);
   11.27      val _ = add_timing comp_time current_result
   11.28      fun with_size test_fun k =
   11.29        if k > Config.get ctxt size then
   11.30 @@ -250,7 +250,7 @@
   11.31            val _ = message ("Test data size: " ^ string_of_int k)
   11.32            val _ = current_size := k
   11.33            val ((result, report), timing) =
   11.34 -            cpu_time ("size " ^ string_of_int k) (fn () => test_fun (k - 1))
   11.35 +            cpu_time ("size " ^ string_of_int k) (fn () => test_fun [1, k - 1])
   11.36            val _ = add_timing timing current_result
   11.37            val _ = add_report k report current_result
   11.38          in
   11.39 @@ -293,19 +293,18 @@
   11.40    let
   11.41      val thy = ProofContext.theory_of ctxt
   11.42      fun message s = if Config.get ctxt quiet then () else Output.urgent_message s
   11.43 -    val (ts, eval_terms) = split_list ts
   11.44 -    val _ = map check_test_term ts
   11.45 -    val names = Term.add_free_names (hd ts) []
   11.46 -    val Ts = map snd (Term.add_frees (hd ts) [])
   11.47 +    val (ts', eval_terms) = split_list ts
   11.48 +    val _ = map check_test_term ts'
   11.49 +    val names = Term.add_free_names (hd ts') []
   11.50 +    val Ts = map snd (Term.add_frees (hd ts') [])
   11.51      val current_result = Unsynchronized.ref empty_result 
   11.52 -    val (test_funs, comp_time) = cpu_time "quickcheck compilation"
   11.53 -      (fn () => map (mk_tester ctxt) (ts ~~ eval_terms))
   11.54 +    val (test_fun, comp_time) = cpu_time "quickcheck compilation" (fn () => mk_tester ctxt ts)
   11.55      val _ = add_timing comp_time current_result
   11.56      fun test_card_size (card, size) =
   11.57        (* FIXME: why decrement size by one? *)
   11.58        let
   11.59          val (ts, timing) = cpu_time ("size " ^ string_of_int size ^ " and card " ^ string_of_int card)
   11.60 -          (fn () => fst (the (nth test_funs (card - 1)) (size - 1)))
   11.61 +          (fn () => fst ((the test_fun) [card - 1, size - 1]))
   11.62          val _ = add_timing timing current_result
   11.63        in
   11.64          Option.map (pair card) ts
   11.65 @@ -319,8 +318,9 @@
   11.66          map_product pair (1 upto (length ts)) (1 upto (Config.get ctxt size))
   11.67          |> sort (fn ((c1, s1), (c2, s2)) => int_ord ((c1 + s1), (c2 + s2)))
   11.68      in
   11.69 -      if (forall is_none test_funs) then !current_result
   11.70 -      else if (forall is_some test_funs) then
   11.71 +      case test_fun of
   11.72 +          NONE => !current_result
   11.73 +        | SOME test_fun =>
   11.74          limit ctxt (limit_time, is_interactive) (fn () =>
   11.75            let
   11.76              val _ = case get_first test_card_size enumeration_card_size of
   11.77 @@ -328,8 +328,6 @@
   11.78              | NONE => ()
   11.79            in !current_result end)
   11.80            (fn () => (message "Quickcheck ran out of time"; !current_result)) ()
   11.81 -      else
   11.82 -        error "Unexpectedly, testers of some cardinalities are executable but others are not"
   11.83      end
   11.84  
   11.85  fun get_finite_types ctxt =