cascading timeout in parallel evaluation, to rapidly find optimum

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Wed Jul 30 23:52:56 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Thu Jul 31 00:45:55 2014 +0200
@@ -174,7 +174,7 @@
             in
               (case preplay_isar_step ctxt timeout hopeless step'' of
                 meths_outcomes as (_, Played time'') :: _ =>
-                (* l' successfully eliminated *)
+                (* "l'" successfully eliminated *)
                 (decrement_step_count ();
                  set_preplay_outcomes_of_isar_step ctxt time'' preplay_data step'' meths_outcomes;
                  map (replace_successor l' [l]) lfs';
@@ -215,13 +215,12 @@
                   val time_slice = time_mult (1.0 / Real.fromInt (length labels)) (reference_time l)
                   val timeouts =
                     map (adjust_merge_timeout preplay_timeout o curry Time.+ time_slice) times0
-                  val meths_outcomess =
-                    map3 (preplay_isar_step ctxt) timeouts hopelesses succs'
+                  val meths_outcomess = map3 (preplay_isar_step ctxt) timeouts hopelesses succs'
                 in
                   (case try (map (fn (_, Played time) :: _ => time)) meths_outcomess of
                     NONE => steps
                   | SOME times =>
-                    (* candidate successfully eliminated *)
+                    (* "l" successfully eliminated *)
                     (decrement_step_count ();
                      map3 (fn time => set_preplay_outcomes_of_isar_step ctxt time preplay_data)
                        times succs' meths_outcomess;

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Wed Jul 30 23:52:56 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Thu Jul 31 00:45:55 2014 +0200
@@ -41,6 +41,26 @@
 
 val trace = Attrib.setup_config_bool @{binding sledgehammer_preplay_trace} (K false)
 
+fun par_list_map_filter_with_timeout get_time timeout0 f xs =
+  let
+    val next_timeout = Unsynchronized.ref timeout0
+
+    fun apply_f x =
+      let val timeout = !next_timeout in
+        if timeout = Time.zeroTime then
+          NONE
+        else
+          let val y = f timeout x in
+            (case get_time y of
+              SOME time => next_timeout := time
+            | _ => ());
+            SOME y
+          end
+      end
+  in
+    map_filter I (Par_List.map apply_f xs)
+  end
+
 fun enrich_context_with_local_facts proof ctxt =
   let
     val thy = Proof_Context.theory_of ctxt
@@ -140,16 +160,16 @@
 fun preplay_isar_step_for_method ctxt timeout meth =
   try (raw_preplay_step_for_method ctxt timeout meth) #> the_default Play_Failed
 
-fun preplay_isar_step ctxt timeout hopeless step =
+fun preplay_isar_step ctxt timeout0 hopeless step =
   let
-    fun try_method meth =
-      (case preplay_isar_step_for_method ctxt timeout meth step of
-        outcome as Played _ => SOME (meth, outcome)
-      | _ => NONE)
+    fun preplay timeout meth = (meth, preplay_isar_step_for_method ctxt timeout meth step)
+    fun get_time (_, Played time) = SOME time
+      | get_time _ = NONE
 
     val meths = proof_methods_of_isar_step step |> subtract (op =) hopeless
   in
-    the_list (Par_List.get_some try_method meths)
+    par_list_map_filter_with_timeout get_time timeout0 preplay meths
+    |> sort (play_outcome_ord o pairself snd)
   end
 
 type isar_preplay_data = (proof_method * play_outcome Lazy.lazy) list Canonical_Label_Tab.table
@@ -181,7 +201,7 @@
   if Lazy.is_finished outcome then Lazy.force outcome else Play_Timed_Out Time.zeroTime
 
 fun get_best_method_outcome force =
-  tap (List.app (K () o Lazy.future Future.default_params o snd)) (* optional parallelism *)
+  tap (List.app (K () o Lazy.future Future.default_params o snd)) (* could be parallelized *)
   #> map (apsnd force)
   #> sort (play_outcome_ord o pairself snd)
   #> hd