1 (* Title: HOL/Tools/SMT/z3_proof_parser.ML |
|
2 Author: Sascha Boehme, TU Muenchen |
|
3 |
|
4 Parser for Z3 proofs. |
|
5 *) |
|
6 |
|
7 signature Z3_PROOF_PARSER = |
|
8 sig |
|
9 (*proof rules*) |
|
10 datatype rule = True_Axiom | Asserted | Goal | Modus_Ponens | Reflexivity | |
|
11 Symmetry | Transitivity | Transitivity_Star | Monotonicity | Quant_Intro | |
|
12 Distributivity | And_Elim | Not_Or_Elim | Rewrite | Rewrite_Star | |
|
13 Pull_Quant | Pull_Quant_Star | Push_Quant | Elim_Unused_Vars | |
|
14 Dest_Eq_Res | Quant_Inst | Hypothesis | Lemma | Unit_Resolution | |
|
15 Iff_True | Iff_False | Commutativity | Def_Axiom | Intro_Def | Apply_Def | |
|
16 Iff_Oeq | Nnf_Pos | Nnf_Neg | Nnf_Star | Cnf_Star | Skolemize | |
|
17 Modus_Ponens_Oeq | Th_Lemma of string list |
|
18 val string_of_rule: rule -> string |
|
19 |
|
20 (*proof parser*) |
|
21 datatype proof_step = Proof_Step of { |
|
22 rule: rule, |
|
23 args: cterm list, |
|
24 prems: int list, |
|
25 prop: cterm } |
|
26 val parse: Proof.context -> typ Symtab.table -> term Symtab.table -> |
|
27 string list -> |
|
28 (int * cterm) list * (int * proof_step) list * string list * Proof.context |
|
29 end |
|
30 |
|
31 structure Z3_Proof_Parser: Z3_PROOF_PARSER = |
|
32 struct |
|
33 |
|
34 |
|
35 (* proof rules *) |
|
36 |
|
37 datatype rule = True_Axiom | Asserted | Goal | Modus_Ponens | Reflexivity | |
|
38 Symmetry | Transitivity | Transitivity_Star | Monotonicity | Quant_Intro | |
|
39 Distributivity | And_Elim | Not_Or_Elim | Rewrite | Rewrite_Star | |
|
40 Pull_Quant | Pull_Quant_Star | Push_Quant | Elim_Unused_Vars | Dest_Eq_Res | |
|
41 Quant_Inst | Hypothesis | Lemma | Unit_Resolution | Iff_True | Iff_False | |
|
42 Commutativity | Def_Axiom | Intro_Def | Apply_Def | Iff_Oeq | Nnf_Pos | |
|
43 Nnf_Neg | Nnf_Star | Cnf_Star | Skolemize | Modus_Ponens_Oeq | |
|
44 Th_Lemma of string list |
|
45 |
|
46 val rule_names = Symtab.make [ |
|
47 ("true-axiom", True_Axiom), |
|
48 ("asserted", Asserted), |
|
49 ("goal", Goal), |
|
50 ("mp", Modus_Ponens), |
|
51 ("refl", Reflexivity), |
|
52 ("symm", Symmetry), |
|
53 ("trans", Transitivity), |
|
54 ("trans*", Transitivity_Star), |
|
55 ("monotonicity", Monotonicity), |
|
56 ("quant-intro", Quant_Intro), |
|
57 ("distributivity", Distributivity), |
|
58 ("and-elim", And_Elim), |
|
59 ("not-or-elim", Not_Or_Elim), |
|
60 ("rewrite", Rewrite), |
|
61 ("rewrite*", Rewrite_Star), |
|
62 ("pull-quant", Pull_Quant), |
|
63 ("pull-quant*", Pull_Quant_Star), |
|
64 ("push-quant", Push_Quant), |
|
65 ("elim-unused", Elim_Unused_Vars), |
|
66 ("der", Dest_Eq_Res), |
|
67 ("quant-inst", Quant_Inst), |
|
68 ("hypothesis", Hypothesis), |
|
69 ("lemma", Lemma), |
|
70 ("unit-resolution", Unit_Resolution), |
|
71 ("iff-true", Iff_True), |
|
72 ("iff-false", Iff_False), |
|
73 ("commutativity", Commutativity), |
|
74 ("def-axiom", Def_Axiom), |
|
75 ("intro-def", Intro_Def), |
|
76 ("apply-def", Apply_Def), |
|
77 ("iff~", Iff_Oeq), |
|
78 ("nnf-pos", Nnf_Pos), |
|
79 ("nnf-neg", Nnf_Neg), |
|
80 ("nnf*", Nnf_Star), |
|
81 ("cnf*", Cnf_Star), |
|
82 ("sk", Skolemize), |
|
83 ("mp~", Modus_Ponens_Oeq), |
|
84 ("th-lemma", Th_Lemma [])] |
|
85 |
|
86 fun string_of_rule (Th_Lemma args) = space_implode " " ("th-lemma" :: args) |
|
87 | string_of_rule r = |
|
88 let fun eq_rule (s, r') = if r = r' then SOME s else NONE |
|
89 in the (Symtab.get_first eq_rule rule_names) end |
|
90 |
|
91 |
|
92 |
|
93 (* certified terms and variables *) |
|
94 |
|
95 val (var_prefix, decl_prefix) = ("v", "sk") |
|
96 (* |
|
97 "decl_prefix" is for skolem constants (represented by free variables), |
|
98 "var_prefix" is for pseudo-schematic variables (schematic with respect |
|
99 to the Z3 proof, but represented by free variables). |
|
100 |
|
101 Both prefixes must be distinct to avoid name interferences. |
|
102 More precisely, the naming of pseudo-schematic variables must be |
|
103 context-independent modulo the current proof context to be able to |
|
104 use fast inference kernel rules during proof reconstruction. |
|
105 *) |
|
106 |
|
107 val maxidx_of = #maxidx o Thm.rep_cterm |
|
108 |
|
109 fun mk_inst ctxt vars = |
|
110 let |
|
111 val max = fold (Integer.max o fst) vars 0 |
|
112 val ns = fst (Variable.variant_fixes (replicate (max + 1) var_prefix) ctxt) |
|
113 fun mk (i, v) = |
|
114 (v, SMT_Utils.certify ctxt (Free (nth ns i, #T (Thm.rep_cterm v)))) |
|
115 in map mk vars end |
|
116 |
|
117 fun close ctxt (ct, vars) = |
|
118 let |
|
119 val inst = mk_inst ctxt vars |
|
120 val names = fold (Term.add_free_names o Thm.term_of o snd) inst [] |
|
121 in (Thm.instantiate_cterm ([], inst) ct, names) end |
|
122 |
|
123 |
|
124 fun mk_bound ctxt (i, T) = |
|
125 let val ct = SMT_Utils.certify ctxt (Var ((Name.uu, 0), T)) |
|
126 in (ct, [(i, ct)]) end |
|
127 |
|
128 local |
|
129 fun mk_quant1 ctxt q T (ct, vars) = |
|
130 let |
|
131 val cv = |
|
132 (case AList.lookup (op =) vars 0 of |
|
133 SOME cv => cv |
|
134 | _ => SMT_Utils.certify ctxt (Var ((Name.uu, maxidx_of ct + 1), T))) |
|
135 fun dec (i, v) = if i = 0 then NONE else SOME (i-1, v) |
|
136 val vars' = map_filter dec vars |
|
137 in (Thm.apply (SMT_Utils.instT' cv q) (Thm.lambda cv ct), vars') end |
|
138 |
|
139 fun quant name = |
|
140 SMT_Utils.mk_const_pat @{theory} name (SMT_Utils.destT1 o SMT_Utils.destT1) |
|
141 val forall = quant @{const_name All} |
|
142 val exists = quant @{const_name Ex} |
|
143 in |
|
144 |
|
145 fun mk_quant is_forall ctxt = |
|
146 fold_rev (mk_quant1 ctxt (if is_forall then forall else exists)) |
|
147 |
|
148 end |
|
149 |
|
150 local |
|
151 fun prep (ct, vars) (maxidx, all_vars) = |
|
152 let |
|
153 val maxidx' = maxidx + maxidx_of ct + 1 |
|
154 |
|
155 fun part (i, cv) = |
|
156 (case AList.lookup (op =) all_vars i of |
|
157 SOME cu => apfst (if cu aconvc cv then I else cons (cv, cu)) |
|
158 | NONE => |
|
159 let val cv' = Thm.incr_indexes_cterm maxidx cv |
|
160 in apfst (cons (cv, cv')) #> apsnd (cons (i, cv')) end) |
|
161 |
|
162 val (inst, vars') = |
|
163 if null vars then ([], vars) |
|
164 else fold part vars ([], []) |
|
165 |
|
166 in (Thm.instantiate_cterm ([], inst) ct, (maxidx', vars' @ all_vars)) end |
|
167 in |
|
168 fun mk_fun f ts = |
|
169 let val (cts, (_, vars)) = fold_map prep ts (0, []) |
|
170 in f cts |> Option.map (rpair vars) end |
|
171 end |
|
172 |
|
173 |
|
174 |
|
175 (* proof parser *) |
|
176 |
|
177 datatype proof_step = Proof_Step of { |
|
178 rule: rule, |
|
179 args: cterm list, |
|
180 prems: int list, |
|
181 prop: cterm } |
|
182 |
|
183 |
|
184 (** parser context **) |
|
185 |
|
186 val not_false = Thm.cterm_of @{theory} (@{const Not} $ @{const False}) |
|
187 |
|
188 fun make_context ctxt typs terms = |
|
189 let |
|
190 val ctxt' = |
|
191 ctxt |
|
192 |> Symtab.fold (Variable.declare_typ o snd) typs |
|
193 |> Symtab.fold (Variable.declare_term o snd) terms |
|
194 |
|
195 fun cert @{const True} = not_false |
|
196 | cert t = SMT_Utils.certify ctxt' t |
|
197 |
|
198 in (typs, Symtab.map (K cert) terms, Inttab.empty, [], [], ctxt') end |
|
199 |
|
200 fun fresh_name n (typs, terms, exprs, steps, vars, ctxt) = |
|
201 let val (n', ctxt') = yield_singleton Variable.variant_fixes n ctxt |
|
202 in (n', (typs, terms, exprs, steps, vars, ctxt')) end |
|
203 |
|
204 fun context_of (_, _, _, _, _, ctxt) = ctxt |
|
205 |
|
206 fun add_decl (n, T) (cx as (_, terms, _, _, _, _)) = |
|
207 (case Symtab.lookup terms n of |
|
208 SOME _ => cx |
|
209 | NONE => cx |> fresh_name (decl_prefix ^ n) |
|
210 |> (fn (m, (typs, terms, exprs, steps, vars, ctxt)) => |
|
211 let |
|
212 val upd = Symtab.update (n, SMT_Utils.certify ctxt (Free (m, T))) |
|
213 in (typs, upd terms, exprs, steps, vars, ctxt) end)) |
|
214 |
|
215 fun mk_typ (typs, _, _, _, _, ctxt) (s as Z3_Interface.Sym (n, _)) = |
|
216 (case Z3_Interface.mk_builtin_typ ctxt s of |
|
217 SOME T => SOME T |
|
218 | NONE => Symtab.lookup typs n) |
|
219 |
|
220 fun mk_num (_, _, _, _, _, ctxt) (i, T) = |
|
221 mk_fun (K (Z3_Interface.mk_builtin_num ctxt i T)) [] |
|
222 |
|
223 fun mk_app (_, terms, _, _, _, ctxt) (s as Z3_Interface.Sym (n, _), es) = |
|
224 mk_fun (fn cts => |
|
225 (case Z3_Interface.mk_builtin_fun ctxt s cts of |
|
226 SOME ct => SOME ct |
|
227 | NONE => |
|
228 Symtab.lookup terms n |> Option.map (Drule.list_comb o rpair cts))) es |
|
229 |
|
230 fun add_expr k t (typs, terms, exprs, steps, vars, ctxt) = |
|
231 (typs, terms, Inttab.update (k, t) exprs, steps, vars, ctxt) |
|
232 |
|
233 fun lookup_expr (_, _, exprs, _, _, _) = Inttab.lookup exprs |
|
234 |
|
235 fun add_proof_step k ((r, args), prop) cx = |
|
236 let |
|
237 val (typs, terms, exprs, steps, vars, ctxt) = cx |
|
238 val (ct, vs) = close ctxt prop |
|
239 fun part (SOME e, _) (cts, ps) = (close ctxt e :: cts, ps) |
|
240 | part (NONE, i) (cts, ps) = (cts, i :: ps) |
|
241 val (args', prems) = fold (part o `(lookup_expr cx)) args ([], []) |
|
242 val (cts, vss) = split_list args' |
|
243 val step = Proof_Step {rule=r, args=rev cts, prems=rev prems, |
|
244 prop = SMT_Utils.mk_cprop ct} |
|
245 val vars' = fold (union (op =)) (vs :: vss) vars |
|
246 in (typs, terms, exprs, (k, step) :: steps, vars', ctxt) end |
|
247 |
|
248 fun finish (_, _, _, steps, vars, ctxt) = |
|
249 let |
|
250 fun coll (p as (k, Proof_Step {prems, rule, prop, ...})) (ars, ps, ids) = |
|
251 (case rule of |
|
252 Asserted => ((k, prop) :: ars, ps, ids) |
|
253 | Goal => ((k, prop) :: ars, ps, ids) |
|
254 | _ => |
|
255 if Inttab.defined ids k then |
|
256 (ars, p :: ps, fold (Inttab.update o rpair ()) prems ids) |
|
257 else (ars, ps, ids)) |
|
258 |
|
259 val (ars, steps', _) = fold coll steps ([], [], Inttab.make [(~1, ())]) |
|
260 in (ars, steps', vars, ctxt) end |
|
261 |
|
262 |
|
263 (** core parser **) |
|
264 |
|
265 fun parse_exn line_no msg = raise SMT_Failure.SMT (SMT_Failure.Other_Failure |
|
266 ("Z3 proof parser (line " ^ string_of_int line_no ^ "): " ^ msg)) |
|
267 |
|
268 fun scan_exn msg ((line_no, _), _) = parse_exn line_no msg |
|
269 |
|
270 fun with_info f cx = |
|
271 (case f ((NONE, 1), cx) of |
|
272 ((SOME _, _), cx') => cx' |
|
273 | ((_, line_no), _) => parse_exn line_no "bad proof") |
|
274 |
|
275 fun parse_line _ _ (st as ((SOME _, _), _)) = st |
|
276 | parse_line scan line ((_, line_no), cx) = |
|
277 let val st = ((line_no, cx), raw_explode line) |
|
278 in |
|
279 (case Scan.catch (Scan.finite' Symbol.stopper (Scan.option scan)) st of |
|
280 (SOME r, ((_, cx'), _)) => ((r, line_no+1), cx') |
|
281 | (NONE, _) => parse_exn line_no ("bad proof line: " ^ quote line)) |
|
282 end |
|
283 |
|
284 fun with_context f x ((line_no, cx), st) = |
|
285 let val (y, cx') = f x cx |
|
286 in (y, ((line_no, cx'), st)) end |
|
287 |
|
288 |
|
289 fun lookup_context f x (st as ((_, cx), _)) = (f cx x, st) |
|
290 |
|
291 |
|
292 (** parser combinators and parsers for basic entities **) |
|
293 |
|
294 fun $$ s = Scan.lift (Scan.$$ s) |
|
295 fun this s = Scan.lift (Scan.this_string s) |
|
296 val is_blank = Symbol.is_ascii_blank |
|
297 fun blank st = Scan.lift (Scan.many1 is_blank) st |
|
298 fun sep scan = blank |-- scan |
|
299 fun seps scan = Scan.repeat (sep scan) |
|
300 fun seps1 scan = Scan.repeat1 (sep scan) |
|
301 fun seps_by scan_sep scan = scan ::: Scan.repeat (scan_sep |-- scan) |
|
302 |
|
303 val lpar = "(" and rpar = ")" |
|
304 val lbra = "[" and rbra = "]" |
|
305 fun par scan = $$ lpar |-- scan --| $$ rpar |
|
306 fun bra scan = $$ lbra |-- scan --| $$ rbra |
|
307 |
|
308 val digit = (fn |
|
309 "0" => SOME 0 | "1" => SOME 1 | "2" => SOME 2 | "3" => SOME 3 | |
|
310 "4" => SOME 4 | "5" => SOME 5 | "6" => SOME 6 | "7" => SOME 7 | |
|
311 "8" => SOME 8 | "9" => SOME 9 | _ => NONE) |
|
312 |
|
313 fun digits st = (Scan.lift (Scan.many1 Symbol.is_ascii_digit) >> implode) st |
|
314 |
|
315 fun nat_num st = (Scan.lift (Scan.repeat1 (Scan.some digit)) >> (fn ds => |
|
316 fold (fn d => fn i => i * 10 + d) ds 0)) st |
|
317 |
|
318 fun int_num st = (Scan.optional ($$ "-" >> K (fn i => ~i)) I :|-- |
|
319 (fn sign => nat_num >> sign)) st |
|
320 |
|
321 val is_char = Symbol.is_ascii_letter orf Symbol.is_ascii_digit orf |
|
322 member (op =) (raw_explode "_+*-/%~=<>$&|?!.@^#") |
|
323 |
|
324 fun name st = (Scan.lift (Scan.many1 is_char) >> implode) st |
|
325 |
|
326 fun sym st = (name -- |
|
327 Scan.optional (bra (seps_by ($$ ":") sym)) [] >> Z3_Interface.Sym) st |
|
328 |
|
329 fun id st = ($$ "#" |-- nat_num) st |
|
330 |
|
331 |
|
332 (** parsers for various parts of Z3 proofs **) |
|
333 |
|
334 fun sort st = Scan.first [ |
|
335 this "array" |-- bra (sort --| $$ ":" -- sort) >> (op -->), |
|
336 par (this "->" |-- seps1 sort) >> ((op --->) o split_last), |
|
337 sym :|-- (fn s as Z3_Interface.Sym (n, _) => lookup_context mk_typ s :|-- (fn |
|
338 SOME T => Scan.succeed T |
|
339 | NONE => scan_exn ("unknown sort: " ^ quote n)))] st |
|
340 |
|
341 fun bound st = (par (this ":var" |-- sep nat_num -- sep sort) :|-- |
|
342 lookup_context (mk_bound o context_of)) st |
|
343 |
|
344 fun numb (n as (i, _)) = lookup_context mk_num n :|-- (fn |
|
345 SOME n' => Scan.succeed n' |
|
346 | NONE => scan_exn ("unknown number: " ^ quote (string_of_int i))) |
|
347 |
|
348 fun appl (app as (Z3_Interface.Sym (n, _), _)) = |
|
349 lookup_context mk_app app :|-- (fn |
|
350 SOME app' => Scan.succeed app' |
|
351 | NONE => scan_exn ("unknown function symbol: " ^ quote n)) |
|
352 |
|
353 fun bv_size st = (digits >> (fn sz => |
|
354 Z3_Interface.Sym ("bv", [Z3_Interface.Sym (sz, [])]))) st |
|
355 |
|
356 fun bv_number_sort st = (bv_size :|-- lookup_context mk_typ :|-- (fn |
|
357 SOME cT => Scan.succeed cT |
|
358 | NONE => scan_exn ("unknown sort: " ^ quote "bv"))) st |
|
359 |
|
360 fun bv_number st = |
|
361 (this "bv" |-- bra (nat_num --| $$ ":" -- bv_number_sort) :|-- numb) st |
|
362 |
|
363 fun frac_number st = ( |
|
364 int_num --| $$ "/" -- int_num --| this "::" -- sort :|-- (fn ((i, j), T) => |
|
365 numb (i, T) -- numb (j, T) :|-- (fn (n, m) => |
|
366 appl (Z3_Interface.Sym ("/", []), [n, m])))) st |
|
367 |
|
368 fun plain_number st = (int_num --| this "::" -- sort :|-- numb) st |
|
369 |
|
370 fun number st = Scan.first [bv_number, frac_number, plain_number] st |
|
371 |
|
372 fun constant st = ((sym >> rpair []) :|-- appl) st |
|
373 |
|
374 fun expr_id st = (id :|-- (fn i => lookup_context lookup_expr i :|-- (fn |
|
375 SOME e => Scan.succeed e |
|
376 | NONE => scan_exn ("unknown term id: " ^ quote (string_of_int i))))) st |
|
377 |
|
378 fun arg st = Scan.first [expr_id, number, constant] st |
|
379 |
|
380 fun application st = par ((sym -- Scan.repeat1 (sep arg)) :|-- appl) st |
|
381 |
|
382 fun variables st = par (this "vars" |-- seps1 (par (name |-- sep sort))) st |
|
383 |
|
384 fun pats st = seps (par ((this ":pat" || this ":nopat") |-- seps1 id)) st |
|
385 |
|
386 val ctrue = Thm.cterm_of @{theory} @{const True} |
|
387 |
|
388 fun pattern st = par (this "pattern" |-- Scan.repeat1 (sep arg) >> |
|
389 (the o mk_fun (K (SOME ctrue)))) st |
|
390 |
|
391 fun quant_kind st = st |> ( |
|
392 this "forall" >> K (mk_quant true o context_of) || |
|
393 this "exists" >> K (mk_quant false o context_of)) |
|
394 |
|
395 fun quantifier st = |
|
396 (par (quant_kind -- sep variables --| pats -- sep arg) :|-- |
|
397 lookup_context (fn cx => fn ((mk_q, Ts), body) => mk_q cx Ts body)) st |
|
398 |
|
399 fun expr k = |
|
400 Scan.first [bound, quantifier, pattern, application, number, constant] :|-- |
|
401 with_context (pair NONE oo add_expr k) |
|
402 |
|
403 val rule_arg = id |
|
404 (* if this is modified, then 'th_lemma_arg' needs reviewing *) |
|
405 |
|
406 fun th_lemma_arg st = Scan.unless (sep rule_arg >> K "" || $$ rbra) (sep name) st |
|
407 |
|
408 fun rule_name st = ((name >> `(Symtab.lookup rule_names)) :|-- (fn |
|
409 (SOME (Th_Lemma _), _) => Scan.repeat th_lemma_arg >> Th_Lemma |
|
410 | (SOME r, _) => Scan.succeed r |
|
411 | (NONE, n) => scan_exn ("unknown proof rule: " ^ quote n))) st |
|
412 |
|
413 fun rule f k = |
|
414 bra (rule_name -- seps id) --| $$ ":" -- sep arg #-> |
|
415 with_context (pair (f k) oo add_proof_step k) |
|
416 |
|
417 fun decl st = (this "decl" |-- sep name --| sep (this "::") -- sep sort :|-- |
|
418 with_context (pair NONE oo add_decl)) st |
|
419 |
|
420 fun def st = (id --| sep (this ":=")) st |
|
421 |
|
422 fun node st = st |> ( |
|
423 decl || |
|
424 def :|-- (fn k => sep (expr k) || sep (rule (K NONE) k)) || |
|
425 rule SOME ~1) |
|
426 |
|
427 |
|
428 (** overall parser **) |
|
429 |
|
430 (* |
|
431 Currently, terms are parsed bottom-up (i.e., along with parsing the proof |
|
432 text line by line), but proofs are reconstructed top-down (i.e. by an |
|
433 in-order top-down traversal of the proof tree/graph). The latter approach |
|
434 was taken because some proof texts comprise irrelevant proof steps which |
|
435 will thus not be reconstructed. This approach might also be beneficial |
|
436 for constructing terms, but it would also increase the complexity of the |
|
437 (otherwise rather modular) code. |
|
438 *) |
|
439 |
|
440 fun parse ctxt typs terms proof_text = |
|
441 make_context ctxt typs terms |
|
442 |> with_info (fold (parse_line node) proof_text) |
|
443 |> finish |
|
444 |
|
445 end |
|