--- a/src/HOL/HOL.thy Thu Mar 27 13:44:42 2025 +0100
+++ b/src/HOL/HOL.thy Thu Mar 27 14:33:08 2025 +0100
@@ -34,6 +34,12 @@
ML_file \<open>~~/src/Tools/subtyping.ML\<close>
ML_file \<open>~~/src/Tools/case_product.ML\<close>
+ML \<open>
+val _ =
+ Try.tool_setup
+ {name = "try0", weight = 30, auto_option = \<^system_option>\<open>auto_methods\<close>,
+ body = fn auto => fst o Try0.generic_try0 (if auto then Try0.Auto_Try else Try0.Try) NONE []}
+\<close>
ML \<open>Plugin_Name.declare_setup \<^binding>\<open>extraction\<close>\<close>
--- a/src/HOL/Tools/Nunchaku/nunchaku_commands.ML Thu Mar 27 13:44:42 2025 +0100
+++ b/src/HOL/Tools/Nunchaku/nunchaku_commands.ML Thu Mar 27 14:33:08 2025 +0100
@@ -246,7 +246,7 @@
fun run_chaku override_params mode i state0 =
let
- val state = Proof.map_contexts (Try0_Util.silence_methods false) state0;
+ val state = Proof.map_contexts Try0_HOL.silence_methods state0;
val thy = Proof.theory_of state;
val ctxt = Proof.context_of state;
val _ = List.app check_raw_param override_params;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Thu Mar 27 13:44:42 2025 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Thu Mar 27 14:33:08 2025 +0100
@@ -292,7 +292,7 @@
fun default_params thy = get_params Normal thy o map (apsnd single)
val silence_state =
- Proof.map_contexts (Try0_Util.silence_methods false #> Config.put SMT_Config.verbose false)
+ Proof.map_contexts (Try0_HOL.silence_methods #> Config.put SMT_Config.verbose false)
(* Sledgehammer the given subgoal *)
--- a/src/HOL/Tools/try0.ML Thu Mar 27 13:44:42 2025 +0100
+++ b/src/HOL/Tools/try0.ML Thu Mar 27 14:33:08 2025 +0100
@@ -17,6 +17,7 @@
val register_proof_method : string -> proof_method_options -> proof_method -> unit
val get_proof_method : string -> proof_method option
+ val get_all_proof_method_names : unit -> string list
datatype mode = Auto_Try | Try | Normal
val generic_try0 : mode -> Time.time option -> tagged_xref list -> Proof.state ->
--- a/src/HOL/Tools/try0_util.ML Thu Mar 27 13:44:42 2025 +0100
+++ b/src/HOL/Tools/try0_util.ML Thu Mar 27 14:33:08 2025 +0100
@@ -8,25 +8,19 @@
signature TRY0_UTIL =
sig
- val silence_methods : bool -> Proof.context -> Proof.context
val string_of_xref : Try0.xref -> string
+ val full_attrs : (Try0.modifier * string) list
+ val clas_attrs : (Try0.modifier * string) list
+ val simp_attrs : (Try0.modifier * string) list
+ val metis_attrs : (Try0.modifier * string) list
+ val no_attrs : (Try0.modifier * string) list
val apply_raw_named_method : string -> bool -> (Try0.modifier * string) list ->
- Time.time option -> Try0.tagged_xref list -> Proof.state -> Try0.result option
+ (Proof.context -> Proof.context) -> Time.time option -> Try0.tagged_xref list -> Proof.state ->
+ Try0.result option
end
structure Try0_Util : TRY0_UTIL = struct
-(* Makes reconstructor tools as silent as possible. The "set_visible" calls suppresses "Unification
- bound exceeded" warnings and the like. *)
-fun silence_methods debug =
- Config.put Metis_Tactic.verbose debug
- #> not debug ? (fn ctxt =>
- ctxt
- |> Simplifier_Trace.disable
- |> Context_Position.set_visible false
- |> Config.put Unify.unify_trace false
- |> Config.put Argo_Tactic.trace "none")
-
fun string_of_xref ((xref, args) : Try0.xref) =
(case xref of
Facts.Fact literal => literal |> Symbol_Pos.explode0 |> Symbol_Pos.implode |> cartouche
@@ -34,6 +28,13 @@
Facts.string_of_ref xref) ^ implode
(map (enclose "[" "]" o Pretty.unformatted_string_of o Token.pretty_src \<^context>) args)
+
+val full_attrs = [(Try0.Simp, "simp"), (Try0.Intro, "intro"), (Try0.Elim, "elim"), (Try0.Dest, "dest")]
+val clas_attrs = [(Try0.Intro, "intro"), (Try0.Elim, "elim"), (Try0.Dest, "dest")]
+val simp_attrs = [(Try0.Simp, "add")]
+val metis_attrs = [(Try0.Simp, ""), (Try0.Intro, ""), (Try0.Elim, ""), (Try0.Dest, "")]
+val no_attrs = []
+
local
fun add_attr_text (tagged : Try0.tagged_xref list) (tag, src) s =
@@ -74,10 +75,11 @@
in
-fun apply_raw_named_method (name : string) all_goals attrs timeout_opt
- (tagged : Try0.tagged_xref list) (st : Proof.state) : Try0.result option =
+fun apply_raw_named_method (name : string) all_goals attrs
+ (silence_methods : Proof.context -> Proof.context) timeout_opt (tagged : Try0.tagged_xref list)
+ (st : Proof.state) : Try0.result option =
let
- val st = Proof.map_contexts (silence_methods false) st
+ val st = Proof.map_contexts silence_methods st
val unused =
tagged
|> filter
--- a/src/HOL/Try0.thy Thu Mar 27 13:44:42 2025 +0100
+++ b/src/HOL/Try0.thy Thu Mar 27 14:33:08 2025 +0100
@@ -10,5 +10,13 @@
begin
ML_file \<open>Tools/try0.ML\<close>
+ML_file \<open>Tools/try0_util.ML\<close>
+
+ML \<open>
+val () =
+ Try0.register_proof_method "simp" {run_if_auto_try = true}
+ (Try0_Util.apply_raw_named_method "simp" false Try0_Util.simp_attrs Simplifier_Trace.disable)
+ handle Symtab.DUP _ => ()
+\<close>
end
\ No newline at end of file
--- a/src/HOL/Try0_HOL.thy Thu Mar 27 13:44:42 2025 +0100
+++ b/src/HOL/Try0_HOL.thy Thu Mar 27 14:33:08 2025 +0100
@@ -7,29 +7,31 @@
imports Try0 Presburger
begin
+ML \<open>
+signature TRY0_HOL =
+sig
+ val silence_methods : Proof.context -> Proof.context
+end
-ML_file \<open>Tools/try0_util.ML\<close>
+structure Try0_HOL : TRY0_HOL = struct
-ML \<open>
-val _ =
- Try.tool_setup
- {name = "try0", weight = 30, auto_option = \<^system_option>\<open>auto_methods\<close>,
- body = fn auto => fst o Try0.generic_try0 (if auto then Try0.Auto_Try else Try0.Try) NONE []}
-\<close>
+(* Makes reconstructor tools as silent as possible. The "set_visible" calls suppresses "Unification
+ bound exceeded" warnings and the like. *)
+fun silence_methods ctxt =
+ ctxt
+ |> Config.put Metis_Tactic.verbose false
+ |> Simplifier_Trace.disable
+ |> Context_Position.set_visible false
+ |> Config.put Unify.unify_trace false
+ |> Config.put Argo_Tactic.trace "none"
-ML \<open>
local
-val full_attrs = [(Try0.Simp, "simp"), (Try0.Intro, "intro"), (Try0.Elim, "elim"), (Try0.Dest, "dest")]
-val clas_attrs = [(Try0.Intro, "intro"), (Try0.Elim, "elim"), (Try0.Dest, "dest")]
-val simp_attrs = [(Try0.Simp, "add")]
-val metis_attrs = [(Try0.Simp, ""), (Try0.Intro, ""), (Try0.Elim, ""), (Try0.Dest, "")]
-val no_attrs = []
+open Try0_Util
(* name * (run_if_auto_try * (all_goals * tags)) *)
val raw_named_methods =
- [("simp", (true, (false, simp_attrs))),
- ("auto", (true, (true, full_attrs))),
+ [("auto", (true, (true, full_attrs))),
("blast", (true, (false, clas_attrs))),
("metis", (true, (false, metis_attrs))),
("argo", (true, (false, no_attrs))),
@@ -47,12 +49,17 @@
val () = raw_named_methods
|> List.app (fn (name, (run_if_auto_try, (all_goals, tags))) =>
- let val meth : Try0.proof_method = Try0_Util.apply_raw_named_method name all_goals tags in
+ let
+ val meth : Try0.proof_method =
+ Try0_Util.apply_raw_named_method name all_goals tags silence_methods
+ in
Try0.register_proof_method name {run_if_auto_try = run_if_auto_try} meth
handle Symtab.DUP _ => ()
end)
end
+
+end
\<close>
end
\ No newline at end of file