centralize more preplaying

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Feb 03 10:14:18 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Feb 03 10:14:18 2014 +0100
@@ -296,7 +296,7 @@
 
         fun str_of_meth l meth =
           string_of_proof_method meth ^ " " ^
-          str_of_preplay_outcome (preplay_outcome_of_isar_step (!preplay_data) l meth)
+          str_of_preplay_outcome (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth)
         fun comment_of l = map (str_of_meth l) #> commas
 
         fun trace_isar_proof label proof =
@@ -314,7 +314,8 @@
           |> try0_isar ? try0_isar_proof ctxt preplay_timeout preplay_data
           |> tap (trace_isar_proof "Tried0")
           |> postprocess_isar_proof_remove_unreferenced_steps
-               (try0_isar ? minimize_isar_step_dependencies ctxt preplay_data)
+               (keep_fastest_method_of_isar_step (!preplay_data)
+                #> try0_isar(*### minimize*) ? minimize_isar_step_dependencies ctxt preplay_data)
           |> tap (trace_isar_proof "Minimized")
           |> `(preplay_outcome_of_isar_proof (!preplay_data))
           ||> chain_isar_proof

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Mon Feb 03 10:14:18 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Mon Feb 03 10:14:18 2014 +0100
@@ -156,7 +156,8 @@
                 try the_single sub_steps
 
               (* only touch proofs that can be preplayed sucessfully *)
-              val Played time' = Lazy.force (preplay_outcome_of_isar_step (!preplay_data) l' meth')
+              val Played time' =
+                Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l' meth')
 
               (* merge steps *)
               val subs'' = subs @ nontriv_subs
@@ -183,7 +184,7 @@
           if subproofs = [] then
             step
           else
-            (case Lazy.force (preplay_outcome_of_isar_step (!preplay_data) l meth) of
+            (case Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth) of
               Played time => elim_one_subproof time qs fix l t lfs gfs meths subproofs []
             | _ => step)
 
@@ -223,12 +224,13 @@
               val succ_meths = map (hd o snd o the o byline_of_isar_step) succs
 
               (* only touch steps that can be preplayed successfully *)
-              val Played time = Lazy.force (preplay_outcome_of_isar_step (!preplay_data) l meth)
+              val Played time =
+                Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth)
 
               val succs' = map (try_merge cand #> the) succs
 
               val times0 = map2 ((fn Played time => time) o Lazy.force oo
-                preplay_outcome_of_isar_step (!preplay_data)) labels succ_meths
+                preplay_outcome_of_isar_step_for_method (!preplay_data)) labels succ_meths
               val time_slice = time_mult (1.0 / (Real.fromInt (length labels))) time
               val timeouts = map (curry Time.+ time_slice #> time_mult merge_timeout_slack) times0
 

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Mon Feb 03 10:14:18 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Mon Feb 03 10:14:18 2014 +0100
@@ -11,6 +11,7 @@
   type isar_proof = Sledgehammer_Isar_Proof.isar_proof
   type isar_preplay_data = Sledgehammer_Isar_Preplay.isar_preplay_data
 
+  val keep_fastest_method_of_isar_step : isar_preplay_data -> isar_step -> isar_step
   val minimize_isar_step_dependencies : Proof.context -> isar_preplay_data Unsynchronized.ref ->
     isar_step -> isar_step
   val postprocess_isar_proof_remove_unreferenced_steps : (isar_step -> isar_step) -> isar_proof ->
@@ -24,12 +25,16 @@
 open Sledgehammer_Isar_Proof
 open Sledgehammer_Isar_Preplay
 
+fun keep_fastest_method_of_isar_step preplay_data
+      (Prove (qs, xs, l, t, subproofs, (facts, _))) =
+    Prove (qs, xs, l, t, subproofs, (facts, [fastest_method_of_isar_step preplay_data l]))
+  | keep_fastest_method_of_isar_step _ step = step
+
 val slack = seconds 0.1
 
-fun minimize_isar_step_dependencies _ _ (step as Let _) = step
-  | minimize_isar_step_dependencies ctxt preplay_data
+fun minimize_isar_step_dependencies ctxt preplay_data
       (step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meths as meth :: _))) =
-    (case Lazy.force (preplay_outcome_of_isar_step (!preplay_data) l meth) of
+    (case Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth) of
       Played time =>
       let
         fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meths))
@@ -51,6 +56,7 @@
         step'
       end
     | _ => step (* don't touch steps that time out or fail *))
+  | minimize_isar_step_dependencies _ _ step = step
 
 fun postprocess_isar_proof_remove_unreferenced_steps postproc_step =
   let

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Mon Feb 03 10:14:18 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Mon Feb 03 10:14:18 2014 +0100
@@ -22,8 +22,9 @@
   val set_preplay_outcomes_of_isar_step : Proof.context -> Time.time ->
     isar_preplay_data Unsynchronized.ref -> isar_step ->
     (proof_method * play_outcome Lazy.lazy) list -> unit
-  val preplay_outcome_of_isar_step : isar_preplay_data -> label -> proof_method ->
+  val preplay_outcome_of_isar_step_for_method : isar_preplay_data -> label -> proof_method ->
     play_outcome Lazy.lazy
+  val fastest_method_of_isar_step : isar_preplay_data -> label -> proof_method
   val preplay_outcome_of_isar_proof : isar_preplay_data -> isar_proof -> play_outcome
 end;
 
@@ -180,16 +181,20 @@
     end
   | set_preplay_outcomes_of_isar_step _ _ _ _ _ = ()
 
-fun preplay_outcome_of_isar_step preplay_data l meth =
-  (case Canonical_Label_Tab.lookup preplay_data l of
-    SOME meths_outcomes =>
-    (case AList.lookup (op =) meths_outcomes meth of
-      SOME outcome => outcome
-    | NONE => raise Fail "Sledgehammer_Isar_Preplay: missing method")
-  | NONE => raise Fail "Sledgehammer_Isar_Preplay: missing label")
+fun preplay_outcome_of_isar_step_for_method preplay_data l meth =
+  let val SOME meths_outcomes = Canonical_Label_Tab.lookup preplay_data l in
+    the (AList.lookup (op =) meths_outcomes meth)
+  end
 
-fun forced_outcome_of_step preplay_data (Prove (_, _, l, _, _, (_, meth :: _))) =
-    Lazy.force (preplay_outcome_of_isar_step preplay_data l meth)
+fun fastest_method_of_isar_step preplay_data l =
+  the (Canonical_Label_Tab.lookup preplay_data l)
+  |> map (fn (meth, outcome) =>
+       (meth, Time.toMilliseconds (case Lazy.force outcome of Played time => time | _ => one_year)))
+  |> sort (int_ord o pairself snd)
+  |> hd |> fst
+
+fun forced_outcome_of_step preplay_data (Prove (_, _, l, _, _, (_, meths))) =
+    Lazy.force (preplay_outcome_of_isar_step_for_method preplay_data l (the_single meths))
   | forced_outcome_of_step _ _ = Played Time.zeroTime
 
 fun preplay_outcome_of_isar_proof preplay_data (Proof (_, _, steps)) =

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML	Mon Feb 03 10:14:18 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML	Mon Feb 03 10:14:18 2014 +0100
@@ -33,7 +33,7 @@
       (step as Prove (_, _, l, _, _, (_, meths as meth :: _))) =
     let
       val timeout =
-        (case Lazy.force (preplay_outcome_of_isar_step (!preplay_data) l meth) of
+        (case Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth) of
           Played time => Time.+ (time, slack)
         | _ => preplay_timeout)