# HG changeset patch
# User blanchet
# Date 1391551878 -3600
# Node ID 0e17e92248ac5eb3cf1354d2b3590999ec96046d
# Parent  3c7f3122ccdcf407315727a69c6420ff9488aa85
tweaked handling of 'hopeless' methods

diff -r 3c7f3122ccdc -r 0e17e92248ac src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Tue Feb 04 23:11:18 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Tue Feb 04 23:11:18 2014 +0100
@@ -76,30 +76,32 @@
 
 fun merge_methods preplay_data (l1, meths1) (l2, meths2) =
   let
-    fun is_method_hopeful l meth =
+    fun is_hopeful l meth =
       let val outcome = preplay_outcome_of_isar_step_for_method preplay_data l meth in
         not (Lazy.is_finished outcome) orelse
-        (case Lazy.force outcome of Played _ => true | _ => false)
+        (case Lazy.force outcome of Played _ => true | Play_Timed_Out _ => true | _ => false)
       end
+
+    val (hopeful, hopeless) =
+      meths2 @ subtract (op =) meths2 meths1
+      |> List.partition (is_hopeful l1 andf is_hopeful l2)
   in
-    meths2 @ subtract (op =) meths2 meths1
-    |> List.partition (is_method_hopeful l1 andf is_method_hopeful l2)
-    |> op @
+    (hopeful @ hopeless, hopeless)
   end
 
-fun try_merge preplay_data (Prove (_, [], l1, _, subproofs1, (lfs1, gfs1), meths1, comment1))
+fun try_merge_steps preplay_data (Prove (_, [], l1, _, subproofs1, (lfs1, gfs1), meths1, comment1))
       (Prove (qs2, fix, l2, t, subproofs2, (lfs2, gfs2), meths2, comment2)) =
     (case merge_methods preplay_data (l1, meths1) (l2, meths2) of
-      [] => NONE
-    | meths =>
+      ([], _) => NONE
+    | (meths, hopeless) =>
       let
         val lfs = union (op =) lfs1 (remove (op =) l1 lfs2)
         val gfs = union (op =) gfs1 gfs2
       in
         SOME (Prove (qs2, fix, l2, t, subproofs1 @ subproofs2, (lfs, gfs), meths,
-          comment1 ^ comment2))
+          comment1 ^ comment2), hopeless)
       end)
-  | try_merge _ _ _ = NONE
+  | try_merge_steps _ _ _ = NONE
 
 val compress_degree = 2
 val merge_timeout_slack_time = seconds 0.005
@@ -173,12 +175,14 @@
               val subs'' = subs @ nontriv_subs
               val lfs'' = union (op =) lfs (subtract (op =) (map fst assms) lfs')
               val gfs'' = union (op =) gfs' gfs
-              val meths'' as _ :: _ = merge_methods (!preplay_data) (l', meths') (l, meths)
+              val (meths'' as _ :: _, hopeless) =
+                merge_methods (!preplay_data) (l', meths') (l, meths)
               val step'' = Prove (qs, fix, l, t, subs'', (lfs'', gfs''), meths'', comment)
 
               (* check if the modified step can be preplayed fast enough *)
               val timeout = slackify_merge_timeout (Time.+ (time, time'))
-              val (_, Played time'') :: meths_outcomes = preplay_isar_step ctxt timeout step''
+              val (_, Played time'') :: meths_outcomes =
+                preplay_isar_step ctxt timeout hopeless step''
             in
               decrement_step_count (); (* l' successfully eliminated! *)
               map (replace_successor l' [l]) lfs';
@@ -231,7 +235,9 @@
               (* only touch steps that can be preplayed successfully; FIXME: more generous *)
               val Played time = forced_intermediate_preplay_outcome_of_isar_step (!preplay_data) l
 
-              val succs' = map (try_merge (!preplay_data) cand #> the) succs
+              val (succs', hopelesses) =
+                map (try_merge_steps (!preplay_data) cand #> the) succs
+                |> split_list
 
               (* FIXME: more generous *)
               val times0 = map ((fn Played time => time) o
@@ -240,7 +246,7 @@
               val timeouts = map (curry Time.+ time_slice #> slackify_merge_timeout) times0
               (* FIXME: "preplay_timeout" should be an ultimate maximum *)
 
-              val meths_outcomess = map2 (preplay_isar_step ctxt) timeouts succs'
+              val meths_outcomess = map3 (preplay_isar_step ctxt) timeouts hopelesses succs'
 
               (* ensure none of the modified successors timed out *)
               val times = map (fn (_, Played time) :: _ => time) meths_outcomess
diff -r 3c7f3122ccdc -r 0e17e92248ac src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Tue Feb 04 23:11:18 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Tue Feb 04 23:11:18 2014 +0100
@@ -20,7 +20,7 @@
   val enrich_context_with_local_facts : isar_proof -> Proof.context -> Proof.context
   val preplay_isar_step_for_method : Proof.context -> Time.time -> proof_method -> isar_step ->
     play_outcome
-  val preplay_isar_step : Proof.context -> Time.time -> isar_step ->
+  val preplay_isar_step : Proof.context -> Time.time -> proof_method list -> isar_step ->
     (proof_method * play_outcome) list
   val set_preplay_outcomes_of_isar_step : Proof.context -> Time.time ->
     isar_preplay_data Unsynchronized.ref -> isar_step -> (proof_method * play_outcome) list -> unit
@@ -140,14 +140,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 step =
+fun preplay_isar_step ctxt timeout 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)
+
+    val meths = proof_methods_of_isar_step step |> subtract (op =) hopeless
   in
-    the_list (Par_List.get_some try_method (proof_methods_of_isar_step step))
+    the_list (Par_List.get_some try_method meths)
   end
 
 type isar_preplay_data = (proof_method * play_outcome Lazy.lazy) list Canonical_Label_Tab.table