--- a/src/HOL/Library/refute.ML Mon Sep 20 10:30:56 2021 +0200
+++ b/src/HOL/Library/refute.ML Thu Oct 14 15:24:28 2021 +0200
@@ -1201,7 +1201,7 @@
let
val t = th |> Thm.prop_of
in
- if Logic.count_prems t = 0 then
+ if Logic.no_prems t then
(writeln "No subgoal!"; "none")
else
let
--- a/src/HOL/Tools/Nitpick/nitpick_commands.ML Mon Sep 20 10:30:56 2021 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_commands.ML Thu Oct 14 15:24:28 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/Nunchaku/nunchaku.ML Mon Sep 20 10:30:56 2021 +0200
+++ b/src/HOL/Tools/Nunchaku/nunchaku.ML Thu Oct 14 15:24:28 2021 +0200
@@ -326,7 +326,7 @@
val ctxt = Proof.context_of state;
val goal = Thm.prop_of (#goal (Proof.raw_goal state));
in
- if Logic.count_prems goal = 0 then
+ if Logic.no_prems goal then
(writeln "No subgoal!"; (noneN, NONE))
else
let
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Mon Sep 20 10:30:56 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Thu Oct 14 15:24:28 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/Sledgehammer/sledgehammer_util.ML Mon Sep 20 10:30:56 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Thu Oct 14 15:24:28 2021 +0200
@@ -72,7 +72,7 @@
seconds (the secs)
end
-val subgoal_count = Try.subgoal_count
+val subgoal_count = Logic.count_prems o Thm.prop_of o #goal o Proof.goal;
exception TOO_MANY of unit
--- a/src/HOL/Tools/try0.ML Mon Sep 20 10:30:56 2021 +0200
+++ b/src/HOL/Tools/try0.ML Thu Oct 14 15:24:28 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/Pure/Isar/element.ML Mon Sep 20 10:30:56 2021 +0200
+++ b/src/Pure/Isar/element.ML Thu Oct 14 15:24:28 2021 +0200
@@ -390,7 +390,7 @@
fun decomp_simp prop =
let
val ctxt = Proof_Context.init_global thy;
- val _ = Logic.count_prems prop = 0 orelse
+ val _ = Logic.no_prems prop orelse
error ("Bad conditional rewrite rule " ^ Syntax.string_of_term ctxt prop);
val lhsrhs = Logic.dest_equals prop
handle TERM _ => error ("Rewrite rule not a meta-equality " ^ Syntax.string_of_term ctxt prop);
--- a/src/Pure/Isar/proof.ML Mon Sep 20 10:30:56 2021 +0200
+++ b/src/Pure/Isar/proof.ML Thu Oct 14 15:24:28 2021 +0200
@@ -40,6 +40,7 @@
val refine_singleton: Method.text -> state -> state
val refine_insert: thm list -> state -> state
val refine_primitive: (Proof.context -> thm -> thm) -> state -> state
+ val goal_finished: state -> bool
val raw_goal: state -> {context: context, facts: thm list, goal: thm}
val goal: state -> {context: context, facts: thm list, goal: thm}
val simple_goal: state -> {context: context, goal: thm}
@@ -532,6 +533,8 @@
(* goal views -- corresponding to methods *)
+val goal_finished = Thm.no_prems o #goal o #2 o find_goal;
+
fun raw_goal state =
let val (ctxt, (using, goal)) = get_goal state
in {context = ctxt, facts = using, goal = goal} end;
--- a/src/Pure/logic.ML Mon Sep 20 10:30:56 2021 +0200
+++ b/src/Pure/logic.ML Thu Oct 14 15:24:28 2021 +0200
@@ -25,6 +25,7 @@
val strip_imp_concl: term -> term
val strip_prems: int * term list * term -> term list * term
val count_prems: term -> int
+ val no_prems: term -> bool
val nth_prem: int * term -> term
val close_term: (string * term) list -> term -> term
val close_prop: (string * term) list -> term list -> term -> term
@@ -208,6 +209,9 @@
fun count_prems (Const ("Pure.imp", _) $ _ $ B) = 1 + count_prems B
| count_prems _ = 0;
+fun no_prems (Const ("Pure.imp", _) $ _ $ _) = false
+ | no_prems _ = true;
+
(*Select Ai from A1\<Longrightarrow>...Ai\<Longrightarrow>B*)
fun nth_prem (1, Const ("Pure.imp", _) $ A $ _) = A
| nth_prem (i, Const ("Pure.imp", _) $ _ $ B) = nth_prem (i - 1, B)
--- a/src/Pure/raw_simplifier.ML Mon Sep 20 10:30:56 2021 +0200
+++ b/src/Pure/raw_simplifier.ML Thu Oct 14 15:24:28 2021 +0200
@@ -981,7 +981,7 @@
else Thm.match (elhs', eta_t');
val thm' = Thm.instantiate insts (Thm.rename_boundvars lhs eta_t rthm);
val prop' = Thm.prop_of thm';
- val unconditional = (Logic.count_prems prop' = 0);
+ val unconditional = Logic.no_prems prop';
val (lhs', rhs') = Logic.dest_equals (Logic.strip_imp_concl prop');
val trace_args = {unconditional = unconditional, term = eta_t, thm = thm', rrule = rrule};
in
--- a/src/Pure/thm.ML Mon Sep 20 10:30:56 2021 +0200
+++ b/src/Pure/thm.ML Thu Oct 14 15:24:28 2021 +0200
@@ -495,7 +495,7 @@
val concl_of = Logic.strip_imp_concl o prop_of;
val prems_of = Logic.strip_imp_prems o prop_of;
val nprems_of = Logic.count_prems o prop_of;
-fun no_prems th = nprems_of th = 0;
+val no_prems = Logic.no_prems o prop_of;
fun major_prem_of th =
(case prems_of th of
--- a/src/Tools/quickcheck.ML Mon Sep 20 10:30:56 2021 +0200
+++ b/src/Tools/quickcheck.ML Thu Oct 14 15:24:28 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 Mon Sep 20 10:30:56 2021 +0200
+++ b/src/Tools/solve_direct.ML Thu Oct 14 15:24:28 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 Mon Sep 20 10:30:56 2021 +0200
+++ b/src/Tools/try.ML Thu Oct 14 15:24:28 2021 +0200
@@ -1,17 +1,15 @@
(* Title: Tools/try.ML
Author: Jasmin Blanchette, TU Muenchen
+ Author: Makarius
Manager for tools that should be tried on conjectures.
*)
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
@@ -20,11 +18,6 @@
structure Try : TRY =
struct
-type tool = string * (int * string * (bool -> Proof.state -> bool * (string * string list)));
-
-val tryN = "try";
-
-
(* helpers *)
fun serial_commas _ [] = ["??"]
@@ -33,13 +26,14 @@
| serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3]
| serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss;
-val subgoal_count = Logic.count_prems o Thm.prop_of o #goal o Proof.goal;
-
(* 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
(
@@ -57,17 +51,17 @@
(* try command *)
fun try_tools state =
- if subgoal_count state = 0 then
+ if Proof.goal_finished state then
(writeln "No subgoal!"; NONE)
else
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" | _ => ());
@@ -78,24 +72,12 @@
(Scan.succeed (Toplevel.keep_proof (ignore o try_tools o Toplevel.proof_of)));
-(* automatic try (TTY) *)
+(* asynchronous print function *)
-fun auto_try state =
- get_tools (Proof.theory_of state)
- |> map_filter (fn (_, (_, auto, tool)) => if Options.default_bool auto then SOME tool else NONE)
- |> Par_List.get_some (fn tool =>
- (case try (tool true) state of
- SOME (true, (_, outcome)) => SOME outcome
- | _ => NONE))
- |> the_default [];
-
-
-(* asynchronous print function (PIDE) *)
-
-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,
@@ -108,7 +90,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 ()
@@ -116,7 +98,7 @@
else NONE);
-(* hybrid tool setup *)
+(* tool setup *)
fun tool_setup tool = (Theory.setup (register_tool tool); print_function tool);