src/HOL/Tools/try0.ML
author wenzelm
Fri Mar 16 18:20:12 2012 +0100 (2012-03-16)
changeset 46961 5c6955f487e5
parent 46641 8801a24f9e9a
child 48535 619531d87ce4
permissions -rw-r--r--
outer syntax command definitions based on formal command_spec derived from theory header declarations;
     1 (*  Title:      HOL/Tools/try0.ML
     2     Author:     Jasmin Blanchette, TU Muenchen
     3 
     4 Try a combination of proof methods.
     5 *)
     6 
     7 signature TRY0 =
     8 sig
     9   val try0N : string
    10   val noneN : string
    11   val auto : bool Unsynchronized.ref
    12   val try0 :
    13     Time.time option -> string list * string list * string list * string list
    14     -> Proof.state -> bool
    15   val setup : theory -> theory
    16 end;
    17 
    18 structure Try0 : TRY0 =
    19 struct
    20 
    21 datatype mode = Auto_Try | Try | Normal
    22 
    23 val try0N = "try0"
    24 
    25 val noneN = "none"
    26 
    27 val auto = Unsynchronized.ref false
    28 
    29 val _ =
    30   ProofGeneralPgip.add_preference Preferences.category_tracing
    31       (Preferences.bool_pref auto "auto-try0" "Try standard proof methods.")
    32 
    33 val default_timeout = seconds 5.0
    34 
    35 fun can_apply timeout_opt pre post tac st =
    36   let val {goal, ...} = Proof.goal st in
    37     case (case timeout_opt of
    38             SOME timeout => TimeLimit.timeLimit timeout
    39           | NONE => fn f => fn x => f x) (Seq.pull o tac) (pre st) of
    40       SOME (x, _) => nprems_of (post x) < nprems_of goal
    41     | NONE => false
    42   end
    43   handle TimeLimit.TimeOut => false
    44 
    45 fun do_generic timeout_opt command pre post apply st =
    46   let val timer = Timer.startRealTimer () in
    47     if can_apply timeout_opt pre post apply st then
    48       SOME (command, Time.toMilliseconds (Timer.checkRealTimer timer))
    49     else
    50       NONE
    51   end
    52 
    53 val parse_method =
    54   enclose "(" ")"
    55   #> Outer_Syntax.scan Position.start
    56   #> filter Token.is_proper
    57   #> Scan.read Token.stopper Method.parse
    58   #> (fn SOME (Method.Source src) => src | _ => raise Fail "expected Source")
    59 
    60 fun apply_named_method_on_first_goal method thy =
    61   method |> parse_method
    62          |> Method.method thy
    63          |> Method.Basic
    64          |> curry Method.SelectGoals 1
    65          |> Proof.refine
    66   handle ERROR _ => K Seq.empty (* e.g., the method isn't available yet *)
    67 
    68 fun add_attr_text (NONE, _) s = s
    69   | add_attr_text (_, []) s = s
    70   | add_attr_text (SOME x, fs) s =
    71     s ^ " " ^ (if x = "" then "" else x ^ ": ") ^ space_implode " " fs
    72 fun attrs_text (sx, ix, ex, dx) (ss, is, es, ds) =
    73   "" |> fold add_attr_text [(sx, ss), (ix, is), (ex, es), (dx, ds)]
    74 
    75 fun do_named_method (name, ((all_goals, run_if_auto_try), attrs)) mode
    76                     timeout_opt quad st =
    77   if mode <> Auto_Try orelse run_if_auto_try then
    78     let val attrs = attrs_text attrs quad in
    79       do_generic timeout_opt
    80                  (name ^ (if all_goals andalso
    81                              nprems_of (#goal (Proof.goal st)) > 1 then
    82                             "[1]"
    83                           else
    84                             "") ^
    85                   attrs) I (#goal o Proof.goal)
    86                  (apply_named_method_on_first_goal (name ^ attrs)
    87                                                    (Proof.theory_of st)) st
    88     end
    89   else
    90     NONE
    91 
    92 val full_attrs = (SOME "simp", SOME "intro", SOME "elim", SOME "dest")
    93 val clas_attrs = (NONE, SOME "intro", SOME "elim", SOME "dest")
    94 val simp_attrs = (SOME "add", NONE, NONE, NONE)
    95 val metis_attrs = (SOME "", SOME "", SOME "", SOME "")
    96 val no_attrs = (NONE, NONE, NONE, NONE)
    97 
    98 (* name * ((all_goals, run_if_auto_try), (simp, intro, elim, dest) *)
    99 val named_methods =
   100   [("simp", ((false, true), simp_attrs)),
   101    ("auto", ((true, true), full_attrs)),
   102    ("fast", ((false, false), clas_attrs)),
   103    ("fastforce", ((false, false), full_attrs)),
   104    ("force", ((false, false), full_attrs)),
   105    ("blast", ((false, true), clas_attrs)),
   106    ("metis", ((false, true), metis_attrs)),
   107    ("linarith", ((false, true), no_attrs)),
   108    ("presburger", ((false, true), no_attrs))]
   109 val do_methods = map do_named_method named_methods
   110 
   111 fun time_string (s, ms) = s ^ ": " ^ string_of_int ms ^ " ms"
   112 
   113 fun do_try0 mode timeout_opt quad st =
   114   let
   115     val st = st |> Proof.map_context (Config.put Metis_Tactic.verbose false #>
   116       Config.put Lin_Arith.verbose false)
   117   in
   118     if mode = Normal then
   119       "Trying " ^ space_implode " " (Try.serial_commas "and"
   120                                       (map (quote o fst) named_methods)) ^ "..."
   121       |> Output.urgent_message
   122     else
   123       ();
   124     case do_methods |> Par_List.map (fn f => f mode timeout_opt quad st)
   125                     |> map_filter I |> sort (int_ord o pairself snd) of
   126       [] =>
   127       (if mode = Normal then Output.urgent_message "No proof found." else ();
   128        (false, (noneN, st)))
   129     | xs as (s, _) :: _ =>
   130       let
   131         val xs = xs |> map (fn (s, n) => (n, hd (space_explode " " s)))
   132                     |> AList.coalesce (op =)
   133                     |> map (swap o apsnd commas)
   134         val need_parens = exists_string (curry (op =) " ") s
   135         val message =
   136           (case mode of
   137              Auto_Try => "Auto Try Methods found a proof"
   138            | Try => "Try Methods found a proof"
   139            | Normal => "Try this") ^ ": " ^
   140           Markup.markup Isabelle_Markup.sendback
   141               ((if nprems_of (#goal (Proof.goal st)) = 1 then "by"
   142                 else "apply") ^ " " ^ (s |> need_parens ? enclose "(" ")")) ^
   143           "\n(" ^ space_implode "; " (map time_string xs) ^ ").\n"
   144       in
   145         (true, (s, st |> (if mode = Auto_Try then
   146                             Proof.goal_message
   147                                 (fn () => Pretty.chunks [Pretty.str "",
   148                                           Pretty.markup Isabelle_Markup.hilite
   149                                                         [Pretty.str message]])
   150                           else
   151                             tap (fn _ => Output.urgent_message message))))
   152       end
   153   end
   154 
   155 fun try0 timeout_opt = fst oo do_try0 Normal timeout_opt
   156 
   157 fun try0_trans quad =
   158   Toplevel.keep (K () o do_try0 Normal (SOME default_timeout) quad
   159                  o Toplevel.proof_of)
   160 
   161 fun merge_attrs (s1, i1, e1, d1) (s2, i2, e2, d2) =
   162   (s1 @ s2, i1 @ i2, e1 @ e2, d1 @ d2)
   163 
   164 fun string_of_xthm (xref, args) =
   165   Facts.string_of_ref xref ^
   166   implode (map (enclose "[" "]" o Pretty.str_of
   167                 o Args.pretty_src @{context}) args)
   168 
   169 val parse_fact_refs =
   170   Scan.repeat1 (Scan.unless (Parse.name -- Args.colon)
   171                             (Parse_Spec.xthm >> string_of_xthm))
   172 val parse_attr =
   173      Args.$$$ "simp" |-- Args.colon |-- parse_fact_refs
   174      >> (fn ss => (ss, [], [], []))
   175   || Args.$$$ "intro" |-- Args.colon |-- parse_fact_refs
   176      >> (fn is => ([], is, [], []))
   177   || Args.$$$ "elim" |-- Args.colon |-- parse_fact_refs
   178      >> (fn es => ([], [], es, []))
   179   || Args.$$$ "dest" |-- Args.colon |-- parse_fact_refs
   180      >> (fn ds => ([], [], [], ds))
   181 fun parse_attrs x =
   182     (Args.parens parse_attrs
   183   || Scan.repeat parse_attr
   184      >> (fn quad => fold merge_attrs quad ([], [], [], []))) x
   185 
   186 val _ =
   187   Outer_Syntax.improper_command @{command_spec "try0"}
   188     "try a combination of proof methods"
   189     (Scan.optional parse_attrs ([], [], [], []) #>> try0_trans)
   190 
   191 fun try_try0 auto =
   192   do_try0 (if auto then Auto_Try else Try) NONE ([], [], [], [])
   193 
   194 val setup = Try.register_tool (try0N, (30, auto, try_try0))
   195 
   196 end;