--- a/src/HOL/IsaMakefile Fri May 27 10:30:08 2011 +0200
+++ b/src/HOL/IsaMakefile Fri May 27 10:30:08 2011 +0200
@@ -138,7 +138,6 @@
$(SRC)/Tools/IsaPlanner/rw_tools.ML \
$(SRC)/Tools/IsaPlanner/zipper.ML \
$(SRC)/Tools/atomize_elim.ML \
- $(SRC)/Tools/auto_tools.ML \
$(SRC)/Tools/case_product.ML \
$(SRC)/Tools/coherent.ML \
$(SRC)/Tools/cong_tac.ML \
@@ -151,6 +150,7 @@
$(SRC)/Tools/project_rule.ML \
$(SRC)/Tools/quickcheck.ML \
$(SRC)/Tools/solve_direct.ML \
+ $(SRC)/Tools/try.ML \
$(SRC)/Tools/value.ML \
HOL.thy \
Tools/hologic.ML \
--- a/src/HOL/Mutabelle/MutabelleExtra.thy Fri May 27 10:30:08 2011 +0200
+++ b/src/HOL/Mutabelle/MutabelleExtra.thy Fri May 27 10:30:08 2011 +0200
@@ -26,7 +26,7 @@
nitpick_params [timeout = 5, sat_solver = MiniSat, no_overlord, verbose, card = 1-5, iter = 1,2,4,8,12]
refute_params [maxtime = 10, minsize = 1, maxsize = 5, satsolver = jerusat]
*)
-ML {* Auto_Tools.time_limit := 10.0 *}
+ML {* Try.auto_time_limit := 10.0 *}
ML {* val mtds = [
MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.finite_types false) "random",
--- a/src/HOL/Mutabelle/mutabelle_extra.ML Fri May 27 10:30:08 2011 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Fri May 27 10:30:08 2011 +0200
@@ -119,7 +119,7 @@
(** quickcheck **)
fun invoke_quickcheck change_options quickcheck_generator thy t =
- TimeLimit.timeLimit (seconds (!Auto_Tools.time_limit))
+ TimeLimit.timeLimit (seconds (!Try.auto_time_limit))
(fn _ =>
let
val [result] = Quickcheck.test_goal_terms (change_options (Proof_Context.init_global thy))
@@ -130,7 +130,7 @@
| SOME _ => (GenuineCex, Quickcheck.timings_of result)
end) ()
handle TimeLimit.TimeOut =>
- (Timeout, [("timelimit", Real.floor (!Auto_Tools.time_limit))])
+ (Timeout, [("timelimit", Real.floor (!Try.auto_time_limit))])
fun quickcheck_mtd change_options quickcheck_generator =
("quickcheck_" ^ quickcheck_generator, invoke_quickcheck change_options quickcheck_generator)
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Fri May 27 10:30:08 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Fri May 27 10:30:08 2011 +0200
@@ -397,6 +397,6 @@
val auto_nitpick = pick_nits [] true 1 0
-val setup = Auto_Tools.register_tool (auto, auto_nitpick)
+val setup = Try.register_tool (auto, auto_nitpick)
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri May 27 10:30:08 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri May 27 10:30:08 2011 +0200
@@ -408,6 +408,6 @@
(minimize_command [] 1) state
end
-val setup = Auto_Tools.register_tool (auto, auto_sledgehammer)
+val setup = Try.register_tool (auto, auto_sledgehammer)
end;
--- a/src/HOL/Tools/try_methods.ML Fri May 27 10:30:08 2011 +0200
+++ b/src/HOL/Tools/try_methods.ML Fri May 27 10:30:08 2011 +0200
@@ -177,6 +177,6 @@
val auto_try_methods = do_try_methods true NONE ([], [], [], [])
-val setup = Auto_Tools.register_tool (auto, auto_try_methods)
+val setup = Try.register_tool (auto, auto_try_methods)
end;
--- a/src/Tools/Code_Generator.thy Fri May 27 10:30:08 2011 +0200
+++ b/src/Tools/Code_Generator.thy Fri May 27 10:30:08 2011 +0200
@@ -8,7 +8,7 @@
imports Pure
uses
"~~/src/Tools/cache_io.ML"
- "~~/src/Tools/auto_tools.ML"
+ "~~/src/Tools/try.ML"
"~~/src/Tools/solve_direct.ML"
"~~/src/Tools/quickcheck.ML"
"~~/src/Tools/value.ML"
--- a/src/Tools/auto_tools.ML Fri May 27 10:30:08 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,71 +0,0 @@
-(* Title: Tools/auto_tools.ML
- Author: Jasmin Blanchette, TU Muenchen
-
-Manager for tools that should be run automatically on newly entered conjectures.
-*)
-
-signature AUTO_TOOLS =
-sig
- val time_limit: real Unsynchronized.ref
-
- val register_tool :
- bool Unsynchronized.ref * (Proof.state -> bool * Proof.state) -> theory
- -> theory
-end;
-
-structure Auto_Tools : AUTO_TOOLS =
-struct
-
-(* preferences *)
-
-val time_limit = Unsynchronized.ref 4.0
-
-val auto_tools_time_limitN = "auto-tools-time-limit"
-val _ =
- ProofGeneralPgip.add_preference Preferences.category_tracing
- (Preferences.real_pref time_limit
- auto_tools_time_limitN "Time limit for automatic tools (in seconds).")
-
-
-(* configuration *)
-
-structure Data = Theory_Data
-(
- type T = (bool Unsynchronized.ref * (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 *)
-
-fun run_tools tools state =
- tools |> map_filter (fn (auto, tool) => if !auto then SOME tool else NONE)
- |> Par_List.get_some (fn tool =>
- case try tool state of
- SOME (true, state) => SOME state
- | _ => NONE)
- |> the_default state
-
-(* Too large values are understood as milliseconds, ensuring compatibility with
- old setting files. No users can possibly in their right mind want the user
- interface to block for more than 100 seconds. *)
-fun smart_seconds r =
- seconds (if r >= 100.0 then
- (legacy_feature (quote auto_tools_time_limitN ^
- " expressed in milliseconds -- use seconds instead"); 0.001 * r)
- else
- r)
-
-val _ = Context.>> (Specification.add_theorem_hook (fn interact => fn state =>
- if interact andalso not (!Toplevel.quiet) andalso !time_limit > 0.0 then
- TimeLimit.timeLimit (smart_seconds (!time_limit))
- (run_tools (Data.get (Proof.theory_of state))) state
- handle TimeLimit.TimeOut => state
- else
- state))
-
-end;
--- a/src/Tools/quickcheck.ML Fri May 27 10:30:08 2011 +0200
+++ b/src/Tools/quickcheck.ML Fri May 27 10:30:08 2011 +0200
@@ -530,7 +530,7 @@
(false, state)
end
-val setup = Auto_Tools.register_tool (auto, auto_quickcheck)
+val setup = Try.register_tool (auto, auto_quickcheck)
(* Isar commands *)
--- a/src/Tools/solve_direct.ML Fri May 27 10:30:08 2011 +0200
+++ b/src/Tools/solve_direct.ML Fri May 27 10:30:08 2011 +0200
@@ -97,8 +97,8 @@
(* hook *)
-val auto_solve_direct = solve_direct true
+val auto_solve_direct = solve_direct true;
-val setup = Auto_Tools.register_tool (auto, auto_solve_direct);
+val setup = Try.register_tool (auto, auto_solve_direct);
end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/try.ML Fri May 27 10:30:08 2011 +0200
@@ -0,0 +1,71 @@
+(* Title: Tools/try.ML
+ Author: Jasmin Blanchette, TU Muenchen
+
+Manager for tools that should be tried on conjectures.
+*)
+
+signature TRY =
+sig
+ val auto_time_limit: real Unsynchronized.ref
+
+ val register_tool :
+ bool Unsynchronized.ref * (Proof.state -> bool * Proof.state) -> theory
+ -> theory
+end;
+
+structure Try : TRY =
+struct
+
+(* preferences *)
+
+val auto_time_limit = Unsynchronized.ref 4.0
+
+val auto_try_time_limitN = "auto-try-time-limit"
+val _ =
+ ProofGeneralPgip.add_preference Preferences.category_tracing
+ (Preferences.real_pref auto_time_limit
+ auto_try_time_limitN "Time limit for automatically tried tools (in seconds).")
+
+
+(* configuration *)
+
+structure Data = Theory_Data
+(
+ type T = (bool Unsynchronized.ref * (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 *)
+
+fun run_tools tools state =
+ tools |> map_filter (fn (auto, tool) => if !auto then SOME tool else NONE)
+ |> Par_List.get_some (fn tool =>
+ case try tool state of
+ SOME (true, state) => SOME state
+ | _ => NONE)
+ |> the_default state
+
+(* Too large values are understood as milliseconds, ensuring compatibility with
+ old setting files. No users can possibly in their right mind want the user
+ interface to block for more than 100 seconds. *)
+fun smart_seconds r =
+ seconds (if r >= 100.0 then
+ (legacy_feature (quote auto_try_time_limitN ^
+ " expressed in milliseconds -- use seconds instead"); 0.001 * r)
+ else
+ r)
+
+val _ = Context.>> (Specification.add_theorem_hook (fn interact => fn state =>
+ if interact andalso not (!Toplevel.quiet) andalso !auto_time_limit > 0.0 then
+ TimeLimit.timeLimit (smart_seconds (!auto_time_limit))
+ (run_tools (Data.get (Proof.theory_of state))) state
+ handle TimeLimit.TimeOut => state
+ else
+ state))
+
+end;