# HG changeset patch # User desharna # Date 1743146647 -3600 # Node ID 7fee9141da5e5cc6e9bbe874a7c1eec658fc8f95 # Parent 5af097d05e99a6726217e6c6612b039e3ebc11a4# Parent 35a219e372b02f8c9e37a1f88db6b164a27bba3f merged diff -r 35a219e372b0 -r 7fee9141da5e src/HOL/HOL.thy --- a/src/HOL/HOL.thy Fri Mar 28 00:26:18 2025 +0000 +++ b/src/HOL/HOL.thy Fri Mar 28 08:24:07 2025 +0100 @@ -5,7 +5,7 @@ section \The basis of Higher-Order Logic\ theory HOL -imports Pure Tools.Code_Generator +imports Pure Try0 Tools.Code_Generator keywords "try" "solve_direct" "quickcheck" "print_coercions" "print_claset" "print_induct_rules" :: diag and @@ -34,6 +34,12 @@ ML_file \~~/src/Tools/subtyping.ML\ ML_file \~~/src/Tools/case_product.ML\ +ML \ +val _ = + Try.tool_setup + {name = "try0", weight = 30, auto_option = \<^system_option>\auto_methods\, + body = fn auto => fst o Try0.generic_try0 (if auto then Try0.Auto_Try else Try0.Try) NONE Try0.empty_facts} +\ ML \Plugin_Name.declare_setup \<^binding>\extraction\\ diff -r 35a219e372b0 -r 7fee9141da5e src/HOL/Mutabelle/mutabelle_extra.ML --- a/src/HOL/Mutabelle/mutabelle_extra.ML Fri Mar 28 00:26:18 2025 +0000 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML Fri Mar 28 08:24:07 2025 +0100 @@ -148,7 +148,7 @@ let val state = Proof.theorem NONE (K I) (map (single o rpair []) [t]) (Proof_Context.init_global thy) in - case Try0.try0 (SOME (seconds 5.0)) [] state of + case Try0.try0 (SOME (seconds 5.0)) Try0.empty_facts state of [] => (Unsolved, []) | _ => (Solved, []) end diff -r 35a219e372b0 -r 7fee9141da5e src/HOL/Sledgehammer.thy --- a/src/HOL/Sledgehammer.thy Fri Mar 28 00:26:18 2025 +0000 +++ b/src/HOL/Sledgehammer.thy Fri Mar 28 08:24:07 2025 +0100 @@ -7,7 +7,7 @@ section \Sledgehammer: Isabelle--ATP Linkup\ theory Sledgehammer -imports Presburger SMT Try0 +imports Presburger SMT Try0_HOL keywords "sledgehammer" :: diag and "sledgehammer_params" :: thy_decl diff -r 35a219e372b0 -r 7fee9141da5e src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML --- a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML Fri Mar 28 00:26:18 2025 +0000 +++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML Fri Mar 28 08:24:07 2025 +0100 @@ -216,7 +216,7 @@ end -val try0 = not o null o Try0.try0 (SOME (Time.fromSeconds 5)) [] +val try0 = not o null o Try0.try0 (SOME (Time.fromSeconds 5)) Try0.empty_facts fun make_action ({arguments, timeout, output_dir, ...} : Mirabelle.action_context) = let diff -r 35a219e372b0 -r 7fee9141da5e src/HOL/Tools/Mirabelle/mirabelle_try0.ML --- a/src/HOL/Tools/Mirabelle/mirabelle_try0.ML Fri Mar 28 00:26:18 2025 +0000 +++ b/src/HOL/Tools/Mirabelle/mirabelle_try0.ML Fri Mar 28 08:24:07 2025 +0100 @@ -12,9 +12,10 @@ fun make_action ({timeout, ...} : Mirabelle.action_context) = let val generous_timeout = Time.scale 10.0 timeout + val try0 = Try0.try0 (SOME timeout) Try0.empty_facts fun run ({pre, ...} : Mirabelle.command) = - if Timeout.apply generous_timeout (not o null o Try0.try0 (SOME timeout) []) pre then + if Timeout.apply generous_timeout (not o null o try0) pre then "succeeded" else "" diff -r 35a219e372b0 -r 7fee9141da5e src/HOL/Tools/Nunchaku/nunchaku_commands.ML --- a/src/HOL/Tools/Nunchaku/nunchaku_commands.ML Fri Mar 28 00:26:18 2025 +0000 +++ b/src/HOL/Tools/Nunchaku/nunchaku_commands.ML Fri Mar 28 08:24:07 2025 +0100 @@ -246,7 +246,7 @@ fun run_chaku override_params mode i state0 = let - val state = Proof.map_contexts (Try0.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; diff -r 35a219e372b0 -r 7fee9141da5e src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Fri Mar 28 00:26:18 2025 +0000 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Fri Mar 28 08:24:07 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.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 *) diff -r 35a219e372b0 -r 7fee9141da5e src/HOL/Tools/try0.ML --- a/src/HOL/Tools/try0.ML Fri Mar 28 00:26:18 2025 +0000 +++ b/src/HOL/Tools/try0.ML Fri Mar 28 08:24:07 2025 +0100 @@ -1,180 +1,130 @@ -(* Title: HOL/Tools/try0.ML - Author: Jasmin Blanchette, TU Muenchen +(* Title: HOL/Tools/try0.ML + Author: Jasmin Blanchette, LMU Muenchen + Author: Martin Desharnais, LMU Muenchen + Author: Fabian Huch, TU Muenchen Try a combination of proof methods. *) signature TRY0 = sig - val silence_methods : bool -> Proof.context -> Proof.context - datatype modifier = Use | Simp | Intro | Elim | Dest - type xthm = Facts.ref * Token.src list - type tagged_xthm = xthm * modifier list + val serial_commas : string -> string list -> string list + + type xref = Facts.ref * Token.src list + + type facts = + {usings: xref list, + simps : xref list, + intros : xref list, + elims : xref list, + dests : xref list} + val empty_facts : facts + type result = {name: string, command: string, time: Time.time, state: Proof.state} - val apply_proof_method : string -> Time.time option -> (xthm * modifier list) list -> - Proof.state -> result option - val try0 : Time.time option -> tagged_xthm list -> Proof.state -> result list + type proof_method = Time.time option -> facts -> Proof.state -> result option + type proof_method_options = {run_if_auto_try: bool} + + 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 -> facts -> Proof.state -> + (bool * (string * string list)) * result list + val try0 : Time.time option -> facts -> Proof.state -> result list end structure Try0 : TRY0 = struct +fun serial_commas _ [] = ["??"] + | serial_commas _ [s] = [s] + | serial_commas conj [s1, s2] = [s1, conj, s2] + | serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3] + | serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss; + val noneN = "none" datatype mode = Auto_Try | Try | Normal val default_timeout = seconds 5.0 -fun run_tac timeout_opt tac st = - let val with_timeout = - (case timeout_opt of SOME timeout => Timeout.apply_physical timeout | NONE => I) - in with_timeout (Seq.pull o tac) st |> Option.map fst end - -val num_goals = Thm.nprems_of o #goal o Proof.goal -fun apply_recursive recurse elapsed0 timeout_opt apply st = - (case Timing.timing (Option.join o try (run_tac timeout_opt apply)) st of - ({elapsed, ...}, SOME st') => - if recurse andalso num_goals st' > 0 andalso num_goals st' < num_goals st then - let val timeout_opt1 = (Option.map (fn timeout => timeout - elapsed) timeout_opt) - in apply_recursive recurse (elapsed0 + elapsed) timeout_opt1 apply st' end - else (elapsed0 + elapsed, st') - |_ => (elapsed0, st)) +datatype modifier = Use | Simp | Intro | Elim | Dest +type xref = Facts.ref * Token.src list +type tagged_xref = xref * modifier list +type facts = + {usings: xref list, + simps : xref list, + intros : xref list, + elims : xref list, + dests : xref list} -fun parse_method ctxt s = - enclose "(" ")" s - |> Token.explode (Thy_Header.get_keywords' ctxt) Position.start - |> filter Token.is_proper - |> Scan.read Token.stopper Method.parse - |> (fn SOME (Method.Source src, _) => src | _ => raise Fail "expected Source") - -datatype modifier = Use | Simp | Intro | Elim | Dest -type xthm = Facts.ref * Token.src list -type tagged_xthm = xthm * modifier list - -fun string_of_xthm ((xref, args) : xthm) = - (case xref of - Facts.Fact literal => literal |> Symbol_Pos.explode0 |> Symbol_Pos.implode |> cartouche - | _ => - Facts.string_of_ref xref) ^ implode - (map (enclose "[" "]" o Pretty.unformatted_string_of o Token.pretty_src \<^context>) args) - -fun add_attr_text (tagged : tagged_xthm list) (tag, src) s = - let - val fs = tagged |> filter (fn (_, tags) => member (op =) tags tag) |> map (string_of_xthm o fst) - in if null fs then s else s ^ " " ^ (if src = "" then "" else src ^ ": ") ^ implode_space fs end - -fun attrs_text tags (tagged : tagged_xthm list) = - "" |> fold (add_attr_text tagged) tags +val empty_facts: facts = {usings = [], simps = [], intros = [], elims = [], dests = []} +fun union_facts (left : facts) (right : facts) : facts = + {usings = #usings left @ #usings right, + simps = #simps left @ #simps right, + intros = #intros left @ #intros right, + elims = #elims left @ #elims right, + dests = #dests left @ #dests right} type result = {name: string, command: string, time: Time.time, state: Proof.state} +type proof_method = Time.time option -> facts -> Proof.state -> result option +type proof_method_options = {run_if_auto_try: bool} + +val noop_proof_method : proof_method = fn _ => fn _ => fn _ => NONE local - -val full_attrs = [(Simp, "simp"), (Intro, "intro"), (Elim, "elim"), (Dest, "dest")] -val clas_attrs = [(Intro, "intro"), (Elim, "elim"), (Dest, "dest")] -val simp_attrs = [(Simp, "add")] -val metis_attrs = [(Simp, ""), (Intro, ""), (Elim, ""), (Dest, "")] -val no_attrs = [] - -(* name * ((all_goals, run_if_auto_try), tags *) -val raw_named_methods = - [("simp", ((false, true), simp_attrs)), - ("auto", ((true, true), full_attrs)), - ("blast", ((false, true), clas_attrs)), - ("metis", ((false, true), metis_attrs)), - ("argo", ((false, true), no_attrs)), - ("linarith", ((false, true), no_attrs)), - ("presburger", ((false, true), no_attrs)), - ("algebra", ((false, true), no_attrs)), - ("fast", ((false, false), clas_attrs)), - ("fastforce", ((false, false), full_attrs)), - ("force", ((false, false), full_attrs)), - ("meson", ((false, false), metis_attrs)), - ("satx", ((false, false), no_attrs)), - ("order", ((false, true), no_attrs))] - -fun apply_raw_named_method (name, ((all_goals, _), attrs)) timeout_opt tagged st : - result option = - let - val unused = - tagged - |> filter - (fn (_, tags) => not (null tags) andalso null (inter (op =) tags (attrs |> map fst))) - |> map fst - - val attrs = attrs_text attrs tagged - - val ctxt = Proof.context_of st - - val text = - name ^ attrs - |> parse_method ctxt - |> Method.method_cmd ctxt - |> Method.Basic - |> (fn m => Method.Combinator (Method.no_combinator_info, Method.Select_Goals 1, [m])) - - val apply = - Proof.using [Attrib.eval_thms ctxt unused |> map (rpair [] o single)] - #> Proof.refine text #> Seq.filter_results - val num_before = num_goals st - val multiple_goals = all_goals andalso num_before > 1 - val (time, st') = apply_recursive multiple_goals Time.zeroTime timeout_opt apply st - val num_after = num_goals st' - val select = "[" ^ string_of_int (num_before - num_after) ^ "]" - val unused = implode_space (unused |> map string_of_xthm) - val command = - (if unused <> "" then "using " ^ unused ^ " " else "") ^ - (if num_after = 0 then "by " else "apply ") ^ - (name ^ attrs |> attrs <> "" ? enclose "(" ")") ^ - (if multiple_goals andalso num_after > 0 then select else "") - in - if num_before > num_after then - SOME {name = name, command = command, time = time, state = st'} - else NONE - end - + val proof_methods = + Synchronized.var "Try0.proof_methods" (Symtab.empty : proof_method Symtab.table); + val auto_try_proof_methods_names = + Synchronized.var "Try0.auto_try_proof_methods" (Symset.empty : Symset.T); in -val named_methods = map fst raw_named_methods - -fun apply_proof_method name timeout_opt tagged st : - result option = - (case AList.lookup (op =) raw_named_methods name of - NONE => NONE - | SOME raw_method => apply_raw_named_method (name, raw_method) timeout_opt tagged st) +fun register_proof_method name ({run_if_auto_try} : proof_method_options) proof_method = + let + val () = if name = "" then error "Registering unnamed proof method" else () + val () = Synchronized.change proof_methods (Symtab.update (name, proof_method)) + val () = + if run_if_auto_try then + Synchronized.change auto_try_proof_methods_names (Symset.insert name) + else + () + in () end -fun maybe_apply_proof_method name mode timeout_opt tagged st : - result option = - (case AList.lookup (op =) raw_named_methods name of - NONE => NONE - | SOME (raw_method as ((_, run_if_auto_try), _)) => - if mode <> Auto_Try orelse run_if_auto_try then - apply_raw_named_method (name, raw_method) timeout_opt tagged st - else - NONE) +fun get_proof_method (name : string) : proof_method option = + Symtab.lookup (Synchronized.value proof_methods) name; + +fun get_all_proof_methods () : (string * proof_method) list = + Symtab.fold (fn x => fn xs => x :: xs) (Synchronized.value proof_methods) [] + +fun get_all_proof_method_names () : string list = + Symtab.fold (fn (name, _) => fn names => name :: names) (Synchronized.value proof_methods) [] + +fun get_all_auto_try_proof_method_names () : string list = + Symset.dest (Synchronized.value auto_try_proof_methods_names) + +fun should_auto_try_proof_method (name : string) : bool = + Symset.member (Synchronized.value auto_try_proof_methods_names) name end -val maybe_apply_methods = map maybe_apply_proof_method named_methods +fun get_proof_method_or_noop name = + (case get_proof_method name of + NONE => noop_proof_method + | SOME proof_method => proof_method) + +fun maybe_apply_proof_method name mode : proof_method = + if mode <> Auto_Try orelse should_auto_try_proof_method name then + get_proof_method_or_noop name + else + noop_proof_method fun time_string time = string_of_int (Time.toMilliseconds time) ^ " ms" fun tool_time_string (s, time) = s ^ ": " ^ time_string time -(* 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 generic_try0 mode timeout_opt (tagged : tagged_xthm list) st = +fun generic_try0 mode timeout_opt (facts : facts) st = let - val st = Proof.map_contexts (silence_methods false) st - fun try_method method = method mode timeout_opt tagged st + fun try_method (method : mode -> proof_method) = method mode timeout_opt facts st fun get_message {command, time, ...} = "Found proof: " ^ Active.sendback_markup_command command ^ " (" ^ time_string time ^ ")" val print_step = Option.map (tap (writeln o get_message)) @@ -188,11 +138,13 @@ methods |> Par_List.get_some try_method |> the_list + val proof_method_names = get_all_proof_method_names () + val maybe_apply_methods = map maybe_apply_proof_method proof_method_names in if mode = Normal then - "Trying " ^ implode_space (Try.serial_commas "and" (map quote named_methods)) ^ - "..." - |> writeln + let val names = map quote proof_method_names in + writeln ("Trying " ^ implode_space (serial_commas "and" names) ^ "...") + end else (); (case get_results maybe_apply_methods of @@ -220,29 +172,28 @@ fun try0 timeout_opt = snd oo generic_try0 Normal timeout_opt -fun try0_trans tagged = +fun try0_trans (facts : facts) = Toplevel.keep_proof - (ignore o generic_try0 Normal (SOME default_timeout) tagged o Toplevel.proof_of) + (ignore o generic_try0 Normal (SOME default_timeout) facts o Toplevel.proof_of) val parse_fact_refs = Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) Parse.thm) val parse_attr = - Args.$$$ "simp" |-- Args.colon |-- parse_fact_refs >> (map (rpair [Simp])) - || Args.$$$ "intro" |-- Args.colon |-- parse_fact_refs >> (map (rpair [Intro])) - || Args.$$$ "elim" |-- Args.colon |-- parse_fact_refs >> (map (rpair [Elim])) - || Args.$$$ "dest" |-- Args.colon |-- parse_fact_refs >> (map (rpair [Dest])) + Args.$$$ "simp" |-- Args.colon |-- parse_fact_refs >> (fn xrefs => + {usings = [], simps = xrefs, intros = [], elims = [], dests = []}) + || Args.$$$ "intro" |-- Args.colon |-- parse_fact_refs >> (fn xrefs => + {usings = [], simps = [], intros = xrefs, elims = [], dests = []}) + || Args.$$$ "elim" |-- Args.colon |-- parse_fact_refs >> (fn xrefs => + {usings = [], simps = [], intros = [], elims = xrefs, dests = []}) + || Args.$$$ "dest" |-- Args.colon |-- parse_fact_refs >> (fn xrefs => + {usings = [], simps = [], intros = [], elims = [], dests = xrefs}) fun parse_attrs x = (Args.parens parse_attrs - || Scan.repeat parse_attr >> (fn tagged => fold (curry (op @)) tagged [])) x + || Scan.repeat parse_attr >> (fn factss => fold union_facts factss empty_facts)) x val _ = Outer_Syntax.command \<^command_keyword>\try0\ "try a combination of proof methods" - (Scan.optional parse_attrs [] #>> try0_trans) - -val _ = - Try.tool_setup - {name = "try0", weight = 30, auto_option = \<^system_option>\auto_methods\, - body = fn auto => fst o generic_try0 (if auto then Auto_Try else Try) NONE []} + (Scan.optional parse_attrs empty_facts #>> try0_trans) end diff -r 35a219e372b0 -r 7fee9141da5e src/HOL/Tools/try0_util.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/try0_util.ML Fri Mar 28 08:24:07 2025 +0100 @@ -0,0 +1,146 @@ +(* Title: HOL/Tools/try0_hol.ML + Author: Jasmin Blanchette, LMU Muenchen + Author: Martin Desharnais, LMU Muenchen + Author: Fabian Huch, TU Muenchen + +General-purpose functions used by Try0. +*) + +signature TRY0_UTIL = +sig + val string_of_xref : Try0.xref -> string + + type facts_prefixes = + {usings: string, + simps : string, + intros : string, + elims : string, + dests : string} + val full_attrs : facts_prefixes + val clas_attrs : facts_prefixes + val simp_attrs : facts_prefixes + val metis_attrs : facts_prefixes + val no_attrs : facts_prefixes + val apply_raw_named_method : string -> bool -> facts_prefixes -> + (Proof.context -> Proof.context) -> Time.time option -> Try0.facts -> Proof.state -> + Try0.result option +end + +structure Try0_Util : TRY0_UTIL = struct + +fun string_of_xref ((xref, args) : Try0.xref) = + (case xref of + Facts.Fact literal => literal |> Symbol_Pos.explode0 |> Symbol_Pos.implode |> cartouche + | _ => + Facts.string_of_ref xref) ^ implode + (map (enclose "[" "]" o Pretty.unformatted_string_of o Token.pretty_src \<^context>) args) + + +type facts_prefixes = + {usings: string, + simps : string, + intros : string, + elims : string, + dests : string} + +val no_attrs : facts_prefixes = + {usings = "", simps = "", intros = "", elims = "", dests = ""} +val full_attrs : facts_prefixes = + {usings = "", simps = "simp", intros = "intro", elims = "elim", dests = "dest"} +val clas_attrs : facts_prefixes = + {usings = "", simps = "", intros = "intro", elims = "elim", dests = "dest"} +val simp_attrs : facts_prefixes = + {usings = "", simps = "add", intros = "", elims = "", dests = ""} +val metis_attrs : facts_prefixes = no_attrs + +local + +fun parse_method ctxt s = + enclose "(" ")" s + |> Token.explode (Thy_Header.get_keywords' ctxt) Position.start + |> filter Token.is_proper + |> Scan.read Token.stopper Method.parse + |> (fn SOME (Method.Source src, _) => src | _ => raise Fail "expected Source") + +fun run_tac timeout_opt tac st = + let val with_timeout = + (case timeout_opt of SOME timeout => Timeout.apply_physical timeout | NONE => I) + in with_timeout (Seq.pull o tac) st |> Option.map fst end + +val num_goals = Thm.nprems_of o #goal o Proof.goal + +fun apply_recursive recurse elapsed0 timeout_opt apply st = + (case Timing.timing (Option.join o try (run_tac timeout_opt apply)) st of + ({elapsed, ...}, SOME st') => + if recurse andalso num_goals st' > 0 andalso num_goals st' < num_goals st then + let val timeout_opt1 = (Option.map (fn timeout => timeout - elapsed) timeout_opt) + in apply_recursive recurse (elapsed0 + elapsed) timeout_opt1 apply st' end + else (elapsed0 + elapsed, st') + |_ => (elapsed0, st)) + +in + +fun apply_raw_named_method (name : string) all_goals (prefixes: facts_prefixes) + (silence_methods : Proof.context -> Proof.context) timeout_opt (facts : Try0.facts) + (st : Proof.state) : Try0.result option = + let + val st = Proof.map_contexts silence_methods st + val ctxt = Proof.context_of st + + val (unused_simps, simps_attrs) = + if #simps prefixes = "" then + (#simps facts, "") + else + ([], " " ^ #simps prefixes ^ ": " ^ space_implode "" (map string_of_xref (#simps facts))) + + val (unused_intros, intros_attrs) = + if #intros prefixes = "" then + (#intros facts, "") + else + ([], " " ^ #intros prefixes ^ ": " ^ space_implode "" (map string_of_xref (#intros facts))) + + val (unused_elims, elims_attrs) = + if #elims prefixes = "" then + (#elims facts, "") + else + ([], " " ^ #elims prefixes ^ ": " ^ space_implode "" (map string_of_xref (#elims facts))) + + val (unused_dests, dests_attrs) = + if #dests prefixes = "" then + (#dests facts, "") + else + ([], " " ^ #dests prefixes ^ ": " ^ space_implode "" (map string_of_xref (#dests facts))) + + val unused = #usings facts @ unused_simps @ unused_intros @ unused_elims @ unused_dests + + val attrs = simps_attrs ^ intros_attrs ^ elims_attrs ^ dests_attrs + val text = + name ^ attrs + |> parse_method ctxt + |> Method.method_cmd ctxt + |> Method.Basic + |> (fn m => Method.Combinator (Method.no_combinator_info, Method.Select_Goals 1, [m])) + + val apply = + Proof.using [Attrib.eval_thms ctxt unused |> map (rpair [] o single)] + #> Proof.refine text #> Seq.filter_results + val num_before = num_goals st + val multiple_goals = all_goals andalso num_before > 1 + val (time, st') = apply_recursive multiple_goals Time.zeroTime timeout_opt apply st + val num_after = num_goals st' + val select = "[" ^ string_of_int (num_before - num_after) ^ "]" + val unused = implode_space (unused |> map string_of_xref) + val command = + (if unused <> "" then "using " ^ unused ^ " " else "") ^ + (if num_after = 0 then "by " else "apply ") ^ + (name ^ attrs |> attrs <> "" ? enclose "(" ")") ^ + (if multiple_goals andalso num_after > 0 then select else "") + in + if num_before > num_after then + SOME {name = name, command = command, time = time, state = st'} + else NONE + end + +end + +end \ No newline at end of file diff -r 35a219e372b0 -r 7fee9141da5e src/HOL/Try0.thy --- a/src/HOL/Try0.thy Fri Mar 28 00:26:18 2025 +0000 +++ b/src/HOL/Try0.thy Fri Mar 28 08:24:07 2025 +0100 @@ -5,10 +5,18 @@ *) theory Try0 - imports Presburger + imports Pure keywords "try0" :: diag begin ML_file \Tools/try0.ML\ +ML_file \Tools/try0_util.ML\ + +ML \ +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 _ => () +\ end \ No newline at end of file diff -r 35a219e372b0 -r 7fee9141da5e src/HOL/Try0_HOL.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Try0_HOL.thy Fri Mar 28 08:24:07 2025 +0100 @@ -0,0 +1,65 @@ +(* Title: HOL/Try0_HOL.thy + Author: Jasmin Blanchette, LMU Muenchen + Author: Martin Desharnais, LMU Muenchen + Author: Fabian Huch, TU Muenchen +*) +theory Try0_HOL + imports Try0 Presburger +begin + +ML \ +signature TRY0_HOL = +sig + val silence_methods : Proof.context -> Proof.context +end + +structure Try0_HOL : TRY0_HOL = struct + +(* 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" + +local + +open Try0_Util + +(* name * (run_if_auto_try * (all_goals * tags)) *) +val raw_named_methods = + [("auto", (true, (true, full_attrs))), + ("blast", (true, (false, clas_attrs))), + ("metis", (true, (false, metis_attrs))), + ("argo", (true, (false, no_attrs))), + ("linarith", (true, (false, no_attrs))), + ("presburger", (true, (false, no_attrs))), + ("algebra", (true, (false, no_attrs))), + ("fast", (false, (false, clas_attrs))), + ("fastforce", (false, (false, full_attrs))), + ("force", (false, (false, full_attrs))), + ("meson", (false, (false, metis_attrs))), + ("satx", (false, (false, no_attrs))), + ("order", (true, (false, no_attrs)))] + +in + +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 silence_methods + in + Try0.register_proof_method name {run_if_auto_try = run_if_auto_try} meth + handle Symtab.DUP _ => () + end) + +end + +end +\ + +end \ No newline at end of file diff -r 35a219e372b0 -r 7fee9141da5e src/Tools/try.ML --- a/src/Tools/try.ML Fri Mar 28 00:26:18 2025 +0000 +++ b/src/Tools/try.ML Fri Mar 28 08:24:07 2025 +0100 @@ -20,11 +20,7 @@ (* helpers *) -fun serial_commas _ [] = ["??"] - | serial_commas _ [s] = [s] - | serial_commas conj [s1, s2] = [s1, conj, s2] - | serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3] - | serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss; +val serial_commas = Try0.serial_commas (* configuration *)