src/HOL/Tools/try0.ML
author wenzelm
Tue Sep 26 20:54:40 2017 +0200 (23 months ago)
changeset 66695 91500c024c7f
parent 63961 2fd9656c4c82
child 67149 e61557884799
permissions -rw-r--r--
tuned;
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@55179
    25
val default_timeout = seconds 5.0;
blanchet@38944
    26
blanchet@39336
    27
fun can_apply timeout_opt pre post tac st =
blanchet@38942
    28
  let val {goal, ...} = Proof.goal st in
blanchet@55182
    29
    (case (case timeout_opt of
wenzelm@62519
    30
            SOME timeout => Timeout.apply timeout
blanchet@39336
    31
          | NONE => fn f => fn x => f x) (Seq.pull o tac) (pre st) of
wenzelm@59582
    32
      SOME (x, _) => Thm.nprems_of (post x) < Thm.nprems_of goal
blanchet@55182
    33
    | NONE => false)
blanchet@55182
    34
  end;
blanchet@38942
    35
blanchet@55181
    36
fun apply_generic timeout_opt name command pre post apply st =
blanchet@38942
    37
  let val timer = Timer.startRealTimer () in
blanchet@55182
    38
    if try (can_apply timeout_opt pre post apply) st = SOME true then
blanchet@54291
    39
      SOME (name, command, Time.toMilliseconds (Timer.checkRealTimer timer))
blanchet@38942
    40
    else
blanchet@38942
    41
      NONE
blanchet@55179
    42
  end;
blanchet@38942
    43
wenzelm@58928
    44
fun parse_method keywords s =
wenzelm@57918
    45
  enclose "(" ")" s
wenzelm@59083
    46
  |> Token.explode keywords Position.start
wenzelm@57918
    47
  |> filter Token.is_proper
wenzelm@57918
    48
  |> Scan.read Token.stopper Method.parse
wenzelm@57918
    49
  |> (fn SOME (Method.Source src, _) => src | _ => raise Fail "expected Source");
blanchet@38942
    50
wenzelm@55742
    51
