"try" -- a new diagnosis tool that tries to apply several methods in parallel

--- a/src/HOL/IsaMakefile	Tue Aug 31 20:23:32 2010 +0200
+++ b/src/HOL/IsaMakefile	Tue Aug 31 20:24:28 2010 +0200
@@ -213,6 +213,7 @@
   Tools/sat_funcs.ML \
   Tools/sat_solver.ML \
   Tools/split_rule.ML \
+  Tools/try.ML \
   Tools/typedef.ML \
   Transitive_Closure.thy \
   Typedef.thy \

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/try.ML	Tue Aug 31 20:24:28 2010 +0200
@@ -0,0 +1,80 @@
+(*  Title:      HOL/Tools/try.ML
+    Author:     Jasmin Blanchette, TU Muenchen
+
+Try a combination of proof methods.
+*)
+
+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 =
+  let val {goal, ...} = Proof.goal st in
+    case TimeLimit.timeLimit time (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 =
+  let val timer = Timer.startRealTimer () in
+    if can_apply timeout pre post apply st then
+      SOME (command, Time.toMilliseconds (Timer.checkRealTimer timer))
+    else
+      NONE
+  end
+
+fun named_method thy name =
+  Method.method thy (Args.src ((name, []), Position.none))
+
+fun apply_named_method name ctxt =
+  let val thy = ProofContext.theory_of ctxt in
+    Method.apply (named_method thy name) ctxt []
+  end
+
+fun do_named_method name timeout st =
+  do_generic name timeout (#goal o Proof.goal) snd
+             (apply_named_method name (Proof.context_of st)) st
+
+fun apply_named_method_on_first_goal name ctxt =
+  let val thy = ProofContext.theory_of ctxt in
+    Proof.refine (Method.SelectGoals (1, Method.Basic (named_method thy name)))
+  end
+
+fun do_named_method_on_first_goal name timeout st =
+  do_generic (name ^ (if nprems_of (#goal (Proof.goal st)) > 1 then "[1]"
+                      else "")) timeout I (#goal o Proof.goal)
+             (apply_named_method_on_first_goal name (Proof.context_of st)) st
+
+val all_goals_named_methods = ["auto", "safe"]
+val first_goal_named_methods =
+  ["simp", "fast", "fastsimp", "force", "best", "blast"]
+val do_methods =
+  map do_named_method_on_first_goal all_goals_named_methods @
+  map do_named_method first_goal_named_methods
+
+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)
+                  |> map_filter I |> sort (int_ord o pairself snd) of
+    [] => writeln "Tried."
+  | xs as (s, _) :: _ =>
+    priority ("Try this command: " ^
+              Markup.markup Markup.sendback ("apply " ^ s) ^ ".\n" ^
+              "(" ^ space_implode "; " (map time_string xs) ^ ")\n")
+
+val tryN = "try"
+
+val _ =
+  Outer_Syntax.improper_command tryN
+      "try a combination of proof methods" Keyword.diag
+      (Scan.succeed (Toplevel.keep (invoke_try o Toplevel.proof_of)))
+
+end;