# HG changeset patch # User Lukas Bartl # Date 1747047772 -7200 # Node ID 2d854f1cd830f8d2b9a769350159a132d0ec805d # Parent bfc920530ae6bbf1ac71cc07bdc4ffad09acebdf clarify Sledgehammer instantiations without preplay (dont_preplay option and tactic provers) diff -r bfc920530ae6 -r 2d854f1cd830 src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Sun May 11 12:05:10 2025 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon May 12 13:02:52 2025 +0200 @@ -145,17 +145,15 @@ end) |> sort (play_outcome_ord o apply2 (fn (_, (play_outcome, _)) => play_outcome)) -fun select_one_line_proof used_facts preferred_meth preplay_results = +fun select_one_line_proof preferred_meth preplay_results = (case preplay_results of (* Select best method if preplay succeeded *) (best_meth, (best_outcome as Played _, best_used_facts)) :: _ => - (best_used_facts, (best_meth, best_outcome)) + SOME (best_used_facts, (best_meth, best_outcome)) (* Otherwise select preferred method *) | _ => - (used_facts, (preferred_meth, - (case AList.lookup (op =) preplay_results preferred_meth of - SOME (outcome, _) => outcome - | NONE => Play_Timed_Out Time.zeroTime)))) + AList.lookup (op =) preplay_results preferred_meth + |> Option.map (fn (outcome, used_facts) => (used_facts, (preferred_meth, outcome)))) fun launch_prover (params as {verbose, spy, slices, timeout, ...}) mode learn (problem as {state, subgoal, factss, ...} : prover_problem) @@ -225,55 +223,59 @@ fun preplay_prover_result ({verbose, instantiate, minimize, preplay_timeout, ...} : params) state goal subgoal (result as {outcome, used_facts, preferred_methss, message, ...} : prover_result) = - let - val used_facts0 = filter_out (fn (_, (sc, _)) => sc = Chained) used_facts - val pretty_used_facts0 = map (apfst Pretty.str) used_facts0 - val (output, pretty_used_facts, preplay_results) = - if outcome = SOME ATP_Proof.TimedOut then - (SH_TimeOut, pretty_used_facts0, []) - else if outcome = SOME ATP_Proof.OutOfResources then - (SH_ResourcesOut, pretty_used_facts0, []) - else if is_some outcome then - (SH_None, pretty_used_facts0, []) - else - let - val preplay = `(fn pretty_used_facts => - play_one_line_proofs minimize preplay_timeout pretty_used_facts - state goal subgoal (snd preferred_methss)) - fun preplay_succeeded ((_, (Played _, _)) :: _, _) _ = true - | preplay_succeeded _ [] = true - | preplay_succeeded _ _ = false - val instantiate_timeout = Time.scale 5.0 preplay_timeout - val instantiate = if null used_facts0 then SOME false else instantiate - val (preplay_results, pretty_used_facts) = - (case instantiate of - SOME false => preplay pretty_used_facts0 - | SOME true => - (* Always try to infer variable instantiations *) + if outcome = SOME ATP_Proof.TimedOut then + (SH_TimeOut, fn () => message NONE) + else if outcome = SOME ATP_Proof.OutOfResources then + (SH_ResourcesOut, fn () => message NONE) + else if is_some outcome then + (SH_None, fn () => message NONE) + else + let + val used_facts0 = filter_out (fn (_, (sc, _)) => sc = Chained) used_facts + val pretty_used_facts0 = map (apfst Pretty.str) used_facts0 + fun preplay methss pretty_used_facts = + play_one_line_proofs minimize preplay_timeout pretty_used_facts state goal subgoal methss + fun preplay_succeeded ((_, (Played _, _)) :: _) = true + | preplay_succeeded _ = false + val instantiate_timeout = + if preplay_timeout = Time.zeroTime then + Time.fromSeconds 5 + else + Time.scale 5.0 preplay_timeout + val instantiate = if null used_facts0 then SOME false else instantiate + val preplay_results = + (case instantiate of + SOME false => preplay (snd preferred_methss) pretty_used_facts0 + | SOME true => + (* Always try to infer variable instantiations *) + (case instantiate_facts state verbose instantiate_timeout goal subgoal used_facts0 of + NONE => preplay (snd preferred_methss) pretty_used_facts0 + | SOME pretty_used_facts => + if preplay_timeout = Time.zeroTime then + [(fst preferred_methss, (Play_Timed_Out Time.zeroTime, pretty_used_facts))] + else if null (snd preferred_methss) then + preplay [[fst preferred_methss]] pretty_used_facts + else + preplay (snd preferred_methss) pretty_used_facts) + | NONE => + let + val preplay_results0 = preplay (snd preferred_methss) pretty_used_facts0 + val preplay_disabled = + preplay_timeout = Time.zeroTime orelse null (snd preferred_methss) + in + if preplay_succeeded preplay_results0 orelse preplay_disabled then + preplay_results0 + else + (* Preplay failed, now try to infer variable instantiations *) instantiate_facts state verbose instantiate_timeout goal subgoal used_facts0 - |> the_default pretty_used_facts0 - |> preplay - | NONE => - let - val preplay_results0 = preplay pretty_used_facts0 - in - if preplay_succeeded preplay_results0 (snd preferred_methss) then - preplay_results0 - else - (* Preplay failed, now try to infer variable instantiations *) - instantiate_facts state verbose instantiate_timeout goal subgoal used_facts0 - |> Option.map preplay - |> the_default preplay_results0 - end) - in - (SH_Some (result, preplay_results), pretty_used_facts, preplay_results) - end - fun chosen_preplay_outcome () = - select_one_line_proof pretty_used_facts (fst preferred_methss) preplay_results - fun output_message () = message chosen_preplay_outcome - in - (output, output_message) - end + |> Option.map (preplay (snd preferred_methss)) + |> the_default preplay_results0 + end) + fun output_message () = + message (select_one_line_proof (fst preferred_methss) preplay_results) + in + (SH_Some (result, preplay_results), output_message) + end fun analyze_prover_result_for_inconsistency (result as {outcome, used_facts, ...} : prover_result) = if outcome = SOME ATP_Proof.TimedOut then diff -r bfc920530ae6 -r 2d854f1cd830 src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Sun May 11 12:05:10 2025 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Mon May 12 13:02:52 2025 +0200 @@ -220,7 +220,6 @@ | apply_on_subgoal 1 _ = "apply " | apply_on_subgoal i n = "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal 1 n -(* FIXME *) fun proof_method_command meth i n extras = let val (indirect_facts, direct_facts) = diff -r bfc920530ae6 -r 2d854f1cd830 src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Sun May 11 12:05:10 2025 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Mon May 12 13:02:52 2025 +0200 @@ -82,7 +82,7 @@ used_from : fact list, preferred_methss : proof_method * proof_method list list, run_time : Time.time, - message : (unit -> (Pretty.T * stature) list * (proof_method * play_outcome)) -> string} + message : ((Pretty.T * stature) list * (proof_method * play_outcome)) option -> string} type prover = params -> prover_problem -> prover_slice -> prover_result @@ -210,7 +210,7 @@ used_from : fact list, preferred_methss : proof_method * proof_method list list, run_time : Time.time, - message : (unit -> (Pretty.T * stature) list * (proof_method * play_outcome)) -> string} + message : ((Pretty.T * stature) list * (proof_method * play_outcome)) option -> string} type prover = params -> prover_problem -> prover_slice -> prover_result diff -r bfc920530ae6 -r 2d854f1cd830 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Sun May 11 12:05:10 2025 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Mon May 12 13:02:52 2025 +0200 @@ -334,7 +334,7 @@ bunches_of_metis_methods ctxt needs_full_types needs_lam_defs) in (NONE, used_facts, preferred_methss, - fn preplay => + fn preplay_outcome => let val _ = if verbose then writeln "Generating proof text..." else () @@ -361,7 +361,11 @@ try0, minimize, full_atp_proof, goal) end - val one_line_params = (preplay (), proof_banner mode name, subgoal, subgoal_count) + val preplay_result = preplay_outcome + |> the_default + (map (apfst Pretty.str) used_facts, + (preferred, Play_Timed_Out Time.zeroTime)) + val one_line_params = (preplay_result, proof_banner mode name, subgoal, subgoal_count) val num_chained = length (#facts (Proof.goal state)) in proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained diff -r bfc920530ae6 -r 2d854f1cd830 src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Sun May 11 12:05:10 2025 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Mon May 12 13:02:52 2025 +0200 @@ -25,7 +25,7 @@ val minimize_facts : (thm list -> unit) -> string -> params -> prover_slice -> bool -> int -> int -> Proof.state -> thm -> ((string * stature) * thm list) list -> prover_result -> ((string * stature) * thm list) list option - * ((unit -> (Pretty.T * stature) list * (proof_method * play_outcome)) -> string) + * (((Pretty.T * stature) list * (proof_method * play_outcome)) option -> string) val get_minimizing_prover : Proof.context -> mode -> (thm list -> unit) -> string -> prover end; diff -r bfc920530ae6 -r 2d854f1cd830 src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Sun May 11 12:05:10 2025 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Mon May 12 13:02:52 2025 +0200 @@ -153,7 +153,7 @@ bunches_of_metis_methods ctxt false true in ((preferred, methss), - fn preplay => + fn preplay_outcome => let val _ = if verbose then writeln "Generating proof text..." else () @@ -161,7 +161,11 @@ (verbose, (NONE, NONE, []), preplay_timeout, compress, try0, minimize, atp_proof (), goal) - val one_line_params = (preplay (), proof_banner mode name, subgoal, subgoal_count) + val preplay_result = preplay_outcome + |> the_default + (map (apfst Pretty.str) used_facts, + (preferred, Play_Timed_Out Time.zeroTime)) + val one_line_params = (preplay_result, proof_banner mode name, subgoal, subgoal_count) val num_chained = length (#facts (Proof.goal state)) in proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained one_line_params diff -r bfc920530ae6 -r 2d854f1cd830 src/HOL/Tools/Sledgehammer/sledgehammer_prover_tactic.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_tactic.ML Sun May 11 12:05:10 2025 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_tactic.ML Mon May 12 13:02:52 2025 +0200 @@ -98,9 +98,17 @@ NONE => (found_something name; map fst facts) | SOME _ => []) - val message = fn _ => + val message = fn preplay_outcome => (case outcome of - NONE => try_command_line (proof_banner mode name) (Played run_time) command + NONE => + let + val banner = proof_banner mode name + in + (case preplay_outcome of + NONE => try_command_line banner (Played run_time) command + | SOME preplay_result => + one_line_proof_text (preplay_result, banner, subgoal, subgoal_count)) + end | SOME failure => string_of_atp_failure failure) in {outcome = outcome, used_facts = used_facts, used_from = facts,