# HG changeset patch # User desharna # Date 1639834213 -3600 # Node ID ae2185967e676f68b7ea2dd91aad327fb98f8d68 # Parent 0b6f795d3b786bf84288f341d3a1892f11991ed7 exported Sledgehammer.launch_prover and use it in Mirabelle diff -r 0b6f795d3b78 -r ae2185967e67 src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML --- 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 diff -r 0b6f795d3b78 -r ae2185967e67 src/HOL/Tools/Sledgehammer/sledgehammer.ML --- 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, [])