# HG changeset patch
# User blanchet
# Date 1391418858 -3600
# Node ID a46458d368d54a1a2120804d53a6b6f71900df15
# Parent  e68fd012bbf3c8d3d751c8a72359bbf78966d331
tuning

diff -r e68fd012bbf3 -r a46458d368d5 src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Mon Feb 03 10:14:18 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Mon Feb 03 10:14:18 2014 +0100
@@ -234,13 +234,6 @@
               val time_slice = time_mult (1.0 / (Real.fromInt (length labels))) time
               val timeouts = map (curry Time.+ time_slice #> time_mult merge_timeout_slack) times0
 
-              (* FIXME: debugging *)
-              val _ =
-                if the (label_of_isar_step cand) <> l then
-                  raise Fail "Sledgehammer_Isar_Compress: try_eliminate"
-                else
-                  ()
-
               (* 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'
 
@@ -282,16 +275,12 @@
           |> remove (op =) dummy_isar_step
         end
 
-      (*
-         Proofs are compressed bottom-up, beginning with the innermost
-         subproofs.
-         On the innermost proof level, the proof steps have no subproofs.
-         In the best case, these steps can be merged into just one step,
-         resulting in a trivial subproof. Going one level up, trivial subproofs
-         can be eliminated. In the best case, this once again leads to a proof
-         whose proof steps do not have subproofs. Applying this approach
-         recursively will result in a flat proof in the best cast.
-      *)
+      (* Proofs are compressed bottom-up, beginning with the innermost subproofs. On the innermost
+         proof level, the proof steps have no subproofs. In the best case, these steps can be merged
+         into just one step, resulting in a trivial subproof. Going one level up, trivial subproofs
+         can be eliminated. In the best case, this once again leads to a proof whose proof steps do
+         not have subproofs. Applying this approach recursively will result in a flat proof in the
+         best cast. *)
       fun compress_proof (proof as (Proof (fix, assms, steps))) =
         if compress_further () then Proof (fix, assms, compress_steps steps) else proof
       and compress_steps steps =
diff -r e68fd012bbf3 -r a46458d368d5 src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Mon Feb 03 10:14:18 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Mon Feb 03 10:14:18 2014 +0100
@@ -33,7 +33,7 @@
 val slack = seconds 0.1
 
 fun minimize_isar_step_dependencies ctxt preplay_data
-      (step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meths as meth :: _))) =
+      (step as Prove (qs, xs, l, t, subproofs, ((lfs0, gfs0), meths as meth :: _))) =
     (case Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth) of
       Played time =>
       let
@@ -46,8 +46,8 @@
               Played time => minimize_facts mk_step time min_facts facts
             | _ => minimize_facts mk_step time (f :: min_facts) facts)
 
-        val (time, min_lfs) = minimize_facts (fn lfs => mk_step_lfs_gfs lfs gfs) time [] lfs
-        val (time, min_gfs) = minimize_facts (mk_step_lfs_gfs min_lfs) time [] gfs
+        val (time, min_lfs) = minimize_facts (fn lfs => mk_step_lfs_gfs lfs gfs0) time [] lfs0
+        val (time, min_gfs) = minimize_facts (mk_step_lfs_gfs min_lfs) time [] gfs0
 
         val step' = mk_step_lfs_gfs min_lfs min_gfs
       in
diff -r e68fd012bbf3 -r a46458d368d5 src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Mon Feb 03 10:14:18 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Mon Feb 03 10:14:18 2014 +0100
@@ -181,17 +181,15 @@
     end
   | set_preplay_outcomes_of_isar_step _ _ _ _ _ = ()
 
-fun preplay_outcome_of_isar_step_for_method preplay_data l meth =
-  let val SOME meths_outcomes = Canonical_Label_Tab.lookup preplay_data l in
-    the (AList.lookup (op =) meths_outcomes meth)
-  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))
 
-fun fastest_method_of_isar_step preplay_data l =
-  the (Canonical_Label_Tab.lookup preplay_data l)
-  |> map (fn (meth, outcome) =>
+fun fastest_method_of_isar_step preplay_data =
+  Canonical_Label_Tab.lookup preplay_data #> the
+  #> map (fn (meth, outcome) =>
        (meth, Time.toMilliseconds (case Lazy.force outcome of Played time => time | _ => one_year)))
-  |> sort (int_ord o pairself snd)
-  |> hd |> fst
+  #> sort (int_ord o pairself snd)
+  #> hd #> fst
 
 fun forced_outcome_of_step preplay_data (Prove (_, _, l, _, _, (_, meths))) =
     Lazy.force (preplay_outcome_of_isar_step_for_method preplay_data l (the_single meths))