--- a/src/HOL/Library/SML_Quickcheck.thy Sun Jul 17 22:25:14 2011 +0200
+++ b/src/HOL/Library/SML_Quickcheck.thy Mon Jul 18 10:34:21 2011 +0200
@@ -23,6 +23,7 @@
case result of NONE => iterate size (j - 1) | SOME q => SOME q
end
in fn [_, size] => (iterate size iterations, NONE) end))
+ #> Context.theory_map (Quickcheck.add_tester ("SML", Quickcheck.generator_test_goal_terms))
*}
end
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Sun Jul 17 22:25:14 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Mon Jul 18 10:34:21 2011 +0200
@@ -488,6 +488,8 @@
thy (SOME target) (K I) (HOLogic.mk_list @{typ "code_numeral => bool"} ts') []
end;
+val test_goals = Quickcheck.generator_test_goal_terms;
+
(* setup *)
val setup =
@@ -500,6 +502,7 @@
#> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
(((@{sort type}, @{sort type}), @{sort bounded_forall}), instantiate_bounded_forall_datatype))*)
#> Context.theory_map (Quickcheck.add_generator ("exhaustive", compile_generator_expr))
+ #> Context.theory_map (Quickcheck.add_tester ("exhaustive", test_goals))
#> Context.theory_map (Quickcheck.add_batch_generator ("exhaustive", compile_generator_exprs))
#> Context.theory_map (Quickcheck.add_batch_validator ("exhaustive", compile_validator_exprs));
--- a/src/HOL/Tools/Quickcheck/random_generators.ML Sun Jul 17 22:25:14 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML Mon Jul 18 10:34:21 2011 +0200
@@ -438,14 +438,15 @@
end
end;
-
+val test_goals = Quickcheck.generator_test_goal_terms;
+
(** setup **)
val setup =
Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
(((@{sort typerep}, @{sort term_of}), @{sort random}), instantiate_random_datatype))
#> Code_Target.extend_target (target, (Code_Runtime.target, K I))
- #> Context.theory_map
- (Quickcheck.add_generator ("random", compile_generator_expr));
+ #> Context.theory_map (Quickcheck.add_generator ("random", compile_generator_expr))
+ #> Context.theory_map (Quickcheck.add_tester ("random", test_goals));
end;
--- a/src/Tools/quickcheck.ML Sun Jul 17 22:25:14 2011 +0200
+++ b/src/Tools/quickcheck.ML Mon Jul 18 10:34:21 2011 +0200
@@ -60,6 +60,8 @@
val instantiate_goals: Proof.context -> (string * typ) list -> (term * term list) list
-> (typ option * (term * term list)) list list
val collect_results: ('a -> result) -> 'a list -> result list -> result list
+ val generator_test_goal_terms: Proof.context -> bool * bool -> (string * typ) list ->
+ (term * term list) list -> result list
(* testing terms and proof states *)
val test_term: Proof.context -> bool * bool -> term * term list -> result
val test_goal_terms:
@@ -469,7 +471,7 @@
collect_results f ts (result :: results)
end
-fun test_goal_terms ctxt (limit_time, is_interactive) insts goals =
+fun generator_test_goal_terms ctxt (limit_time, is_interactive) insts goals =
let
fun test_term' goal =
case goal of
@@ -477,15 +479,18 @@
| ts => test_term_with_increasing_cardinality ctxt (limit_time, is_interactive) (map snd ts)
val correct_inst_goals = instantiate_goals ctxt insts goals
in
- case lookup_tester ctxt (Config.get ctxt tester) of
- SOME test_goal_terms => test_goal_terms ctxt (limit_time, is_interactive) insts goals
- | NONE =>
- if Config.get ctxt finite_types then
- collect_results test_term' correct_inst_goals []
- else
- collect_results (test_term ctxt (limit_time, is_interactive)) (maps (map snd) correct_inst_goals) []
+ if Config.get ctxt finite_types then
+ collect_results test_term' correct_inst_goals []
+ else
+ collect_results (test_term ctxt (limit_time, is_interactive))
+ (maps (map snd) correct_inst_goals) []
end;
+fun test_goal_terms ctxt (limit_time, is_interactive) insts goals =
+ case lookup_tester ctxt (Config.get ctxt tester) of
+ SOME test_goal_terms => test_goal_terms ctxt (limit_time, is_interactive) insts goals
+ | NONE => error ("Unknown tester: " ^ Config.get ctxt tester)
+
fun test_goal (time_limit, is_interactive) (insts, eval_terms) i state =
let
val lthy = Proof.context_of state;