# HG changeset patch # User smolkas # Date 1373566086 -7200 # Node ID 8a25b17e3d797a7b1bcd5fe65441cfe59180ace3 # Parent 760a567f1609f97de76d6ea80052b6e4b5f65ad0 optimize isar-proofs by trying different proof methods diff -r 760a567f1609 -r 8a25b17e3d79 src/HOL/Sledgehammer.thy --- a/src/HOL/Sledgehammer.thy Thu Jul 11 13:33:20 2013 +0200 +++ b/src/HOL/Sledgehammer.thy Thu Jul 11 20:08:06 2013 +0200 @@ -21,6 +21,7 @@ ML_file "Tools/Sledgehammer/sledgehammer_print.ML" 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_reconstruct.ML" ML_file "Tools/Sledgehammer/sledgehammer_provers.ML" ML_file "Tools/Sledgehammer/sledgehammer_minimize.ML" diff -r 760a567f1609 -r 8a25b17e3d79 src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML Thu Jul 11 13:33:20 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML Thu Jul 11 20:08:06 2013 +0200 @@ -3,6 +3,7 @@ Author: Steffen Juilf Smolka, TU Muenchen Compression of isar proofs. +Only proof steps using the MetisM proof_method are compressed. PRE CONDITION: the proof must be labeled canocially, see Slegehammer_Proof.relabel_proof_canonically @@ -102,13 +103,13 @@ (* tries merging the first step into the second step *) fun try_merge - (Prove (_, Fix [], lbl1, _, [], By_Metis (lfs1, gfs1))) - (Prove (qs2, fix, lbl2, t, subproofs, By_Metis (lfs2, gfs2))) = + (Prove (_, Fix [], lbl1, _, [], By ((lfs1, gfs1), MetisM))) + (Prove (qs2, fix, lbl2, t, subproofs, By ((lfs2, gfs2), MetisM))) = let val lfs = remove (op =) lbl1 lfs2 |> union (op =) lfs1 val gfs = union (op =) gfs1 gfs2 in - SOME (Prove (qs2, fix, lbl2, t, subproofs, By_Metis (lfs, gfs))) + SOME (Prove (qs2, fix, lbl2, t, subproofs, By ((lfs, gfs), MetisM))) end | try_merge _ _ = NONE @@ -129,7 +130,7 @@ val (compress_further : unit -> bool, decrement_step_count : unit -> unit) = let - val number_of_steps = add_metis_steps (steps_of_proof proof) 0 + val number_of_steps = add_proof_steps (steps_of_proof proof) 0 val target_number_of_steps = Real.fromInt number_of_steps / isar_compress |> Real.round @@ -147,7 +148,7 @@ let fun add_refs (Let _) tab = tab - | add_refs (Prove (_, _, l as v, _, _, By_Metis (lfs, _))) tab = + | add_refs (Prove (_, _, l as v, _, _, By ((lfs, _), _))) tab = fold (fn lf as key => Canonical_Lbl_Tab.cons_list (key, v)) lfs tab val tab = @@ -170,21 +171,22 @@ end + (** elimination of trivial, one-step subproofs **) fun elim_subproofs' time qs fix l t lfs gfs subs nontriv_subs = if null subs orelse not (compress_further ()) then (set_time l (false, time); Prove (qs, fix, l, t, List.revAppend (nontriv_subs, subs), - By_Metis (lfs, gfs) )) + By_Metis (lfs, gfs)) ) else case subs of ((sub as Proof(_, Assume assms, sub_steps)) :: subs) => (let (* trivial subproofs have exactly one Prove step *) - val SOME (Prove (_, Fix [], l', _, [], By_Metis(lfs', gfs'))) = - (try the_single) sub_steps + val SOME (Prove (_, Fix [], l', _, [], + By ((lfs', gfs'), MetisM))) = (try the_single) sub_steps (* only touch proofs that can be preplayed sucessfully *) val (false, time') = get_time l' @@ -215,7 +217,7 @@ fun elim_subproofs (step as Let _) = step | elim_subproofs - (step as Prove (qs, fix, l, t, subproofs, By_Metis(lfs, gfs))) = + (step as Prove (qs, fix, l, t, subproofs, By ((lfs, gfs), MetisM))) = if subproofs = [] then step else case get_time l of (true, _) => step (* timeout *) @@ -271,8 +273,8 @@ map (curry Time.+ timeslice #> time_mult merge_timeout_slack) succ_times - val ((cand as Prove (_, _, l, _, _, By_Metis(lfs, _))) :: steps') = - drop i steps + val ((cand as Prove (_, _, l, _, _, + By ((lfs, _), MetisM))) :: steps') = drop i steps (* FIXME: debugging *) val _ = (if (label_of_step cand |> the) <> l then diff -r 760a567f1609 -r 8a25b17e3d79 src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Thu Jul 11 13:33:20 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Thu Jul 11 20:08:06 2013 +0200 @@ -24,11 +24,12 @@ set_time : label -> preplay_time -> unit, preplay_quietly : Time.time -> isar_step -> preplay_time, preplay_fail : unit -> bool, + set_preplay_fail : bool -> unit, overall_preplay_stats : unit -> preplay_time * bool } val proof_preplay_interface : - bool -> Proof.context -> string -> string -> bool -> Time.time option - -> bool -> isar_proof -> preplay_interface + bool -> Proof.context -> string -> string -> bool -> Time.time -> bool + -> isar_proof -> preplay_interface end @@ -104,11 +105,24 @@ |> thm_of_term ctxt end +(* mapping of proof methods to tactics *) +fun tac_of_method method type_enc lam_trans ctxt facts = + case method of + MetisM => Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts + | _ => + Method.insert_tac facts + THEN' (case method of + SimpM => Simplifier.asm_full_simp_tac + | AutoM => (fn ctxt => K (Clasimp.auto_tac ctxt)) + | FastforceM => Clasimp.fast_force_tac + | ArithM => Arith_Data.arith_tac + | _ => raise Fail "Sledgehammer_Preplay: tac_of_method") ctxt + (* main function for preplaying isar_steps *) fun preplay _ _ _ _ _ _ (Let _) = zero_preplay_time | preplay debug trace type_enc lam_trans ctxt timeout - (Prove (_, Fix xs, _, t, subproofs, By_Metis fact_names)) = + (Prove (_, Fix xs, _, t, subproofs, By (fact_names, proof_method))) = let val (prop, obtain) = (case xs of @@ -138,7 +152,7 @@ val goal = Goal.prove (Config.put Metis_Tactic.verbose debug ctxt) [] [] prop fun tac {context = ctxt, prems = _} = - Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts 1 + HEADGOAL (tac_of_method proof_method type_enc lam_trans ctxt facts) fun run_tac () = goal tac handle ERROR msg => error ("preplay error: " ^ msg) val preplay_time = take_time timeout run_tac () @@ -157,6 +171,7 @@ set_time : label -> preplay_time -> unit, preplay_quietly : Time.time -> isar_step -> preplay_time, preplay_fail : unit -> bool, + set_preplay_fail : bool -> unit, overall_preplay_stats : unit -> preplay_time * bool } @@ -197,19 +212,19 @@ set_time = K (K ()), preplay_quietly = K (K zero_preplay_time), preplay_fail = K false, + set_preplay_fail = K (), overall_preplay_stats = K (zero_preplay_time, false)} else let - (* 60 seconds seems like a good interpreation of "no timeout" *) - val preplay_timeout = preplay_timeout |> the_default (seconds 60.0) - (* add local proof facts to context *) val ctxt = enrich_context proof ctxt val fail = Unsynchronized.ref false fun preplay_fail () = !fail + 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 @@ -230,7 +245,7 @@ Canonical_Lbl_Tab.update_new (l, (fn () => preplay' preplay_timeout step) |> Lazy.lazy) tab - handle (exn as Canonical_Lbl_Tab.DUP _) => + handle Canonical_Lbl_Tab.DUP _ => raise Fail "Sledgehammer_Preplay: preplay time table" in Canonical_Lbl_Tab.empty @@ -265,6 +280,7 @@ set_time = set_time, preplay_quietly = preplay_quietly, preplay_fail = preplay_fail, + set_preplay_fail = set_preplay_fail, overall_preplay_stats = overall_preplay_stats} end diff -r 760a567f1609 -r 8a25b17e3d79 src/HOL/Tools/Sledgehammer/sledgehammer_print.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML Thu Jul 11 13:33:20 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML Thu Jul 11 20:08:06 2013 +0200 @@ -121,6 +121,7 @@ fun string_of_proof ctxt type_enc lam_trans i n proof = let + val ctxt = (* make sure type constraint are actually printed *) ctxt |> Config.put show_markup false @@ -129,11 +130,17 @@ |> Config.put show_types false |> Config.put show_sorts false |> Config.put show_consts false + val register_fixes = map Free #> fold Variable.auto_fixes + fun add_suffix suffix (s, ctxt) = (s ^ suffix, ctxt) + fun of_indent ind = replicate_string (ind * indent_size) " " + fun of_moreover ind = of_indent ind ^ "moreover\n" + fun of_label l = if l = no_label then "" else string_of_label l ^ ": " + fun of_obtain qs nr = (if nr > 1 orelse (nr = 1 andalso member (op =) qs Then) then "ultimately " @@ -141,8 +148,11 @@ "then " else "") ^ "obtain" + fun of_show_have qs = if member (op =) qs Show then "show" else "have" + fun of_thus_hence qs = if member (op =) qs Show then "thus" else "hence" + fun of_prove qs nr = if nr > 1 orelse (nr = 1 andalso member (op =) qs Then) then "ultimately " ^ of_show_have qs @@ -150,6 +160,7 @@ of_thus_hence qs else of_show_have qs + fun add_term term (s, ctxt) = (s ^ (term |> singleton (Syntax.uncheck_terms ctxt) @@ -158,31 +169,57 @@ |> simplify_spaces |> maybe_quote), ctxt |> Variable.auto_fixes term) - val reconstr = Metis (type_enc, lam_trans) - fun of_metis ind options (ls, ss) = - "\n" ^ of_indent (ind + 1) ^ options ^ - reconstructor_command reconstr 1 1 [] 0 - (ls |> sort_distinct (prod_ord string_ord int_ord), - ss |> sort_distinct string_ord) + + fun by_method method = "by " ^ + (case method of + SimpM => "simp" + | AutoM => "auto" + | FastforceM => "fastforce" + | ArithM => "arith" + | _ => raise Fail "Sledgehammer_Print: by_method") + + fun using_facts [] [] = "" + | using_facts ls ss = + "using " ^ space_implode " " (map string_of_label ls @ ss) ^ " " + + fun of_method ls ss MetisM = + reconstructor_command (Metis (type_enc, lam_trans)) 1 1 [] 0 (ls, ss) + | of_method ls ss method = + using_facts ls ss ^ by_method method + + fun of_byline ind options (ls, ss) method = + let + val ls = ls |> sort_distinct label_ord + val ss = ss |> sort_distinct string_ord + in + "\n" ^ of_indent (ind + 1) ^ options ^ of_method ls ss method + end + fun of_free (s, T) = maybe_quote s ^ " :: " ^ maybe_quote (simplify_spaces (with_vanilla_print_mode (Syntax.string_of_typ ctxt) T)) + fun add_frees xs (s, ctxt) = (s ^ space_implode " and " (map of_free xs), ctxt |> register_fixes xs) + fun add_fix _ [] = I | add_fix ind xs = add_suffix (of_indent ind ^ "fix ") #> add_frees xs #> add_suffix "\n" + fun add_assm ind (l, t) = add_suffix (of_indent ind ^ "assume " ^ of_label l) #> add_term t #> add_suffix "\n" + fun add_assms ind assms = fold (add_assm ind) assms - fun add_step_post ind l t facts options = + + fun add_step_post ind l t facts method options = add_suffix (of_label l) #> add_term t - #> add_suffix (of_metis ind options facts ^ "\n") + #> add_suffix (of_byline ind options facts method ^ "\n") + fun of_subproof ind ctxt proof = let val ind = ind + 1 @@ -195,24 +232,27 @@ SOME (size s - ind * indent_size - 1)) ^ suffix ^ "\n" end + and of_subproofs _ _ _ [] = "" | of_subproofs ind ctxt qs subproofs = (if member (op =) qs Then then of_moreover ind else "") ^ space_implode (of_moreover ind) (map (of_subproof ind ctxt) subproofs) + and add_step_pre ind qs subproofs (s, ctxt) = (s ^ of_subproofs ind ctxt qs subproofs ^ of_indent ind, ctxt) + and add_step ind (Let (t1, t2)) = add_suffix (of_indent ind ^ "let ") #> add_term t1 #> add_suffix " = " #> add_term t2 #> add_suffix "\n" - | add_step ind (Prove (qs, Fix xs, l, t, subproofs, By_Metis facts)) = + | add_step ind (Prove (qs, Fix xs, l, t, subproofs, By (facts, method))) = (case xs of [] => (* have *) add_step_pre ind qs subproofs #> add_suffix (of_prove qs (length subproofs) ^ " ") - #> add_step_post ind l t facts "" + #> add_step_post ind l t facts method "" | _ => (* obtain *) add_step_pre ind qs subproofs #> add_suffix (of_obtain qs (length subproofs) ^ " ") @@ -221,26 +261,32 @@ (* The new skolemizer puts the arguments in the same order as the ATPs (E and Vampire -- but see also "atp_proof_reconstruct.ML" regarding Vampire). *) - #> add_step_post ind l t facts - (if exists (fn (_, T) => length (binder_types T) > 1) xs then + #> add_step_post ind l t facts method + (if exists (fn (_, T) => length (binder_types T) > 1) xs + andalso method = MetisM then "using [[metis_new_skolem]] " else "")) + and add_steps ind = fold (add_step ind) + and of_proof ind ctxt (Proof (Fix xs, Assume assms, steps)) = ("", ctxt) |> add_fix ind xs |> add_assms ind assms |> add_steps ind steps |> fst + in + (* FIXME: sh_try0 might produce one-step proofs that are better than the + Metis one-liners *) (* One-step proofs are pointless; better use the Metis one-liner directly. *) - case proof of + (*case proof of Proof (Fix [], Assume [], [Prove (_, Fix [], _, _, [], _)]) => "" - | _ => (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^ + | _ =>*) (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^ of_indent 0 ^ "proof -\n" ^ of_proof 1 ctxt proof ^ of_indent 0 ^ (if n <> 1 then "next" else "qed") end - end +end diff -r 760a567f1609 -r 8a25b17e3d79 src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Thu Jul 11 13:33:20 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Thu Jul 11 20:08:06 2013 +0200 @@ -23,16 +23,26 @@ (* for |fix|>0, this is an obtain step; step may contain subproofs *) Prove of isar_qualifier list * fix * label * term * isar_proof list * byline and byline = - By_Metis of facts + By of facts * proof_method + and proof_method = + MetisM | + SimpM | + AutoM | + FastforceM | + ArithM + + (* legacy *) + val By_Metis : facts -> byline val no_label : label val no_facts : facts - (*val label_ord : label * label -> order*) + val label_ord : label * label -> order val dummy_isar_step : isar_step val string_of_label : label -> string + val fix_of_proof : isar_proof -> fix val assms_of_proof : isar_proof -> assms val steps_of_proof : isar_proof -> isar_step list @@ -40,13 +50,17 @@ val label_of_step : isar_step -> label option val subproofs_of_step : isar_step -> isar_proof list option val byline_of_step : isar_step -> byline option + val proof_method_of_step : isar_step -> proof_method option val fold_isar_step : (isar_step -> 'a -> 'a) -> isar_step -> 'a -> 'a val fold_isar_steps : (isar_step -> 'a -> 'a) -> isar_step list -> 'a -> 'a - val add_metis_steps_top_level : isar_step list -> int -> int - val add_metis_steps : isar_step list -> int -> int + val map_isar_steps : (isar_step -> isar_step) -> isar_proof -> isar_proof + + val map_facts_of_byline : (facts -> facts) -> byline -> byline + + val add_proof_steps : isar_step list -> int -> int (** canonical proof labels: 1, 2, 3, ... in post traversal order **) val canonical_label_ord : (label * label) -> order @@ -74,12 +88,21 @@ (* for |fix|>0, this is an obtain step; step may contain subproofs *) Prove of isar_qualifier list * fix * label * term * isar_proof list * byline and byline = - By_Metis of facts + By of facts * proof_method +and proof_method = + MetisM | + SimpM | + AutoM | + FastforceM | + ArithM + +(* legacy *) +fun By_Metis facts = By (facts, MetisM) val no_label = ("", ~1) val no_facts = ([],[]) -(*val label_ord = pairself swap #> prod_ord int_ord fast_string_ord*) +val label_ord = pairself swap #> prod_ord int_ord fast_string_ord val dummy_isar_step = Let (Term.dummy, Term.dummy) @@ -98,18 +121,35 @@ fun byline_of_step (Prove (_, _, _, _, _, byline)) = SOME byline | byline_of_step _ = NONE +fun proof_method_of_step (Prove (_, _, _, _, _, By(_, method))) = SOME method + | proof_method_of_step _ = NONE + fun fold_isar_steps f = fold (fold_isar_step f) and fold_isar_step f step s = fold (steps_of_proof #> fold_isar_steps f) (these (subproofs_of_step step)) s |> f step -val add_metis_steps_top_level = - fold (byline_of_step #> (fn SOME (By_Metis _) => Integer.add 1 | _ => I)) +fun map_isar_steps f proof = + let + fun do_proof (Proof (fix, assms, steps)) = + Proof (fix, assms, map do_step steps) -val add_metis_steps = - fold_isar_steps - (byline_of_step #> (fn SOME (By_Metis _) => Integer.add 1 | _ => I)) + and do_step (step as Let _) = f step + | do_step (Prove (qs, xs, l, t, subproofs, by)) = + let + val subproofs = map do_proof subproofs + val step = Prove (qs, xs, l, t, subproofs, by) + in + f step + end + in + do_proof proof + end + +fun map_facts_of_byline f (By (facts, method)) = By (f facts, method) + +val add_proof_steps = fold_isar_steps (fn Prove _ => Integer.add 1 | _ => I) (** canonical proof labels: 1, 2, 3, ... in post traversal order **) @@ -127,8 +167,8 @@ fun next_label l (next, subst) = (lbl next, (next + 1, (l, lbl next) :: subst)) - fun do_byline (By_Metis (lfs, gfs)) (_, subst) = - By_Metis (map (AList.lookup (op =) subst #> the) lfs, gfs) + fun do_byline by (_, subst) = + by |> map_facts_of_byline (apfst (map (AList.lookup (op =) subst #> the))) handle Option.Option => raise Fail "Sledgehammer_Compress: relabel_proof_canonically" diff -r 760a567f1609 -r 8a25b17e3d79 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Jul 11 13:33:20 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Jul 11 20:08:06 2013 +0200 @@ -46,6 +46,7 @@ open Sledgehammer_Print open Sledgehammer_Preplay open Sledgehammer_Compress +open Sledgehammer_Try0 structure String_Redirect = ATP_Proof_Redirect( type key = step_name @@ -325,7 +326,7 @@ val add_labels_of_proof = steps_of_proof #> fold_isar_steps - (byline_of_step #> (fn SOME (By_Metis (ls, _)) => union (op =) ls + (byline_of_step #> (fn SOME (By ((ls, _), _)) => union (op =) ls | _ => I)) fun kill_useless_labels_in_proof proof = @@ -378,8 +379,8 @@ let val (assms, subst) = do_assms subst depth assms in Proof (fix, assms, do_steps subst depth 1 steps) end - and do_byline subst depth (By_Metis facts) = - By_Metis (do_facts subst facts) + and do_byline subst depth byline = + map_facts_of_byline (do_facts subst) byline and do_proofs subst depth = map (do_proof subst (depth + 1)) in do_proof [] 0 end @@ -389,10 +390,11 @@ | do_qs_lfs (SOME l0) lfs = if member (op =) lfs l0 then ([Then], lfs |> remove (op =) l0) else ([], lfs) - fun chain_step lbl (Prove (qs, xs, l, t, subproofs, By_Metis (lfs, gfs))) = + fun chain_step lbl + (Prove (qs, xs, l, t, subproofs, By ((lfs, gfs), method))) = let val (qs', lfs) = do_qs_lfs lbl lfs in Prove (qs' @ qs, xs, l, t, chain_proofs subproofs, - By_Metis (lfs, gfs)) + By ((lfs, gfs), method)) end | chain_step _ step = step and chain_steps _ [] = [] @@ -571,6 +573,9 @@ do_proof true params assms infs end + (* 60 seconds seems like a good interpreation of "no timeout" *) + val preplay_timeout = preplay_timeout |> the_default (seconds 60.0) + val clean_up_labels_in_proof = chain_direct_proof #> kill_useless_labels_in_proof @@ -588,6 +593,7 @@ (if isar_proofs = SOME true then isar_compress else 1000.0) (if isar_proofs = SOME true then isar_compress_degree else 100) merge_timeout_slack preplay_interface + |> try0 preplay_timeout preplay_interface |> clean_up_labels_in_proof val isar_text = string_of_proof ctxt type_enc lam_trans subgoal subgoal_count @@ -605,7 +611,7 @@ val msg = (if verbose then let - val num_steps = add_metis_steps (steps_of_proof isar_proof) 0 + val num_steps = add_proof_steps (steps_of_proof isar_proof) 0 in [string_of_int num_steps ^ " step" ^ plural_s num_steps] end else []) @ diff -r 760a567f1609 -r 8a25b17e3d79 src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML Thu Jul 11 20:08:06 2013 +0200 @@ -0,0 +1,116 @@ +(* Title: HOL/Tools/Sledgehammer/sledgehammer_try0.ML + Author: Jasmin Blanchette, TU Muenchen + Author: Steffen Juilf Smolka, TU Muenchen + +Try replacing calls to metis with calls to other proof methods in order to +speed up proofs, eliminate dependencies, and repair broken proof steps. +*) + +signature SLEDGEHAMMER_TRY0 = +sig + type isar_proof = Sledgehammer_Proof.isar_proof + type preplay_interface = Sledgehammer_Preplay.preplay_interface + + val try0 : Time.time -> preplay_interface -> isar_proof -> isar_proof +end + +structure Sledgehammer_Try0 : SLEDGEHAMMER_TRY0 = +struct + +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 + 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)) + in + (* 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 + end + +fun try0_step preplay_timeout preplay_interface (step as Let _) = step + | try0_step preplay_timeout ({preplay_quietly, get_time, set_time, + set_preplay_fail, ...} : preplay_interface) + (step as Prove (_, _, l, _, _, _)) = + let + + val (preplay_fail, timeout) = + case get_time l of + (true, _) => (true, preplay_timeout) + | (false, t) => (false, t) + + fun try_variant variant = + case preplay_quietly timeout variant of + (true, _) => NONE + | time as (false, _) => SOME (variant, time) + + in + case Par_List.get_some try_variant (variants step) of + SOME (step, time) => (set_time l time; step) + | NONE => (if preplay_fail then set_preplay_fail true else (); step) + end + +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) + +end