--- a/src/HOL/Sledgehammer.thy Fri Jul 12 15:39:46 2013 +0200
+++ b/src/HOL/Sledgehammer.thy Fri Jul 12 15:51:25 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"
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML Fri Jul 12 15:39:46 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML Fri Jul 12 15:51:25 2013 +0200
@@ -138,7 +138,7 @@
val delta =
number_of_steps - target_number_of_steps |> Unsynchronized.ref
in
- (fn () => not (preplay_fail ()) andalso !delta > 0,
+ (fn () => !delta > 0,
fn () => delta := !delta - 1)
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML Fri Jul 12 15:51:25 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_preplay.ML Fri Jul 12 15:39:46 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Fri Jul 12 15:51:25 2013 +0200
@@ -225,15 +225,12 @@
fun set_preplay_fail b = fail := b
- fun preplay' timeout step =
- (* after preplay has failed once, exact preplay times are pointless *)
- if preplay_fail () then some_preplay_time
- else preplay debug preplay_trace type_enc lam_trans ctxt timeout step
+ val preplay = preplay debug preplay_trace type_enc lam_trans ctxt
(* preplay steps without registering preplay_fails, treating exceptions
like timeouts *)
fun preplay_quietly timeout step =
- try (preplay' timeout) step
+ try (preplay timeout) step
|> the_default (true, timeout)
val preplay_time_tab =
@@ -243,7 +240,7 @@
NONE => tab
| SOME l =>
Canonical_Lbl_Tab.update_new
- (l, (fn () => preplay' preplay_timeout step) |> Lazy.lazy)
+ (l, (fn () => preplay preplay_timeout step) |> Lazy.lazy)
tab
handle Canonical_Lbl_Tab.DUP _ =>
raise Fail "Sledgehammer_Preplay: preplay time table"
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Fri Jul 12 15:39:46 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Fri Jul 12 15:51:25 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 15:39:46 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML Fri Jul 12 15:51:25 2013 +0200
@@ -20,72 +20,21 @@
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))) =
+fun variants (Let _) = raise Fail "Sledgehammer_Try0: variants"
+ | variants (Prove (qs, xs, l, t, subproofs, By (facts, _))) =
let
val methods = [SimpM, AutoM, FastforceM, ArithM]
fun step method = Prove (qs, xs, l, t, subproofs, By (facts, method))
- fun step_without_facts method =
- Prove (qs, xs, l, t, subproofs, By (no_facts, method))
+ (*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
+fun try0_step _ _ (step as Let _) = step
| try0_step preplay_timeout ({preplay_quietly, get_time, set_time,
set_preplay_fail, ...} : preplay_interface)
(step as Prove (_, _, l, _, _, _)) =
@@ -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
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Jul 12 15:39:46 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Jul 12 15:51:25 2013 +0200
@@ -4,6 +4,8 @@
General-purpose functions used by the Sledgehammer modules.
*)
+infix 1 |>! #>!
+
signature SLEDGEHAMMER_UTIL =
sig
val sledgehammerN : string
@@ -31,6 +33,12 @@
val max : ('a * 'a -> order) -> 'a -> 'a -> 'a
val max_option : ('a * 'a -> order) -> 'a option -> 'a option -> 'a option
val max_list : ('a * 'a -> order) -> 'a list -> 'a option
+
+ (** debugging **)
+ val print_timing : ('a -> 'b) -> 'a -> 'b
+ (* infix versions of print_timing; meant to replace '|>' and '#>' *)
+ val |>! : 'a * ('a -> 'b) -> 'b
+ val #>! : ('a -> 'b) * ('b -> 'c) -> 'a -> 'c
end;
structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
@@ -165,4 +173,14 @@
fun max_list ord xs = fold (SOME #> max_option ord) xs NONE
+(** debugging **)
+fun print_timing f x =
+ Timing.timing f x
+ |>> Timing.message
+ |>> warning
+ |> snd
+
+fun x |>! f = print_timing f x
+fun (f #>! g) x = x |> f |>! g
+
end;