renamed "metis_timeout" to "preplay_timeout" and continued implementation

--- 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
@@ -88,7 +88,7 @@
    ("isar_proof", "false"),
    ("isar_shrink_factor", "1"),
    ("slicing", "true"),
-   ("metis_timeout", "5")]
+   ("preplay_timeout", "5")]
 
 val alias_params =
   [("prover", "provers"),
@@ -107,7 +107,7 @@
 val params_for_minimize =
   ["debug", "verbose", "overlord", "type_sys", "full_types", "max_mono_iters",
    "max_new_mono_instances", "isar_proof", "isar_shrink_factor", "timeout",
-   "metis_timeout"]
+   "preplay_timeout"]
 
 val property_dependent_params = ["provers", "full_types", "timeout"]
 
@@ -277,8 +277,9 @@
     val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor")
     val slicing = not auto andalso lookup_bool "slicing"
     val timeout = (if auto then NONE else lookup_time "timeout") |> the_timeout
-    val metis_timeout =
-      if auto then Time.zeroTime else lookup_time "metis_timeout" |> the_timeout
+    val preplay_timeout =
+      if auto then Time.zeroTime
+      else lookup_time "preplay_timeout" |> the_timeout
     val expect = lookup_string "expect"
   in
     {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
@@ -287,7 +288,7 @@
      max_new_mono_instances = max_new_mono_instances, type_sys = type_sys,
      explicit_apply = explicit_apply, isar_proof = isar_proof,
      isar_shrink_factor = isar_shrink_factor, slicing = slicing,
-     timeout = timeout, metis_timeout = metis_timeout, expect = expect}
+     timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
   end
 
 fun get_params auto ctxt = extract_params auto (default_raw_params ctxt)

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Fri May 27 10:30:08 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Fri May 27 10:30:08 2011 +0200
@@ -44,7 +44,7 @@
 
 fun test_facts ({debug, verbose, overlord, provers, max_mono_iters,
                  max_new_mono_instances, type_sys, isar_proof,
-                 isar_shrink_factor, metis_timeout, ...} : params)
+                 isar_shrink_factor, preplay_timeout, ...} : params)
         explicit_apply_opt silent (prover : prover) timeout i n state facts =
   let
     val ctxt = Proof.context_of state
@@ -70,7 +70,7 @@
        max_mono_iters = max_mono_iters,
        max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
        isar_shrink_factor = isar_shrink_factor, slicing = false,
-       timeout = timeout, metis_timeout = metis_timeout, expect = ""}
+       timeout = timeout, preplay_timeout = preplay_timeout, expect = ""}
     val facts =
       facts |> maps (fn (n, ths) => ths |> map (Untranslated_Fact o pair n))
     val problem =

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri May 27 10:30:08 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri May 27 10:30:08 2011 +0200
@@ -35,7 +35,7 @@
      isar_shrink_factor: int,
      slicing: bool,
      timeout: Time.time,
-     metis_timeout: Time.time,
+     preplay_timeout: Time.time,
      expect: string}
 
   datatype prover_fact =
@@ -279,7 +279,7 @@
    isar_shrink_factor: int,
    slicing: bool,
    timeout: Time.time,
-   metis_timeout: Time.time,
+   preplay_timeout: Time.time,
    expect: string}
 
 datatype prover_fact =
@@ -870,23 +870,32 @@
       end
   in do_slice timeout 1 NONE Time.zeroTime end
 
-(* taken from "Mirabelle" and generalized *)
-fun can_apply timeout tac state i =
+(* based on "Mirabelle.can_apply" and generalized *)
+fun try_apply timeout tac state i =
   let
     val {context = ctxt, facts, goal} = Proof.goal state
     val full_tac = Method.insert_tac facts i THEN tac ctxt i
-  in
-    case try (TimeLimit.timeLimit timeout (Seq.pull o full_tac)) goal of
-      SOME (SOME _) => true
-    | _ => false
+  in try (TimeLimit.timeLimit timeout (Seq.pull o full_tac)) goal end
+
+fun try_metis debug timeout ths =
+  try_apply timeout (Config.put Metis_Tactics.verbose debug
+                     #> (fn ctxt => Metis_Tactics.metis_tac ctxt ths))
+
+datatype metis_try =
+  Preplayed of string * Time.time |
+  Preplay_Timed_Out |
+  Preplay_Failed
+
+fun preplay debug timeout ths state i =
+  let val timer = Timer.startRealTimer () in
+    case try_metis debug timeout ths state i of
+      SOME (SOME _) => Preplayed ("metis", Timer.checkRealTimer timer)
+    | SOME NONE => Preplay_Failed
+    | NONE => Preplay_Timed_Out
   end
 
-fun can_apply_metis debug timeout ths =
-  can_apply timeout (Config.put Metis_Tactics.verbose debug
-                     #> (fn ctxt => Metis_Tactics.metis_tac ctxt ths))
-
 fun run_smt_solver auto name
-        (params as {debug, verbose, blocking, metis_timeout, ...})
+        (params as {debug, verbose, blocking, preplay_timeout, ...})
         minimize_command
         ({state, subgoal, subgoal_count, facts, smt_filter, ...}
          : prover_problem) =
@@ -903,13 +912,13 @@
       case outcome of
         NONE =>
         let
-          val (method, settings) =
-            if can_apply_metis debug metis_timeout (map snd used_facts) state
-                               subgoal then
-              ("metis", "")
-            else
-              ("smt", if name = SMT_Solver.solver_name_of ctxt then ""
-                      else "smt_solver = " ^ maybe_quote name)
+          val (settings, method, time) =
+            case preplay debug preplay_timeout (map snd used_facts) state
+                         subgoal of
+              Preplayed (method, time) => (method, "", SOME time)
+            | _ => (if name = SMT_Solver.solver_name_of ctxt then ""
+                    else "smt_solver = " ^ maybe_quote name,
+                    "smt", NONE)
         in
           try_command_line (proof_banner auto blocking name)
               (apply_on_subgoal settings subgoal subgoal_count ^