1(*  Title:      HOL/Tools/Sledgehammer/sledgehammer.ML
2    Author:     Fabian Immler, TU Muenchen
3    Author:     Makarius
4    Author:     Jasmin Blanchette, TU Muenchen
5
6Sledgehammer's heart.
7*)
8
9signature SLEDGEHAMMER =
10sig
11  type stature = ATP_Problem_Generate.stature
12  type fact = Sledgehammer_Fact.fact
13  type fact_override = Sledgehammer_Fact.fact_override
14  type proof_method = Sledgehammer_Proof_Methods.proof_method
15  type play_outcome = Sledgehammer_Proof_Methods.play_outcome
16  type mode = Sledgehammer_Prover.mode
17  type params = Sledgehammer_Prover.params
18
19  val someN : string
20  val noneN : string
21  val timeoutN : string
22  val unknownN : string
23
24  val play_one_line_proof : bool -> Time.time -> (string * stature) list -> Proof.state -> int ->
25    proof_method * proof_method list list -> (string * stature) list * (proof_method * play_outcome)
26  val string_of_factss : (string * fact list) list -> string
27  val run_sledgehammer : params -> mode -> (string -> unit) option -> int -> fact_override ->
28    Proof.state -> bool * (string * string list)
29end;
30
31structure Sledgehammer : SLEDGEHAMMER =
32struct
33
34open ATP_Util
35open ATP_Proof
36open ATP_Problem_Generate
37open Sledgehammer_Util
38open Sledgehammer_Fact
39open Sledgehammer_Proof_Methods
40open Sledgehammer_Isar_Proof
41open Sledgehammer_Isar_Preplay
42open Sledgehammer_Isar_Minimize
43open Sledgehammer_Prover
44open Sledgehammer_Prover_ATP
45open Sledgehammer_Prover_Minimize
46open Sledgehammer_MaSh
47
48val someN = "some"
49val noneN = "none"
50val timeoutN = "timeout"
51val unknownN = "unknown"
52
53val ordered_outcome_codes = [someN, unknownN, timeoutN, noneN]
54
55fun max_outcome_code codes =
56  NONE
57  |> fold (fn candidate =>
58      fn accum as SOME _ => accum
59       | NONE => if member (op =) codes candidate then SOME candidate else NONE)
60    ordered_outcome_codes
61  |> the_default unknownN
62
63fun is_metis_method (Metis_Method _) = true
64  | is_metis_method _ = false
65
66fun play_one_line_proof minimize timeout used_facts state i (preferred_meth, methss) =
67  (if timeout = Time.zeroTime then
68     (used_facts, (preferred_meth, Play_Timed_Out Time.zeroTime))
69   else
70     let
71       val ctxt = Proof.context_of state
72
73       val fact_names = map fst used_facts
74       val {facts = chained, goal, ...} = Proof.goal state
75       val goal_t = Logic.get_goal (Thm.prop_of goal) i
76
77       fun try_methss [] [] = (used_facts, (preferred_meth, Play_Timed_Out Time.zeroTime))
78         | try_methss ress [] =
79           (used_facts,
80            (case AList.lookup (op =) ress preferred_meth of
81              SOME play => (preferred_meth, play)
82            | NONE => hd (sort (play_outcome_ord o apply2 snd) (rev ress))))
83         | try_methss ress (meths :: methss) =
84           let
85             fun mk_step fact_names meths =
86               Prove ([], [], ("", 0), goal_t, [], ([], fact_names), meths, "")
87           in
88             (case preplay_isar_step ctxt chained timeout [] (mk_step fact_names meths) of
89               (res as (meth, Played time)) :: _ =>
90               (* if a fact is needed by an ATP, it will be needed by "metis" *)
91               if not minimize orelse is_metis_method meth then
92                 (used_facts, res)
93               else
94                 let
95                   val (time', used_names') =
96                     minimized_isar_step ctxt chained time (mk_step fact_names [meth])
97                     ||> (facts_of_isar_step #> snd)
98                   val used_facts' = filter (member (op =) used_names' o fst) used_facts
99                 in
100                   (used_facts', (meth, Played time'))
101                 end
102             | ress' => try_methss (ress' @ ress) methss)
103           end
104     in
105       try_methss [] methss
106     end)
107  |> (fn (used_facts, (meth, play)) =>
108        (used_facts |> not (proof_method_distinguishes_chained_and_direct meth)
109           ? filter_out (fn (_, (sc, _)) => sc = Chained),
110         (meth, play)))
111
112fun launch_prover (params as {debug, verbose, spy, max_facts, minimize, timeout, preplay_timeout,
113      expect, ...}) mode writeln_result only learn
114    {comment, state, goal, subgoal, subgoal_count, factss as (_, facts) :: _, found_proof} name =
115  let
116    val ctxt = Proof.context_of state
117
118    val hard_timeout = time_mult 5.0 timeout
119    val _ = spying spy (fn () => (state, subgoal, name, "Launched"));
120    val max_facts = max_facts |> the_default (default_max_facts_of_prover ctxt name)
121    val num_facts = length facts |> not only ? Integer.min max_facts
122
123    val problem =
124      {comment = comment, state = state, goal = goal, subgoal = subgoal,
125       subgoal_count = subgoal_count,
126       factss = factss
127       |> map (apsnd ((not (is_ho_atp ctxt name)
128           ? filter_out (fn ((_, (_, Induction)), _) => true | _ => false))
129         #> take num_facts)),
130       found_proof = found_proof}
131
132    fun print_used_facts used_facts used_from =
133      tag_list 1 used_from
134      |> map (fn (j, fact) => fact |> apsnd (K j))
135      |> filter_used_facts false used_facts
136      |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j)
137      |> commas
138      |> prefix ("Fact" ^ plural_s (length facts) ^ " in " ^ quote name ^
139        " proof (of " ^ string_of_int (length facts) ^ "): ")
140      |> writeln
141
142    fun spying_str_of_res ({outcome = NONE, used_facts, used_from, ...} : prover_result) =
143        let
144          val num_used_facts = length used_facts
145
146          fun find_indices facts =
147            tag_list 1 facts
148            |> map (fn (j, fact) => fact |> apsnd (K j))
149            |> filter_used_facts false used_facts
150            |> distinct (eq_fst (op =))
151            |> map (prefix "@" o string_of_int o snd)
152
153          fun filter_info (fact_filter, facts) =
154            let
155              val indices = find_indices facts
156              (* "Int.max" is there for robustness -- it shouldn't be necessary *)
157              val unknowns = replicate (Int.max (0, num_used_facts - length indices)) "?"
158            in
159              (commas (indices @ unknowns), fact_filter)
160            end
161
162          val filter_infos =
163            map filter_info (("actual", used_from) :: factss)
164            |> AList.group (op =)
165            |> map (fn (indices, fact_filters) => commas fact_filters ^ ": " ^ indices)
166        in
167          "Success: Found proof with " ^ string_of_int num_used_facts ^ " of " ^
168          string_of_int num_facts ^ " fact" ^ plural_s num_facts ^
169          (if num_used_facts = 0 then "" else ": " ^ commas filter_infos)
170        end
171      | spying_str_of_res {outcome = SOME failure, ...} =
172        "Failure: " ^ string_of_atp_failure failure
173
174    fun really_go () =
175      problem
176      |> get_minimizing_prover ctxt mode learn name params
177      |> verbose ? tap (fn {outcome = NONE, used_facts as _ :: _, used_from, ...} =>
178          print_used_facts used_facts used_from
179        | _ => ())
180      |> spy ? tap (fn res => spying spy (fn () => (state, subgoal, name, spying_str_of_res res)))
181      |> (fn {outcome, used_facts, preferred_methss, message, ...} =>
182        (if outcome = SOME ATP_Proof.TimedOut then timeoutN
183         else if is_some outcome then noneN
184         else someN,
185         fn () => message (fn () => play_one_line_proof minimize preplay_timeout used_facts state
186           subgoal preferred_methss)))
187
188    fun go () =
189      let
190        val (outcome_code, message) =
191          if debug then
192            really_go ()
193          else
194            (really_go ()
195             handle
196               ERROR msg => (unknownN, fn () => "Error: " ^ msg ^ "\n")
197             | exn =>
198               if Exn.is_interrupt exn then Exn.reraise exn
199               else (unknownN, fn () => "Internal error:\n" ^ Runtime.exn_message exn ^ "\n"))
200
201        val _ =
202          (* The "expect" argument is deliberately ignored if the prover is
203             missing so that the "Metis_Examples" can be processed on any
204             machine. *)
205          if expect = "" orelse outcome_code = expect orelse
206             not (is_prover_installed ctxt name) then
207            ()
208          else
209            error ("Unexpected outcome: " ^ quote outcome_code)
210      in (outcome_code, message) end
211  in
212    if mode = Auto_Try then
213      let val (outcome_code, message) = Timeout.apply timeout go () in
214        (outcome_code, if outcome_code = someN then [message ()] else [])
215      end
216    else
217      let
218        val (outcome_code, message) = Timeout.apply hard_timeout go ()
219        val outcome =
220          if outcome_code = someN orelse mode = Normal then quote name ^ ": " ^ message () else ""
221        val _ =
222          if outcome <> "" andalso is_some writeln_result then the writeln_result outcome
223          else writeln outcome
224      in (outcome_code, []) end
225  end
226
227val auto_try_max_facts_divisor = 2 (* FUDGE *)
228
229fun string_of_facts facts =
230  "Including " ^ string_of_int (length facts) ^ " relevant fact" ^ plural_s (length facts) ^ ": " ^
231  (facts |> map (fst o fst) |> space_implode " ")
232
233fun string_of_factss factss =
234  if forall (null o snd) factss then
235    "Found no relevant facts"
236  else
237    cat_lines (map (fn (filter, facts) =>
238      (if filter = "" then "" else quote filter ^ ": ") ^ string_of_facts facts) factss)
239
240fun run_sledgehammer (params as {verbose, spy, provers, max_facts, ...}) mode writeln_result i
241    (fact_override as {only, ...}) state =
242  if null provers then
243    error "No prover is set"
244  else
245    (case subgoal_count state of
246      0 => (error "No subgoal!"; (false, (noneN, [])))
247    | n =>
248      let
249        val _ = Proof.assert_backward state
250        val print = if mode = Normal andalso is_none writeln_result then writeln else K ()
251
252        val found_proof =
253          if mode = Normal then
254            let val proof_found = Synchronized.var "proof_found" false in
255              fn () =>
256                if Synchronized.change_result proof_found (rpair true) then ()
257                else (writeln_result |> the_default writeln) "Proof found..."
258            end
259          else
260            I
261
262        val ctxt = Proof.context_of state
263        val keywords = Thy_Header.get_keywords' ctxt
264        val {facts = chained, goal, ...} = Proof.goal state
265        val (_, hyp_ts, concl_t) = strip_subgoal goal i ctxt
266        val ho_atp = exists (is_ho_atp ctxt) provers
267        val css = clasimpset_rule_table_of ctxt
268        val all_facts =
269          nearly_all_facts ctxt ho_atp fact_override keywords css chained hyp_ts concl_t
270        val _ =
271          (case find_first (not o is_prover_supported ctxt) provers of
272            SOME name => error ("No such prover: " ^ name)
273          | NONE => ())
274        val _ = print "Sledgehammering..."
275        val _ = spying spy (fn () => (state, i, "***", "Starting " ^ str_of_mode mode ^ " mode"))
276
277        val spying_str_of_factss =
278          commas o map (fn (filter, facts) => filter ^ ": " ^ string_of_int (length facts))
279
280        fun get_factss provers =
281          let
282            val max_max_facts =
283              (case max_facts of
284                SOME n => n
285              | NONE =>
286                0 |> fold (Integer.max o default_max_facts_of_prover ctxt) provers
287                  |> mode = Auto_Try ? (fn n => n div auto_try_max_facts_divisor))
288            val _ = spying spy (fn () => (state, i, "All",
289              "Filtering " ^ string_of_int (length all_facts) ^ " facts (MaSh algorithm: " ^
290              str_of_mash_algorithm (the_mash_algorithm ()) ^ ")"));
291          in
292            all_facts
293            |> relevant_facts ctxt params (hd provers) max_max_facts fact_override hyp_ts concl_t
294            |> tap (fn factss => if verbose then print (string_of_factss factss) else ())
295            |> spy ? tap (fn factss => spying spy (fn () =>
296              (state, i, "All", "Selected facts: " ^ spying_str_of_factss factss)))
297          end
298
299        fun launch_provers () =
300          let
301            val factss = get_factss provers
302            val problem =
303              {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n,
304               factss = factss, found_proof = found_proof}
305            val learn = mash_learn_proof ctxt params (Thm.prop_of goal)
306            val launch = launch_prover params mode writeln_result only learn
307          in
308            if mode = Auto_Try then
309              (unknownN, [])
310              |> fold (fn prover => fn accum as (outcome_code, _) =>
311                  if outcome_code = someN then accum else launch problem prover)
312                provers
313            else
314              (learn chained;
315               provers
316               |> Par_List.map (launch problem #> fst)
317               |> max_outcome_code |> rpair [])
318          end
319      in
320        launch_provers ()
321        handle Timeout.TIMEOUT _ =>
322          (print "Sledgehammer ran out of time"; (unknownN, []))
323      end
324      |> `(fn (outcome_code, _) => outcome_code = someN))
325
326end;
327