more thorough, hybrid compression

--- 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,8 +156,7 @@
                 try the_single sub_steps
 
               (* only touch proofs that can be preplayed sucessfully *)
-              val Played time' =
-                Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l' meth')
+              val Played time' = forced_preplay_outcome_of_isar_step (!preplay_data) l'
 
               (* merge steps *)
               val subs'' = subs @ nontriv_subs
@@ -184,7 +183,7 @@
           if subproofs = [] then
             step
           else
-            (case Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth) of
+            (case forced_preplay_outcome_of_isar_step (!preplay_data) l of
               Played time => elim_one_subproof time qs fix l t lfs gfs meths subproofs []
             | _ => step)
 
@@ -224,13 +223,12 @@
               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_for_method (!preplay_data) l meth)
+              val Played time = forced_preplay_outcome_of_isar_step (!preplay_data) l
 
               val succs' = map (try_merge cand #> the) succs
 
-              val times0 = map2 ((fn Played time => time) o Lazy.force oo
-                preplay_outcome_of_isar_step_for_method (!preplay_data)) labels succ_meths
+              val times0 = map ((fn Played time => time) o
+                forced_preplay_outcome_of_isar_step (!preplay_data)) labels
               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_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,6 +22,7 @@
   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 forced_preplay_outcome_of_isar_step : isar_preplay_data -> label -> play_outcome
   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
@@ -181,14 +182,31 @@
     end
   | set_preplay_outcomes_of_isar_step _ _ _ _ _ = ()
 
+fun peek_at_outcome outcome = if Lazy.is_finished outcome then Lazy.force outcome else Not_Played
+
+(*
+*)
+fun forced_preplay_outcome_of_isar_step preplay_data l =
+  let
+    fun get_best_outcome_available get_one =
+      the (Canonical_Label_Tab.lookup preplay_data l)
+      |> map (apsnd get_one)
+      |> sort (play_outcome_ord o pairself snd)
+      |> hd |> snd
+  in
+    (case get_best_outcome_available peek_at_outcome of
+      Not_Played => get_best_outcome_available Lazy.force
+    | outcome => outcome)
+  end
+
 fun preplay_outcome_of_isar_step_for_method preplay_data l =
   the o AList.lookup (op =) (the (Canonical_Label_Tab.lookup preplay_data l))
 
 fun fastest_method_of_isar_step preplay_data =
-  Canonical_Label_Tab.lookup preplay_data #> the
-  #> map (fn (meth, outcome) =>
-       (meth, Time.toMilliseconds (case Lazy.force outcome of Played time => time | _ => one_year)))
-  #> sort (int_ord o pairself snd)
+  the o Canonical_Label_Tab.lookup preplay_data
+  #> tap (List.app (K () o Lazy.future Future.default_params o snd)) (* optional parallelism *)
+  #> map (apsnd Lazy.force)
+  #> sort (play_outcome_ord o pairself snd)
   #> hd #> fst
 
 fun forced_outcome_of_step preplay_data (Prove (_, _, l, _, _, (_, meths))) =

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML	Mon Feb 03 10:14:18 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML	Mon Feb 03 10:14:18 2014 +0100
@@ -27,8 +27,9 @@
 
   val string_of_reconstructor : reconstructor -> string
   val string_of_play_outcome : play_outcome -> string
+  val play_outcome_ord : play_outcome * play_outcome -> order
+
   val one_line_proof_text : int -> one_line_params -> string
-
   val silence_reconstructors : bool -> Proof.context -> Proof.context
 end;
 
@@ -63,6 +64,19 @@
   | string_of_play_outcome Play_Failed = "failed"
   | string_of_play_outcome _ = "unknown"
 
+fun play_outcome_ord (Played time1, Played time2) =
+    int_ord (pairself Time.toMilliseconds (time1, time2))
+  | play_outcome_ord (Played _, _) = LESS
+  | play_outcome_ord (_, Played _) = GREATER
+  | play_outcome_ord (Not_Played, Not_Played) = EQUAL
+  | play_outcome_ord (Not_Played, _) = LESS
+  | play_outcome_ord (_, Not_Played) = GREATER
+  | play_outcome_ord (Play_Timed_Out time1, Play_Timed_Out time2) =
+    int_ord (pairself Time.toMilliseconds (time1, time2))
+  | play_outcome_ord (Play_Timed_Out _, _) = LESS
+  | play_outcome_ord (_, Play_Timed_Out _) = GREATER
+  | play_outcome_ord (Play_Failed, Play_Failed) = EQUAL
+
 (* FIXME: Various bugs, esp. with "unfolding"
 fun unusing_chained_facts _ 0 = ""
   | unusing_chained_facts used_chaineds num_chained =