# HG changeset patch # User wenzelm # Date 1634115875 -7200 # Node ID 3315c551fe6e149ed2f926dda98021930729e45f # Parent a241eadc0e3fec75b74bb8c984ae75946f00c13a clarified signature; diff -r a241eadc0e3f -r 3315c551fe6e src/HOL/Tools/Nitpick/nitpick_commands.ML --- a/src/HOL/Tools/Nitpick/nitpick_commands.ML Wed Oct 13 10:35:01 2021 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_commands.ML Wed Oct 13 11:04:35 2021 +0200 @@ -375,8 +375,9 @@ "set and display the default parameters for Nitpick" (parse_params #>> nitpick_params_trans) -fun try_nitpick auto = pick_nits [] (if auto then Auto_Try else Try) 1 0 - -val _ = Try.tool_setup (nitpickN, (50, \<^system_option>\auto_nitpick\, try_nitpick)) +val _ = + Try.tool_setup + {name = nitpickN, weight = 50, auto_option = \<^system_option>\auto_nitpick\, + body = fn auto => pick_nits [] (if auto then Auto_Try else Try) 1 0} end; diff -r a241eadc0e3f -r 3315c551fe6e src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Wed Oct 13 10:35:01 2021 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Wed Oct 13 11:04:35 2021 +0200 @@ -385,16 +385,17 @@ [] => "none" | params => params |> map string_of_raw_param |> sort_strings |> cat_lines)))))) -fun try_sledgehammer auto state = - let - val thy = Proof.theory_of state - val mode = if auto then Auto_Try else Try - val i = 1 - in - run_sledgehammer (get_params mode thy []) mode NONE i no_fact_override (silence_state state) - end - -val _ = Try.tool_setup (sledgehammerN, (40, \<^system_option>\auto_sledgehammer\, try_sledgehammer)) +val _ = + Try.tool_setup + {name = sledgehammerN, weight = 40, auto_option = \<^system_option>\auto_sledgehammer\, + body = fn auto => fn state => + let + val thy = Proof.theory_of state + val mode = if auto then Auto_Try else Try + val i = 1 + in + run_sledgehammer (get_params mode thy []) mode NONE i no_fact_override (silence_state state) + end} val _ = Query_Operation.register {name = sledgehammerN, pri = 0} diff -r a241eadc0e3f -r 3315c551fe6e src/HOL/Tools/try0.ML --- a/src/HOL/Tools/try0.ML Wed Oct 13 10:35:01 2021 +0200 +++ b/src/HOL/Tools/try0.ML Wed Oct 13 11:04:35 2021 +0200 @@ -6,9 +6,7 @@ signature TRY0 = sig - val try0N : string 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 @@ -17,7 +15,6 @@ structure Try0 : TRY0 = struct -val try0N = "try0"; val noneN = "none"; datatype mode = Auto_Try | Try | Normal; @@ -191,8 +188,9 @@ Outer_Syntax.command \<^command_keyword>\try0\ "try a combination of proof methods" (Scan.optional parse_attrs ([], [], [], []) #>> try0_trans); -fun try_try0 auto = generic_try0 (if auto then Auto_Try else Try) NONE ([], [], [], []); - -val _ = Try.tool_setup (try0N, (30, \<^system_option>\auto_methods\, try_try0)); +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 ([], [], [], [])}; end; diff -r a241eadc0e3f -r 3315c551fe6e src/Tools/quickcheck.ML --- a/src/Tools/quickcheck.ML Wed Oct 13 10:35:01 2021 +0200 +++ b/src/Tools/quickcheck.ML Wed Oct 13 11:04:35 2021 +0200 @@ -538,32 +538,32 @@ (fn (args, i) => Toplevel.keep_proof (quickcheck_cmd args i))); -(* automatic testing *) +(* 'try' setup *) -fun try_quickcheck auto state = - let - val ctxt = Proof.context_of state; - val i = 1; - val res = - state - |> Proof.map_context (Config.put report false #> Config.put quiet true) - |> try (test_goal (false, false) ([], []) i); - in - (case res of - NONE => (unknownN, []) - | SOME results => - let - val msg = - Pretty.string_of - (pretty_counterex ctxt auto (Option.map (the o get_first response_of) results)) - in - if is_some results then (genuineN, if auto then [msg] else (writeln msg; [])) - else (noneN, []) - end) - end - |> `(fn (outcome_code, _) => outcome_code = genuineN); - -val _ = Try.tool_setup (quickcheckN, (20, \<^system_option>\auto_quickcheck\, try_quickcheck)); +val _ = + Try.tool_setup + {name = quickcheckN, weight = 20, auto_option = \<^system_option>\auto_quickcheck\, + body = fn auto => fn state => + let + val ctxt = Proof.context_of state; + val i = 1; + val res = + state + |> Proof.map_context (Config.put report false #> Config.put quiet true) + |> try (test_goal (false, false) ([], []) i); + in + (case res of + NONE => (unknownN, []) + | SOME results => + let + val msg = + Pretty.string_of + (pretty_counterex ctxt auto (Option.map (the o get_first response_of) results)) + in + if is_some results then (genuineN, if auto then [msg] else (writeln msg; [])) + else (noneN, []) + end) + end + |> `(fn (outcome_code, _) => outcome_code = genuineN)}; end; - diff -r a241eadc0e3f -r 3315c551fe6e src/Tools/solve_direct.ML --- a/src/Tools/solve_direct.ML Wed Oct 13 10:35:01 2021 +0200 +++ b/src/Tools/solve_direct.ML Wed Oct 13 11:04:35 2021 +0200 @@ -95,11 +95,11 @@ (Scan.succeed (Toplevel.keep_proof (ignore o solve_direct o Toplevel.proof_of))); -(* hook *) - -fun try_solve_direct auto = do_solve_direct (if auto then Auto_Try else Try) +(* 'try' setup *) val _ = - Try.tool_setup (solve_directN, (10, \<^system_option>\auto_solve_direct\, try_solve_direct)); + Try.tool_setup + {name = solve_directN, weight = 10, auto_option = \<^system_option>\auto_solve_direct\, + body = fn auto => do_solve_direct (if auto then Auto_Try else Try)}; end; diff -r a241eadc0e3f -r 3315c551fe6e src/Tools/try.ML --- a/src/Tools/try.ML Wed Oct 13 10:35:01 2021 +0200 +++ b/src/Tools/try.ML Wed Oct 13 11:04:35 2021 +0200 @@ -7,12 +7,10 @@ signature TRY = sig - type tool = string * (int * string * (bool -> Proof.state -> bool * (string * string list))) - - val tryN: string - val serial_commas: string -> string list -> string list val subgoal_count: Proof.state -> int + type body = bool -> Proof.state -> bool * (string * string list) + type tool = {name: string, weight: int, auto_option: string, body: body} val get_tools: theory -> tool list val try_tools: Proof.state -> (string * string) option val tool_setup: tool -> unit @@ -21,11 +19,6 @@ structure Try : TRY = struct -type tool = string * (int * string * (bool -> Proof.state -> bool * (string * string list))); - -val tryN = "try"; - - (* helpers *) fun serial_commas _ [] = ["??"] @@ -39,8 +32,11 @@ (* configuration *) -fun tool_ord ((name1, (weight1, _, _)), (name2, (weight2, _, _))) = - prod_ord int_ord string_ord ((weight1, name1), (weight2, name2)); +type body = bool -> Proof.state -> bool * (string * string list); +type tool = {name: string, weight: int, auto_option: string, body: body}; + +fun tool_ord (tool1: tool, tool2: tool) = + prod_ord int_ord string_ord ((#weight tool1, #name tool1), (#weight tool2, #name tool2)); structure Data = Theory_Data ( @@ -64,11 +60,11 @@ get_tools (Proof.theory_of state) |> tap (fn tools => "Trying " ^ space_implode " " - (serial_commas "and" (map (quote o fst) tools)) ^ "..." + (serial_commas "and" (map (quote o #name) tools)) ^ "..." |> writeln) |> Par_List.get_some - (fn (name, (_, _, tool)) => - case try (tool false) state of + (fn {name, body, ...} => + case try (body false) state of SOME (true, (outcome_code, _)) => SOME (name, outcome_code) | _ => NONE) |> tap (fn NONE => writeln "Tried in vain" | _ => ()); @@ -81,10 +77,10 @@ (* asynchronous print function *) -fun print_function ((name, (weight, auto, tool)): tool) = +fun print_function ({name, weight, auto_option, body}: tool) = Command.print_function ("auto_" ^ name) (fn {keywords, command_name, ...} => - if Keyword.is_theory_goal keywords command_name andalso Options.default_bool auto then + if Keyword.is_theory_goal keywords command_name andalso Options.default_bool auto_option then SOME {delay = SOME (seconds (Options.default_real \<^system_option>\auto_time_start\)), pri = ~ weight, @@ -97,7 +93,7 @@ val auto_time_limit = Options.default_real \<^system_option>\auto_time_limit\ in if auto_time_limit > 0.0 then - (case Timeout.apply (seconds auto_time_limit) (fn () => tool true state) () of + (case Timeout.apply (seconds auto_time_limit) (fn () => body true state) () of (true, (_, outcome)) => List.app Output.information outcome | _ => ()) else () @@ -105,7 +101,7 @@ else NONE); -(* hybrid tool setup *) +(* tool setup *) fun tool_setup tool = (Theory.setup (register_tool tool); print_function tool);