# HG changeset patch
# User blanchet
# Date 1391423453 -3600
# Node ID 73372494fd80b47812306674e0547e53f9286f7b
# Parent  93c7fcfbe6f5b13232433913995eb4d24f6fd2ee
more flexible compression, choosing whichever proof method works

diff -r 93c7fcfbe6f5 -r 73372494fd80 src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Mon Feb 03 10:19:19 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Mon Feb 03 11:30:53 2014 +0100
@@ -95,7 +95,7 @@
 
 val compress_degree = 2
 val merge_timeout_slack_time = seconds 0.005
-val merge_timeout_slack_factor = 1.5
+val merge_timeout_slack_factor = 1.25
 
 fun slackify_merge_timeout time =
   time_mult merge_timeout_slack_factor (Time.+ (merge_timeout_slack_time, time))
@@ -146,8 +146,7 @@
             val subproofs = List.revAppend (nontriv_subs, subs)
             val step = Prove (qs, fix, l, t, subproofs, ((lfs, gfs), meths))
           in
-            set_preplay_outcomes_of_isar_step ctxt time preplay_data step
-              [(meth, Lazy.value (Played time))];
+            set_preplay_outcomes_of_isar_step ctxt time preplay_data step [(meth, Played time)];
             step
           end
         else
@@ -169,7 +168,7 @@
 
               (* check if the modified step can be preplayed fast enough *)
               val timeout = slackify_merge_timeout (Time.+ (time, time'))
-              val Played time'' = preplay_isar_step ctxt timeout (hd meths)(*FIXME*) step''
+              val outcomes as (_, Played time'') :: _ = preplay_isar_step ctxt timeout step''
             in
               decrement_step_count (); (* l' successfully eliminated! *)
               map (replace_successor l' [l]) lfs';
@@ -221,7 +220,6 @@
               val ((cand as Prove (_, _, _, _, _, ((lfs, _), _))) :: steps') = drop i steps
 
               val succs = collect_successors steps' labels
-              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 = forced_intermediate_preplay_outcome_of_isar_step (!preplay_data) l
@@ -233,23 +231,18 @@
               val time_slice = time_mult (1.0 / (Real.fromInt (length labels))) time
               val timeouts = map (curry Time.+ time_slice #> slackify_merge_timeout) times0
 
-              (* TODO: should be lazy: stop preplaying as soon as one step fails/times out *)
-              val play_outcomes = map3 (preplay_isar_step ctxt) timeouts succ_meths succs'
+              val meths_outcomess = map2 (preplay_isar_step ctxt) timeouts succs'
 
               (* ensure none of the modified successors timed out *)
-              val times = map (fn Played time => time) play_outcomes
+              val times = map (fn (_, Played time) :: _ => time) meths_outcomess
 
               val (steps1, _ :: steps2) = chop i steps
               (* replace successors with their modified versions *)
               val steps2 = update_steps steps2 succs'
-
-              val succ_meths_outcomess =
-                map2 (fn meth => fn outcome => [(meth, Lazy.value outcome)]) succ_meths
-                  play_outcomes
             in
               decrement_step_count (); (* candidate successfully eliminated *)
               map3 (fn time => set_preplay_outcomes_of_isar_step ctxt time preplay_data) times
-                succs' succ_meths_outcomess;
+                succs' meths_outcomess;
               map (replace_successor l labels) lfs;
               (* removing the step would mess up the indices; replace with dummy step instead *)
               steps1 @ dummy_isar_step :: steps2
diff -r 93c7fcfbe6f5 -r 73372494fd80 src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Mon Feb 03 10:19:19 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Mon Feb 03 11:30:53 2014 +0100
@@ -41,7 +41,7 @@
 
         fun minimize_facts _ time min_facts [] = (time, min_facts)
           | minimize_facts mk_step time min_facts (f :: facts) =
-            (case preplay_isar_step ctxt (Time.+ (time, slack)) meth
+            (case preplay_isar_step_for_method ctxt (Time.+ (time, slack)) meth
                 (mk_step (min_facts @ facts)) of
               Played time => minimize_facts mk_step time min_facts facts
             | _ => minimize_facts mk_step time (f :: min_facts) facts)
@@ -51,8 +51,7 @@
 
         val step' = mk_step_lfs_gfs min_lfs min_gfs
       in
-        set_preplay_outcomes_of_isar_step ctxt time preplay_data step'
-          [(meth, Lazy.value (Played time))];
+        set_preplay_outcomes_of_isar_step ctxt time preplay_data step' [(meth, Played time)];
         step'
       end
     | _ => step (* don't touch steps that time out or fail *))
diff -r 93c7fcfbe6f5 -r 73372494fd80 src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Mon Feb 03 10:19:19 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Mon Feb 03 11:30:53 2014 +0100
@@ -18,10 +18,12 @@
   type isar_preplay_data
 
   val enrich_context_with_local_facts : isar_proof -> Proof.context -> Proof.context
-  val preplay_isar_step : Proof.context -> Time.time -> proof_method -> isar_step -> play_outcome
+  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 ->
+    (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 Lazy.lazy) list -> unit
+    isar_preplay_data Unsynchronized.ref -> isar_step -> (proof_method * play_outcome) list -> unit
   val forced_intermediate_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
@@ -120,7 +122,8 @@
     | _ => raise Fail "Sledgehammer_Isar_Preplay: tac_of_method"))
 
 (* main function for preplaying Isar steps; may throw exceptions *)
-fun raw_preplay_step ctxt timeout meth (Prove (_, xs, _, t, subproofs, (fact_names, _))) =
+fun raw_preplay_step_for_method ctxt timeout meth
+    (Prove (_, xs, _, t, subproofs, (fact_names, _))) =
   let
     val goal =
       (case xs of
@@ -156,8 +159,20 @@
      play_outcome)
   end
 
-fun preplay_isar_step ctxt timeout meth =
-  try (raw_preplay_step ctxt timeout meth) #> the_default Play_Failed
+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 =
+  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 = snd (byline_of_isar_step step)
+  in
+    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
 
@@ -173,9 +188,11 @@
 fun set_preplay_outcomes_of_isar_step ctxt timeout preplay_data
       (step as Prove (_, _, l, _, _, (_, meths))) meths_outcomes0 =
     let
-      fun preplay meth = Lazy.lazy (fn () => preplay_isar_step ctxt timeout meth step)
-      val meths_outcomes =
-        fold (fn meth => AList.default (op =) (meth, preplay meth)) meths meths_outcomes0
+      fun lazy_preplay meth =
+        Lazy.lazy (fn () => preplay_isar_step_for_method ctxt timeout meth step)
+      val meths_outcomes = meths_outcomes0
+        |> map (apsnd Lazy.value)
+        |> fold (fn meth => AList.default (op =) (meth, lazy_preplay meth)) meths
     in
       preplay_data := Canonical_Label_Tab.map_default (l, [])
         (fold (AList.update (op =)) meths_outcomes) (!preplay_data)
diff -r 93c7fcfbe6f5 -r 73372494fd80 src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Mon Feb 03 10:19:19 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Mon Feb 03 11:30:53 2014 +0100
@@ -43,7 +43,7 @@
   val steps_of_isar_proof : isar_proof -> isar_step list
 
   val label_of_isar_step : isar_step -> label option
-  val byline_of_isar_step : isar_step -> (facts * proof_method list) option
+  val byline_of_isar_step : isar_step -> facts * proof_method list
 
   val fold_isar_steps : (isar_step -> 'a -> 'a) -> isar_step list -> 'a -> 'a
   val map_isar_steps : (isar_step -> isar_step) -> isar_proof -> isar_proof
@@ -127,8 +127,8 @@
 fun subproofs_of_isar_step (Prove (_, _, _, _, subproofs, _)) = SOME subproofs
   | subproofs_of_isar_step _ = NONE
 
-fun byline_of_isar_step (Prove (_, _, _, _, _, byline)) = SOME byline
-  | byline_of_isar_step _ = NONE
+fun byline_of_isar_step (Prove (_, _, _, _, _, byline)) = byline
+  | byline_of_isar_step _ = (([], []), [])
 
 fun fold_isar_step f step =
   fold (steps_of_isar_proof #> fold_isar_steps f) (these (subproofs_of_isar_step step)) #> f step
@@ -169,7 +169,7 @@
 fun kill_useless_labels_in_isar_proof proof =
   let
     val used_ls =
-      fold_isar_steps (byline_of_isar_step #> (fn SOME ((ls, _), _) => union (op =) ls | _ => I))
+      fold_isar_steps (byline_of_isar_step #> (fn ((ls, _), _) => union (op =) ls | _ => I))
         (steps_of_isar_proof proof) []
 
     fun kill_label l = if member (op =) used_ls l then l else no_label