1.1 --- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Mon Jul 18 10:34:21 2011 +0200
1.2 +++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Mon Jul 18 10:34:21 2011 +0200
1.3 @@ -501,7 +501,6 @@
1.4 (((@{sort typerep}, @{sort term_of}), @{sort fast_exhaustive}), instantiate_fast_exhaustive_datatype))
1.5 #> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
1.6 (((@{sort type}, @{sort type}), @{sort bounded_forall}), instantiate_bounded_forall_datatype))*)
1.7 - #> Context.theory_map (Quickcheck.add_generator ("exhaustive", compile_generator_expr))
1.8 #> Context.theory_map (Quickcheck.add_tester ("exhaustive", test_goals))
1.9 #> Context.theory_map (Quickcheck.add_batch_generator ("exhaustive", compile_generator_exprs))
1.10 #> Context.theory_map (Quickcheck.add_batch_validator ("exhaustive", compile_validator_exprs));
2.1 --- a/src/HOL/Tools/Quickcheck/random_generators.ML Mon Jul 18 10:34:21 2011 +0200
2.2 +++ b/src/HOL/Tools/Quickcheck/random_generators.ML Mon Jul 18 10:34:21 2011 +0200
2.3 @@ -446,7 +446,6 @@
2.4 Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
2.5 (((@{sort typerep}, @{sort term_of}), @{sort random}), instantiate_random_datatype))
2.6 #> Code_Target.extend_target (target, (Code_Runtime.target, K I))
2.7 - #> Context.theory_map (Quickcheck.add_generator ("random", compile_generator_expr))
2.8 #> Context.theory_map (Quickcheck.add_tester ("random", test_goals));
2.9
2.10 end;
3.1 --- a/src/HOL/Tools/inductive_codegen.ML Mon Jul 18 10:34:21 2011 +0200
3.2 +++ b/src/HOL/Tools/inductive_codegen.ML Mon Jul 18 10:34:21 2011 +0200
3.3 @@ -924,7 +924,9 @@
3.4 | test_term ctxt _ =
3.5 error "Compilation of multiple instances is not supported by tester SML_inductive";
3.6
3.7 +val test_goal = Quickcheck.generator_test_goal_terms test_term;
3.8 +
3.9 val quickcheck_setup =
3.10 - Context.theory_map (Quickcheck.add_generator ("SML_inductive", test_term));
3.11 + Context.theory_map (Quickcheck.add_tester ("SML_inductive", test_goal));
3.12
3.13 end;
4.1 --- a/src/Tools/quickcheck.ML Mon Jul 18 10:34:21 2011 +0200
4.2 +++ b/src/Tools/quickcheck.ML Mon Jul 18 10:34:21 2011 +0200
4.3 @@ -43,9 +43,9 @@
4.4 val counterexample_of : result -> (string * term) list option
4.5 val timings_of : result -> (string * int) list
4.6 (* registering generators *)
4.7 - val add_generator:
4.8 + (*val add_generator:
4.9 string * (Proof.context -> (term * term list) list -> int list -> term list option * report option)
4.10 - -> Context.generic -> Context.generic
4.11 + -> Context.generic -> Context.generic*)
4.12 val add_tester:
4.13 string * (Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list -> result list)
4.14 -> Context.generic -> Context.generic
4.15 @@ -196,17 +196,16 @@
4.16 structure Data = Generic_Data
4.17 (
4.18 type T =
4.19 - (((string * (Proof.context -> (term * term list) list -> int list -> term list option * report option)) list
4.20 - * (string * (Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list -> result list)) list)
4.21 + ((string * (Proof.context -> bool * bool ->
4.22 + (string * typ) list -> (term * term list) list -> result list)) list
4.23 * ((string * (Proof.context -> term list -> (int -> term list option) list)) list
4.24 * ((string * (Proof.context -> term list -> (int -> bool) list)) list)))
4.25 * test_params;
4.26 - val empty = ((([], []), ([], [])), Test_Params {default_type = [], expect = No_Expectation});
4.27 + val empty = (([], ([], [])), Test_Params {default_type = [], expect = No_Expectation});
4.28 val extend = I;
4.29 - fun merge ((((generators1, testers1), (batch_generators1, batch_validators1)), params1),
4.30 - (((generators2, testers2), (batch_generators2, batch_validators2)), params2)) : T =
4.31 - (((AList.merge (op =) (K true) (generators1, generators2),
4.32 - AList.merge (op =) (K true) (testers1, testers2)),
4.33 + fun merge (((testers1, (batch_generators1, batch_validators1)), params1),
4.34 + ((testers2, (batch_generators2, batch_validators2)), params2)) : T =
4.35 + ((AList.merge (op =) (K true) (testers1, testers2),
4.36 (AList.merge (op =) (K true) (batch_generators1, batch_generators2),
4.37 AList.merge (op =) (K true) (batch_validators1, batch_validators2))),
4.38 merge_test_params (params1, params2));
4.39 @@ -220,9 +219,9 @@
4.40
4.41 val map_test_params = Data.map o apsnd o map_test_params'
4.42
4.43 -val add_generator = Data.map o apfst o apfst o apfst o AList.update (op =);
4.44 +(*val add_generator = Data.map o apfst o apfst o apfst o AList.update (op =);*)
4.45
4.46 -val add_tester = Data.map o apfst o apfst o apsnd o AList.update (op =);
4.47 +val add_tester = Data.map o apfst o apfst o AList.update (op =);
4.48
4.49 val add_batch_generator = Data.map o apfst o apsnd o apfst o AList.update (op =);
4.50
4.51 @@ -255,9 +254,8 @@
4.52 gen_mk_tester (fn ctxt => AList.lookup (op =) ((fst o snd o fst o Data.get o Context.Proof) ctxt))
4.53 val mk_batch_validator =
4.54 gen_mk_tester (fn ctxt => AList.lookup (op =) ((snd o snd o fst o Data.get o Context.Proof) ctxt))
4.55 -
4.56
4.57 -fun lookup_tester ctxt = AList.lookup (op =) ((snd o fst o fst o Data.get o Context.Proof) ctxt)
4.58 +fun lookup_tester ctxt = AList.lookup (op =) ((fst o fst o Data.get o Context.Proof) ctxt)
4.59
4.60 (* testing propositions *)
4.61
4.62 @@ -578,10 +576,8 @@
4.63 | read_expectation "counterexample" = Counterexample
4.64 | read_expectation s = error ("Not an expectation value: " ^ s)
4.65
4.66 -fun valid_tester_name genctxt name =
4.67 - AList.defined (op =) (fst (fst (fst (Data.get genctxt)))) name orelse
4.68 - AList.defined (op =) (snd (fst (fst (Data.get genctxt)))) name
4.69 -
4.70 +fun valid_tester_name genctxt name = AList.defined (op =) (fst (fst (Data.get genctxt))) name
4.71 +
4.72 fun parse_tester name genctxt =
4.73 if valid_tester_name genctxt name then
4.74 Config.put_generic tester name genctxt