1.1 --- a/src/Tools/quickcheck.ML Tue May 31 11:21:47 2011 +0200
1.2 +++ b/src/Tools/quickcheck.ML Tue May 31 15:45:24 2011 +0200
1.3 @@ -31,16 +31,6 @@
1.4 datatype report = Report of
1.5 { iterations : int, raised_match_errors : int,
1.6 satisfied_assms : int list, positive_concl_tests : int }
1.7 - (* registering generators *)
1.8 - val add_generator:
1.9 - string * (Proof.context -> (term * term list) list -> int list -> term list option * report option)
1.10 - -> Context.generic -> Context.generic
1.11 - val add_batch_generator:
1.12 - string * (Proof.context -> term list -> (int -> term list option) list)
1.13 - -> Context.generic -> Context.generic
1.14 - val add_batch_validator:
1.15 - string * (Proof.context -> term list -> (int -> bool) list)
1.16 - -> Context.generic -> Context.generic
1.17 (* quickcheck's result *)
1.18 datatype result =
1.19 Result of
1.20 @@ -50,6 +40,19 @@
1.21 reports : (int * report) list}
1.22 val counterexample_of : result -> (string * term) list option
1.23 val timings_of : result -> (string * int) list
1.24 + (* registering generators *)
1.25 + val add_generator:
1.26 + string * (Proof.context -> (term * term list) list -> int list -> term list option * report option)
1.27 + -> Context.generic -> Context.generic
1.28 + val add_tester:
1.29 + string * (Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list -> result list)
1.30 + -> Context.generic -> Context.generic
1.31 + val add_batch_generator:
1.32 + string * (Proof.context -> term list -> (int -> term list option) list)
1.33 + -> Context.generic -> Context.generic
1.34 + val add_batch_validator:
1.35 + string * (Proof.context -> term list -> (int -> bool) list)
1.36 + -> Context.generic -> Context.generic
1.37 (* testing terms and proof states *)
1.38 val test_term: Proof.context -> bool * bool -> term * term list -> result
1.39 val test_goal_terms:
1.40 @@ -174,17 +177,19 @@
1.41 structure Data = Generic_Data
1.42 (
1.43 type T =
1.44 - ((string * (Proof.context -> (term * term list) list -> int list -> term list option * report option)) list
1.45 + (((string * (Proof.context -> (term * term list) list -> int list -> term list option * report option)) list
1.46 + * (string * (Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list -> result list)) list)
1.47 * ((string * (Proof.context -> term list -> (int -> term list option) list)) list
1.48 * ((string * (Proof.context -> term list -> (int -> bool) list)) list)))
1.49 * test_params;
1.50 - val empty = (([], ([], [])), Test_Params {default_type = [], expect = No_Expectation});
1.51 + val empty = ((([], []), ([], [])), Test_Params {default_type = [], expect = No_Expectation});
1.52 val extend = I;
1.53 - fun merge (((generators1, (batch_generators1, batch_validators1)), params1),
1.54 - ((generators2, (batch_generators2, batch_validators2)), params2)) : T =
1.55 - ((AList.merge (op =) (K true) (generators1, generators2),
1.56 - (AList.merge (op =) (K true) (batch_generators1, batch_generators2),
1.57 - AList.merge (op =) (K true) (batch_validators1, batch_validators2))),
1.58 + fun merge ((((generators1, testers1), (batch_generators1, batch_validators1)), params1),
1.59 + (((generators2, testers2), (batch_generators2, batch_validators2)), params2)) : T =
1.60 + (((AList.merge (op =) (K true) (generators1, generators2),
1.61 + AList.merge (op =) (K true) (testers1, testers2)),
1.62 + (AList.merge (op =) (K true) (batch_generators1, batch_generators2),
1.63 + AList.merge (op =) (K true) (batch_validators1, batch_validators2))),
1.64 merge_test_params (params1, params2));
1.65 );
1.66
1.67 @@ -196,7 +201,9 @@
1.68
1.69 val map_test_params = Data.map o apsnd o map_test_params'
1.70
1.71 -val add_generator = Data.map o apfst o apfst o AList.update (op =);
1.72 +val add_generator = Data.map o apfst o apfst o apfst o AList.update (op =);
1.73 +
1.74 +val add_tester = Data.map o apfst o apfst o apsnd o AList.update (op =);
1.75
1.76 val add_batch_generator = Data.map o apfst o apsnd o apfst o AList.update (op =);
1.77
1.78 @@ -223,12 +230,15 @@
1.79 end
1.80
1.81 val mk_tester =
1.82 - gen_mk_tester (fn ctxt => AList.lookup (op =) ((fst o fst o Data.get o Context.Proof) ctxt))
1.83 + gen_mk_tester (fn ctxt => AList.lookup (op =) ((fst o fst o fst o Data.get o Context.Proof) ctxt))
1.84 val mk_batch_tester =
1.85 gen_mk_tester (fn ctxt => AList.lookup (op =) ((fst o snd o fst o Data.get o Context.Proof) ctxt))
1.86 val mk_batch_validator =
1.87 gen_mk_tester (fn ctxt => AList.lookup (op =) ((snd o snd o fst o Data.get o Context.Proof) ctxt))
1.88
1.89 +
1.90 +fun lookup_tester ctxt = AList.lookup (op =) ((snd o fst o fst o Data.get o Context.Proof) ctxt)
1.91 +
1.92 (* testing propositions *)
1.93
1.94 fun check_test_term t =
1.95 @@ -470,8 +480,9 @@
1.96 | SOME locale =>
1.97 map (fn (_, phi) => (Morphism.term phi proto_goal, map (Morphism.term phi) eval_terms))
1.98 (Locale.registrations_of (Context.Theory thy) (*FIXME*) locale);
1.99 + val test_goals = the_default test_goal_terms (lookup_tester lthy (Config.get lthy tester))
1.100 in
1.101 - test_goal_terms lthy (time_limit, is_interactive) insts check_goals
1.102 + test_goals lthy (time_limit, is_interactive) insts check_goals
1.103 end
1.104
1.105 (* pretty printing *)
1.106 @@ -544,7 +555,7 @@
1.107 | read_expectation "counterexample" = Counterexample
1.108 | read_expectation s = error ("Not an expectation value: " ^ s)
1.109
1.110 -fun valid_tester_name genctxt = AList.defined (op =) (fst (fst (Data.get genctxt)))
1.111 +fun valid_tester_name genctxt = AList.defined (op =) (fst (fst (fst (Data.get genctxt))))
1.112
1.113 fun parse_tester name genctxt =
1.114 if valid_tester_name genctxt name then