# HG changeset patch # User desharna # Date 1743175059 -3600 # Node ID 3c3ae21cf12d6de4bfb17d6a5c01be91b96b777a # Parent eae75676ecd7a5721659e68fa7777499f30da636# Parent 07e95760a612dd34067fe8cabdbe17384ea13b53 merged diff -r 07e95760a612 -r 3c3ae21cf12d src/HOL/Tools/Sledgehammer/sledgehammer_prover_tactic.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_tactic.ML Fri Mar 28 11:56:18 2025 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_tactic.ML Fri Mar 28 16:17:39 2025 +0100 @@ -93,38 +93,46 @@ let val (basic_slice as (slice_size, _, _, _, _), No_Slice) = slice val facts = facts_of_basic_slice basic_slice factss - val {facts = chained, ...} = Proof.goal state val ctxt = Proof.context_of state - val (local_facts, global_facts) = - ([], []) - |> fold (fn ((_, (scope, _)), thm) => - if scope = Global then apsnd (cons thm) - else if scope = Chained then I - else apfst (cons thm)) facts - |> apfst (append chained) - - val run_timeout = slice_timeout slice_size slices timeout + fun run_try0 () : Try0.result option = + let + val _ = Proof_Context.get_fact + val _ = Args.named_fact + val _ = Pretty.pure_string_of + val _ = Thm.pretty_thm + val run_timeout = slice_timeout slice_size slices timeout + fun is_cartouche str = String.isPrefix "\" str andalso String.isSuffix "\" str + fun xref_of_fact (((name, (_, status)), thm) : Sledgehammer_Fact.fact) = + let + val xref = + if is_cartouche name then + (* Facts.Fact (Thm.string_of_thm ctxt thm |> @{print}) *) + Facts.Fact (Pretty.pure_string_of (Thm.pretty_thm ctxt thm) |> @{print}) + else + Facts.named name + in + (xref, []) + end + val xrefs = map xref_of_fact facts + val facts : Try0.facts = {usings = xrefs, simps = [], intros = [], elims = [], dests = []} + in + Try0.get_proof_method_or_noop name (SOME run_timeout) facts state + end val timer = Timer.startRealTimer () - val out = - (Timeout.apply run_timeout - (Goal.prove ctxt [] [] (Logic.get_goal (Thm.prop_of goal) subgoal)) - (fn {context = ctxt, ...} => - HEADGOAL (tac_of ctxt name (local_facts, global_facts))); - NONE) + (case run_try0 () of + NONE => SOME GaveUp + | SOME _ => NONE) handle ERROR _ => SOME GaveUp | Exn.Interrupt_Breakdown => SOME GaveUp | Timeout.TIMEOUT _ => SOME TimedOut - val run_time = Timer.checkRealTimer timer val (outcome, used_facts) = (case out of - NONE => - (found_something name; - (NONE, map fst facts)) + NONE => (found_something name; (NONE, map fst facts)) | some_failure => (some_failure, [])) val message = fn _ => diff -r 07e95760a612 -r 3c3ae21cf12d src/HOL/Tools/try0.ML --- a/src/HOL/Tools/try0.ML Fri Mar 28 11:56:18 2025 +0100 +++ b/src/HOL/Tools/try0.ML Fri Mar 28 16:17:39 2025 +0100 @@ -26,6 +26,7 @@ val register_proof_method : string -> proof_method_options -> proof_method -> unit val get_proof_method : string -> proof_method option + val get_proof_method_or_noop : string -> proof_method val get_all_proof_method_names : unit -> string list datatype mode = Auto_Try | Try | Normal diff -r 07e95760a612 -r 3c3ae21cf12d src/HOL/Tools/try0_util.ML --- a/src/HOL/Tools/try0_util.ML Fri Mar 28 11:56:18 2025 +0100 +++ b/src/HOL/Tools/try0_util.ML Fri Mar 28 16:17:39 2025 +0100 @@ -11,11 +11,10 @@ val string_of_xref : Try0.xref -> string type facts_prefixes = - {usings: string, - simps : string, - intros : string, - elims : string, - dests : string} + {simps : string option, + intros : string option, + elims : string option, + dests : string option} val full_attrs : facts_prefixes val clas_attrs : facts_prefixes val simp_attrs : facts_prefixes @@ -37,21 +36,21 @@ type facts_prefixes = - {usings: string, - simps : string, - intros : string, - elims : string, - dests : string} + {simps : string option, + intros : string option, + elims : string option, + dests : string option} val no_attrs : facts_prefixes = - {usings = "", simps = "", intros = "", elims = "", dests = ""} + {simps = NONE, intros = NONE, elims = NONE, dests = NONE} val full_attrs : facts_prefixes = - {usings = "", simps = "simp", intros = "intro", elims = "elim", dests = "dest"} + {simps = SOME "simp: ", intros = SOME "intro: ", elims = SOME "elim: ", dests = SOME "dest: "} val clas_attrs : facts_prefixes = - {usings = "", simps = "", intros = "intro", elims = "elim", dests = "dest"} + {simps = NONE, intros = SOME "intro: ", elims = SOME "elim: ", dests = SOME "dest: "} val simp_attrs : facts_prefixes = - {usings = "", simps = "add", intros = "", elims = "", dests = ""} -val metis_attrs : facts_prefixes = no_attrs + {simps = SOME "add: ", intros = NONE, elims = NONE, dests = NONE} +val metis_attrs : facts_prefixes = + {simps = SOME "", intros = SOME "", elims = SOME "", dests = SOME ""} local @@ -88,28 +87,36 @@ val ctxt = Proof.context_of st val (unused_simps, simps_attrs) = - if #simps prefixes = "" then - (#simps facts, "") + if null (#simps facts) then + ([], "") else - ([], " " ^ #simps prefixes ^ ": " ^ space_implode "" (map string_of_xref (#simps facts))) + (case #simps prefixes of + NONE => (#simps facts, "") + | SOME prefix => ([], " " ^ prefix ^ space_implode "" (map string_of_xref (#simps facts)))) val (unused_intros, intros_attrs) = - if #intros prefixes = "" then - (#intros facts, "") + if null (#intros facts) then + ([], "") else - ([], " " ^ #intros prefixes ^ ": " ^ space_implode "" (map string_of_xref (#intros facts))) + (case #intros prefixes of + NONE => (#intros facts, "") + | SOME prefix => ([], " " ^ prefix ^ space_implode "" (map string_of_xref (#intros facts)))) val (unused_elims, elims_attrs) = - if #elims prefixes = "" then - (#elims facts, "") + if null (#elims facts) then + ([], "") else - ([], " " ^ #elims prefixes ^ ": " ^ space_implode "" (map string_of_xref (#elims facts))) + (case #elims prefixes of + NONE => (#elims facts, "") + | SOME prefix => ([], " " ^ prefix ^ space_implode "" (map string_of_xref (#elims facts)))) val (unused_dests, dests_attrs) = - if #dests prefixes = "" then - (#dests facts, "") + if null (#dests facts) then + ([], "") else - ([], " " ^ #dests prefixes ^ ": " ^ space_implode "" (map string_of_xref (#dests facts))) + (case #dests prefixes of + NONE => (#dests facts, "") + | SOME prefix => ([], " " ^ prefix ^ space_implode "" (map string_of_xref (#dests facts)))) val unused = #usings facts @ unused_simps @ unused_intros @ unused_elims @ unused_dests