# HG changeset patch # User smolkas # Date 1373631486 -7200 # Node ID 831f7479c74f43b1e96d5a36c6856bfa93e09618 # Parent 78a64edf431fa2cd66823ba4ed7b044f0d3b2dc0 minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps diff -r 78a64edf431f -r 831f7479c74f src/HOL/Sledgehammer.thy --- a/src/HOL/Sledgehammer.thy Fri Jul 12 13:12:21 2013 +0200 +++ b/src/HOL/Sledgehammer.thy Fri Jul 12 14:18:06 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 78a64edf431f -r 831f7479c74f 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 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 diff -r 78a64edf431f -r 831f7479c74f src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Fri Jul 12 13:12:21 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Fri Jul 12 14:18:06 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 78a64edf431f -r 831f7479c74f src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML Fri Jul 12 13:12:21 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML Fri Jul 12 14:18:06 2013 +0200 @@ -20,58 +20,6 @@ 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))) = let @@ -80,9 +28,10 @@ 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 @@ -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