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
--- 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
--- 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
--- 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)
--- 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 =
--- 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 **)
--- 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;
--- 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))
--- 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;
--- 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 #>
--- 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 *}
--- 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 =