# HG changeset patch
# User blanchet
# Date 1391551878 -3600
# Node ID 3c2dbd2e221f3db7e298990be2cd502f836675fa
# Parent  0e17e92248ac5eb3cf1354d2b3590999ec96046d
more generous Isar proof compression -- try to remove failing steps

diff -r 0e17e92248ac -r 3c2dbd2e221f src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Feb 04 23:11:18 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Feb 04 23:11:18 2014 +0100
@@ -316,15 +316,19 @@
         val (play_outcome, isar_proof) =
           canonical_isar_proof
           |> tap (trace_isar_proof "Original")
-          |> compress_isar_proof ctxt compress_isar preplay_data
+          |> compress_isar_proof ctxt compress_isar preplay_timeout preplay_data
           |> tap (trace_isar_proof "Compressed")
           |> postprocess_isar_proof_remove_unreferenced_steps
                (keep_fastest_method_of_isar_step (!preplay_data)
                 #> minimize ? minimize_isar_step_dependencies ctxt preplay_data)
           |> tap (trace_isar_proof "Minimized")
+          (* It's not clear whether this is worth the trouble (and if so, "isar_compress" has an
+             unnatural semantics): *)
+(*
           |> minimize
-               ? (compress_isar_proof ctxt compress_isar preplay_data
+               ? (compress_isar_proof ctxt compress_isar preplay_timeout preplay_data
                   #> tap (trace_isar_proof "Compressed again"))
+*)
           |> `(preplay_outcome_of_isar_proof (!preplay_data))
           ||> (comment_isar_proof comment_of
                #> chain_isar_proof
diff -r 0e17e92248ac -r 3c2dbd2e221f 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
@@ -11,8 +11,8 @@
   type isar_proof = Sledgehammer_Isar_Proof.isar_proof
   type isar_preplay_data = Sledgehammer_Isar_Preplay.isar_preplay_data
 
-  val compress_isar_proof : Proof.context -> real -> isar_preplay_data Unsynchronized.ref ->
-    isar_proof -> isar_proof
+  val compress_isar_proof : Proof.context -> real -> Time.time ->
+    isar_preplay_data Unsynchronized.ref -> isar_proof -> isar_proof
 end;
 
 structure Sledgehammer_Isar_Compress : SLEDGEHAMMER_ISAR_COMPRESS =
@@ -27,17 +27,17 @@
 
 fun collect_successors steps lbls =
   let
-    fun collect_steps _ ([], accu) = ([], accu)
+    fun collect_steps _ (accum as ([], _)) = accum
       | collect_steps [] accum = accum
       | collect_steps (step :: steps) accum = collect_steps steps (collect_step step accum)
-    and collect_step (Let _) x = x
-      | collect_step (step as Prove (_, _, l, _, subproofs, _, _, _)) x =
+    and collect_step (step as Prove (_, _, l, _, subproofs, _, _, _)) x =
         (case collect_subproofs subproofs x of
-          ([], accu) => ([], accu)
+          (accum as ([], _)) => accum
         | accum as (l' :: lbls', accu) => if l = l' then (lbls', step :: accu) else accum)
-    and collect_subproofs [] x = x
-      | collect_subproofs (proof :: subproofs) x =
-        (case collect_steps (steps_of_isar_proof proof) x of
+        | collect_step _ accum = accum
+    and collect_subproofs [] accum = accum
+      | collect_subproofs (proof :: subproofs) accum =
+        (case collect_steps (steps_of_isar_proof proof) accum of
           accum as ([], _) => accum
         | accum => collect_subproofs subproofs accum)
   in
@@ -50,7 +50,6 @@
       | update_steps steps [] = (steps, [])
       | update_steps (step :: steps) updates = update_step step (update_steps steps updates)
     and update_step step (steps, []) = (step :: steps, [])
-      | update_step (step as Let _) (steps, updates) = (step :: steps, updates)
       | update_step (Prove (qs, xs, l, t, subproofs, facts, meths, comment))
           (steps,
            updates as Prove (qs', xs', l', t', subproofs', facts', meths', comment') :: updates') =
@@ -61,6 +60,7 @@
            update_subproofs subproofs updates
            |>> (fn subproofs => Prove (qs, xs, l, t, subproofs, facts, meths, comment)))
         |>> (fn step => step :: steps)
+      | update_step step (steps, updates) = (step :: steps, updates)
     and update_subproofs [] updates = ([], updates)
       | update_subproofs steps [] = (steps, [])
       | update_subproofs (proof :: subproofs) updates =
@@ -89,29 +89,30 @@
     (hopeful @ hopeless, hopeless)
   end
 
-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, 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), hopeless)
-      end)
+fun try_merge_steps preplay_data (Prove ([], fix1, l1, _, subproofs1, (lfs1, gfs1), meths1, comment1))
+      (Prove (qs2, fix2, l2, t, subproofs2, (lfs2, gfs2), meths2, comment2)) =
+    let
+      val (meths, hopeless) = merge_methods preplay_data (l1, meths1) (l2, meths2)
+      val lfs = union (op =) lfs1 (remove (op =) l1 lfs2)
+      val gfs = union (op =) gfs1 gfs2
+    in
+      SOME (Prove (qs2, union (op =) fix1 fix2, l2, t, subproofs1 @ subproofs2, (lfs, gfs), meths,
+        comment1 ^ comment2), hopeless)
+    end
   | try_merge_steps _ _ _ = NONE
 
+val merge_slack_time = seconds 0.005
+val merge_slack_factor = 1.5
+
+fun adjust_merge_timeout max time =
+  let val timeout = time_mult merge_slack_factor (Time.+ (merge_slack_time, time)) in
+    if Time.< (max, timeout) then max else timeout
+  end
+
 val compress_degree = 2
-val merge_timeout_slack_time = seconds 0.005
-val merge_timeout_slack_factor = 1.5
-
-fun slackify_merge_timeout time =
-  time_mult merge_timeout_slack_factor (Time.+ (merge_timeout_slack_time, time))
 
 (* Precondition: The proof must be labeled canonically. *)
-fun compress_isar_proof ctxt compress_isar preplay_data proof =
+fun compress_isar_proof ctxt compress_isar preplay_timeout preplay_data proof =
   if compress_isar <= 1.0 then
     proof
   else
@@ -180,7 +181,7 @@
               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 timeout = adjust_merge_timeout preplay_timeout (Time.+ (time, time'))
               val (_, Played time'') :: meths_outcomes =
                 preplay_isar_step ctxt timeout hopeless step''
             in
@@ -190,7 +191,8 @@
                 nontriv_subs
             end
             handle Bind =>
-              elim_one_subproof time [] qs fix l t lfs gfs meths comment subs (sub :: nontriv_subs))
+                   elim_one_subproof time [] qs fix l t lfs gfs meths comment subs
+                     (sub :: nontriv_subs))
           | _ => raise Fail "Sledgehammer_Isar_Compress: elim_one_subproof")
 
       fun elim_subproofs (step as Prove (qs, fix, l, t, subproofs, (lfs, gfs), meths, comment)) =
@@ -232,18 +234,20 @@
 
               val succs = collect_successors steps' labels
 
-              (* 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 time =
+                (case forced_intermediate_preplay_outcome_of_isar_step (!preplay_data) l of
+                  Played time => time
+                | _ => preplay_timeout)
 
               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
                 forced_intermediate_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 #> slackify_merge_timeout) times0
+              val timeouts =
+                map (curry Time.+ time_slice #> adjust_merge_timeout preplay_timeout) times0
               (* FIXME: "preplay_timeout" should be an ultimate maximum *)
 
               val meths_outcomess = map3 (preplay_isar_step ctxt) timeouts hopelesses succs'
@@ -294,12 +298,12 @@
         (* bottom-up: compress innermost proofs first *)
         steps |> map (fn step => step |> compress_further () ? compress_sub_levels)
               |> compress_further () ? compress_top_level
-      and compress_sub_levels (step as Let _) = step
-        | compress_sub_levels (Prove (qs, xs, l, t, subproofs, facts, meths, comment)) =
+      and compress_sub_levels (Prove (qs, xs, l, t, subproofs, facts, meths, comment)) =
           (* compress subproofs *)
           Prove (qs, xs, l, t, map compress_proof subproofs, facts, meths, comment)
           (* eliminate trivial subproofs *)
           |> compress_further () ? elim_subproofs
+        | compress_sub_levels step = step
     in
       compress_proof proof
     end
diff -r 0e17e92248ac -r 3c2dbd2e221f 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
@@ -133,8 +133,8 @@
 
     val play_outcome = take_time timeout prove ()
   in
-    (if Config.get ctxt trace then preplay_trace ctxt assmsp goal play_outcome else ();
-     play_outcome)
+    if Config.get ctxt trace then preplay_trace ctxt assmsp goal play_outcome else ();
+    play_outcome
   end
 
 fun preplay_isar_step_for_method ctxt timeout meth =
@@ -200,7 +200,8 @@
   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))
+  AList.lookup (op =) (the (Canonical_Label_Tab.lookup preplay_data l))
+  #> the_default (Lazy.value Not_Played)
 
 fun fastest_method_of_isar_step preplay_data =
   the o Canonical_Label_Tab.lookup preplay_data