src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML

 (*  Title:      HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML
+    Author:     Steffen Juilf Smolka, TU Muenchen
     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_step = Sledgehammer_Proof.isar_step
   type isar_proof = Sledgehammer_Proof.isar_proof
-  val minimize_dependencies_and_remove_unrefed_steps :
-    bool -> preplay_interface -> isar_proof -> isar_proof
+
+  val min_deps_of_step : preplay_interface -> isar_step -> isar_step
+  val postprocess_remove_unreferenced_steps : (isar_step -> isar_step) -> 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
+val slack = seconds 0.1
 
 fun min_deps_of_step (_ : preplay_interface) (step as Let _) = step
   | min_deps_of_step {get_preplay_time, set_preplay_time, preplay_quietly, ...}
-      (step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), method))) =
-  (case get_preplay_time l of
-    (* don't touch steps that time out or fail; minimizing won't help *)
-    (true, _) => step
-  | (false, time) =>
-    let
-      fun mk_step_lfs_gfs lfs gfs =
-        Prove (qs, xs, l, t, subproofs, ((lfs, gfs), method))
-      val mk_step_gfs_lfs = curry (swap #> uncurry mk_step_lfs_gfs)
+      (step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meth))) =
+    (case get_preplay_time l of
+      (* don't touch steps that time out or fail; minimizing won't help (not true -- FIXME) *)
+      (true, _) => step
+    | (false, time) =>
+      let
+        fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meth))
+        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)
+        fun minimize_facts _ time min_facts [] = (time, min_facts)
+          | minimize_facts mk_step time min_facts (f :: facts) =
+            (case preplay_quietly (Time.+ (time, slack)) (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
+        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_preplay_time l (false, time); mk_step_lfs_gfs min_lfs min_gfs
+      end)
 
-    in
-      set_preplay_time l (false, time);
-      mk_step_lfs_gfs min_lfs min_gfs
-    end)
-
-fun minimize_dependencies_and_remove_unrefed_steps isar_try0 preplay_interface
-        proof =
+fun postprocess_remove_unreferenced_steps postproc_step =
   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
+      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
+            ||> (fn x => x :: accu)
           else
             (refed, accu)
-
-    and do_refed_step step =
-      step
-      |> isar_try0 ? min_deps_of_step preplay_interface
-      |> do_refed_step'
-
+    and do_refed_step step = step |> postproc_step |> do_refed_step'
     and do_refed_step' (Let _) = raise Fail "Sledgehammer_Minimize_Isar"
       | do_refed_step' (Prove (qs, xs, l, t, subproofs, ((lfs, gfs), m))) =
         let
           val (refed, subproofs) =
             map do_proof subproofs

           val step = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), m))
         in
           (refed, step)
         end
   in
-    snd (do_proof proof)
+    snd o do_proof
   end
 
 end;