wneuper/isa: src/HOL/Tools/try_methods.ML@58150aa44941

     1 (*  Title:      HOL/Tools/try_methods.ML

     2     Author:     Jasmin Blanchette, TU Muenchen

     4 Try a combination of proof methods.

     5 *)

     7 signature TRY_METHODS =

     8 sig

     9   val try_methodsN : string

    10   val noneN : string

    11   val auto : bool Unsynchronized.ref

    12   val try_methods :

    13     Time.time option -> string list * string list * string list * string list

    14     -> Proof.state -> bool

    15   val setup : theory -> theory

    16 end;

    18 structure Try_Methods : TRY_METHODS =

    19 struct

    21 val try_methodsN = "try_methods"

    23 val noneN = "none"

    25 val auto = Unsynchronized.ref false

    27 val _ =

    28   ProofGeneralPgip.add_preference Preferences.category_tracing

    29       (Preferences.bool_pref auto "auto-try-methods"

    30                              "Try standard proof methods.")

    32 val default_timeout = seconds 5.0

    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

    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

    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")

    59 fun apply_named_method_on_first_goal method thy =

    60   method |> parse_method

    61          |> Method.method thy

    62          |> Method.Basic

    63          |> curry Method.SelectGoals 1

    64          |> Proof.refine

    65   handle ERROR _ => K Seq.empty (* e.g., the method isn't available yet *)

    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)]

    74 fun do_named_method (name, ((all_goals, run_if_auto), attrs)) auto timeout_opt

    75                     quad st =

    76   if not auto orelse run_if_auto then

    77     let val attrs = attrs_text attrs quad in

    78       do_generic timeout_opt

    79                  (name ^ (if all_goals andalso

    80                              nprems_of (#goal (Proof.goal st)) > 1 then

    81                             "[1]"

    82                           else

    83                             "") ^

    84                   attrs) I (#goal o Proof.goal)

    85                  (apply_named_method_on_first_goal (name ^ attrs)

    86                                                    (Proof.theory_of st)) st

    87     end

    88   else

    89     NONE

    91 val full_attrs = (SOME "simp", SOME "intro", SOME "elim", SOME "dest")

    92 val clas_attrs = (NONE, SOME "intro", SOME "elim", SOME "dest")

    93 val simp_attrs = (SOME "add", NONE, NONE, NONE)

    94 val metis_attrs = (SOME "", SOME "", SOME "", SOME "")

    95 val no_attrs = (NONE, NONE, NONE, NONE)

    97 (* name * ((all_goals, run_if_auto), (simp, intro, elim, dest) *)

    98 val named_methods =

    99   [("simp", ((false, true), simp_attrs)),

   100    ("auto", ((true, true), full_attrs)),

   101    ("fast", ((false, false), clas_attrs)),

   102    ("fastsimp", ((false, false), full_attrs)),

   103    ("force", ((false, false), full_attrs)),

   104    ("blast", ((false, true), clas_attrs)),

   105    ("metis", ((false, true), metis_attrs)),

   106    ("linarith", ((false, true), no_attrs)),

   107    ("presburger", ((false, true), no_attrs))]

   108 val do_methods = map do_named_method named_methods

   110 fun time_string (s, ms) = s ^ ": " ^ string_of_int ms ^ " ms"

   112 fun do_try_methods auto timeout_opt quad st =

   113   let

   114     val st = st |> Proof.map_context (Config.put Metis_Tactics.verbose false)

   115   in

   116     case do_methods |> Par_List.map (fn f => f auto timeout_opt quad st)

   117                     |> map_filter I |> sort (int_ord o pairself snd) of

   118       [] => (if auto then () else writeln "No proof found.";

   119              (false, (noneN, st)))

   120     | xs as (s, _) :: _ =>

   121       let

   122         val xs = xs |> map (fn (s, n) => (n, hd (space_explode " " s)))

   123                     |> AList.coalesce (op =)

   124                     |> map (swap o apsnd commas)

   125         val need_parens = exists_string (curry (op =) " ") s

   126         val message =

   127           (if auto then "Auto Try Methods found a proof"

   128            else "Try this command") ^ ": " ^

   129           Markup.markup Markup.sendback

   130               ((if nprems_of (#goal (Proof.goal st)) = 1 then "by"

   131                 else "apply") ^ " " ^ (s |> need_parens ? enclose "(" ")")) ^

   132           "\n(" ^ space_implode "; " (map time_string xs) ^ ").\n"

   133       in

   134         (true, (s, st |> (if auto then

   135                             Proof.goal_message

   136                                 (fn () => Pretty.chunks [Pretty.str "",

   137                                           Pretty.markup Markup.hilite

   138                                                         [Pretty.str message]])

   139                           else

   140                             tap (fn _ => Output.urgent_message message))))

   141       end

   142   end

   144 fun try_methods timeout_opt = fst oo do_try_methods false timeout_opt

   146 fun try_methods_trans quad =

   147   Toplevel.keep (K () o do_try_methods false (SOME default_timeout) quad

   148                  o Toplevel.proof_of)

   150 fun merge_attrs (s1, i1, e1, d1) (s2, i2, e2, d2) =

   151   (s1 @ s2, i1 @ i2, e1 @ e2, d1 @ d2)

   153 fun string_of_xthm (xref, args) =

   154   Facts.string_of_ref xref ^

   155   implode (map (enclose "[" "]" o Pretty.str_of

   156                 o Args.pretty_src @{context}) args)

   158 val parse_fact_refs =

   159   Scan.repeat1 (Scan.unless (Parse.name -- Args.colon)

   160                             (Parse_Spec.xthm >> string_of_xthm))

   161 val parse_attr =

   162      Args.$$$ "simp" |-- Args.colon |-- parse_fact_refs

   163      >> (fn ss => (ss, [], [], []))

   164   || Args.$$$ "intro" |-- Args.colon |-- parse_fact_refs

   165      >> (fn is => ([], is, [], []))

   166   || Args.$$$ "elim" |-- Args.colon |-- parse_fact_refs

   167      >> (fn es => ([], [], es, []))

   168   || Args.$$$ "dest" |-- Args.colon |-- parse_fact_refs

   169      >> (fn ds => ([], [], [], ds))

   170 fun parse_attrs x =

   171     (Args.parens parse_attrs

   172   || Scan.repeat parse_attr

   173      >> (fn quad => fold merge_attrs quad ([], [], [], []))) x

   175 val parse_try_methods_command =

   176   Scan.optional parse_attrs ([], [], [], []) #>> try_methods_trans

   178 val _ =

   179   Outer_Syntax.improper_command try_methodsN

   180       "try a combination of proof methods" Keyword.diag

   181       parse_try_methods_command

   183 fun try_try_methods auto = do_try_methods auto NONE ([], [], [], [])

   185 val setup = Try.register_tool (try_methodsN, (20, auto, try_try_methods))

   187 end;

author	blanchet
	Fri, 27 May 2011 10:30:08 +0200
changeset 43865	58150aa44941
parent 43861	abb5d1f907e4
child 43867	0f15575a6465
permissions	-rw-r--r--