--- 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"
--- 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
--- 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
--- 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
--- 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"
--- 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
[]) @
--- /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