1 (* Title: HOL/Tools/Sledgehammer/sledgehammer_run.ML |
|
2 Author: Fabian Immler, TU Muenchen |
|
3 Author: Makarius |
|
4 Author: Jasmin Blanchette, TU Muenchen |
|
5 |
|
6 Sledgehammer's heart. |
|
7 *) |
|
8 |
|
9 signature SLEDGEHAMMER_RUN = |
|
10 sig |
|
11 type fact = Sledgehammer_Fact.fact |
|
12 type fact_override = Sledgehammer_Fact.fact_override |
|
13 type minimize_command = Sledgehammer_Reconstructor.minimize_command |
|
14 type mode = Sledgehammer_Prover.mode |
|
15 type params = Sledgehammer_Prover.params |
|
16 |
|
17 val someN : string |
|
18 val noneN : string |
|
19 val timeoutN : string |
|
20 val unknownN : string |
|
21 val string_of_factss : (string * fact list) list -> string |
|
22 val run_sledgehammer : params -> mode -> (string -> unit) option -> int -> fact_override -> |
|
23 ((string * string list) list -> string -> minimize_command) -> Proof.state -> |
|
24 bool * (string * Proof.state) |
|
25 end; |
|
26 |
|
27 structure Sledgehammer_Run : SLEDGEHAMMER_RUN = |
|
28 struct |
|
29 |
|
30 open ATP_Util |
|
31 open ATP_Problem_Generate |
|
32 open ATP_Proof |
|
33 open ATP_Proof_Reconstruct |
|
34 open Sledgehammer_Util |
|
35 open Sledgehammer_Fact |
|
36 open Sledgehammer_Prover |
|
37 open Sledgehammer_Minimize |
|
38 open Sledgehammer_MaSh |
|
39 |
|
40 val someN = "some" |
|
41 val noneN = "none" |
|
42 val timeoutN = "timeout" |
|
43 val unknownN = "unknown" |
|
44 |
|
45 val ordered_outcome_codes = [someN, unknownN, timeoutN, noneN] |
|
46 |
|
47 fun max_outcome_code codes = |
|
48 NONE |
|
49 |> fold (fn candidate => |
|
50 fn accum as SOME _ => accum |
|
51 | NONE => if member (op =) codes candidate then SOME candidate |
|
52 else NONE) |
|
53 ordered_outcome_codes |
|
54 |> the_default unknownN |
|
55 |
|
56 fun prover_description ctxt ({verbose, blocking, ...} : params) name num_facts i |
|
57 n goal = |
|
58 (quote name, |
|
59 (if verbose then |
|
60 " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts |
|
61 else |
|
62 "") ^ |
|
63 " on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^ |
|
64 (if blocking then "." |
|
65 else "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)))) |
|
66 |
|
67 fun launch_prover (params as {debug, verbose, spy, blocking, max_facts, timeout, expect, ...}) mode |
|
68 output_result minimize_command only learn |
|
69 {comment, state, goal, subgoal, subgoal_count, factss as (_, facts) :: _} name = |
|
70 let |
|
71 val ctxt = Proof.context_of state |
|
72 |
|
73 val hard_timeout = time_mult 3.0 timeout |
|
74 val _ = spying spy (fn () => (state, subgoal, name, "Launched")); |
|
75 val birth_time = Time.now () |
|
76 val death_time = Time.+ (birth_time, hard_timeout) |
|
77 val max_facts = max_facts |> the_default (default_max_facts_of_prover ctxt name) |
|
78 val num_facts = length facts |> not only ? Integer.min max_facts |
|
79 |
|
80 fun desc () = prover_description ctxt params name num_facts subgoal subgoal_count goal |
|
81 |
|
82 val problem = |
|
83 {comment = comment, state = state, goal = goal, subgoal = subgoal, |
|
84 subgoal_count = subgoal_count, |
|
85 factss = factss |
|
86 |> map (apsnd ((not (is_ho_atp ctxt name) |
|
87 ? filter_out (fn ((_, (_, Induction)), _) => true |
|
88 | _ => false)) |
|
89 #> take num_facts))} |
|
90 |
|
91 fun print_used_facts used_facts used_from = |
|
92 tag_list 1 used_from |
|
93 |> map (fn (j, fact) => fact |> apsnd (K j)) |
|
94 |> filter_used_facts false used_facts |
|
95 |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j) |
|
96 |> commas |
|
97 |> enclose ("Fact" ^ plural_s (length facts) ^ " in " ^ quote name ^ |
|
98 " proof (of " ^ string_of_int (length facts) ^ "): ") "." |
|
99 |> Output.urgent_message |
|
100 |
|
101 fun spying_str_of_res ({outcome = NONE, used_facts, used_from, ...} : prover_result) = |
|
102 let |
|
103 val num_used_facts = length used_facts |
|
104 |
|
105 fun find_indices facts = |
|
106 tag_list 1 facts |
|
107 |> map (fn (j, fact) => fact |> apsnd (K j)) |
|
108 |> filter_used_facts false used_facts |
|
109 |> distinct (eq_fst (op =)) |
|
110 |> map (prefix "@" o string_of_int o snd) |
|
111 |
|
112 fun filter_info (fact_filter, facts) = |
|
113 let |
|
114 val indices = find_indices facts |
|
115 (* "Int.max" is there for robustness -- it shouldn't be necessary *) |
|
116 val unknowns = replicate (Int.max (0, num_used_facts - length indices)) "?" |
|
117 in |
|
118 (commas (indices @ unknowns), fact_filter) |
|
119 end |
|
120 |
|
121 val filter_infos = |
|
122 map filter_info (("actual", used_from) :: factss) |
|
123 |> AList.group (op =) |
|
124 |> map (fn (indices, fact_filters) => commas fact_filters ^ ": " ^ indices) |
|
125 in |
|
126 "Success: Found proof with " ^ string_of_int num_used_facts ^ |
|
127 " of " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts ^ |
|
128 (if num_used_facts = 0 then "" else ": " ^ commas filter_infos) |
|
129 end |
|
130 | spying_str_of_res {outcome = SOME failure, ...} = |
|
131 "Failure: " ^ string_of_atp_failure failure |
|
132 |
|
133 fun really_go () = |
|
134 problem |
|
135 |> get_minimizing_prover ctxt mode learn name params minimize_command |
|
136 |> verbose |
|
137 ? tap (fn {outcome = NONE, used_facts as _ :: _, used_from, ...} => |
|
138 print_used_facts used_facts used_from |
|
139 | _ => ()) |
|
140 |> spy |
|
141 ? tap (fn res => spying spy (fn () => (state, subgoal, name, spying_str_of_res res))) |
|
142 |> (fn {outcome, preplay, message, message_tail, ...} => |
|
143 (if outcome = SOME ATP_Proof.TimedOut then timeoutN |
|
144 else if is_some outcome then noneN |
|
145 else someN, fn () => message (Lazy.force preplay) ^ message_tail)) |
|
146 |
|
147 fun go () = |
|
148 let |
|
149 val (outcome_code, message) = |
|
150 if debug then |
|
151 really_go () |
|
152 else |
|
153 (really_go () |
|
154 handle ERROR msg => (unknownN, fn () => "Error: " ^ msg ^ "\n") |
|
155 | exn => |
|
156 if Exn.is_interrupt exn then |
|
157 reraise exn |
|
158 else |
|
159 (unknownN, fn () => "Internal error:\n" ^ |
|
160 ML_Compiler.exn_message exn ^ "\n")) |
|
161 val _ = |
|
162 (* The "expect" argument is deliberately ignored if the prover is |
|
163 missing so that the "Metis_Examples" can be processed on any |
|
164 machine. *) |
|
165 if expect = "" orelse outcome_code = expect orelse |
|
166 not (is_prover_installed ctxt name) then |
|
167 () |
|
168 else if blocking then |
|
169 error ("Unexpected outcome: " ^ quote outcome_code ^ ".") |
|
170 else |
|
171 warning ("Unexpected outcome: " ^ quote outcome_code ^ "."); |
|
172 in (outcome_code, message) end |
|
173 in |
|
174 if mode = Auto_Try then |
|
175 let val (outcome_code, message) = TimeLimit.timeLimit timeout go () in |
|
176 (outcome_code, |
|
177 state |
|
178 |> outcome_code = someN |
|
179 ? Proof.goal_message (fn () => |
|
180 Pretty.mark Markup.information (Pretty.str (message ())))) |
|
181 end |
|
182 else if blocking then |
|
183 let |
|
184 val (outcome_code, message) = TimeLimit.timeLimit hard_timeout go () |
|
185 val outcome = |
|
186 if outcome_code = someN orelse mode = Normal then |
|
187 quote name ^ ": " ^ message () |
|
188 else "" |
|
189 val _ = |
|
190 if outcome <> "" andalso is_some output_result then |
|
191 the output_result outcome |
|
192 else |
|
193 outcome |
|
194 |> Async_Manager.break_into_chunks |
|
195 |> List.app Output.urgent_message |
|
196 in (outcome_code, state) end |
|
197 else |
|
198 (Async_Manager.thread SledgehammerN birth_time death_time (desc ()) |
|
199 ((fn (outcome_code, message) => |
|
200 (verbose orelse outcome_code = someN, |
|
201 message ())) o go); |
|
202 (unknownN, state)) |
|
203 end |
|
204 |
|
205 val auto_try_max_facts_divisor = 2 (* FUDGE *) |
|
206 |
|
207 fun string_of_facts facts = |
|
208 "Including " ^ string_of_int (length facts) ^ |
|
209 " relevant fact" ^ plural_s (length facts) ^ ":\n" ^ |
|
210 (facts |> map (fst o fst) |> space_implode " ") ^ "." |
|
211 |
|
212 fun string_of_factss factss = |
|
213 if forall (null o snd) factss then |
|
214 "Found no relevant facts." |
|
215 else case factss of |
|
216 [(_, facts)] => string_of_facts facts |
|
217 | _ => |
|
218 factss |
|
219 |> map (fn (filter, facts) => quote filter ^ ": " ^ string_of_facts facts) |
|
220 |> space_implode "\n\n" |
|
221 |
|
222 fun run_sledgehammer (params as {debug, verbose, spy, blocking, provers, max_facts, ...}) mode |
|
223 output_result i (fact_override as {only, ...}) minimize_command state = |
|
224 if null provers then |
|
225 error "No prover is set." |
|
226 else case subgoal_count state of |
|
227 0 => |
|
228 ((if blocking then error else Output.urgent_message) "No subgoal!"; (false, (noneN, state))) |
|
229 | n => |
|
230 let |
|
231 val _ = Proof.assert_backward state |
|
232 val print = |
|
233 if mode = Normal andalso is_none output_result then Output.urgent_message else K () |
|
234 val state = state |> Proof.map_context (Config.put SMT_Config.verbose debug) |
|
235 val ctxt = Proof.context_of state |
|
236 val {facts = chained, goal, ...} = Proof.goal state |
|
237 val (_, hyp_ts, concl_t) = strip_subgoal goal i ctxt |
|
238 val ho_atp = exists (is_ho_atp ctxt) provers |
|
239 val reserved = reserved_isar_keyword_table () |
|
240 val css = clasimpset_rule_table_of ctxt |
|
241 val all_facts = |
|
242 nearly_all_facts ctxt ho_atp fact_override reserved css chained hyp_ts |
|
243 concl_t |
|
244 val _ = () |> not blocking ? kill_provers |
|
245 val _ = case find_first (not o is_prover_supported ctxt) provers of |
|
246 SOME name => error ("No such prover: " ^ name ^ ".") |
|
247 | NONE => () |
|
248 val _ = print "Sledgehammering..." |
|
249 val _ = spying spy (fn () => (state, i, "***", "Starting " ^ @{make_string} mode ^ " mode")) |
|
250 |
|
251 val spying_str_of_factss = |
|
252 commas o map (fn (filter, facts) => filter ^ ": " ^ string_of_int (length facts)) |
|
253 |
|
254 fun get_factss provers = |
|
255 let |
|
256 val max_max_facts = |
|
257 case max_facts of |
|
258 SOME n => n |
|
259 | NONE => |
|
260 0 |> fold (Integer.max o default_max_facts_of_prover ctxt) provers |
|
261 |> mode = Auto_Try ? (fn n => n div auto_try_max_facts_divisor) |
|
262 val _ = spying spy (fn () => (state, i, "All", |
|
263 "Filtering " ^ string_of_int (length all_facts) ^ " facts")); |
|
264 in |
|
265 all_facts |
|
266 |> relevant_facts ctxt params (hd provers) max_max_facts fact_override hyp_ts concl_t |
|
267 |> tap (fn factss => if verbose then print (string_of_factss factss) else ()) |
|
268 |> spy ? tap (fn factss => spying spy (fn () => |
|
269 (state, i, "All", "Selected facts: " ^ spying_str_of_factss factss))) |
|
270 end |
|
271 |
|
272 fun launch_provers state = |
|
273 let |
|
274 val factss = get_factss provers |
|
275 val problem = |
|
276 {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n, |
|
277 factss = factss} |
|
278 val learn = mash_learn_proof ctxt params (prop_of goal) all_facts |
|
279 val launch = launch_prover params mode output_result minimize_command only learn |
|
280 in |
|
281 if mode = Auto_Try then |
|
282 (unknownN, state) |
|
283 |> fold (fn prover => fn accum as (outcome_code, _) => |
|
284 if outcome_code = someN then accum |
|
285 else launch problem prover) |
|
286 provers |
|
287 else |
|
288 provers |
|
289 |> (if blocking then Par_List.map else map) (launch problem #> fst) |
|
290 |> max_outcome_code |> rpair state |
|
291 end |
|
292 |
|
293 fun maybe f (accum as (outcome_code, _)) = |
|
294 accum |> (mode = Normal orelse outcome_code <> someN) ? f |
|
295 in |
|
296 (if blocking then launch_provers state |
|
297 else (Future.fork (tap (fn () => launch_provers state)); (unknownN, state))) |
|
298 handle TimeLimit.TimeOut => (print "Sledgehammer ran out of time."; (unknownN, state)) |
|
299 end |
|
300 |> `(fn (outcome_code, _) => outcome_code = someN) |
|
301 |
|
302 end; |
|