# HG changeset patch # User bulwahn # Date 1300468782 -3600 # Node ID 5e40c152c3963c34f4db00cfa77eb0fe43f16c0f # Parent da9b58f1db42a84d7d0de18131f40343e6dd626a extending the test data generators to take the evaluation terms as arguments diff -r da9b58f1db42 -r 5e40c152c396 src/HOL/Tools/Quickcheck/exhaustive_generators.ML --- 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' = diff -r da9b58f1db42 -r 5e40c152c396 src/HOL/Tools/Quickcheck/narrowing_generators.ML --- 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 diff -r da9b58f1db42 -r 5e40c152c396 src/HOL/Tools/Quickcheck/random_generators.ML --- 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 diff -r da9b58f1db42 -r 5e40c152c396 src/HOL/Tools/inductive_codegen.ML --- 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 #>