|
1 (* Title: mirabelle.ML |
|
2 Author: Jasmin Blanchette and Sascha Boehme |
|
3 *) |
|
4 |
|
5 signature MIRABELLE = |
|
6 sig |
|
7 type action |
|
8 type settings |
|
9 val register : string -> action -> theory -> theory |
|
10 val invoke : string -> settings -> theory -> theory |
|
11 |
|
12 val timeout : int Config.T |
|
13 val verbose : bool Config.T |
|
14 val start_line : int Config.T |
|
15 val end_line : int Config.T |
|
16 val set_logfile : string -> theory -> theory |
|
17 |
|
18 val setup : theory -> theory |
|
19 |
|
20 val step_hook : Toplevel.transition -> Toplevel.state -> Toplevel.state -> |
|
21 unit |
|
22 |
|
23 val goal_thm_of : Proof.state -> thm |
|
24 val can_apply : (Proof.context -> int -> tactic) -> Proof.state -> bool |
|
25 val theorems_in_proof_term : Thm.thm -> Thm.thm list |
|
26 val theorems_of_sucessful_proof : Toplevel.state -> Thm.thm list |
|
27 val get_setting : settings -> string * string -> string |
|
28 val get_int_setting : settings -> string * int -> int |
|
29 |
|
30 (* FIXME val refute_action : action *) |
|
31 val quickcheck_action : action |
|
32 val arith_action : action |
|
33 val sledgehammer_action : action |
|
34 val metis_action : action |
|
35 end |
|
36 |
|
37 |
|
38 |
|
39 structure Mirabelle (*: MIRABELLE*) = |
|
40 struct |
|
41 |
|
42 (* Mirabelle core *) |
|
43 |
|
44 type settings = (string * string) list |
|
45 type invoked = {pre: Proof.state, post: Toplevel.state option} -> string option |
|
46 type action = settings -> invoked |
|
47 |
|
48 structure Registered = TheoryDataFun |
|
49 ( |
|
50 type T = action Symtab.table |
|
51 val empty = Symtab.empty |
|
52 val copy = I |
|
53 val extend = I |
|
54 fun merge _ = Symtab.merge (K true) |
|
55 ) |
|
56 |
|
57 fun register name act = Registered.map (Symtab.update_new (name, act)) |
|
58 |
|
59 |
|
60 structure Invoked = TheoryDataFun |
|
61 ( |
|
62 type T = (string * invoked) list |
|
63 val empty = [] |
|
64 val copy = I |
|
65 val extend = I |
|
66 fun merge _ = Library.merge (K true) |
|
67 ) |
|
68 |
|
69 fun invoke name sts thy = |
|
70 let |
|
71 val act = |
|
72 (case Symtab.lookup (Registered.get thy) name of |
|
73 SOME act => act |
|
74 | NONE => error ("The invoked action " ^ quote name ^ |
|
75 " is not registered.")) |
|
76 in Invoked.map (cons (name, act sts)) thy end |
|
77 |
|
78 val (logfile, setup1) = Attrib.config_string "mirabelle_logfile" "" |
|
79 val (timeout, setup2) = Attrib.config_int "mirabelle_timeout" 30 |
|
80 val (verbose, setup3) = Attrib.config_bool "mirabelle_verbose" true |
|
81 val (start_line, setup4) = Attrib.config_int "mirabelle_start_line" 0 |
|
82 val (end_line, setup5) = Attrib.config_int "mirabelle_end_line" ~1 |
|
83 |
|
84 val setup_config = setup1 #> setup2 #> setup3 #> setup4 #> setup5 |
|
85 |
|
86 fun set_logfile name = |
|
87 let val _ = File.write (Path.explode name) "" (* erase file content *) |
|
88 in Config.put_thy logfile name end |
|
89 |
|
90 local |
|
91 |
|
92 fun log thy s = |
|
93 let fun append_to n = if n = "" then K () else File.append (Path.explode n) |
|
94 in append_to (Config.get_thy thy logfile) (s ^ "\n") end |
|
95 (* FIXME: with multithreading and parallel proofs enabled, we might need to |
|
96 encapsulate this inside a critical section *) |
|
97 |
|
98 fun verbose_msg verbose msg = if verbose then SOME msg else NONE |
|
99 |
|
100 fun with_time_limit (verb, secs) f x = TimeLimit.timeLimit secs f x |
|
101 handle TimeLimit.TimeOut => verbose_msg verb "time out" |
|
102 | ERROR msg => verbose_msg verb ("error: " ^ msg) |
|
103 |
|
104 fun capture_exns verb f x = |
|
105 (case try f x of NONE => verbose_msg verb "exception" | SOME msg => msg) |
|
106 |
|
107 fun apply_action (c as (verb, _)) st (name, invoked) = |
|
108 Option.map (pair name) (capture_exns verb (with_time_limit c invoked) st) |
|
109 |
|
110 fun in_range _ _ NONE = true |
|
111 | in_range l r (SOME i) = (l <= i andalso (r < 0 orelse i <= r)) |
|
112 |
|
113 fun only_within_range thy pos f x = |
|
114 let val l = Config.get_thy thy start_line and r = Config.get_thy thy end_line |
|
115 in if in_range l r (Position.line_of pos) then f x else [] end |
|
116 |
|
117 fun pretty_print verbose pos name msgs = |
|
118 let |
|
119 val file = the_default "unknown file" (Position.file_of pos) |
|
120 |
|
121 val str0 = string_of_int o the_default 0 |
|
122 val loc = str0 (Position.line_of pos) ^ ":" ^ str0 (Position.column_of pos) |
|
123 |
|
124 val full_loc = if verbose then file ^ ":" ^ loc else "at " ^ loc |
|
125 val head = full_loc ^ " (" ^ name ^ "):" |
|
126 |
|
127 fun pretty_msg (name, msg) = Pretty.block (map Pretty.str [name, ": ", msg]) |
|
128 in |
|
129 Pretty.string_of (Pretty.big_list head (map pretty_msg msgs)) |
|
130 end |
|
131 |
|
132 in |
|
133 |
|
134 fun basic_hook tr pre post = |
|
135 let |
|
136 val thy = Proof.theory_of pre |
|
137 val pos = Toplevel.pos_of tr |
|
138 val name = Toplevel.name_of tr |
|
139 val verb = Config.get_thy thy verbose |
|
140 val secs = Time.fromSeconds (Config.get_thy thy timeout) |
|
141 val st = {pre=pre, post=post} |
|
142 in |
|
143 Invoked.get thy |
|
144 |> only_within_range thy pos (map_filter (apply_action (verb, secs) st)) |
|
145 |> (fn [] => () | msgs => log thy (pretty_print verb pos name msgs)) |
|
146 end |
|
147 |
|
148 end |
|
149 |
|
150 fun step_hook tr pre post = |
|
151 (* FIXME: might require wrapping into "interruptible" *) |
|
152 if can (Proof.assert_backward o Toplevel.proof_of) pre andalso |
|
153 not (member (op =) ["disable_pr", "enable_pr"] (Toplevel.name_of tr)) |
|
154 then basic_hook tr (Toplevel.proof_of pre) (SOME post) |
|
155 else () (* FIXME: add theory_hook here *) |
|
156 |
|
157 |
|
158 |
|
159 (* Mirabelle utility functions *) |
|
160 |
|
161 val goal_thm_of = snd o snd o Proof.get_goal |
|
162 |
|
163 fun can_apply tac st = |
|
164 let val (ctxt, (facts, goal)) = Proof.get_goal st |
|
165 in |
|
166 (case Seq.pull (HEADGOAL (Method.insert_tac facts THEN' tac ctxt) goal) of |
|
167 SOME (thm, _) => true |
|
168 | NONE => false) |
|
169 end |
|
170 |
|
171 local |
|
172 |
|
173 fun fold_body_thms f = |
|
174 let |
|
175 fun app n (PBody {thms, ...}) = thms |> fold (fn (i, (name, prop, body)) => |
|
176 fn (x, seen) => |
|
177 if Inttab.defined seen i then (x, seen) |
|
178 else |
|
179 let |
|
180 val body' = Future.join body |
|
181 val (x', seen') = app (n + (if name = "" then 0 else 1)) body' |
|
182 (x, Inttab.update (i, ()) seen) |
|
183 in (x' |> n = 0 ? f (name, prop, body'), seen') end) |
|
184 in fn bodies => fn x => #1 (fold (app 0) bodies (x, Inttab.empty)) end |
|
185 |
|
186 in |
|
187 |
|
188 fun theorems_in_proof_term thm = |
|
189 let |
|
190 val all_thms = PureThy.all_thms_of (Thm.theory_of_thm thm) |
|
191 fun collect (s, _, _) = if s <> "" then insert (op =) s else I |
|
192 fun member_of xs (x, y) = if member (op =) xs x then SOME y else NONE |
|
193 fun resolve_thms names = map_filter (member_of names) all_thms |
|
194 in |
|
195 resolve_thms (fold_body_thms collect [Thm.proof_body_of thm] []) |
|
196 end |
|
197 |
|
198 end |
|
199 |
|
200 fun theorems_of_sucessful_proof state = |
|
201 (case state of |
|
202 NONE => [] |
|
203 | SOME st => |
|
204 if not (Toplevel.is_proof st) then [] |
|
205 else theorems_in_proof_term (goal_thm_of (Toplevel.proof_of st))) |
|
206 |
|
207 fun get_setting settings (key, default) = |
|
208 the_default default (AList.lookup (op =) settings key) |
|
209 |
|
210 fun get_int_setting settings (key, default) = |
|
211 (case Option.map Int.fromString (AList.lookup (op =) settings key) of |
|
212 SOME (SOME i) => i |
|
213 | SOME NONE => error ("bad option: " ^ key) |
|
214 | NONE => default) |
|
215 |
|
216 |
|
217 |
|
218 (* Mirabelle actions *) |
|
219 |
|
220 (* FIXME |
|
221 fun refute_action settings {pre=st, ...} = |
|
222 let |
|
223 val params = [("minsize", "2") (*"maxsize", "2"*)] |
|
224 val subgoal = 0 |
|
225 val thy = Proof.theory_of st |
|
226 val thm = goal_thm_of st |
|
227 |
|
228 val _ = Refute.refute_subgoal thy parms thm subgoal |
|
229 in |
|
230 val writ_log = Substring.full (the (Symtab.lookup tab "writeln")) |
|
231 val warn_log = Substring.full (the (Symtab.lookup tab "warning")) |
|
232 |
|
233 val r = |
|
234 if Substring.isSubstring "model found" writ_log |
|
235 then |
|
236 if Substring.isSubstring "spurious" warn_log |
|
237 then SOME "potential counterexample" |
|
238 else SOME "real counterexample (bug?)" |
|
239 else |
|
240 if Substring.isSubstring "time limit" writ_log |
|
241 then SOME "no counterexample (time out)" |
|
242 else if Substring.isSubstring "Search terminated" writ_log |
|
243 then SOME "no counterexample (normal termination)" |
|
244 else SOME "no counterexample (unknown)" |
|
245 in r end |
|
246 *) |
|
247 |
|
248 fun quickcheck_action settings {pre=st, ...} = |
|
249 let |
|
250 val has_valid_key = member (op =) ["iterations", "size", "generator"] o fst |
|
251 val args = filter has_valid_key settings |
|
252 in |
|
253 (case Quickcheck.quickcheck args 1 st of |
|
254 NONE => SOME "no counterexample" |
|
255 | SOME _ => SOME "counterexample found") |
|
256 end |
|
257 |
|
258 |
|
259 fun arith_action _ {pre=st, ...} = |
|
260 if can_apply Arith_Data.arith_tac st |
|
261 then SOME "succeeded" |
|
262 else NONE |
|
263 |
|
264 |
|
265 fun sledgehammer_action settings {pre=st, ...} = |
|
266 let |
|
267 val prover_name = hd (space_explode " " (AtpManager.get_atps ())) |
|
268 val thy = Proof.theory_of st |
|
269 |
|
270 val prover = the (AtpManager.get_prover prover_name thy) |
|
271 val timeout = AtpManager.get_timeout () |
|
272 |
|
273 val (success, message) = |
|
274 let |
|
275 val (success, message, _, _, _) = |
|
276 prover timeout NONE NONE prover_name 1 (Proof.get_goal st) |
|
277 in (success, message) end |
|
278 handle ResHolClause.TOO_TRIVIAL => (true, "trivial") |
|
279 | ERROR msg => (false, "error: " ^ msg) |
|
280 in |
|
281 if success |
|
282 then SOME ("success (" ^ prover_name ^ ": " ^ message ^ ")") |
|
283 else NONE |
|
284 end |
|
285 |
|
286 |
|
287 fun metis_action settings {pre, post} = |
|
288 let |
|
289 val thms = theorems_of_sucessful_proof post |
|
290 val names = map Thm.get_name thms |
|
291 |
|
292 val facts = Facts.props (ProofContext.facts_of (Proof.context_of pre)) |
|
293 |
|
294 fun metis ctxt = MetisTools.metis_tac ctxt (thms @ facts) |
|
295 in |
|
296 (if can_apply metis pre then "succeeded" else "failed") |
|
297 |> suffix (" (" ^ commas names ^ ")") |
|
298 |> SOME |
|
299 end |
|
300 |
|
301 |
|
302 |
|
303 (* Mirabelle setup *) |
|
304 |
|
305 val setup = |
|
306 setup_config #> |
|
307 (* FIXME register "refute" refute_action #> *) |
|
308 register "quickcheck" quickcheck_action #> |
|
309 register "arith" arith_action #> |
|
310 register "sledgehammer" sledgehammer_action #> |
|
311 register "metis" metis_action (* #> FIXME: |
|
312 Context.theory_map (Specification.add_theorem_hook theorem_hook) *) |
|
313 |
|
314 end |
|
315 |
|
316 val _ = Toplevel.add_hook Mirabelle.step_hook |
|
317 |
|
318 (* no multithreading, no parallel proofs *) |
|
319 val _ = Multithreading.max_threads := 1 |
|
320 val _ = Goal.parallel_proofs := 0 |