1(*  Title:      HOL/Tools/try0.ML
2    Author:     Jasmin Blanchette, TU Muenchen
3
4Try a combination of proof methods.
5*)
6
7signature TRY0 =
8sig
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
15end;
16
17structure Try0 : TRY0 =
18struct
19
20val try0N = "try0";
21val noneN = "none";
22
23datatype mode = Auto_Try | Try | Normal;
24
25val default_timeout = seconds 5.0;
26
27fun 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
36fun 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
44fun 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
51fun 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
58fun 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
63fun attrs_text (sx, ix, ex, dx) (ss, is, es, ds) =
64  "" |> fold add_attr_text [(sx, ss), (ix, is), (ex, es), (dx, ds)];
65
66fun 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
79val full_attrs = (SOME "simp", SOME "intro", SOME "elim", SOME "dest");
80val clas_attrs = (NONE, SOME "intro", SOME "elim", SOME "dest");
81val simp_attrs = (SOME "add", NONE, NONE, NONE);
82val metis_attrs = (SOME "", SOME "", SOME "", SOME "");
83val no_attrs = (NONE, NONE, NONE, NONE);
84
85(* name * ((all_goals, run_if_auto_try), (simp, intro, elim, dest) *)
86val 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
101val apply_methods = map apply_named_method named_methods;
102
103fun time_string ms = string_of_int ms ^ " ms";
104fun 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. *)
108fun 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
121fun 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
165fun try0 timeout_opt = fst oo generic_try0 Normal timeout_opt;
166
167fun try0_trans quad =
168  Toplevel.keep_proof
169    (ignore o generic_try0 Normal (SOME default_timeout) quad o Toplevel.proof_of);
170
171fun merge_attrs (s1, i1, e1, d1) (s2, i2, e2, d2) = (s1 @ s2, i1 @ i2, e1 @ e2, d1 @ d2);
172
173fun 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
177val parse_fact_refs =
178  Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) (Parse.thm >> string_of_xthm));
179
180val 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
186fun parse_attrs x =
187  (Args.parens parse_attrs
188   || Scan.repeat parse_attr >> (fn quad => fold merge_attrs quad ([], [], [], []))) x;
189
190val _ =
191  Outer_Syntax.command \<^command_keyword>\<open>try0\<close> "try a combination of proof methods"
192    (Scan.optional parse_attrs ([], [], [], []) #>> try0_trans);
193
194fun try_try0 auto = generic_try0 (if auto then Auto_Try else Try) NONE ([], [], [], []);
195
196val _ = Try.tool_setup (try0N, (30, \<^system_option>\<open>auto_methods\<close>, try_try0));
197
198end;
199