src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Fri Jan 31 10:23:32 2014 +0100
@@ -0,0 +1,95 @@
+(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML
+    Author:     Steffen Juilf Smolka, TU Muenchen
+    Author:     Jasmin Blanchette, TU Muenchen
+
+Minimize dependencies (used facts) of Isar proof steps.
+*)
+
+signature SLEDGEHAMMER_ISAR_MINIMIZE =
+sig
+  type preplay_interface = Sledgehammer_Isar_Preplay.preplay_interface
+  type isar_step = Sledgehammer_Isar_Proof.isar_step
+  type isar_proof = Sledgehammer_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_Isar_Minimize : SLEDGEHAMMER_ISAR_MINIMIZE =
+struct
+
+open Sledgehammer_Util
+open Sledgehammer_Reconstructor
+open Sledgehammer_Isar_Proof
+open Sledgehammer_Isar_Preplay
+
+val slack = seconds 0.1
+
+fun min_deps_of_step (_ : preplay_interface) (step as Let _) = step
+  | min_deps_of_step {get_preplay_outcome, set_preplay_outcome, preplay_quietly, ...}
+      (step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meth))) =
+    (case get_preplay_outcome l of
+      Played 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.+ (time, slack)) (mk_step (min_facts @ facts)) of
+              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 (mk_step_gfs_lfs gfs) time [] lfs
+        val (time, min_gfs) = minimize_facts (mk_step_lfs_gfs min_lfs) time [] gfs
+      in
+        set_preplay_outcome l (Played time); mk_step_lfs_gfs min_lfs min_gfs
+      end
+    | _ => step (* don't touch steps that time out or fail *))
+
+fun postprocess_remove_unreferenced_steps postproc_step =
+  let
+    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 [] = ([], [])
+      | 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
+          ||> (fn x => x :: accu)
+        else
+          (refed, accu))
+    and do_refed_step step = step |> postproc_step |> do_refed_step'
+    and do_refed_step' (Let _) = raise Fail "Sledgehammer_Isar_Minimize"
+      | do_refed_step' (Prove (qs, xs, l, t, subproofs, ((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, ((lfs, gfs), m))
+        in
+          (refed, step)
+        end
+  in
+    snd o do_proof
+  end
+
+end;