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