# HG changeset patch # User desharna # Date 1743066403 -3600 # Node ID 79a86a1ecb3d969b878d4d1f8ade8ea172e96a38 # Parent 4ace4f6f710164e0ddc9e0f746f7a2c1ab454c80 refactored try0's internals diff -r 4ace4f6f7101 -r 79a86a1ecb3d src/HOL/Tools/try0.ML --- a/src/HOL/Tools/try0.ML Wed Mar 26 09:51:26 2025 +0100 +++ b/src/HOL/Tools/try0.ML Thu Mar 27 10:06:43 2025 +0100 @@ -67,6 +67,149 @@ "" |> fold (add_attr_text tagged) tags 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_options = {run_if_auto_try: bool} + +val noop_proof_method : proof_method = fn _ => fn _ => fn _ => NONE + +local + 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 + +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 () = + if run_if_auto_try then + Synchronized.change auto_try_proof_methods_names (Symset.insert name) + else + () + in () end +val _ = Symset.dest + +fun get_proof_method name = Symtab.lookup (Synchronized.value proof_methods) name; + +fun get_all_proof_methods () = + Symtab.fold (fn x => fn xs => x :: xs) (Synchronized.value proof_methods) [] + +fun get_all_proof_method_names () = + 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 + +fun get_proof_method_or_noop name = + (case get_proof_method name of + NONE => noop_proof_method + | SOME proof_method => proof_method) + +val apply_proof_method = get_proof_method_or_noop + +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_xref list) st = + let + 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)) + fun get_results methods : result list = + if mode = Normal then + methods + |> Par_List.map (try_method #> print_step) + |> map_filter I + |> sort (Time.compare o apply2 #time) + else + 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 + let val names = map quote proof_method_names in + writeln ("Trying " ^ implode_space (Try.serial_commas "and" names) ^ "...") + end + else + (); + (case get_results maybe_apply_methods of + [] => (if mode = Normal then writeln "No proof found" else (); ((false, (noneN, [])), [])) + | results as {name, command, ...} :: _ => + let + 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 command ^ + (case method_times of + [(_, ms)] => " (" ^ time_string ms ^ ")" + | method_times => "\n(" ^ space_implode "; " (map tool_time_string method_times) ^ ")") + in + ((true, (name, if mode = Auto_Try then [message] else (writeln message; []))), results) + end) + end + +fun try0 timeout_opt = snd oo generic_try0 Normal timeout_opt + +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) + +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])) + +fun parse_attrs x = + (Args.parens parse_attrs + || 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) + +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 []} + local @@ -133,116 +276,17 @@ else NONE end -in - -val named_methods = map fst raw_named_methods - -fun apply_proof_method name timeout_opt tagged st : - result option = +fun apply_proof_method name timeout_opt (tagged : tagged_xref list) 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 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) +in + +val () = List.app (fn (name, ((_, run_if_auto_try), _)) => + register_proof_method name {run_if_auto_try = run_if_auto_try} (apply_proof_method name) + handle Symtab.DUP _ => ()) raw_named_methods end -val maybe_apply_methods = map maybe_apply_proof_method named_methods - -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_xref list) st = - let - 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)) - fun get_results methods : result list = - if mode = Normal then - methods - |> Par_List.map (try_method #> print_step) - |> map_filter I - |> sort (Time.compare o apply2 #time) - else - methods - |> Par_List.get_some try_method - |> the_list - in - if mode = Normal then - "Trying " ^ implode_space (Try.serial_commas "and" (map quote named_methods)) ^ - "..." - |> writeln - else - (); - (case get_results maybe_apply_methods of - [] => (if mode = Normal then writeln "No proof found" else (); ((false, (noneN, [])), [])) - | results as {name, command, ...} :: _ => - let - 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 command ^ - (case method_times of - [(_, ms)] => " (" ^ time_string ms ^ ")" - | method_times => "\n(" ^ space_implode "; " (map tool_time_string method_times) ^ ")") - in - ((true, (name, if mode = Auto_Try then [message] else (writeln message; []))), results) - end) - end - -fun try0 timeout_opt = snd oo generic_try0 Normal timeout_opt - -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) - -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])) - -fun parse_attrs x = - (Args.parens parse_attrs - || 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) - -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 []} - end