# HG changeset patch # User desharna # Date 1634217868 -7200 # Node ID c434f4e749471bcecd58c273442b39dda954d1dd # Parent 6d111935299ca098b6cce9a9ea55a474d68d0547# Parent 21a20b9907243a3f1ce9d4e7fbb1613c06542609 merged diff -r 6d111935299c -r c434f4e74947 src/HOL/Library/refute.ML --- 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 diff -r 6d111935299c -r c434f4e74947 src/HOL/Tools/Nitpick/nitpick_commands.ML --- 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>\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 6d111935299c -r c434f4e74947 src/HOL/Tools/Nunchaku/nunchaku.ML --- 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 diff -r 6d111935299c -r c434f4e74947 src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML --- 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>\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 6d111935299c -r c434f4e74947 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- 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 diff -r 6d111935299c -r c434f4e74947 src/HOL/Tools/try0.ML --- 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>\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 6d111935299c -r c434f4e74947 src/Pure/Isar/element.ML --- 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); diff -r 6d111935299c -r c434f4e74947 src/Pure/Isar/proof.ML --- 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; diff -r 6d111935299c -r c434f4e74947 src/Pure/logic.ML --- 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\...Ai\B*) fun nth_prem (1, Const ("Pure.imp", _) $ A $ _) = A | nth_prem (i, Const ("Pure.imp", _) $ _ $ B) = nth_prem (i - 1, B) diff -r 6d111935299c -r c434f4e74947 src/Pure/raw_simplifier.ML --- 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 diff -r 6d111935299c -r c434f4e74947 src/Pure/thm.ML --- 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 diff -r 6d111935299c -r c434f4e74947 src/Tools/quickcheck.ML --- 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>\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 6d111935299c -r c434f4e74947 src/Tools/solve_direct.ML --- 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>\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 6d111935299c -r c434f4e74947 src/Tools/try.ML --- 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>\auto_time_start\)), pri = ~ weight, @@ -108,7 +90,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 () @@ -116,7 +98,7 @@ else NONE); -(* hybrid tool setup *) +(* tool setup *) fun tool_setup tool = (Theory.setup (register_tool tool); print_function tool);