fun apply_named_method_on_first_goal ctxt =
wenzelm@58928
    52
  parse_method (Thy_Header.get_keywords' ctxt)
wenzelm@55997
    53
  #> Method.method_cmd ctxt
blanchet@55182
    54
  #> Method.Basic
wenzelm@58005
    55
  #> (fn m => Method.Combinator (Method.no_combinator_info, Method.Select_Goals 1, [m]))
blanchet@55182
    56
  #> Proof.refine;
blanchet@38942
    57
blanchet@41999
    58
fun add_attr_text (NONE, _) s = s
blanchet@41999
    59
  | add_attr_text (_, []) s = s
blanchet@41999
    60
  | add_attr_text (SOME x, fs) s =
blanchet@55179
    61
    s ^ " " ^ (if x = "" then "" else x ^ ": ") ^ space_implode " " fs;
blanchet@55179
    62
blanchet@42179
    63
fun attrs_text (sx, ix, ex, dx) (ss, is, es, ds) =
blanchet@55179
    64
  "" |> fold add_attr_text [(sx, ss), (ix, is), (ex, es), (dx, ds)];
blanchet@41999
    65
blanchet@55181
    66
fun apply_named_method (name, ((all_goals, run_if_auto_try), attrs)) mode timeout_opt quad st =
blanchet@43026
    67
  if mode <> Auto_Try orelse run_if_auto_try then
blanchet@42179
    68
    let val attrs = attrs_text attrs quad in
blanchet@55181
    69
      apply_generic timeout_opt name
blanchet@54291
    70
        ((name ^ attrs |> attrs <> "" ? enclose "(" ")") ^
wenzelm@59582
    71
         (if all_goals andalso Thm.nprems_of (#goal (Proof.goal st)) > 1 then "[1]" else ""))
blanchet@54291
    72
        I (#goal o Proof.goal)
wenzelm@61841
    73
        (apply_named_method_on_first_goal (Proof.context_of st) (name ^ attrs)
wenzelm@61841
    74
          #> Seq.filter_results) st
blanchet@41999
    75
    end
blanchet@40222
    76
  else
blanchet@55179
    77
    NONE;
blanchet@38942
    78
blanchet@55179
    79
val full_attrs = (SOME "simp", SOME "intro", SOME "elim", SOME "dest");
blanchet@55179
    80
val clas_attrs = (NONE, SOME "intro", SOME "elim", SOME "dest");
blanchet@55179
    81
val simp_attrs = (SOME "add", NONE, NONE, NONE);
blanchet@55179
    82
val metis_attrs = (SOME "", SOME "", SOME "", SOME "");
blanchet@55179
    83
val no_attrs = (NONE, NONE, NONE, NONE);
blanchet@41999
    84
blanchet@43026
    85
(* name * ((all_goals, run_if_auto_try), (simp, intro, elim, dest) *)
blanchet@39547
    86
val named_methods =
blanchet@41999
    87
  [("simp", ((false, true), simp_attrs)),
blanchet@41999
    88
   ("auto", ((true, true), full_attrs)),
blanchet@55178
    89
   ("blast", ((false, true), clas_attrs)),
blanchet@55178
    90
   ("metis", ((false, true), metis_attrs)),
boehmes@63961
    91
   ("argo", ((false, true), no_attrs)),
blanchet@55178
    92
   ("linarith", ((false, true), no_attrs)),
blanchet@55178
    93
   ("presburger", ((false, true), no_attrs)),
blanchet@55178
    94
   ("algebra", ((false, true), no_attrs)),
blanchet@41999
    95
   ("fast", ((false, false), clas_attrs)),
nipkow@44890
    96
   ("fastforce", ((false, false), full_attrs)),
blanchet@41999
    97
   ("force", ((false, false), full_attrs)),
blanchet@56850
    98
   ("meson", ((false, false), metis_attrs)),
blanchet@56850
    99
   ("satx", ((false, false), no_attrs))];
blanchet@55179
   100
blanchet@55181
   101
val apply_methods = map apply_named_method named_methods;
blanchet@38942
   102
blanchet@55179
   103
fun time_string ms = string_of_int ms ^ " ms";
blanchet@55179
   104
fun tool_time_string (s, ms) = s ^ ": " ^ time_string ms;
blanchet@38942
   105
blanchet@55177
   106
(* Makes reconstructor tools as silent as possible. The "set_visible" calls suppresses "Unification
blanchet@55177
   107
   bound exceeded" warnings and the like. *)
blanchet@55177
   108
fun silence_methods debug =
blanchet@55177
   109
  Config.put Metis_Tactic.verbose debug
wenzelm@60275
   110
  #> not debug ? (fn ctxt =>
wenzelm@60275
   111
      ctxt
wenzelm@62984
   112
      |> Simplifier_Trace.disable
wenzelm@60275
   113
      |> Context_Position.set_visible false
wenzelm@60275
   114
      |> Config.put Unify.trace_bound (Config.get ctxt Unify.search_bound)
boehmes@63961
   115
      |> Config.put Argo_Tactic.trace "none"
wenzelm@60275
   116
      |> Proof_Context.background_theory (fn thy =>
wenzelm@60275
   117
          thy
wenzelm@60275
   118
          |> Context_Position.set_visible_global false
wenzelm@60275
   119
          |> Config.put_global Unify.trace_bound (Config.get_global thy Unify.search_bound)));
blanchet@55177
   120
blanchet@55181
   121
fun generic_try0 mode timeout_opt quad st =
blanchet@41038
   122
  let
blanchet@56982
   123
    val st = Proof.map_contexts (silence_methods false) st;
blanchet@55179
   124
    fun trd (_, _, t) = t;
blanchet@54248
   125
    fun par_map f =
wenzelm@59058
   126
      if mode = Normal then Par_List.map f #> map_filter I #> sort (int_ord o apply2 trd)
blanchet@55179
   127
      else Par_List.get_some f #> the_list;
blanchet@41038
   128
  in
blanchet@43026
   129
    if mode = Normal then
blanchet@55179
   130
      "Trying " ^ space_implode " " (Try.serial_commas "and" (map (quote o fst) named_methods)) ^
blanchet@55179
   131
      "..."
wenzelm@58843
   132
      |> writeln
blanchet@43026
   133
    else
blanchet@43026
   134
      ();
blanchet@55181
   135
    (case par_map (fn f => f mode timeout_opt quad st) apply_methods of
blanchet@43026
   136
      [] =>
blanchet@63690
   137
      (if mode = Normal then writeln "No proof found" else (); (false, (noneN, [])))
blanchet@54291
   138
    | xs as (name, command, _) :: _ =>
blanchet@41038
   139
      let
blanchet@54291
   140
        val xs = xs |> map (fn (name, _, n) => (n, name))
blanchet@41999
   141
                    |> AList.coalesce (op =)
blanchet@63690
   142
                    |> map (swap o apsnd commas);
blanchet@41038
   143
        val message =
blanchet@43026
   144
          (case mode of
blanchet@52970
   145
             Auto_Try => "Auto Try0 found a proof"
blanchet@52970
   146
           | Try => "Try0 found a proof"
blanchet@43031
   147
           | Normal => "Try this") ^ ": " ^
wenzelm@63518
   148
          Active.sendback_markup_command
wenzelm@59582
   149
              ((if Thm.nprems_of (#goal (Proof.goal st)) = 1 then "by"
blanchet@54291
   150
                else "apply") ^ " " ^ command) ^
blanchet@54248
   151
          (case xs of
blanchet@63690
   152
            [(_, ms)] => " (" ^ time_string ms ^ ")"
blanchet@63690
   153
          | xs => "\n(" ^ space_implode "; " (map tool_time_string xs) ^ ")");
blanchet@41038
   154
      in
wenzelm@59184
   155
        (true, (name, if mode = Auto_Try then [message] else (writeln message; [])))
blanchet@54291
   156
      end)
blanchet@55179
   157
  end;
blanchet@39331
   158
blanchet@55181
   159
fun try0 timeout_opt = fst oo generic_try0 Normal timeout_opt;
blanchet@38942
   160
blanchet@46641
   161
fun try0_trans quad =
wenzelm@60190
   162
  Toplevel.keep_proof
wenzelm@60190
   163
    (ignore o generic_try0 Normal (SOME default_timeout) quad o Toplevel.proof_of);
blanchet@41999
   164
blanchet@55179
   165
fun merge_attrs (s1, i1, e1, d1) (s2, i2, e2, d2) = (s1 @ s2, i1 @ i2, e1 @ e2, d1 @ d2);
blanchet@41999
   166
blanchet@41999
   167
fun string_of_xthm (xref, args) =
blanchet@41999
   168
  Facts.string_of_ref xref ^
wenzelm@61877
   169
  implode (map (enclose "[" "]" o Pretty.unformatted_string_of o Token.pretty_src @{context}) args);
blanchet@41999
   170
blanchet@41999
   171
val parse_fact_refs =
wenzelm@62969
   172
  Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) (Parse.thm >> string_of_xthm));
blanchet@55179
   173
blanchet@41999
   174
val parse_attr =
blanchet@55179
   175
  Args.$$$ "simp" |-- Args.colon |-- parse_fact_refs >> (fn ss => (ss, [], [], []))
blanchet@55179
   176
  || Args.$$$ "intro" |-- Args.colon |-- parse_fact_refs >> (fn is => ([], is, [], []))
blanchet@55179
   177
  || Args.$$$ "elim" |-- Args.colon |-- parse_fact_refs >> (fn es => ([], [], es, []))
blanchet@55179
   178
  || Args.$$$ "dest" |-- Args.colon |-- parse_fact_refs >> (fn ds => ([], [], [], ds));
blanchet@55179
   179
blanchet@41999
   180
fun parse_attrs x =
blanchet@55179
   181
  (Args.parens parse_attrs
blanchet@55179
   182
   || Scan.repeat parse_attr >> (fn quad => fold merge_attrs quad ([], [], [], []))) x;
blanchet@41999
   183
blanchet@38942
   184
val _ =
wenzelm@59936
   185
  Outer_Syntax.command @{command_keyword try0} "try a combination of proof methods"
blanchet@55179
   186
    (Scan.optional parse_attrs ([], [], [], []) #>> try0_trans);
blanchet@38942
   187
blanchet@55181
   188
fun try_try0 auto = generic_try0 (if auto then Auto_Try else Try) NONE ([], [], [], []);
blanchet@39331
   189
wenzelm@56467
   190
val _ = Try.tool_setup (try0N, (30, @{system_option auto_methods}, try_try0));
blanchet@39331
   191
blanchet@38942
   192
end;