--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/auto_tools.ML Sat Sep 11 10:28:44 2010 +0200
@@ -0,0 +1,59 @@
+(* Title: Tools/auto_counterexample.ML
+ Author: Jasmin Blanchette, TU Muenchen
+
+Counterexample Search Unit (do not abbreviate!).
+*)
+
+signature AUTO_COUNTEREXAMPLE =
+sig
+ val time_limit: int Unsynchronized.ref
+
+ val register_tool :
+ string * (Proof.state -> bool * Proof.state) -> theory -> theory
+end;
+
+structure Auto_Counterexample : AUTO_COUNTEREXAMPLE =
+struct
+
+(* preferences *)
+
+val time_limit = Unsynchronized.ref 2500
+
+val _ =
+ ProofGeneralPgip.add_preference Preferences.category_tracing
+ (Preferences.nat_pref time_limit
+ "auto-counterexample-time-limit"
+ "Time limit for automatic counterexample search (in milliseconds).")
+
+
+(* configuration *)
+
+structure Data = Theory_Data
+(
+ type T = (string * (Proof.state -> bool * Proof.state)) list
+ val empty = []
+ val extend = I
+ fun merge data : T = AList.merge (op =) (K true) data
+)
+
+val register_tool = Data.map o AList.update (op =)
+
+
+(* automatic testing *)
+
+val _ = Context.>> (Specification.add_theorem_hook (fn interact => fn state =>
+ case !time_limit of
+ 0 => state
+ | ms =>
+ TimeLimit.timeLimit (Time.fromMilliseconds ms)
+ (fn () =>
+ if interact andalso not (!Toplevel.quiet) then
+ fold_rev (fn (_, tool) => fn (true, state) => (true, state)
+ | (false, state) => tool state)
+ (Data.get (Proof.theory_of state)) (false, state) |> snd
+ else
+ state) ()
+ handle TimeLimit.TimeOut =>
+ (warning "Automatic counterexample search timed out."; state)))
+
+end;