src/HOL/Tools/try0.ML
author haftmann
Fri Oct 10 19:55:32 2014 +0200 (2014-10-10)
changeset 58646 cd63a4b12a33
parent 58028 e4250d370657
child 58842 22b87ab47d3b
permissions -rw-r--r--
specialized specification: avoid trivial instances
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@55177
    11
blanchet@55177
    12
  val silence_methods : bool -> Proof.context -> Proof.context
blanchet@55179
    13
  val try0 : Time.time option -> string list * string list * string list * string list ->
blanchet@55179
    14
    Proof.state -> bool
blanchet@38942
    15
end;
blanchet@38942
    16
blanchet@46641
    17
structure Try0 : TRY0 =
blanchet@38942
    18
struct
blanchet@38942
    19
blanchet@55179
    20
val try0N = "try0";
blanchet@55179
    21
val noneN = "none";
blanchet@43026
    22
blanchet@55179
    23
datatype mode = Auto_Try | Try | Normal;
blanchet@43020
    24
blanchet@39333
    25
val _ =
wenzelm@52639
    26
  ProofGeneral.preference_option ProofGeneral.category_tracing
wenzelm@52017
    27
    NONE
wenzelm@56467
    28
    @{system_option auto_methods}
wenzelm@52017
    29
    "auto-try0"
blanchet@55179
    30
    "Try standard proof methods";
blanchet@39333
    31
blanchet@55179
    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@55182
    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@55182
    40
    | NONE => false)
blanchet@55182
    41
  end;
blanchet@38942
    42
blanchet@55181
    43
fun apply_generic timeout_opt name command pre post apply st =
blanchet@38942
    44
  let val timer = Timer.startRealTimer () in
blanchet@55182
    45
    if try (can_apply timeout_opt pre post apply) st = SOME true then
blanchet@54291
    46
      SOME (name, command, Time.toMilliseconds (Timer.checkRealTimer timer))
blanchet@38942
    47
    else
blanchet@38942
    48
      NONE
blanchet@55179
    49
  end;
blanchet@38942
    50
wenzelm@57918
    51
fun parse_method s =
wenzelm@57918
    52
  enclose "(" ")" s
wenzelm@57918
    53
  |> Outer_Syntax.scan (Keyword.get_lexicons ()) Position.start
wenzelm@57918
    54
  |> filter Token.is_proper
wenzelm@57918
    55
  |> Scan.read Token.stopper Method.parse
wenzelm@57918
    56
  |> (fn SOME (Method.Source src, _) => src | _ => raise Fail "expected Source");
blanchet@38942
    57
wenzelm@55742
    58
fun apply_named_method_on_first_goal ctxt =
blanchet@55182
    59
  parse_method
wenzelm@55997
    60
  #> Method.method_cmd ctxt
blanchet@55182
    61
  #> Method.Basic
wenzelm@58005
    62
  #> (fn m => Method.Combinator (Method.no_combinator_info, Method.Select_Goals 1, [m]))
blanchet@55182
    63
  #> Proof.refine;
blanchet@38942
    64
blanchet@41999
    65
fun add_attr_text (NONE, _) s = s
blanchet@41999
    66
  | add_attr_text (_, []) s = s
blanchet@41999
    67
  | add_attr_text (SOME x, fs) s =
blanchet@55179
    68
    s ^ " " ^ (if x = "" then "" else x ^ ": ") ^ space_implode " " fs;
blanchet@55179
    69
blanchet@42179
    70
fun attrs_text (sx, ix, ex, dx) (ss, is, es, ds) =
blanchet@55179
    71
  "" |> fold add_attr_text [(sx, ss), (ix, is), (ex, es), (dx, ds)];
blanchet@41999
    72
blanchet@55181
    73
fun apply_named_method (name, ((all_goals, run_if_auto_try), attrs)) mode timeout_opt quad st =
blanchet@43026
    74
  if mode <> Auto_Try orelse run_if_auto_try then
blanchet@42179
    75
    let val attrs = attrs_text attrs quad in
blanchet@55181
    76
      apply_generic timeout_opt name
