--- /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