src/HOL/Tools/try0.ML
author wenzelm
Thu Jul 18 20:53:22 2013 +0200 (2013-07-18 ago)
changeset 52697 6fb98a20c349
parent 52643 34c29356930e
child 52717 da7bf8b3d24a
permissions -rw-r--r--
explicit padding on command boundary for "auto" generated sendback -- do not replace the corresponding goal command, but append to it;
     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 try0 :
    12     Time.time option -> string list * string list * string list * string list
    13     -> Proof.state -> bool
    14 end;
    15 
    16 structure Try0 : TRY0 =
    17 struct
    18 
    19 datatype mode = Auto_Try | Try | Normal
    20 
    21 val try0N = "try0"
    22 
    23 val noneN = "none"
    24 
    25 val _ =
    26   ProofGeneral.preference_option ProofGeneral.category_tracing
    27     NONE
    28     @{option auto_try0}
    29     "auto-try0"
    30     "Try standard proof methods"
    31 
    32 val default_timeout = seconds 5.0
    33 
    34 fun can_apply timeout_opt pre post tac st =
    35   let val {goal, ...} = Proof.goal st in
    36     case (case timeout_opt of
    37             SOME timeout => TimeLimit.timeLimit timeout
    38           | NONE => fn f => fn x => f x) (Seq.pull o tac) (pre st) of
    39       SOME (x, _) => nprems_of (post x) < nprems_of goal
    40     | NONE => false
    41   end
    42   handle TimeLimit.TimeOut => false
    43 
    44 fun do_generic timeout_opt command pre post apply st =
    45   let val timer = Timer.startRealTimer () in
    46     if can_apply timeout_opt pre post apply st then
    47       SOME (command, Time.toMilliseconds (Timer.checkRealTimer timer))
    48     else
    49       NONE
    50   end
    51 
    52 val parse_method =
    53   enclose "(" ")"
    54   #> Outer_Syntax.scan Position.start
    55   #> filter Token.is_proper
    56   #> Scan.read Token.stopper Method.parse
    57   #> (fn SOME (Method.Source src, _) => src | _ => raise Fail "expected Source")
    58 
    59 fun apply_named_method_on_first_goal method thy =
    60   method |> parse_method
    61          |> Method.method thy
    62          |> Method.Basic
    63          |> curry Method.Select_Goals 1
    64          |> Proof.refine
    65   handle ERROR _ => K Seq.empty (* e.g., the method isn't available yet *)
    66 
    67 fun add_attr_text (NONE, _) s = s
    68   | add_attr_text (_, []) s = s
    69   | add_attr_text (SOME x, fs) s =
    70     s ^ " " ^ (if x = "" then "" else x ^ ": ") ^ space_implode " " fs
    71 fun attrs_text (sx, ix, ex, dx) (ss, is, es, ds) =
    72   "" |> fold add_attr_text [(sx, ss), (ix, is), (ex, es), (dx, ds)]
    73 
    74 fun do_named_method (name, ((all_goals, run_if_auto_try), attrs)) mode
    75                     timeout_opt quad st =
    76   if mode <> Auto_Try orelse run_if_auto_try then
    77     let val attrs = attrs_text attrs quad in
    78       do_generic timeout_opt
    79                  (name ^ attrs ^
    80                   (if all_goals andalso
    81                       nprems_of (#goal (Proof.goal st)) > 1 then
    82                      " [1]"
    83                    else
    84                      ""))
    85                  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           Active.sendback_markup (if mode = Auto_Try then [Markup.padding_command] else [])
   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) ^ ")."
   144       in
   145         (true, (s, st |> (if mode = Auto_Try then
   146                             Proof.goal_message
   147                                 (fn () => Pretty.markup Markup.information
   148                                                         [Pretty.str message])
   149                           else
   150                             tap (fn _ => Output.urgent_message message))))
   151       end
   152   end
   153 
   154 fun try0 timeout_opt = fst oo do_try0 Normal timeout_opt
   155 
   156 fun try0_trans quad =
   157   Toplevel.unknown_proof o
   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 _ = Try.tool_setup (try0N, (30, @{option auto_try0}, try_try0))
   195 
   196 end;