--- 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 "\<open>" str andalso String.isSuffix "\<close>" 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 _ =>
--- 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
--- 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