# HG changeset patch # User wenzelm # Date 1373637085 -7200 # Node ID 0d0c20a0a34f901032ec14691a0910828099f4c7 # Parent 1e930ee99b0cc9b6df3b1357cedfaca9deee1f5b# Parent 0b30bde83185800efaaec2b4c21054cde8fe09d4 merged diff -r 0b30bde83185 -r 0d0c20a0a34f src/HOL/Sledgehammer.thy --- 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" diff -r 0b30bde83185 -r 0d0c20a0a34f src/HOL/Tools/Sledgehammer/sledgehammer_compress.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 diff -r 0b30bde83185 -r 0d0c20a0a34f src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML --- /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 diff -r 0b30bde83185 -r 0d0c20a0a34f src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML --- 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" diff -r 0b30bde83185 -r 0d0c20a0a34f src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- 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 diff -r 0b30bde83185 -r 0d0c20a0a34f src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML --- 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 diff -r 0b30bde83185 -r 0d0c20a0a34f src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- 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;