# HG changeset patch
# User blanchet
# Date 1391551878 -3600
# Node ID 462ffd3b70651d3439792550955b18ef9b7824c2
# Parent  e04b75bd18e0216941bbe2d59fbf4b0066fce6bd
tuned code

diff -r e04b75bd18e0 -r 462ffd3b7065 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
@@ -323,10 +323,10 @@
                 #> minimize ? minimize_isar_step_dependencies ctxt preplay_data)
           |> tap (trace_isar_proof "Minimized")
           |> `(preplay_outcome_of_isar_proof (!preplay_data))
-          ||> comment_isar_proof comment_of
-          ||> chain_isar_proof
-          ||> kill_useless_labels_in_isar_proof
-          ||> relabel_isar_proof_nicely
+          ||> (comment_isar_proof comment_of
+               #> chain_isar_proof
+               #> kill_useless_labels_in_isar_proof
+               #> relabel_isar_proof_nicely)
       in
         (case string_of_isar_proof isar_proof of
           "" =>
diff -r e04b75bd18e0 -r 462ffd3b7065 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
@@ -25,7 +25,6 @@
 
 val dummy_isar_step = Let (Term.dummy, Term.dummy)
 
-(* traverses steps in post-order and collects the steps with the given labels *)
 fun collect_successors steps lbls =
   let
     fun collect_steps _ ([], accu) = ([], accu)
@@ -45,7 +44,6 @@
     rev (snd (collect_steps steps (lbls, [])))
   end
 
-(* traverses steps in reverse post-order and inserts the given updates *)
 fun update_steps steps updates =
   let
     fun update_steps [] updates = ([], updates)
@@ -85,7 +83,8 @@
       end
   in
     meths2 @ subtract (op =) meths2 meths1
-    |> filter (is_method_hopeful l1 andf is_method_hopeful l2)
+    |> List.partition (is_method_hopeful l1 andf is_method_hopeful l2)
+    |> op @
   end
 
 fun try_merge preplay_data (Prove (_, [], l1, _, subproofs1, (lfs1, gfs1), meths1, comment1))
@@ -104,7 +103,7 @@
 
 val compress_degree = 2
 val merge_timeout_slack_time = seconds 0.005
-val merge_timeout_slack_factor = 1.25
+val merge_timeout_slack_factor = 1.5
 
 fun slackify_merge_timeout time =
   time_mult merge_timeout_slack_factor (Time.+ (merge_timeout_slack_time, time))
@@ -205,26 +204,22 @@
           fun cand_key (i, l, t_size) = (length (get_successors l), (t_size, i))
 
           val compression_ord =
-            prod_ord int_ord (prod_ord (int_ord #> rev_order) int_ord)
-            #> rev_order
+            prod_ord int_ord (prod_ord (int_ord #> rev_order) int_ord) #> rev_order
 
           val cand_ord = pairself cand_key #> compression_ord
 
           fun pop_next_candidate [] = (NONE, [])
             | pop_next_candidate (cands as (cand :: cands')) =
-              let
-                val best as (i, _, _) =
-                  fold (fn x => fn y => if cand_ord (x, y) = GREATER then x else y) cands' cand
-              in (SOME best, filter_out (fn (j, _, _) => j = i) cands) end
+              fold (fn x => fn y => if cand_ord (x, y) = GREATER then x else y) cands' cand
+              |> (fn best => (SOME best, remove (op =) best cands))
 
           val candidates =
             let
               fun add_cand (i, Prove (_, _, l, t, _, _, _, _)) = cons (i, l, size_of_term t)
                 | add_cand _ = I
             in
-              (steps
-               |> split_last |> fst (* keep last step *)
-               |> fold_index add_cand) []
+              (* the very last step is not a candidate *)
+              (steps |> split_last |> fst |> fold_index add_cand) []
             end
 
           fun try_eliminate (i, l, _) labels steps =
@@ -271,10 +266,10 @@
             else
               (case pop_next_candidate candidates of
                 (NONE, _) => steps (* no more candidates for elimination *)
-              | (SOME (cand as (_, l, _)), candidates) =>
+              | (SOME (cand as (i, l, _)), candidates') =>
                 let val successors = get_successors l in
                   if length successors > compress_degree then steps
-                  else compression_loop candidates (try_eliminate cand successors steps)
+                  else compression_loop candidates' (try_eliminate cand successors steps)
                 end)
         in
           compression_loop candidates steps