--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Fri Mar 18 18:19:42 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Fri Mar 18 18:19:42 2011 +0100
@@ -7,7 +7,7 @@
signature EXHAUSTIVE_GENERATORS =
sig
val compile_generator_expr:
- Proof.context -> term -> int -> term list option * Quickcheck.report option
+ 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)
@@ -293,7 +293,7 @@
(** generator compiliation **)
-fun compile_generator_expr ctxt t =
+fun compile_generator_expr ctxt (t, eval_terms) =
let
val thy = ProofContext.theory_of ctxt
val t' =
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Fri Mar 18 18:19:42 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Fri Mar 18 18:19:42 2011 +0100
@@ -7,7 +7,7 @@
signature NARROWING_GENERATORS =
sig
val compile_generator_expr:
- Proof.context -> term -> int -> term list option * Quickcheck.report option
+ Proof.context -> term * term list -> int -> 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
@@ -213,7 +213,7 @@
list_abs (names ~~ Ts', t'')
end
-fun compile_generator_expr ctxt t size =
+fun compile_generator_expr ctxt (t, eval_terms) size =
let
val thy = ProofContext.theory_of ctxt
val t' = if Config.get ctxt finite_functions then finitize_functions t else t
--- a/src/HOL/Tools/Quickcheck/random_generators.ML Fri Mar 18 18:19:42 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML Fri Mar 18 18:19:42 2011 +0100
@@ -11,7 +11,7 @@
-> (seed -> ('b * (unit -> term)) * seed) -> (seed -> seed * seed)
-> seed -> (('a -> 'b) * (unit -> term)) * seed
val compile_generator_expr:
- Proof.context -> term -> int -> term list option * Quickcheck.report option
+ Proof.context -> term * term list -> int -> term list option * Quickcheck.report option
val put_counterexample: (unit -> int -> seed -> term list option * seed)
-> Proof.context -> Proof.context
val put_counterexample_report: (unit -> int -> seed -> (term list option * (bool list * bool)) * seed)
@@ -375,7 +375,7 @@
val empty_report = Quickcheck.Report { iterations = 0, raised_match_errors = 0,
satisfied_assms = [], positive_concl_tests = 0 }
-fun compile_generator_expr ctxt t =
+fun compile_generator_expr ctxt (t, eval_terms) =
let
val Ts = (map snd o fst o strip_abs) t;
val thy = ProofContext.theory_of ctxt
--- a/src/HOL/Tools/inductive_codegen.ML Fri Mar 18 18:19:42 2011 +0100
+++ b/src/HOL/Tools/inductive_codegen.ML Fri Mar 18 18:19:42 2011 +0100
@@ -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 -> int -> term list option * Quickcheck.report option
+ Proof.context -> term * term list -> int -> 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 thy = ProofContext.theory_of ctxt;
val (xs, p) = strip_abs t;
@@ -854,7 +854,8 @@
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;
+ in test end
+ | test_term ctxt (t, _) = error "Option eval is not supported by tester SML_inductive";
val quickcheck_setup =
setup_depth_bound #>