minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps

--- a/src/HOL/Sledgehammer.thy	Fri Jul 12 13:12:21 2013 +0200
+++ b/src/HOL/Sledgehammer.thy	Fri Jul 12 14:18:06 2013 +0200
@@ -22,6 +22,7 @@
 ML_file "Tools/Sledgehammer/sledgehammer_preplay.ML"
 ML_file "Tools/Sledgehammer/sledgehammer_compress.ML"
 ML_file "Tools/Sledgehammer/sledgehammer_try0.ML"
+ML_file "Tools/Sledgehammer/sledgehammer_minimize_isar.ML"
 ML_file "Tools/Sledgehammer/sledgehammer_reconstruct.ML"
 ML_file "Tools/Sledgehammer/sledgehammer_provers.ML"
 ML_file "Tools/Sledgehammer/sledgehammer_minimize.ML"

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML	Fri Jul 12 14:18:06 2013 +0200
@@ -0,0 +1,112 @@
+(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML
+    Author:     Jasmin Blanchette, TU Muenchen
+    Author:     Steffen Juilf Smolka, TU Muenchen
+
+Minimize dependencies (used facts) of Isar proof steps.
+*)
+
+signature SLEDGEHAMMER_MINIMIZE_ISAR =
+sig
+  type preplay_interface = Sledgehammer_Preplay.preplay_interface
+  type isar_proof = Sledgehammer_Proof.isar_proof
+  val minimize_dependencies_and_remove_unrefed_steps :
+    preplay_interface -> isar_proof -> isar_proof
+end
+
+
+structure Sledgehammer_Minimize_Isar : SLEDGEHAMMER_MINIMIZE_ISAR =
+struct
+
+open Sledgehammer_Util
+open Sledgehammer_Proof
+open Sledgehammer_Preplay
+
+val slack = 1.3
+
+fun min_deps_of_step (_ : preplay_interface) (step as Let _) = step
+  | min_deps_of_step {get_time, set_time, preplay_quietly, set_preplay_fail, ...}
+      (step as Prove (qs, xs, l, t, subproofs, By ((lfs, gfs), method))) =
+  (case get_time l of
+    (* don't touch steps that time out *)
+    (true, _) => (set_preplay_fail true; step)
+  | (false, time) =>
+    let
+      fun mk_step_lfs_gfs lfs gfs =
+        Prove (qs, xs, l, t, subproofs, By ((lfs, gfs), method))
+      val mk_step_gfs_lfs = curry (swap #> uncurry mk_step_lfs_gfs)
+
+      fun minimize_facts _ time min_facts [] = (time, min_facts)
+        | minimize_facts mk_step time min_facts (f :: facts) =
+          (case preplay_quietly (time_mult slack time)
+                  (mk_step (min_facts @ facts)) of
+            (true, _) => minimize_facts mk_step time (f :: min_facts) facts
+          | (false, time) => minimize_facts mk_step time min_facts facts)
+
+      val (time, min_lfs) = minimize_facts (mk_step_gfs_lfs gfs) time [] lfs
+      val (time, min_gfs) = minimize_facts (mk_step_lfs_gfs min_lfs) time [] gfs
+
+    in
+      set_time l (false, time);
+      mk_step_lfs_gfs min_lfs min_gfs
+    end)
+
+fun minimize_dependencies_and_remove_unrefed_steps (preplay_interface as
+  {set_time, set_preplay_fail, ...} : preplay_interface) proof =
+  let
+    fun cons_to xs x = x :: xs
+
+    val add_lfs = fold (Ord_List.insert label_ord)
+
+    fun do_proof (Proof (fix, assms, steps)) =
+      let
+        val (refed, steps) = do_steps steps
+      in
+        (refed, Proof (fix, assms, steps))
+      end
+
+    and do_steps steps =
+      let
+        (* the last step is always implicitly referenced *)
+        val (steps, (refed, concl)) =
+          split_last steps
+          ||> do_refed_step
+      in
+        fold_rev do_step steps (refed, [concl])
+      end
+
+    and do_step step (refed, accu) =
+      case label_of_step step of
+        NONE => (refed, step :: accu)
+      | SOME l =>
+          if Ord_List.member label_ord refed l then
+            do_refed_step step
+            |>> Ord_List.union label_ord refed
+            ||> cons_to accu
+          else
+            (set_time l zero_preplay_time; (* remove unrefed step! *)
+             (refed, accu))
+
+    and do_refed_step step =
+      min_deps_of_step preplay_interface step
+      |> do_refed_step'
+
+    and do_refed_step' (Let _) = raise Fail "Sledgehammer_Minimize_Isar"
+      | do_refed_step' (Prove (qs, xs, l, t, subproofs, By ((lfs, gfs), m))) =
+        let
+          val (refed, subproofs) =
+            map do_proof subproofs
+            |> split_list
+            |>> Ord_List.unions label_ord
+            |>> add_lfs lfs
+          val step = Prove (qs, xs, l, t, subproofs, By ((lfs, gfs), m))
+        in
+          (refed, step)
+        end
+
+  in
+    set_preplay_fail false; (* step(s) causing the failure may be removed *)
+    snd (do_proof proof)
+  end
+
+
+end

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Fri Jul 12 13:12:21 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Fri Jul 12 14:18:06 2013 +0200
@@ -47,6 +47,7 @@
 open Sledgehammer_Preplay
 open Sledgehammer_Compress
 open Sledgehammer_Try0
+open Sledgehammer_Minimize_Isar
 
 structure String_Redirect = ATP_Proof_Redirect(
   type key = step_name
@@ -594,6 +595,7 @@
                (if isar_proofs = SOME true then isar_compress_degree else 100)
                merge_timeout_slack preplay_interface
           |> try0 preplay_timeout preplay_interface
+          |> minimize_dependencies_and_remove_unrefed_steps preplay_interface
           |> clean_up_labels_in_proof
         val isar_text =
           string_of_proof ctxt type_enc lam_trans subgoal subgoal_count

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML	Fri Jul 12 13:12:21 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML	Fri Jul 12 14:18:06 2013 +0200
@@ -20,58 +20,6 @@
 open Sledgehammer_Proof
 open Sledgehammer_Preplay
 
-
-fun reachable_labels proof =
-  let
-    val refs_of_step =
-      byline_of_step #> (fn SOME (By ((lfs, _), _)) => lfs | NONE => [])
-
-    val union = fold (Ord_List.insert label_ord)
-
-    fun do_proof proof reachable =
-      let
-        val (steps, concl) = split_last (steps_of_proof proof)
-        val reachable =
-          union (refs_of_step concl) reachable
-          |> union (the_list (label_of_step concl))
-      in
-        fold_rev do_step steps reachable
-      end
-
-    and do_step (Let _) reachable = reachable
-      | do_step (Prove (_, _, l, _, subproofs, By ((lfs, _), _))) reachable =
-        if Ord_List.member label_ord reachable l
-          then fold do_proof subproofs (union lfs reachable)
-          else reachable
-
-  in
-    do_proof proof []
-  end
-
-(** removes steps not referenced by the final proof step or any of its
-    predecessors **)
-fun remove_unreachable_steps ({set_time, ...} : preplay_interface) proof =
-  let
-
-    val reachable = reachable_labels proof
-
-    fun do_proof (Proof (fix, assms, steps)) =
-      Proof (fix, assms, do_steps steps)
-
-    and do_steps steps =
-      uncurry (fold_rev do_step) (split_last steps ||> single)
-
-    and do_step (step as Let _) accu = step :: accu
-      | do_step (Prove (qs, xs, l, t, subproofs, by)) accu =
-          if Ord_List.member label_ord reachable l
-            then Prove (qs, xs, l, t, map do_proof subproofs, by) :: accu
-            else (set_time l zero_preplay_time; accu)
-
-  in
-    do_proof proof
-  end
-
-
 fun variants (step as Let _) = raise Fail "Sledgehammer_Try0: variants"
   | variants (Prove (qs, xs, l, t, subproofs, By (facts, method))) =
       let
@@ -80,9 +28,10 @@
         fun step_without_facts method =
           Prove (qs, xs, l, t, subproofs, By (no_facts, method))
       in
+        (* FIXME *)
         (* There seems to be a bias for methods earlier in the list, so we put
            the variants using no facts first. *)
-        map step_without_facts methods @ map step methods
+        (*map step_without_facts methods @*) map step methods
       end
 
 fun try0_step preplay_timeout preplay_interface (step as Let _) = step
@@ -109,8 +58,7 @@
 
 fun try0 preplay_timeout
   (preplay_interface as {set_preplay_fail, ...} : preplay_interface) proof =
-    (set_preplay_fail false; (* reset preplay fail *)
-     map_isar_steps (try0_step preplay_timeout preplay_interface) proof
-     |> remove_unreachable_steps preplay_interface)
+    (set_preplay_fail false; (* failure might be fixed *)
+     map_isar_steps (try0_step preplay_timeout preplay_interface) proof)
 
 end