--- a/src/Tools/quickcheck.ML Wed Oct 28 11:55:48 2009 +0100
+++ b/src/Tools/quickcheck.ML Wed Oct 28 17:43:43 2009 +0100
@@ -7,10 +7,10 @@
signature QUICKCHECK =
sig
val auto: bool Unsynchronized.ref
- val auto_time_limit: int Unsynchronized.ref
val test_term: Proof.context -> bool -> string option -> int -> int -> term ->
(string * term) list option
val add_generator: string * (Proof.context -> term -> int -> term list option) -> theory -> theory
+ val setup: theory -> theory
val quickcheck: (string * string) list -> int -> Proof.state -> (string * term) list option
end;
@@ -20,20 +20,13 @@
(* preferences *)
val auto = Unsynchronized.ref false;
-val auto_time_limit = Unsynchronized.ref 2500;
val _ =
ProofGeneralPgip.add_preference Preferences.category_tracing
(setmp_CRITICAL auto true (fn () =>
Preferences.bool_pref auto
"auto-quickcheck"
- "Whether to enable quickcheck automatically.") ());
-
-val _ =
- ProofGeneralPgip.add_preference Preferences.category_tracing
- (Preferences.nat_pref auto_time_limit
- "auto-quickcheck-time-limit"
- "Time limit for automatic quickcheck (in milliseconds).");
+ "Whether to run Quickcheck automatically.") ());
(* quickcheck configuration -- default parameters, test generators *)
@@ -159,28 +152,26 @@
(* automatic testing *)
-val _ = Context.>> (Specification.add_theorem_hook (fn int => fn state =>
- let
- val ctxt = Proof.context_of state;
- val assms = map term_of (Assumption.all_assms_of ctxt);
- val Test_Params { size, iterations, default_type } =
- (snd o Data.get o Proof.theory_of) state;
- fun test () =
- let
- val res = TimeLimit.timeLimit (Time.fromMilliseconds (!auto_time_limit))
- (try (test_goal true NONE size iterations default_type [] 1 assms)) state;
- in
- case res of
- NONE => state
- | SOME NONE => state
- | SOME cex => Proof.goal_message (fn () => Pretty.chunks [Pretty.str "",
- Pretty.mark Markup.hilite (pretty_counterex ctxt cex)]) state
- end handle TimeLimit.TimeOut => (warning "Auto quickcheck: timeout."; state);
- in
- if int andalso !auto andalso not (!Toplevel.quiet)
- then test ()
- else state
- end));
+fun auto_quickcheck state =
+ if not (!auto) then
+ (false, state)
+ else
+ let
+ val ctxt = Proof.context_of state;
+ val assms = map term_of (Assumption.all_assms_of ctxt);
+ val Test_Params { size, iterations, default_type } =
+ (snd o Data.get o Proof.theory_of) state;
+ val res =
+ try (test_goal true NONE size iterations default_type [] 1 assms) state;
+ in
+ case res of
+ NONE => (false, state)
+ | SOME NONE => (false, state)
+ | SOME cex => (true, Proof.goal_message (K (Pretty.chunks [Pretty.str "",
+ Pretty.mark Markup.hilite (pretty_counterex ctxt cex)])) state)
+ end
+
+val setup = Auto_Counterexample.register_tool ("quickcheck", auto_quickcheck)
(* Isar commands *)
@@ -251,4 +242,3 @@
val auto_quickcheck = Quickcheck.auto;
-val auto_quickcheck_time_limit = Quickcheck.auto_time_limit;