--- 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>\<open>auto_nitpick\<close>, try_nitpick))
+val _ =
+ Try.tool_setup
+ {name = nitpickN, weight = 50, auto_option = \<^system_option>\<open>auto_nitpick\<close>,
+ body = fn auto => pick_nits [] (if auto then Auto_Try else Try) 1 0}
end;
--- 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>\<open>auto_sledgehammer\<close>, try_sledgehammer))
+val _ =
+ Try.tool_setup
+ {name = sledgehammerN, weight = 40, auto_option = \<^system_option>\<open>auto_sledgehammer\<close>,
+ 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}
--- 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>\<open>try0\<close> "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>\<open>auto_methods\<close>, try_try0));
+val _ =
+ Try.tool_setup
+ {name = "try0", weight = 30, auto_option = \<^system_option>\<open>auto_methods\<close>,
+ body = fn auto => generic_try0 (if auto then Auto_Try else Try) NONE ([], [], [], [])};
end;
--- 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>\<open>auto_quickcheck\<close>, try_quickcheck));
+val _ =
+ Try.tool_setup
+ {name = quickcheckN, weight = 20, auto_option = \<^system_option>\<open>auto_quickcheck\<close>,
+ 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;
-
--- 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>\<open>auto_solve_direct\<close>, try_solve_direct));
+ Try.tool_setup
+ {name = solve_directN, weight = 10, auto_option = \<^system_option>\<open>auto_solve_direct\<close>,
+ body = fn auto => do_solve_direct (if auto then Auto_Try else Try)};
end;
--- 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>\<open>auto_time_start\<close>)),
pri = ~ weight,
@@ -97,7 +93,7 @@
val auto_time_limit = Options.default_real \<^system_option>\<open>auto_time_limit\<close>
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);