# HG changeset patch # User desharna # Date 1743089741 -3600 # Node ID 5af097d05e99a6726217e6c6612b039e3ebc11a4 # Parent 3a7fc54b50cab1b3a5c0cc3b96dbfa4b409e95d4 tuned signature diff -r 3a7fc54b50ca -r 5af097d05e99 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Thu Mar 27 14:33:08 2025 +0100 +++ b/src/HOL/HOL.thy Thu Mar 27 16:35:41 2025 +0100 @@ -38,7 +38,7 @@ 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 []} + 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 3a7fc54b50ca -r 5af097d05e99 src/HOL/Mutabelle/mutabelle_extra.ML --- a/src/HOL/Mutabelle/mutabelle_extra.ML Thu Mar 27 14:33:08 2025 +0100 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML Thu Mar 27 16:35:41 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 3a7fc54b50ca -r 5af097d05e99 src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML --- a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML Thu Mar 27 14:33:08 2025 +0100 +++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML Thu Mar 27 16:35:41 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 3a7fc54b50ca -r 5af097d05e99 src/HOL/Tools/Mirabelle/mirabelle_try0.ML --- a/src/HOL/Tools/Mirabelle/mirabelle_try0.ML Thu Mar 27 14:33:08 2025 +0100 +++ b/src/HOL/Tools/Mirabelle/mirabelle_try0.ML Thu Mar 27 16:35:41 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 3a7fc54b50ca -r 5af097d05e99 src/HOL/Tools/try0.ML --- a/src/HOL/Tools/try0.ML Thu Mar 27 14:33:08 2025 +0100 +++ b/src/HOL/Tools/try0.ML Thu Mar 27 16:35:41 2025 +0100 @@ -1,5 +1,7 @@ -(* 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. *) @@ -8,11 +10,18 @@ sig val serial_commas : string -> string list -> string list - 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} + val empty_facts : facts + type result = {name: string, command: string, time: Time.time, state: Proof.state} - type proof_method = Time.time option -> tagged_xref list -> Proof.state -> result option + 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 @@ -20,9 +29,9 @@ 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 -> + val generic_try0 : mode -> Time.time option -> facts -> Proof.state -> (bool * (string * string list)) * result list - val try0 : Time.time option -> tagged_xref list -> Proof.state -> result list + val try0 : Time.time option -> facts -> Proof.state -> result list end structure Try0 : TRY0 = @@ -43,9 +52,23 @@ 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} + +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 -> tagged_xref list -> Proof.state -> result option +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 @@ -60,7 +83,7 @@ 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_new (name, proof_method)) + 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) @@ -99,9 +122,9 @@ fun time_string time = string_of_int (Time.toMilliseconds time) ^ " ms" fun tool_time_string (s, time) = s ^ ": " ^ time_string time -fun generic_try0 mode timeout_opt (tagged : tagged_xref list) st = +fun generic_try0 mode timeout_opt (facts : facts) st = let - 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)) @@ -149,24 +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) + (Scan.optional parse_attrs empty_facts #>> try0_trans) end diff -r 3a7fc54b50ca -r 5af097d05e99 src/HOL/Tools/try0_util.ML --- a/src/HOL/Tools/try0_util.ML Thu Mar 27 14:33:08 2025 +0100 +++ b/src/HOL/Tools/try0_util.ML Thu Mar 27 16:35:41 2025 +0100 @@ -9,13 +9,20 @@ signature TRY0_UTIL = sig 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 -> - (Proof.context -> Proof.context) -> Time.time option -> Try0.tagged_xref list -> Proof.state -> + + 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 @@ -29,27 +36,25 @@ (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 = [] +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 add_attr_text (tagged : Try0.tagged_xref list) (tag, src) s = - let - val fs = tagged - |> map_filter (fn (xref, tags) => - if member (op =) tags tag then - SOME (string_of_xref xref) - else - NONE) - in if null fs then s else s ^ " " ^ (if src = "" then "" else src ^ ": ") ^ implode_space fs end - -fun attrs_text tags (tagged : Try0.tagged_xref list) = - "" |> fold (add_attr_text tagged) tags - fun parse_method ctxt s = enclose "(" ")" s |> Token.explode (Thy_Header.get_keywords' ctxt) Position.start @@ -75,21 +80,40 @@ in -fun apply_raw_named_method (name : string) all_goals attrs - (silence_methods : Proof.context -> Proof.context) timeout_opt (tagged : Try0.tagged_xref list) +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 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 (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 @@ -98,8 +122,8 @@ |> (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 + 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