# HG changeset patch # User blanchet # Date 1330079014 -3600 # Node ID 8801a24f9e9a0514e48d48dd75242929291a9e6c # Parent 622691cec7c30c85dc30c4eaf19cfc767f47537a renamed 'try_methods' to 'try0' diff -r 622691cec7c3 -r 8801a24f9e9a NEWS --- a/NEWS Fri Feb 24 11:23:33 2012 +0100 +++ b/NEWS Fri Feb 24 11:23:34 2012 +0100 @@ -336,6 +336,9 @@ - Added possibility to specify lambda translations scheme as a parenthesized argument (e.g., "by (metis (lifting) ...)"). +* Command 'try0': + - Renamed from 'try_methods'. INCOMPATIBILITY. + *** FOL *** diff -r 622691cec7c3 -r 8801a24f9e9a doc-src/IsarRef/Thy/HOL_Specific.thy --- a/doc-src/IsarRef/Thy/HOL_Specific.thy Fri Feb 24 11:23:33 2012 +0100 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Fri Feb 24 11:23:34 2012 +0100 @@ -1571,7 +1571,7 @@ \begin{matharray}{rcl} @{command_def (HOL) "solve_direct"}@{text "\<^sup>*"} & : & @{text "proof \"} \\ @{command_def (HOL) "try"}@{text "\<^sup>*"} & : & @{text "proof \"} \\ - @{command_def (HOL) "try_methods"}@{text "\<^sup>*"} & : & @{text "proof \"} \\ + @{command_def (HOL) "try0"}@{text "\<^sup>*"} & : & @{text "proof \"} \\ @{command_def (HOL) "sledgehammer"}@{text "\<^sup>*"} & : & @{text "proof \"} \\ @{command_def (HOL) "sledgehammer_params"} & : & @{text "theory \ theory"} \end{matharray} @@ -1580,7 +1580,7 @@ @@{command (HOL) try} ; - @@{command (HOL) try_methods} ( ( ( 'simp' | 'intro' | 'elim' | 'dest' ) ':' @{syntax thmrefs} ) + ) ? + @@{command (HOL) try0} ( ( ( 'simp' | 'intro' | 'elim' | 'dest' ) ':' @{syntax thmrefs} ) + ) ? @{syntax nat}? ; @@ -1603,7 +1603,7 @@ subgoals can be solved directly by an existing theorem. Duplicate lemmas can be detected in this way. - \item @{command (HOL) "try_methods"} attempts to prove a subgoal + \item @{command (HOL) "try0"} attempts to prove a subgoal using a combination of standard proof methods (@{method auto}, @{method simp}, @{method blast}, etc.). Additional facts supplied via @{text "simp:"}, @{text "intro:"}, @{text "elim:"}, and @{text @@ -1612,7 +1612,7 @@ \item @{command (HOL) "try"} attempts to prove or disprove a subgoal using a combination of provers and disprovers (@{command (HOL) "solve_direct"}, @{command (HOL) "quickcheck"}, @{command (HOL) - "try_methods"}, @{command (HOL) "sledgehammer"}, @{command (HOL) + "try0"}, @{command (HOL) "sledgehammer"}, @{command (HOL) "nitpick"}). \item @{command (HOL) "sledgehammer"} attempts to prove a subgoal diff -r 622691cec7c3 -r 8801a24f9e9a doc-src/IsarRef/Thy/document/HOL_Specific.tex --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Fri Feb 24 11:23:33 2012 +0100 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Fri Feb 24 11:23:34 2012 +0100 @@ -2207,7 +2207,7 @@ \begin{matharray}{rcl} \indexdef{HOL}{command}{solve\_direct}\hypertarget{command.HOL.solve-direct}{\hyperlink{command.HOL.solve-direct}{\mbox{\isa{\isacommand{solve{\isaliteral{5F}{\isacharunderscore}}direct}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\ \indexdef{HOL}{command}{try}\hypertarget{command.HOL.try}{\hyperlink{command.HOL.try}{\mbox{\isa{\isacommand{try}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\ - \indexdef{HOL}{command}{try\_methods}\hypertarget{command.HOL.try-methods}{\hyperlink{command.HOL.try-methods}{\mbox{\isa{\isacommand{try{\isaliteral{5F}{\isacharunderscore}}methods}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\ + \indexdef{HOL}{command}{try0}\hypertarget{command.HOL.try0}{\hyperlink{command.HOL.try0}{\mbox{\isa{\isacommand{try0}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\ \indexdef{HOL}{command}{sledgehammer}\hypertarget{command.HOL.sledgehammer}{\hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\ \indexdef{HOL}{command}{sledgehammer\_params}\hypertarget{command.HOL.sledgehammer-params}{\hyperlink{command.HOL.sledgehammer-params}{\mbox{\isa{\isacommand{sledgehammer{\isaliteral{5F}{\isacharunderscore}}params}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \end{matharray} @@ -2217,7 +2217,7 @@ \rail@term{\hyperlink{command.HOL.try}{\mbox{\isa{\isacommand{try}}}}}[] \rail@end \rail@begin{6}{} -\rail@term{\hyperlink{command.HOL.try-methods}{\mbox{\isa{\isacommand{try{\isaliteral{5F}{\isacharunderscore}}methods}}}}}[] +\rail@term{\hyperlink{command.HOL.try0}{\mbox{\isa{\isacommand{try0}}}}}[] \rail@bar \rail@nextbar{1} \rail@plus @@ -2304,13 +2304,13 @@ subgoals can be solved directly by an existing theorem. Duplicate lemmas can be detected in this way. - \item \hyperlink{command.HOL.try-methods}{\mbox{\isa{\isacommand{try{\isaliteral{5F}{\isacharunderscore}}methods}}}} attempts to prove a subgoal + \item \hyperlink{command.HOL.try0}{\mbox{\isa{\isacommand{try0}}}} attempts to prove a subgoal using a combination of standard proof methods (\hyperlink{method.auto}{\mbox{\isa{auto}}}, \hyperlink{method.simp}{\mbox{\isa{simp}}}, \hyperlink{method.blast}{\mbox{\isa{blast}}}, etc.). Additional facts supplied via \isa{{\isaliteral{22}{\isachardoublequote}}simp{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}intro{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}elim{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}}, and \isa{{\isaliteral{22}{\isachardoublequote}}dest{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} are passed to the appropriate proof methods. \item \hyperlink{command.HOL.try}{\mbox{\isa{\isacommand{try}}}} attempts to prove or disprove a subgoal - using a combination of provers and disprovers (\hyperlink{command.HOL.solve-direct}{\mbox{\isa{\isacommand{solve{\isaliteral{5F}{\isacharunderscore}}direct}}}}, \hyperlink{command.HOL.quickcheck}{\mbox{\isa{\isacommand{quickcheck}}}}, \hyperlink{command.HOL.try-methods}{\mbox{\isa{\isacommand{try{\isaliteral{5F}{\isacharunderscore}}methods}}}}, \hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}}, \hyperlink{command.HOL.nitpick}{\mbox{\isa{\isacommand{nitpick}}}}). + using a combination of provers and disprovers (\hyperlink{command.HOL.solve-direct}{\mbox{\isa{\isacommand{solve{\isaliteral{5F}{\isacharunderscore}}direct}}}}, \hyperlink{command.HOL.quickcheck}{\mbox{\isa{\isacommand{quickcheck}}}}, \hyperlink{command.HOL.try0}{\mbox{\isa{\isacommand{try0}}}}, \hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}}, \hyperlink{command.HOL.nitpick}{\mbox{\isa{\isacommand{nitpick}}}}). \item \hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}} attempts to prove a subgoal using external automatic provers (resolution provers and SMT diff -r 622691cec7c3 -r 8801a24f9e9a etc/isar-keywords.el --- a/etc/isar-keywords.el Fri Feb 24 11:23:33 2012 +0100 +++ b/etc/isar-keywords.el Fri Feb 24 11:23:34 2012 +0100 @@ -254,7 +254,7 @@ "thy_deps" "translations" "try" - "try_methods" + "try0" "txt" "txt_raw" "typ" @@ -413,7 +413,7 @@ "thm_deps" "thy_deps" "try" - "try_methods" + "try0" "typ" "unused_thms" "value" diff -r 622691cec7c3 -r 8801a24f9e9a src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Fri Feb 24 11:23:33 2012 +0100 +++ b/src/HOL/IsaMakefile Fri Feb 24 11:23:34 2012 +0100 @@ -263,7 +263,7 @@ Tools/sat_funcs.ML \ Tools/sat_solver.ML \ Tools/split_rule.ML \ - Tools/try_methods.ML \ + Tools/try0.ML \ Tools/typedef.ML \ Transitive_Closure.thy \ Typedef.thy \ diff -r 622691cec7c3 -r 8801a24f9e9a src/HOL/Metis.thy --- a/src/HOL/Metis.thy Fri Feb 24 11:23:33 2012 +0100 +++ b/src/HOL/Metis.thy Fri Feb 24 11:23:34 2012 +0100 @@ -12,7 +12,7 @@ ("Tools/Metis/metis_generate.ML") ("Tools/Metis/metis_reconstruct.ML") ("Tools/Metis/metis_tactic.ML") - ("Tools/try_methods.ML") + ("Tools/try0.ML") begin subsection {* Literal selection and lambda-lifting helpers *} @@ -52,10 +52,10 @@ select_FalseI lambda_def eq_lambdaI -subsection {* Try Methods *} +subsection {* Try0 *} -use "Tools/try_methods.ML" +use "Tools/try0.ML" -setup {* Try_Methods.setup *} +setup {* Try0.setup *} end diff -r 622691cec7c3 -r 8801a24f9e9a src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Feb 24 11:23:33 2012 +0100 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Feb 24 11:23:34 2012 +0100 @@ -662,7 +662,7 @@ val minimize = AList.defined (op =) args minimizeK val metis_ft = AList.defined (op =) args metis_ftK val trivial = - Try_Methods.try_methods (SOME try_timeout) ([], [], [], []) pre + Try0.try0 (SOME try_timeout) ([], [], [], []) pre handle TimeLimit.TimeOut => false fun apply_reconstructor m1 m2 = if metis_ft diff -r 622691cec7c3 -r 8801a24f9e9a src/HOL/Mutabelle/mutabelle_extra.ML --- a/src/HOL/Mutabelle/mutabelle_extra.ML Fri Feb 24 11:23:33 2012 +0100 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML Fri Feb 24 11:23:34 2012 +0100 @@ -24,7 +24,7 @@ val quickcheck_mtd : (Proof.context -> Proof.context) -> string -> mtd val solve_direct_mtd : mtd -val try_methods_mtd : mtd +val try0_mtd : mtd (* val sledgehammer_mtd : mtd *) @@ -138,18 +138,18 @@ val solve_direct_mtd = ("solve_direct", invoke_solve_direct) -(** try **) +(** try0 **) -fun invoke_try_methods thy t = +fun invoke_try0 thy t = let val state = Proof.theorem NONE (K I) (map (single o rpair []) [t]) (Proof_Context.init_global thy) in - case Try_Methods.try_methods (SOME (seconds 5.0)) ([], [], [], []) state of + case Try0.try0 (SOME (seconds 5.0)) ([], [], [], []) state of true => (Solved, []) | false => (Unsolved, []) end -val try_methods_mtd = ("try_methods", invoke_try_methods) +val try0_mtd = ("try0", invoke_try0) (** sledgehammer **) (* diff -r 622691cec7c3 -r 8801a24f9e9a src/HOL/Tools/try0.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/try0.ML Fri Feb 24 11:23:34 2012 +0100 @@ -0,0 +1,199 @@ +(* Title: HOL/Tools/try0.ML + Author: Jasmin Blanchette, TU Muenchen + +Try a combination of proof methods. +*) + +signature TRY0 = +sig + val try0N : string + val noneN : string + val auto : bool Unsynchronized.ref + val try0 : + Time.time option -> string list * string list * string list * string list + -> Proof.state -> bool + val setup : theory -> theory +end; + +structure Try0 : TRY0 = +struct + +datatype mode = Auto_Try | Try | Normal + +val try0N = "try0" + +val noneN = "none" + +val auto = Unsynchronized.ref false + +val _ = + ProofGeneralPgip.add_preference Preferences.category_tracing + (Preferences.bool_pref auto "auto-try0" "Try standard proof methods.") + +val default_timeout = seconds 5.0 + +fun can_apply timeout_opt pre post tac st = + let val {goal, ...} = Proof.goal st in + case (case timeout_opt of + SOME timeout => TimeLimit.timeLimit timeout + | NONE => fn f => fn x => f x) (Seq.pull o tac) (pre st) of + SOME (x, _) => nprems_of (post x) < nprems_of goal + | NONE => false + end + handle TimeLimit.TimeOut => false + +fun do_generic timeout_opt command pre post apply st = + let val timer = Timer.startRealTimer () in + if can_apply timeout_opt pre post apply st then + SOME (command, Time.toMilliseconds (Timer.checkRealTimer timer)) + else + NONE + end + +val parse_method = + enclose "(" ")" + #> Outer_Syntax.scan Position.start + #> filter Token.is_proper + #> Scan.read Token.stopper Method.parse + #> (fn SOME (Method.Source src) => src | _ => raise Fail "expected Source") + +fun apply_named_method_on_first_goal method thy = + method |> parse_method + |> Method.method thy + |> Method.Basic + |> curry Method.SelectGoals 1 + |> Proof.refine + handle ERROR _ => K Seq.empty (* e.g., the method isn't available yet *) + +fun add_attr_text (NONE, _) s = s + | add_attr_text (_, []) s = s + | add_attr_text (SOME x, fs) s = + s ^ " " ^ (if x = "" then "" else x ^ ": ") ^ space_implode " " fs +fun attrs_text (sx, ix, ex, dx) (ss, is, es, ds) = + "" |> fold add_attr_text [(sx, ss), (ix, is), (ex, es), (dx, ds)] + +fun do_named_method (name, ((all_goals, run_if_auto_try), attrs)) mode + timeout_opt quad st = + if mode <> Auto_Try orelse run_if_auto_try then + let val attrs = attrs_text attrs quad in + do_generic timeout_opt + (name ^ (if all_goals andalso + nprems_of (#goal (Proof.goal st)) > 1 then + "[1]" + else + "") ^ + attrs) I (#goal o Proof.goal) + (apply_named_method_on_first_goal (name ^ attrs) + (Proof.theory_of st)) st + end + else + NONE + +val full_attrs = (SOME "simp", SOME "intro", SOME "elim", SOME "dest") +val clas_attrs = (NONE, SOME "intro", SOME "elim", SOME "dest") +val simp_attrs = (SOME "add", NONE, NONE, NONE) +val metis_attrs = (SOME "", SOME "", SOME "", SOME "") +val no_attrs = (NONE, NONE, NONE, NONE) + +(* name * ((all_goals, run_if_auto_try), (simp, intro, elim, dest) *) +val named_methods = + [("simp", ((false, true), simp_attrs)), + ("auto", ((true, true), full_attrs)), + ("fast", ((false, false), clas_attrs)), + ("fastforce", ((false, false), full_attrs)), + ("force", ((false, false), full_attrs)), + ("blast", ((false, true), clas_attrs)), + ("metis", ((false, true), metis_attrs)), + ("linarith", ((false, true), no_attrs)), + ("presburger", ((false, true), no_attrs))] +val do_methods = map do_named_method named_methods + +fun time_string (s, ms) = s ^ ": " ^ string_of_int ms ^ " ms" + +fun do_try0 mode timeout_opt quad st = + let + val st = st |> Proof.map_context (Config.put Metis_Tactic.verbose false #> + Config.put Lin_Arith.verbose false) + in + if mode = Normal then + "Trying " ^ space_implode " " (Try.serial_commas "and" + (map (quote o fst) named_methods)) ^ "..." + |> Output.urgent_message + else + (); + case do_methods |> Par_List.map (fn f => f mode timeout_opt quad st) + |> map_filter I |> sort (int_ord o pairself snd) of + [] => + (if mode = Normal then Output.urgent_message "No proof found." else (); + (false, (noneN, st))) + | xs as (s, _) :: _ => + let + val xs = xs |> map (fn (s, n) => (n, hd (space_explode " " s))) + |> AList.coalesce (op =) + |> map (swap o apsnd commas) + val need_parens = exists_string (curry (op =) " ") s + val message = + (case mode of + Auto_Try => "Auto Try Methods found a proof" + | Try => "Try Methods found a proof" + | Normal => "Try this") ^ ": " ^ + Markup.markup Isabelle_Markup.sendback + ((if nprems_of (#goal (Proof.goal st)) = 1 then "by" + else "apply") ^ " " ^ (s |> need_parens ? enclose "(" ")")) ^ + "\n(" ^ space_implode "; " (map time_string xs) ^ ").\n" + in + (true, (s, st |> (if mode = Auto_Try then + Proof.goal_message + (fn () => Pretty.chunks [Pretty.str "", + Pretty.markup Isabelle_Markup.hilite + [Pretty.str message]]) + else + tap (fn _ => Output.urgent_message message)))) + end + end + +fun try0 timeout_opt = fst oo do_try0 Normal timeout_opt + +fun try0_trans quad = + Toplevel.keep (K () o do_try0 Normal (SOME default_timeout) quad + o Toplevel.proof_of) + +fun merge_attrs (s1, i1, e1, d1) (s2, i2, e2, d2) = + (s1 @ s2, i1 @ i2, e1 @ e2, d1 @ d2) + +fun string_of_xthm (xref, args) = + Facts.string_of_ref xref ^ + implode (map (enclose "[" "]" o Pretty.str_of + o Args.pretty_src @{context}) args) + +val parse_fact_refs = + Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) + (Parse_Spec.xthm >> string_of_xthm)) +val parse_attr = + Args.$$$ "simp" |-- Args.colon |-- parse_fact_refs + >> (fn ss => (ss, [], [], [])) + || Args.$$$ "intro" |-- Args.colon |-- parse_fact_refs + >> (fn is => ([], is, [], [])) + || Args.$$$ "elim" |-- Args.colon |-- parse_fact_refs + >> (fn es => ([], [], es, [])) + || Args.$$$ "dest" |-- Args.colon |-- parse_fact_refs + >> (fn ds => ([], [], [], ds)) +fun parse_attrs x = + (Args.parens parse_attrs + || Scan.repeat parse_attr + >> (fn quad => fold merge_attrs quad ([], [], [], []))) x + +val parse_try0_command = + Scan.optional parse_attrs ([], [], [], []) #>> try0_trans + +val _ = + Outer_Syntax.improper_command try0N + "try a combination of proof methods" Keyword.diag + parse_try0_command + +fun try_try0 auto = + do_try0 (if auto then Auto_Try else Try) NONE ([], [], [], []) + +val setup = Try.register_tool (try0N, (30, auto, try_try0)) + +end; diff -r 622691cec7c3 -r 8801a24f9e9a src/HOL/Tools/try_methods.ML --- a/src/HOL/Tools/try_methods.ML Fri Feb 24 11:23:33 2012 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,200 +0,0 @@ -(* Title: HOL/Tools/try_methods.ML - Author: Jasmin Blanchette, TU Muenchen - -Try a combination of proof methods. -*) - -signature TRY_METHODS = -sig - val try_methodsN : string - val noneN : string - val auto : bool Unsynchronized.ref - val try_methods : - Time.time option -> string list * string list * string list * string list - -> Proof.state -> bool - val setup : theory -> theory -end; - -structure Try_Methods : TRY_METHODS = -struct - -datatype mode = Auto_Try | Try | Normal - -val try_methodsN = "try_methods" - -val noneN = "none" - -val auto = Unsynchronized.ref false - -val _ = - ProofGeneralPgip.add_preference Preferences.category_tracing - (Preferences.bool_pref auto "auto-try-methods" - "Try standard proof methods.") - -val default_timeout = seconds 5.0 - -fun can_apply timeout_opt pre post tac st = - let val {goal, ...} = Proof.goal st in - case (case timeout_opt of - SOME timeout => TimeLimit.timeLimit timeout - | NONE => fn f => fn x => f x) (Seq.pull o tac) (pre st) of - SOME (x, _) => nprems_of (post x) < nprems_of goal - | NONE => false - end - handle TimeLimit.TimeOut => false - -fun do_generic timeout_opt command pre post apply st = - let val timer = Timer.startRealTimer () in - if can_apply timeout_opt pre post apply st then - SOME (command, Time.toMilliseconds (Timer.checkRealTimer timer)) - else - NONE - end - -val parse_method = - enclose "(" ")" - #> Outer_Syntax.scan Position.start - #> filter Token.is_proper - #> Scan.read Token.stopper Method.parse - #> (fn SOME (Method.Source src) => src | _ => raise Fail "expected Source") - -fun apply_named_method_on_first_goal method thy = - method |> parse_method - |> Method.method thy - |> Method.Basic - |> curry Method.SelectGoals 1 - |> Proof.refine - handle ERROR _ => K Seq.empty (* e.g., the method isn't available yet *) - -fun add_attr_text (NONE, _) s = s - | add_attr_text (_, []) s = s - | add_attr_text (SOME x, fs) s = - s ^ " " ^ (if x = "" then "" else x ^ ": ") ^ space_implode " " fs -fun attrs_text (sx, ix, ex, dx) (ss, is, es, ds) = - "" |> fold add_attr_text [(sx, ss), (ix, is), (ex, es), (dx, ds)] - -fun do_named_method (name, ((all_goals, run_if_auto_try), attrs)) mode - timeout_opt quad st = - if mode <> Auto_Try orelse run_if_auto_try then - let val attrs = attrs_text attrs quad in - do_generic timeout_opt - (name ^ (if all_goals andalso - nprems_of (#goal (Proof.goal st)) > 1 then - "[1]" - else - "") ^ - attrs) I (#goal o Proof.goal) - (apply_named_method_on_first_goal (name ^ attrs) - (Proof.theory_of st)) st - end - else - NONE - -val full_attrs = (SOME "simp", SOME "intro", SOME "elim", SOME "dest") -val clas_attrs = (NONE, SOME "intro", SOME "elim", SOME "dest") -val simp_attrs = (SOME "add", NONE, NONE, NONE) -val metis_attrs = (SOME "", SOME "", SOME "", SOME "") -val no_attrs = (NONE, NONE, NONE, NONE) - -(* name * ((all_goals, run_if_auto_try), (simp, intro, elim, dest) *) -val named_methods = - [("simp", ((false, true), simp_attrs)), - ("auto", ((true, true), full_attrs)), - ("fast", ((false, false), clas_attrs)), - ("fastforce", ((false, false), full_attrs)), - ("force", ((false, false), full_attrs)), - ("blast", ((false, true), clas_attrs)), - ("metis", ((false, true), metis_attrs)), - ("linarith", ((false, true), no_attrs)), - ("presburger", ((false, true), no_attrs))] -val do_methods = map do_named_method named_methods - -fun time_string (s, ms) = s ^ ": " ^ string_of_int ms ^ " ms" - -fun do_try_methods mode timeout_opt quad st = - let - val st = st |> Proof.map_context (Config.put Metis_Tactic.verbose false #> - Config.put Lin_Arith.verbose false) - in - if mode = Normal then - "Trying " ^ space_implode " " (Try.serial_commas "and" - (map (quote o fst) named_methods)) ^ "..." - |> Output.urgent_message - else - (); - case do_methods |> Par_List.map (fn f => f mode timeout_opt quad st) - |> map_filter I |> sort (int_ord o pairself snd) of - [] => - (if mode = Normal then Output.urgent_message "No proof found." else (); - (false, (noneN, st))) - | xs as (s, _) :: _ => - let - val xs = xs |> map (fn (s, n) => (n, hd (space_explode " " s))) - |> AList.coalesce (op =) - |> map (swap o apsnd commas) - val need_parens = exists_string (curry (op =) " ") s - val message = - (case mode of - Auto_Try => "Auto Try Methods found a proof" - | Try => "Try Methods found a proof" - | Normal => "Try this") ^ ": " ^ - Markup.markup Isabelle_Markup.sendback - ((if nprems_of (#goal (Proof.goal st)) = 1 then "by" - else "apply") ^ " " ^ (s |> need_parens ? enclose "(" ")")) ^ - "\n(" ^ space_implode "; " (map time_string xs) ^ ").\n" - in - (true, (s, st |> (if mode = Auto_Try then - Proof.goal_message - (fn () => Pretty.chunks [Pretty.str "", - Pretty.markup Isabelle_Markup.hilite - [Pretty.str message]]) - else - tap (fn _ => Output.urgent_message message)))) - end - end - -fun try_methods timeout_opt = fst oo do_try_methods Normal timeout_opt - -fun try_methods_trans quad = - Toplevel.keep (K () o do_try_methods Normal (SOME default_timeout) quad - o Toplevel.proof_of) - -fun merge_attrs (s1, i1, e1, d1) (s2, i2, e2, d2) = - (s1 @ s2, i1 @ i2, e1 @ e2, d1 @ d2) - -fun string_of_xthm (xref, args) = - Facts.string_of_ref xref ^ - implode (map (enclose "[" "]" o Pretty.str_of - o Args.pretty_src @{context}) args) - -val parse_fact_refs = - Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) - (Parse_Spec.xthm >> string_of_xthm)) -val parse_attr = - Args.$$$ "simp" |-- Args.colon |-- parse_fact_refs - >> (fn ss => (ss, [], [], [])) - || Args.$$$ "intro" |-- Args.colon |-- parse_fact_refs - >> (fn is => ([], is, [], [])) - || Args.$$$ "elim" |-- Args.colon |-- parse_fact_refs - >> (fn es => ([], [], es, [])) - || Args.$$$ "dest" |-- Args.colon |-- parse_fact_refs - >> (fn ds => ([], [], [], ds)) -fun parse_attrs x = - (Args.parens parse_attrs - || Scan.repeat parse_attr - >> (fn quad => fold merge_attrs quad ([], [], [], []))) x - -val parse_try_methods_command = - Scan.optional parse_attrs ([], [], [], []) #>> try_methods_trans - -val _ = - Outer_Syntax.improper_command try_methodsN - "try a combination of proof methods" Keyword.diag - parse_try_methods_command - -fun try_try_methods auto = - do_try_methods (if auto then Auto_Try else Try) NONE ([], [], [], []) - -val setup = Try.register_tool (try_methodsN, (30, auto, try_try_methods)) - -end;