--- a/src/HOL/HOL.thy Tue Aug 31 21:00:57 2010 +0200
+++ b/src/HOL/HOL.thy Tue Aug 31 21:01:47 2010 +0200
@@ -30,6 +30,7 @@
"~~/src/Tools/induct.ML"
("~~/src/Tools/induct_tacs.ML")
("Tools/recfun_codegen.ML")
+ "Tools/try.ML"
begin
setup {* Intuitionistic.method_setup @{binding iprover} *}
--- a/src/HOL/Tools/try.ML Tue Aug 31 21:00:57 2010 +0200
+++ b/src/HOL/Tools/try.ML Tue Aug 31 21:01:47 2010 +0200
@@ -6,23 +6,24 @@
signature TRY =
sig
- val timeout : int Unsynchronized.ref
val invoke_try : Proof.state -> unit
end;
structure Try : TRY =
struct
-fun can_apply time pre post tac st =
+val timeout = Time.fromSeconds 5
+
+fun can_apply pre post tac st =
let val {goal, ...} = Proof.goal st in
- case TimeLimit.timeLimit time (Seq.pull o tac) (pre st) of
+ case TimeLimit.timeLimit timeout (Seq.pull o tac) (pre st) of
SOME (x, _) => nprems_of (post x) < nprems_of goal
| NONE => false
end
-fun do_generic command timeout pre post apply st =
+fun do_generic command pre post apply st =
let val timer = Timer.startRealTimer () in
- if can_apply timeout pre post apply st then
+ if can_apply pre post apply st then
SOME (command, Time.toMilliseconds (Timer.checkRealTimer timer))
else
NONE
@@ -36,8 +37,8 @@
Method.apply (named_method thy name) ctxt []
end
-fun do_named_method name timeout st =
- do_generic name timeout (#goal o Proof.goal) snd
+fun do_named_method name st =
+ do_generic name (#goal o Proof.goal) snd
(apply_named_method name (Proof.context_of st)) st
fun apply_named_method_on_first_goal name ctxt =
@@ -45,9 +46,9 @@
Proof.refine (Method.SelectGoals (1, Method.Basic (named_method thy name)))
end
-fun do_named_method_on_first_goal name timeout st =
+fun do_named_method_on_first_goal name st =
do_generic (name ^ (if nprems_of (#goal (Proof.goal st)) > 1 then "[1]"
- else "")) timeout I (#goal o Proof.goal)
+ else "")) I (#goal o Proof.goal)
(apply_named_method_on_first_goal name (Proof.context_of st)) st
val all_goals_named_methods = ["auto", "safe"]
@@ -59,12 +60,10 @@
fun time_string (s, ms) = s ^ ": " ^ string_of_int ms ^ " ms"
-val timeout = Unsynchronized.ref 5
-
fun invoke_try st =
- case do_methods |> Par_List.map (fn f => f (Time.fromSeconds (!timeout)) st)
+ case do_methods |> Par_List.map (fn f => f st)
|> map_filter I |> sort (int_ord o pairself snd) of
- [] => writeln "Tried."
+ [] => writeln "No proof found."
| xs as (s, _) :: _ =>
priority ("Try this command: " ^
Markup.markup Markup.sendback ("apply " ^ s) ^ ".\n" ^