extending the test data generators to take the evaluation terms as arguments
authorbulwahn
Fri Mar 18 18:19:42 2011 +0100 (2011-03-18)
changeset 420275e40c152c396
parent 42026 da9b58f1db42
child 42028 bd6515e113b2
extending the test data generators to take the evaluation terms as arguments
src/HOL/Tools/Quickcheck/exhaustive_generators.ML
src/HOL/Tools/Quickcheck/narrowing_generators.ML
src/HOL/Tools/Quickcheck/random_generators.ML
src/HOL/Tools/inductive_codegen.ML
     1.1 --- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Fri Mar 18 18:19:42 2011 +0100
     1.2 +++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Fri Mar 18 18:19:42 2011 +0100
     1.3 @@ -7,7 +7,7 @@
     1.4  signature EXHAUSTIVE_GENERATORS =
     1.5  sig
     1.6    val compile_generator_expr:
     1.7 -    Proof.context -> term -> int -> term list option * Quickcheck.report option
     1.8 +    Proof.context -> term * term list -> int -> term list option * Quickcheck.report option
     1.9    val compile_generator_exprs:
    1.10      Proof.context -> term list -> (int -> term list option) list
    1.11    val put_counterexample: (unit -> int -> term list option)
    1.12 @@ -293,7 +293,7 @@
    1.13  
    1.14  (** generator compiliation **)
    1.15  
    1.16 -fun compile_generator_expr ctxt t =
    1.17 +fun compile_generator_expr ctxt (t, eval_terms) =
    1.18    let
    1.19      val thy = ProofContext.theory_of ctxt
    1.20      val t' =
     2.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Mar 18 18:19:42 2011 +0100
     2.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Mar 18 18:19:42 2011 +0100
     2.3 @@ -7,7 +7,7 @@
     2.4  signature NARROWING_GENERATORS =
     2.5  sig
     2.6    val compile_generator_expr:
     2.7 -    Proof.context -> term -> int -> term list option * Quickcheck.report option
     2.8 +    Proof.context -> term * term list -> int -> term list option * Quickcheck.report option
     2.9    val put_counterexample: (unit -> term list option) -> Proof.context -> Proof.context
    2.10    val finite_functions : bool Config.T
    2.11    val setup: theory -> theory
    2.12 @@ -213,7 +213,7 @@
    2.13      list_abs (names ~~ Ts', t'')
    2.14    end
    2.15  
    2.16 -fun compile_generator_expr ctxt t size =
    2.17 +fun compile_generator_expr ctxt (t, eval_terms) size =
    2.18    let
    2.19      val thy = ProofContext.theory_of ctxt
    2.20      val t' = if Config.get ctxt finite_functions then finitize_functions t else t
     3.1 --- a/src/HOL/Tools/Quickcheck/random_generators.ML	Fri Mar 18 18:19:42 2011 +0100
     3.2 +++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Fri Mar 18 18:19:42 2011 +0100
     3.3 @@ -11,7 +11,7 @@
     3.4      -> (seed -> ('b * (unit -> term)) * seed) -> (seed -> seed * seed)
     3.5      -> seed -> (('a -> 'b) * (unit -> term)) * seed
     3.6    val compile_generator_expr:
     3.7 -    Proof.context -> term -> int -> term list option * Quickcheck.report option
     3.8 +    Proof.context -> term * term list -> int -> term list option * Quickcheck.report option
     3.9    val put_counterexample: (unit -> int -> seed -> term list option * seed)
    3.10      -> Proof.context -> Proof.context
    3.11    val put_counterexample_report: (unit -> int -> seed -> (term list option * (bool list * bool)) * seed)
    3.12 @@ -375,7 +375,7 @@
    3.13  val empty_report = Quickcheck.Report { iterations = 0, raised_match_errors = 0,
    3.14    satisfied_assms = [], positive_concl_tests = 0 }
    3.15      
    3.16 -fun compile_generator_expr ctxt t =
    3.17 +fun compile_generator_expr ctxt (t, eval_terms) =
    3.18    let
    3.19      val Ts = (map snd o fst o strip_abs) t;
    3.20      val thy = ProofContext.theory_of ctxt
     4.1 --- a/src/HOL/Tools/inductive_codegen.ML	Fri Mar 18 18:19:42 2011 +0100
     4.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Fri Mar 18 18:19:42 2011 +0100
     4.3 @@ -9,7 +9,7 @@
     4.4    val add : string option -> int option -> attribute
     4.5    val test_fn : (int * int * int -> term list option) Unsynchronized.ref  (* FIXME *)
     4.6    val test_term:
     4.7 -    Proof.context -> term -> int -> term list option * Quickcheck.report option
     4.8 +    Proof.context -> term * term list -> int -> term list option * Quickcheck.report option
     4.9    val setup : theory -> theory
    4.10    val quickcheck_setup : theory -> theory
    4.11  end;
    4.12 @@ -808,7 +808,7 @@
    4.13  val (random_values, setup_random_values) = Attrib.config_int "ind_quickcheck_random" (K 5);
    4.14  val (size_offset, setup_size_offset) = Attrib.config_int "ind_quickcheck_size_offset" (K 0);
    4.15  
    4.16 -fun test_term ctxt t =
    4.17 +fun test_term ctxt (t, []) =
    4.18    let
    4.19      val thy = ProofContext.theory_of ctxt;
    4.20      val (xs, p) = strip_abs t;
    4.21 @@ -854,7 +854,8 @@
    4.22      fun test k = (deepen bound (fn i =>
    4.23        (Output.urgent_message ("Search depth: " ^ string_of_int i);
    4.24         test_fn' (i, values, k+offset))) start, NONE);
    4.25 -  in test end;
    4.26 +  in test end
    4.27 +  | test_term ctxt (t, _) = error "Option eval is not supported by tester SML_inductive";
    4.28  
    4.29  val quickcheck_setup =
    4.30    setup_depth_bound #>