# HG changeset patch # User bulwahn # Date 1306849524 -7200 # Node ID 3117573292b8ba4232efe8c788cd69d65bed15a0 # Parent 946c8e171ffdca793b1b2d0e94c23c8d68a3639e adding registration of testers in Quickcheck for its use in Quickcheck_Narrowing diff -r 946c8e171ffd -r 3117573292b8 src/Tools/quickcheck.ML --- a/src/Tools/quickcheck.ML Tue May 31 11:21:47 2011 +0200 +++ b/src/Tools/quickcheck.ML Tue May 31 15:45:24 2011 +0200 @@ -31,16 +31,6 @@ datatype report = Report of { iterations : int, raised_match_errors : int, satisfied_assms : int list, positive_concl_tests : int } - (* registering generators *) - val add_generator: - string * (Proof.context -> (term * term list) list -> int list -> term list option * report option) - -> Context.generic -> Context.generic - val add_batch_generator: - string * (Proof.context -> term list -> (int -> term list option) list) - -> Context.generic -> Context.generic - val add_batch_validator: - string * (Proof.context -> term list -> (int -> bool) list) - -> Context.generic -> Context.generic (* quickcheck's result *) datatype result = Result of @@ -50,6 +40,19 @@ reports : (int * report) list} val counterexample_of : result -> (string * term) list option val timings_of : result -> (string * int) list + (* registering generators *) + val add_generator: + string * (Proof.context -> (term * term list) list -> int list -> term list option * report option) + -> Context.generic -> Context.generic + val add_tester: + string * (Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list -> result list) + -> Context.generic -> Context.generic + val add_batch_generator: + string * (Proof.context -> term list -> (int -> term list option) list) + -> Context.generic -> Context.generic + val add_batch_validator: + string * (Proof.context -> term list -> (int -> bool) list) + -> Context.generic -> Context.generic (* testing terms and proof states *) val test_term: Proof.context -> bool * bool -> term * term list -> result val test_goal_terms: @@ -174,17 +177,19 @@ structure Data = Generic_Data ( type T = - ((string * (Proof.context -> (term * term list) list -> int list -> term list option * report option)) list + (((string * (Proof.context -> (term * term list) list -> int list -> term list option * report option)) list + * (string * (Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list -> result list)) list) * ((string * (Proof.context -> term list -> (int -> term list option) list)) list * ((string * (Proof.context -> term list -> (int -> bool) list)) list))) * test_params; - val empty = (([], ([], [])), Test_Params {default_type = [], expect = No_Expectation}); + val empty = ((([], []), ([], [])), Test_Params {default_type = [], expect = No_Expectation}); val extend = I; - fun merge (((generators1, (batch_generators1, batch_validators1)), params1), - ((generators2, (batch_generators2, batch_validators2)), params2)) : T = - ((AList.merge (op =) (K true) (generators1, generators2), - (AList.merge (op =) (K true) (batch_generators1, batch_generators2), - AList.merge (op =) (K true) (batch_validators1, batch_validators2))), + fun merge ((((generators1, testers1), (batch_generators1, batch_validators1)), params1), + (((generators2, testers2), (batch_generators2, batch_validators2)), params2)) : T = + (((AList.merge (op =) (K true) (generators1, generators2), + AList.merge (op =) (K true) (testers1, testers2)), + (AList.merge (op =) (K true) (batch_generators1, batch_generators2), + AList.merge (op =) (K true) (batch_validators1, batch_validators2))), merge_test_params (params1, params2)); ); @@ -196,7 +201,9 @@ val map_test_params = Data.map o apsnd o map_test_params' -val add_generator = Data.map o apfst o apfst o AList.update (op =); +val add_generator = Data.map o apfst o apfst o apfst o AList.update (op =); + +val add_tester = Data.map o apfst o apfst o apsnd o AList.update (op =); val add_batch_generator = Data.map o apfst o apsnd o apfst o AList.update (op =); @@ -223,12 +230,15 @@ end val mk_tester = - gen_mk_tester (fn ctxt => AList.lookup (op =) ((fst o fst o Data.get o Context.Proof) ctxt)) + gen_mk_tester (fn ctxt => AList.lookup (op =) ((fst o fst o fst o Data.get o Context.Proof) ctxt)) val mk_batch_tester = gen_mk_tester (fn ctxt => AList.lookup (op =) ((fst o snd o fst o Data.get o Context.Proof) ctxt)) val mk_batch_validator = gen_mk_tester (fn ctxt => AList.lookup (op =) ((snd o snd o fst o Data.get o Context.Proof) ctxt)) + +fun lookup_tester ctxt = AList.lookup (op =) ((snd o fst o fst o Data.get o Context.Proof) ctxt) + (* testing propositions *) fun check_test_term t = @@ -470,8 +480,9 @@ | SOME locale => map (fn (_, phi) => (Morphism.term phi proto_goal, map (Morphism.term phi) eval_terms)) (Locale.registrations_of (Context.Theory thy) (*FIXME*) locale); + val test_goals = the_default test_goal_terms (lookup_tester lthy (Config.get lthy tester)) in - test_goal_terms lthy (time_limit, is_interactive) insts check_goals + test_goals lthy (time_limit, is_interactive) insts check_goals end (* pretty printing *) @@ -544,7 +555,7 @@ | read_expectation "counterexample" = Counterexample | read_expectation s = error ("Not an expectation value: " ^ s) -fun valid_tester_name genctxt = AList.defined (op =) (fst (fst (Data.get genctxt))) +fun valid_tester_name genctxt = AList.defined (op =) (fst (fst (fst (Data.get genctxt)))) fun parse_tester name genctxt = if valid_tester_name genctxt name then