--- a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML Sat Dec 18 13:27:42 2021 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML Sat Dec 18 14:30:13 2021 +0100
@@ -246,24 +246,6 @@
end
-fun get_prover_name thy args =
- let
- fun default_prover_name () =
- hd (#provers (Sledgehammer_Commands.default_params thy []))
- handle List.Empty => error "No ATP available"
- in
- (case AList.lookup (op =) args proverK of
- SOME name => name
- | NONE => default_prover_name ())
- end
-
-fun get_prover ctxt name params goal =
- let
- val learn = Sledgehammer_MaSh.mash_learn_proof ctxt params (Thm.prop_of goal)
- in
- Sledgehammer_Prover_Minimize.get_minimizing_prover ctxt Sledgehammer_Prover.Normal learn name
- end
-
type stature = ATP_Problem_Generate.stature
fun is_good_line s =
@@ -345,7 +327,7 @@
val induction_rules =
Sledgehammer.induction_rules_for_prover ctxt prover_name induction_rules
val inst_inducts = induction_rules = Sledgehammer_Prover.Instantiate
- val fact_override = Sledgehammer_Fact.no_fact_override
+ val fact_override as {only, ...} = Sledgehammer_Fact.no_fact_override
val {facts = chained_thms, goal, ...} = Proof.goal state
val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal i ctxt
val facts = Sledgehammer_Fact.nearly_all_facts_of_context ctxt inst_inducts fact_override
@@ -357,12 +339,14 @@
facts
|> Sledgehammer_MaSh.relevant_facts ctxt params prover_name max_facts fact_override
hyp_ts concl_t
- |> map (apsnd (Sledgehammer_Prover.maybe_filter_out_induction_rules induction_rules))
- val prover = get_prover ctxt prover_name params goal
val problem =
{comment = "", state = state', goal = goal, subgoal = i,
subgoal_count = Sledgehammer_Util.subgoal_count state, factss = factss, found_proof = I}
- in prover params problem end)) ()
+
+ val learn = Sledgehammer_MaSh.mash_learn_proof ctxt params (Thm.prop_of goal)
+ in
+ Sledgehammer.launch_prover params Sledgehammer_Prover.Normal only learn problem prover_name
+ end)) ()
handle Timeout.TIMEOUT _ => failed ATP_Proof.TimedOut
| Fail "inappropriate" => failed ATP_Proof.Inappropriate
val time_prover = run_time |> Time.toMilliseconds
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Sat Dec 18 13:27:42 2021 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Sat Dec 18 14:30:13 2021 +0100
@@ -16,6 +16,8 @@
type mode = Sledgehammer_Prover.mode
type params = Sledgehammer_Prover.params
type induction_rules = Sledgehammer_Prover.induction_rules
+ type prover_problem = Sledgehammer_Prover.prover_problem
+ type prover_result = Sledgehammer_Prover.prover_result
val someN : string
val noneN : string
@@ -26,6 +28,8 @@
induction_rules
val play_one_line_proof : bool -> Time.time -> (string * stature) list -> Proof.state -> int ->
proof_method * proof_method list list -> (string * stature) list * (proof_method * play_outcome)
+ val launch_prover : params -> mode -> bool -> (thm list -> unit) -> prover_problem -> string ->
+ prover_result
val string_of_factss : (string * fact list) list -> string
val run_sledgehammer : params -> mode -> (string -> unit) option -> int -> fact_override ->
Proof.state -> bool * (string * string list)
@@ -121,23 +125,24 @@
|> (fn (used_facts, (meth, play)) =>
(used_facts |> filter_out (fn (_, (sc, _)) => sc = Chained), (meth, play)))
-fun launch_prover (params as {debug, verbose, spy, max_facts, minimize, timeout, preplay_timeout,
- expect, induction_rules, ...}) mode writeln_result only learn
- {comment, state, goal, subgoal, subgoal_count, factss as (_, facts) :: _, found_proof} name =
+fun launch_prover (params as {verbose, spy, max_facts, induction_rules, ...}) mode only learn
+ ({comment, state, goal, subgoal, subgoal_count, factss, found_proof} : prover_problem) name =
let
val ctxt = Proof.context_of state
- val hard_timeout = Time.scale 5.0 timeout
val _ = spying spy (fn () => (state, subgoal, name, "Launched"))
val max_facts = max_facts |> the_default (default_max_facts_of_prover ctxt name)
- val num_facts = length facts |> not only ? Integer.min max_facts
+ val num_facts =
+ (case factss of
+ (_, facts) :: _ => length facts |> not only ? Integer.min max_facts
+ | _ => 0)
val induction_rules = induction_rules_for_prover ctxt name induction_rules
val problem =
{comment = comment, state = state, goal = goal, subgoal = subgoal,
subgoal_count = subgoal_count,
factss = factss
- (* We take num_facts because factss contain facts for the maximum of all called provers. *)
+ (* We take num_facts because factss contains the maximum of all called provers. *)
|> map (apsnd (take num_facts o maybe_filter_out_induction_rules induction_rules)),
found_proof = found_proof}
@@ -147,8 +152,8 @@
|> filter_used_facts false used_facts
|> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j)
|> commas
- |> prefix ("Fact" ^ plural_s (length facts) ^ " in " ^ quote name ^
- " proof (of " ^ string_of_int (length facts) ^ "): ")
+ |> prefix ("Fact" ^ plural_s num_facts ^ " in " ^ quote name ^
+ " proof (of " ^ string_of_int num_facts ^ "): ")
|> writeln
fun spying_str_of_res ({outcome = NONE, used_facts, used_from, ...} : prover_result) =
@@ -182,20 +187,40 @@
end
| spying_str_of_res {outcome = SOME failure, ...} =
"Failure: " ^ string_of_atp_failure failure
+ in
+ problem
+ |> get_minimizing_prover ctxt mode learn name params
+ |> verbose ? tap (fn {outcome = NONE, used_facts as _ :: _, used_from, ...} =>
+ print_used_facts used_facts used_from
+ | _ => ())
+ |> spy ? tap (fn res => spying spy (fn () => (state, subgoal, name, spying_str_of_res res)))
+ end
+
+fun preplay_prover_result ({ minimize, preplay_timeout, ...} : params) state subgoal
+ ({outcome, used_facts, preferred_methss, message, ...} : prover_result) =
+ let
+ val output =
+ if outcome = SOME ATP_Proof.TimedOut then
+ timeoutN
+ else if is_some outcome then
+ noneN
+ else
+ someN
+ fun output_message () = message (fn () =>
+ play_one_line_proof minimize preplay_timeout used_facts state subgoal preferred_methss)
+ in
+ (output, output_message)
+ end
+
+fun launch_prover_and_preplay (params as {debug, timeout, expect, ...}) mode writeln_result only
+ learn (problem as {state, subgoal, ...}) name =
+ let
+ val ctxt = Proof.context_of state
+ val hard_timeout = Time.scale 5.0 timeout
fun really_go () =
- problem
- |> get_minimizing_prover ctxt mode learn name params
- |> verbose ? tap (fn {outcome = NONE, used_facts as _ :: _, used_from, ...} =>
- print_used_facts used_facts used_from
- | _ => ())
- |> spy ? tap (fn res => spying spy (fn () => (state, subgoal, name, spying_str_of_res res)))
- |> (fn {outcome, used_facts, preferred_methss, message, ...} =>
- (if outcome = SOME ATP_Proof.TimedOut then timeoutN
- else if is_some outcome then noneN
- else someN,
- fn () => message (fn () => play_one_line_proof minimize preplay_timeout used_facts state
- subgoal preferred_methss)))
+ launch_prover params mode only learn problem name
+ |> preplay_prover_result params state subgoal
fun go () =
let
@@ -313,7 +338,7 @@
{comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n,
factss = factss, found_proof = found_proof}
val learn = mash_learn_proof ctxt params (Thm.prop_of goal)
- val launch = launch_prover params mode writeln_result only learn
+ val launch = launch_prover_and_preplay params mode writeln_result only learn
in
if mode = Auto_Try then
(unknownN, [])