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