blanchet@54291
    77
        ((name ^ attrs |> attrs <> "" ? enclose "(" ")") ^
blanchet@54291
    78
         (if all_goals andalso nprems_of (#goal (Proof.goal st)) > 1 then "[1]" else ""))
blanchet@54291
    79
        I (#goal o Proof.goal)
wenzelm@55742
    80
        (apply_named_method_on_first_goal (Proof.context_of st) (name ^ attrs)) st
blanchet@41999
    81
    end
blanchet@40222
    82
  else
blanchet@55179
    83
    NONE;
blanchet@38942
    84
blanchet@55179
    85
val full_attrs = (SOME "simp", SOME "intro", SOME "elim", SOME "dest");
blanchet@55179
    86
val clas_attrs = (NONE, SOME "intro", SOME "elim", SOME "dest");
blanchet@55179
    87
val simp_attrs = (SOME "add", NONE, NONE, NONE);
blanchet@55179
    88
val metis_attrs = (SOME "", SOME "", SOME "", SOME "");
blanchet@55179
    89
val no_attrs = (NONE, NONE, NONE, NONE);
blanchet@41999
    90
blanchet@43026
    91
(* name * ((all_goals, run_if_auto_try), (simp, intro, elim, dest) *)
blanchet@39547
    92
val named_methods =
blanchet@41999
    93
  [("simp", ((false, true), simp_attrs)),
blanchet@41999
    94
   ("auto", ((true, true), full_attrs)),
blanchet@55178
    95
   ("blast", ((false, true), clas_attrs)),
blanchet@55178
    96
   ("metis", ((false, true), metis_attrs)),
blanchet@55178
    97
   ("linarith", ((false, true), no_attrs)),
blanchet@55178
    98
   ("presburger", ((false, true), no_attrs)),
blanchet@55178
    99
   ("algebra", ((false, true), no_attrs)),
blanchet@41999
   100
   ("fast", ((false, false), clas_attrs)),
nipkow@44890
   101
   ("fastforce", ((false, false), full_attrs)),
blanchet@41999
   102
   ("force", ((false, false), full_attrs)),
blanchet@56850
   103
   ("meson", ((false, false), metis_attrs)),
blanchet@56850
   104
   ("satx", ((false, false), no_attrs))];
blanchet@55179
   105
blanchet@55181
   106
val apply_methods = map apply_named_method named_methods;
blanchet@38942
   107
blanchet@55179
   108
fun time_string ms = string_of_int ms ^ " ms";
blanchet@55179
   109
fun tool_time_string (s, ms) = s ^ ": " ^ time_string ms;
blanchet@38942
   110
blanchet@55177
   111
(* Makes reconstructor tools as silent as possible. The "set_visible" calls suppresses "Unification
blanchet@55177
   112
   bound exceeded" warnings and the like. *)
blanchet@55177
   113
fun silence_methods debug =
blanchet@55177
   114
  Config.put Metis_Tactic.verbose debug
blanchet@55177
   115
  #> Config.put Lin_Arith.verbose debug
blanchet@55177
   116
  #> (not debug ?
blanchet@55177
   117
    (Context_Position.set_visible false
blanchet@55177
   118
     #> Proof_Context.background_theory (fn thy =>
blanchet@55177
   119
       thy
blanchet@55177
   120
       |> Context_Position.set_visible_global false
blanchet@55179
   121
       |> Config.put_global Unify.trace_bound (Config.get_global thy Unify.search_bound))));
blanchet@55177
   122
blanchet@55181
   123
fun generic_try0 mode timeout_opt quad st =
blanchet@41038
   124
  let
blanchet@56982
   125
    val st = Proof.map_contexts (silence_methods false) st;
blanchet@55179
   126
    fun trd (_, _, t) = t;
blanchet@54248
   127
    fun par_map f =
blanchet@54431
   128
      if mode = Normal then Par_List.map f #> map_filter I #> sort (int_ord o pairself trd)
blanchet@55179
   129
      else Par_List.get_some f #> the_list;
blanchet@41038
   130
  in
blanchet@43026
   131
    if mode = Normal then
blanchet@55179
   132
      "Trying " ^ space_implode " " (Try.serial_commas "and" (map (quote o fst) named_methods)) ^
blanchet@55179
   133
      "..."
blanchet@43026
   134
      |> Output.urgent_message
blanchet@43026
   135
    else
blanchet@43026
   136
      ();
blanchet@55181
   137
    (case par_map (fn f => f mode timeout_opt quad st) apply_methods of
blanchet@43026
   138
      [] =>
blanchet@55179
   139
      (if mode = Normal then Output.urgent_message "No proof found." else (); (false, (noneN, st)))
blanchet@54291
   140
    | xs as (name, command, _) :: _ =>
blanchet@41038
   141
      let
blanchet@54291
   142
        val xs = xs |> map (fn (name, _, n) => (n, name))
blanchet@41999
   143
                    |> AList.coalesce (op =)
blanchet@41038
   144
                    |> map (swap o apsnd commas)
blanchet@41038
   145
        val message =
blanchet@43026
   146
          (case mode of
blanchet@52970
   147
             Auto_Try => "Auto Try0 found a proof"
blanchet@52970
   148
           | Try => "Try0 found a proof"
blanchet@43031
   149
           | Normal => "Try this") ^ ": " ^
wenzelm@53052
   150
          Active.sendback_markup [Markup.padding_command]
blanchet@41038
   151
              ((if nprems_of (#goal (Proof.goal st)) = 1 then "by"
blanchet@54291
   152
                else "apply") ^ " " ^ command) ^
blanchet@54248
   153
          (case xs of
blanchet@54248
   154
            [(_, ms)] => " (" ^ time_string ms ^ ")."
blanchet@54248
   155
          | xs => "\n(" ^ space_implode "; " (map tool_time_string xs) ^ ").")
blanchet@41038
   156
      in
blanchet@54291
   157
        (true, (name,
blanchet@55179
   158
           st
blanchet@55179
   159
           |> (if mode = Auto_Try then
blanchet@55179
   160
                 Proof.goal_message (fn () => Pretty.markup Markup.information [Pretty.str message])
blanchet@55179
   161
               else
blanchet@55179
   162
                 tap (fn _ => Output.urgent_message message))))
blanchet@54291
   163
      end)
blanchet@55179
   164
  end;
blanchet@39331
   165
blanchet@55181
   166
fun try0 timeout_opt = fst oo generic_try0 Normal timeout_opt;
blanchet@38942
   167
blanchet@46641
   168
fun try0_trans quad =
wenzelm@51557
   169
  Toplevel.unknown_proof o
blanchet@55181
   170
  Toplevel.keep (K () o generic_try0 Normal (SOME default_timeout) quad o Toplevel.proof_of);
blanchet@41999
   171
blanchet@55179
   172
fun merge_attrs (s1, i1, e1, d1) (s2, i2, e2, d2) = (s1 @ s2, i1 @ i2, e1 @ e2, d1 @ d2);
blanchet@41999
   173
blanchet@41999
   174
fun string_of_xthm (xref, args) =
blanchet@41999
   175
  Facts.string_of_ref xref ^
wenzelm@58011
   176
  implode (map (enclose "[" "]" o Pretty.str_of o Token.pretty_src @{context}) args);
blanchet@41999
   177
blanchet@41999
   178
val parse_fact_refs =
wenzelm@58028
   179
  Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) (Parse.xthm >> string_of_xthm));
blanchet@55179
   180
blanchet@41999
   181
val parse_attr =
blanchet@55179
   182
  Args.$$$ "simp" |-- Args.colon |-- parse_fact_refs >> (fn ss => (ss, [], [], []))
blanchet@55179
   183
  || Args.$$$ "intro" |-- Args.colon |-- parse_fact_refs >> (fn is => ([], is, [], []))
blanchet@55179
   184
  || Args.$$$ "elim" |-- Args.colon |-- parse_fact_refs >> (fn es => ([], [], es, []))
blanchet@55179
   185
  || Args.$$$ "dest" |-- Args.colon |-- parse_fact_refs >> (fn ds => ([], [], [], ds));
blanchet@55179
   186
blanchet@41999
   187
fun parse_attrs x =
blanchet@55179
   188
  (Args.parens parse_attrs
blanchet@55179
   189
   || Scan.repeat parse_attr >> (fn quad => fold merge_attrs quad ([], [], [], []))) x;
blanchet@41999
   190
blanchet@38942
   191
val _ =
blanchet@55179
   192
  Outer_Syntax.improper_command @{command_spec "try0"} "try a combination of proof methods"
blanchet@55179
   193
    (Scan.optional parse_attrs ([], [], [], []) #>> try0_trans);
blanchet@38942
   194
blanchet@55181
   195
fun try_try0 auto = generic_try0 (if auto then Auto_Try else Try) NONE ([], [], [], []);
blanchet@39331
   196
wenzelm@56467
   197
val _ = Try.tool_setup (try0N, (30, @{system_option auto_methods}, try_try0));
blanchet@39331
   198
blanchet@38942
   199
end;