# HG changeset patch # User blanchet # Date 1306485008 -7200 # Node ID 42330f25142c9675f43dd4fed7f60a3a30e6e312 # Parent 21b6baec55b1ed1834ec155212af7808563ba3c8 renamed "try" "try_methods" diff -r 21b6baec55b1 -r 42330f25142c doc-src/IsarRef/Thy/HOL_Specific.thy --- a/doc-src/IsarRef/Thy/HOL_Specific.thy Fri May 27 10:30:08 2011 +0200 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Fri May 27 10:30:08 2011 +0200 @@ -931,13 +931,13 @@ \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) "sledgehammer"}@{text "\<^sup>*"} & : & @{text "proof \"} \\ @{command_def (HOL) "sledgehammer_params"} & : & @{text "theory \ theory"} \end{matharray} @{rail " - @@{command (HOL) try} ( ( ( 'simp' | 'intro' | 'elim' | 'dest' ) ':' @{syntax thmrefs} ) + ) ? + @@{command (HOL) try_methods} ( ( ( 'simp' | 'intro' | 'elim' | 'dest' ) ':' @{syntax thmrefs} ) + ) ? @{syntax nat}? ; @@{command (HOL) sledgehammer} ( '[' args ']' )? facts? @{syntax nat}? @@ -951,7 +951,7 @@ facts: '(' ( ( ( ( 'add' | 'del' ) ':' ) ? @{syntax thmrefs} ) + ) ? ')' ; - "} % FIXME try: proper clasimpmod!? + "} % FIXME try_methods: proper clasimpmod!? % FIXME check args "value" \begin{description} @@ -960,7 +960,7 @@ be solved directly by an existing theorem. Duplicate lemmas can be detected in this way. - \item @{command (HOL) "try"} attempts to prove a subgoal using a combination + \item @{command (HOL) "try_methods"} attempts to prove a subgoal using a combination of standard proof methods (@{text auto}, @{text simp}, @{text blast}, etc.). Additional facts supplied via @{text "simp:"}, @{text "intro:"}, @{text "elim:"}, and @{text "dest:"} are passed to the appropriate proof diff -r 21b6baec55b1 -r 42330f25142c src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Fri May 27 10:30:08 2011 +0200 +++ b/src/HOL/IsaMakefile Fri May 27 10:30:08 2011 +0200 @@ -245,7 +245,7 @@ Tools/sat_funcs.ML \ Tools/sat_solver.ML \ Tools/split_rule.ML \ - Tools/try.ML \ + Tools/try_methods.ML \ Tools/typedef.ML \ Tools/enriched_type.ML \ Transitive_Closure.thy \ diff -r 21b6baec55b1 -r 42330f25142c src/HOL/Metis.thy --- a/src/HOL/Metis.thy Fri May 27 10:30:08 2011 +0200 +++ b/src/HOL/Metis.thy Fri May 27 10:30:08 2011 +0200 @@ -12,7 +12,7 @@ ("Tools/Metis/metis_translate.ML") ("Tools/Metis/metis_reconstruct.ML") ("Tools/Metis/metis_tactics.ML") - ("Tools/try.ML") + ("Tools/try_methods.ML") begin @@ -70,10 +70,10 @@ fequal_def select_def not_atomize atomize_not_select not_atomize_select select_FalseI -subsection {* Try *} +subsection {* Try Methods *} -use "Tools/try.ML" +use "Tools/try_methods.ML" -setup {* Try.setup *} +setup {* Try_Methods.setup *} end diff -r 21b6baec55b1 -r 42330f25142c src/HOL/Tools/try.ML --- a/src/HOL/Tools/try.ML Fri May 27 10:30:08 2011 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,179 +0,0 @@ -(* Title: HOL/Tools/try.ML - Author: Jasmin Blanchette, TU Muenchen - -Try a combination of proof methods. -*) - -signature TRY = -sig - val auto : bool Unsynchronized.ref - val invoke_try : - Time.time option -> string list * string list * string list * string list - -> Proof.state -> bool - val setup : theory -> theory -end; - -structure Try : TRY = -struct - -val auto = Unsynchronized.ref false - -val _ = - ProofGeneralPgip.add_preference Preferences.category_tracing - (Preferences.bool_pref auto "auto-try" "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), attrs)) auto timeout_opt - quad st = - if not auto orelse run_if_auto 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), (simp, intro, elim, dest) *) -val named_methods = - [("simp", ((false, true), simp_attrs)), - ("auto", ((true, true), full_attrs)), - ("fast", ((false, false), clas_attrs)), - ("fastsimp", ((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 auto timeout_opt quad st = - let - val st = st |> Proof.map_context (Config.put Metis_Tactics.verbose false) - in - case do_methods |> Par_List.map (fn f => f auto timeout_opt quad st) - |> map_filter I |> sort (int_ord o pairself snd) of - [] => (if auto then () else writeln "No proof found."; (false, 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 = - (if auto then "Auto Try found a proof" else "Try this command") ^ - ": " ^ - Markup.markup 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, st |> (if auto then - Proof.goal_message - (fn () => Pretty.chunks [Pretty.str "", - Pretty.markup Markup.hilite - [Pretty.str message]]) - else - tap (fn _ => Output.urgent_message message))) - end - end - -fun invoke_try timeout_opt = fst oo do_try false timeout_opt - -val tryN = "try" - -fun try_trans quad = - Toplevel.keep (K () o do_try false (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_command = Scan.optional parse_attrs ([], [], [], []) #>> try_trans - -val _ = - Outer_Syntax.improper_command tryN - "try a combination of proof methods" Keyword.diag parse_try_command - -val auto_try = do_try true NONE ([], [], [], []) - -val setup = Auto_Tools.register_tool (auto, auto_try) - -end; diff -r 21b6baec55b1 -r 42330f25142c src/HOL/Tools/try_methods.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/try_methods.ML Fri May 27 10:30:08 2011 +0200 @@ -0,0 +1,182 @@ +(* Title: HOL/Tools/try_methods.ML + Author: Jasmin Blanchette, TU Muenchen + +Try a combination of proof methods. +*) + +signature TRY_METHODS = +sig + 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 + +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), attrs)) auto timeout_opt + quad st = + if not auto orelse run_if_auto 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), (simp, intro, elim, dest) *) +val named_methods = + [("simp", ((false, true), simp_attrs)), + ("auto", ((true, true), full_attrs)), + ("fast", ((false, false), clas_attrs)), + ("fastsimp", ((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 auto timeout_opt quad st = + let + val st = st |> Proof.map_context (Config.put Metis_Tactics.verbose false) + in + case do_methods |> Par_List.map (fn f => f auto timeout_opt quad st) + |> map_filter I |> sort (int_ord o pairself snd) of + [] => (if auto then () else writeln "No proof found."; (false, 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 = + (if auto then "Auto Try Methods found a proof" + else "Try this command") ^ ": " ^ + Markup.markup 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, st |> (if auto then + Proof.goal_message + (fn () => Pretty.chunks [Pretty.str "", + Pretty.markup Markup.hilite + [Pretty.str message]]) + else + tap (fn _ => Output.urgent_message message))) + end + end + +fun try_methods timeout_opt = fst oo do_try_methods false timeout_opt + +val try_methodsN = "try_methods" + +fun try_methods_trans quad = + Toplevel.keep (K () o do_try_methods false (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 + +val auto_try_methods = do_try_methods true NONE ([], [], [], []) + +val setup = Auto_Tools.register_tool (auto, auto_try_methods) + +end;