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