# HG changeset patch # User wenzelm # Date 1731102749 -3600 # Node ID 07c802837a8cf04ee088c4049d8d4679134671c8 # Parent 8abdd60acd60245cf57f00fb949977f13afd44f9# Parent 37cff2ad31daeff7f0294f3e918cab599933c089 merged diff -r 37cff2ad31da -r 07c802837a8c src/HOL/Mutabelle/mutabelle_extra.ML --- a/src/HOL/Mutabelle/mutabelle_extra.ML Fri Nov 08 19:18:32 2024 +0100 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML Fri Nov 08 22:52:29 2024 +0100 @@ -148,9 +148,9 @@ 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 - true => (Solved, []) - | false => (Unsolved, []) + case Try0.try0 (SOME (seconds 5.0)) [] state of + [] => (Unsolved, []) + | _ => (Solved, []) end val try0_mtd = ("try0", invoke_try0) diff -r 37cff2ad31da -r 07c802837a8c src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML --- a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML Fri Nov 08 19:18:32 2024 +0100 +++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML Fri Nov 08 22:52:29 2024 +0100 @@ -218,7 +218,7 @@ end -val try0 = Try0.try0 (SOME (Time.fromSeconds 5)) ([], [], [], []) +val try0 = not o null o Try0.try0 (SOME (Time.fromSeconds 5)) [] fun make_action ({arguments, timeout, output_dir, ...} : Mirabelle.action_context) = let diff -r 37cff2ad31da -r 07c802837a8c src/HOL/Tools/Mirabelle/mirabelle_try0.ML --- a/src/HOL/Tools/Mirabelle/mirabelle_try0.ML Fri Nov 08 19:18:32 2024 +0100 +++ b/src/HOL/Tools/Mirabelle/mirabelle_try0.ML Fri Nov 08 22:52:29 2024 +0100 @@ -14,7 +14,7 @@ val generous_timeout = Time.scale 10.0 timeout fun run ({pre, ...} : Mirabelle.command) = - if Timeout.apply generous_timeout (Try0.try0 (SOME timeout) ([], [], [], [])) pre then + if Timeout.apply generous_timeout (not o null o Try0.try0 (SOME timeout) []) pre then "succeeded" else "" diff -r 37cff2ad31da -r 07c802837a8c src/HOL/Tools/try0.ML --- a/src/HOL/Tools/try0.ML Fri Nov 08 19:18:32 2024 +0100 +++ b/src/HOL/Tools/try0.ML Fri Nov 08 22:52:29 2024 +0100 @@ -8,78 +8,110 @@ sig val noneN : string val silence_methods : bool -> Proof.context -> Proof.context - val try0 : Time.time option -> string list * string list * string list * string list -> - Proof.state -> bool -end; + datatype modifier = Use | Simp | Intro | Elim | Dest + type result = {name: string, command: string, time: int, state: Proof.state} + val try0 : Time.time option -> ((Facts.ref * Token.src list) * modifier list) list -> + Proof.state -> result list +end structure Try0 : TRY0 = struct -val noneN = "none"; +val noneN = "none" + +datatype mode = Auto_Try | Try | Normal -datatype mode = Auto_Try | Try | Normal; +val default_timeout = seconds 5.0 -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 -fun can_apply timeout_opt pre post tac st = - let val {goal, ...} = Proof.goal st in - (case (case timeout_opt of - SOME timeout => Timeout.apply_physical timeout - | NONE => fn f => fn x => f x) (Seq.pull o tac) (pre st) of - SOME (x, _) => Thm.nprems_of (post x) < Thm.nprems_of goal - | NONE => false) - 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)) -fun apply_generic timeout_opt name command pre post apply st = - let val time_start = Time.now () in - if try (can_apply timeout_opt pre post apply) st = SOME true then - SOME (name, command, Time.toMilliseconds (Time.now () - time_start)) - else - NONE - end; - -fun parse_method keywords s = +fun parse_method ctxt s = enclose "(" ")" s - |> Token.explode keywords Position.start + |> 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"); + |> (fn SOME (Method.Source src, _) => src | _ => raise Fail "expected Source") + +datatype modifier = Use | Simp | Intro | Elim | Dest -fun apply_named_method_on_first_goal ctxt = - parse_method (Thy_Header.get_keywords' ctxt) - #> Method.method_cmd ctxt - #> Method.Basic - #> (fn m => Method.Combinator (Method.no_combinator_info, Method.Select_Goals 1, [m])) - #> Proof.refine; +fun string_of_xthm (xref, args) = + (case xref of Facts.Fact literal => cartouche literal | _ => Facts.string_of_ref xref) ^ + implode (map (enclose "[" "]" o Pretty.unformatted_string_of o Token.pretty_src \<^context>) args) -fun add_attr_text (NONE, _) s = s - | add_attr_text (_, []) s = s - | add_attr_text (SOME x, fs) s = - s ^ " " ^ (if x = "" then "" else x ^ ": ") ^ implode_space fs; +fun add_attr_text tagged (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 (sx, ix, ex, dx) (ss, is, es, ds) = - "" |> fold add_attr_text [(sx, ss), (ix, is), (ex, es), (dx, ds)]; +fun attrs_text tags tagged = + "" |> fold (add_attr_text tagged) tags -fun apply_named_method (name, ((all_goals, run_if_auto_try), attrs)) mode timeout_opt quad st = +type result = {name: string, command: string, time: int, state: Proof.state} + +fun apply_named_method (name, ((all_goals, run_if_auto_try), attrs)) mode timeout_opt tagged st = if mode <> Auto_Try orelse run_if_auto_try then - let val attrs = attrs_text attrs quad in - apply_generic timeout_opt name - ((name ^ attrs |> attrs <> "" ? enclose "(" ")") ^ - (if all_goals andalso Thm.nprems_of (#goal (Proof.goal st)) > 1 then "[1]" else "")) - I (#goal o Proof.goal) - (apply_named_method_on_first_goal (Proof.context_of st) (name ^ attrs) - #> Seq.filter_results) st + 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 using_text = + (K (Method.insert (Attrib.eval_thms ctxt unused))) + |> Method.Basic + + 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])) + |> (fn m => Method.Combinator (Method.no_combinator_info, Method.Then, [using_text, m])) + + val apply = text |> Proof.refine #> 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.toMilliseconds time, state = st'} + else NONE end - else - NONE; + else NONE -val full_attrs = (SOME "simp", SOME "intro", SOME "elim", SOME "dest"); -val clas_attrs = (NONE, SOME "intro", SOME "elim", SOME "dest"); -val simp_attrs = (SOME "add", NONE, NONE, NONE); -val metis_attrs = (SOME "", SOME "", SOME "", SOME ""); -val no_attrs = (NONE, NONE, NONE, NONE); +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), (simp, intro, elim, dest) *) +(* name * ((all_goals, run_if_auto_try), tags *) val named_methods = [("simp", ((false, true), simp_attrs)), ("auto", ((true, true), full_attrs)), @@ -94,12 +126,12 @@ ("force", ((false, false), full_attrs)), ("meson", ((false, false), metis_attrs)), ("satx", ((false, false), no_attrs)), - ("order", ((false, true), no_attrs))]; + ("order", ((false, true), no_attrs))] -val apply_methods = map apply_named_method named_methods; +val apply_methods = map apply_named_method named_methods -fun time_string ms = string_of_int ms ^ " ms"; -fun tool_time_string (s, ms) = s ^ ": " ^ time_string ms; +fun time_string ms = string_of_int ms ^ " ms" +fun tool_time_string (s, ms) = s ^ ": " ^ time_string ms (* Makes reconstructor tools as silent as possible. The "set_visible" calls suppresses "Unification bound exceeded" warnings and the like. *) @@ -110,25 +142,19 @@ |> Simplifier_Trace.disable |> Context_Position.set_visible false |> Config.put Unify.unify_trace false - |> Config.put Argo_Tactic.trace "none" - |> Proof_Context.background_theory (fn thy => - thy - |> Context_Position.set_visible_global false - |> Config.put_global Unify.unify_trace false)); + |> Config.put Argo_Tactic.trace "none") -fun generic_try0 mode timeout_opt quad st = +fun generic_try0 mode timeout_opt tagged st = let - val st = Proof.map_contexts (silence_methods false) st; - fun trd (_, _, t) = t; - fun try_method method = method mode timeout_opt quad st; - fun get_message (_, command, ms) = "Found proof: " ^ Active.sendback_markup_command - ((if Thm.nprems_of (#goal (Proof.goal st)) = 1 then "by" else "apply") ^ " " ^ command) ^ - " (" ^ time_string ms ^ ")"; - val print_step = Option.map (tap (writeln o get_message)); + val st = Proof.map_contexts (silence_methods false) st + fun try_method method = method mode timeout_opt tagged 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)) val get_results = if mode = Normal - then Par_List.map (try_method #> print_step) #> map_filter I #> sort (int_ord o apply2 trd) - else Par_List.get_some try_method #> the_list; + then Par_List.map (try_method #> print_step) #> map_filter I #> sort (int_ord o apply2 #time) + else Par_List.get_some try_method #> the_list in if mode = Normal then "Trying " ^ implode_space (Try.serial_commas "and" (map (quote o fst) named_methods)) ^ @@ -137,61 +163,53 @@ else (); (case get_results apply_methods of - [] => - (if mode = Normal then writeln "No proof found" else (); (false, (noneN, []))) - | xs as (name, command, _) :: _ => + [] => (if mode = Normal then writeln "No proof found" else (); ((false, (noneN, [])), [])) + | results as {name, command, ...} :: _ => let - val xs = xs |> map (fn (name, _, n) => (n, name)) - |> AList.coalesce (op =) - |> map (swap o apsnd commas); + val method_times = + results + |> map (fn {name, time, ...} => (time, name)) + |> AList.coalesce (op =) + |> map (swap o apsnd commas) val message = (case mode of Auto_Try => "Auto Try0 found a proof" | Try => "Try0 found a proof" | Normal => "Try this") ^ ": " ^ - Active.sendback_markup_command - ((if Thm.nprems_of (#goal (Proof.goal st)) = 1 then "by" - else "apply") ^ " " ^ command) ^ - (case xs of + Active.sendback_markup_command command ^ + (case method_times of [(_, ms)] => " (" ^ time_string ms ^ ")" - | xs => "\n(" ^ space_implode "; " (map tool_time_string xs) ^ ")"); + | method_times => "\n(" ^ space_implode "; " (map tool_time_string method_times) ^ ")") in - (true, (name, if mode = Auto_Try then [message] else (writeln message; []))) + ((true, (name, if mode = Auto_Try then [message] else (writeln message; []))), results) end) - end; - -fun try0 timeout_opt = fst oo generic_try0 Normal timeout_opt; + end -fun try0_trans quad = - Toplevel.keep_proof - (ignore o generic_try0 Normal (SOME default_timeout) quad o Toplevel.proof_of); - -fun merge_attrs (s1, i1, e1, d1) (s2, i2, e2, d2) = (s1 @ s2, i1 @ i2, e1 @ e2, d1 @ d2); +fun try0 timeout_opt = snd oo generic_try0 Normal timeout_opt -fun string_of_xthm (xref, args) = - Facts.string_of_ref xref ^ - implode (map (enclose "[" "]" o Pretty.unformatted_string_of o Token.pretty_src \<^context>) args); +fun try0_trans tagged = + Toplevel.keep_proof + (ignore o generic_try0 Normal (SOME default_timeout) tagged o Toplevel.proof_of) -val parse_fact_refs = - Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) (Parse.thm >> string_of_xthm)); +val parse_fact_refs = Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) Parse.thm) val parse_attr = - Args.$$$ "simp" |-- Args.colon |-- parse_fact_refs >> (fn ss => (ss, [], [], [])) - || Args.$$$ "intro" |-- Args.colon |-- parse_fact_refs >> (fn is => ([], is, [], [])) - || Args.$$$ "elim" |-- Args.colon |-- parse_fact_refs >> (fn es => ([], [], es, [])) - || Args.$$$ "dest" |-- Args.colon |-- parse_fact_refs >> (fn ds => ([], [], [], ds)); + 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])) fun parse_attrs x = (Args.parens parse_attrs - || Scan.repeat parse_attr >> (fn quad => fold merge_attrs quad ([], [], [], []))) x; + || Scan.repeat parse_attr >> (fn tagged => fold (curry (op @)) tagged [])) x val _ = Outer_Syntax.command \<^command_keyword>\try0\ "try a combination of proof methods" - (Scan.optional parse_attrs ([], [], [], []) #>> try0_trans); + (Scan.optional parse_attrs [] #>> try0_trans) val _ = Try.tool_setup {name = "try0", weight = 30, auto_option = \<^system_option>\auto_methods\, - body = fn auto => generic_try0 (if auto then Auto_Try else Try) NONE ([], [], [], [])}; + body = fn auto => fst o generic_try0 (if auto then Auto_Try else Try) NONE []} -end; +end