1 (* Title: HOL/Library/Old_SMT/old_z3_proof_parser.ML |
|
2 Author: Sascha Boehme, TU Muenchen |
|
3 |
|
4 Parser for Z3 proofs. |
|
5 *) |
|
6 |
|
7 signature OLD_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 Old_Z3_Proof_Parser: OLD_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 fun mk_inst ctxt vars = |
|
108 let |
|
109 val max = fold (Integer.max o fst) vars 0 |
|
110 val ns = fst (Variable.variant_fixes (replicate (max + 1) var_prefix) ctxt) |
|
111 fun mk (i, v) = |
|
112 (dest_Var (Thm.term_of v), Thm.cterm_of ctxt (Free (nth ns i, Thm.typ_of_cterm v))) |
|
113 in map mk vars end |
|
114 |
|
115 fun close ctxt (ct, vars) = |
|
116 let |
|
117 val inst = mk_inst ctxt vars |
|
118 val names = fold (Term.add_free_names o Thm.term_of o snd) inst [] |
|
119 in (Thm.instantiate_cterm ([], inst) ct, names) end |
|
120 |
|
121 |
|
122 fun mk_bound ctxt (i, T) = |
|
123 let val ct = Thm.cterm_of ctxt (Var ((Name.uu, 0), T)) |
|
124 in (ct, [(i, ct)]) end |
|
125 |
|
126 local |
|
127 fun mk_quant1 ctxt q T (ct, vars) = |
|
128 let |
|
129 val cv = |
|
130 (case AList.lookup (op =) vars 0 of |
|
131 SOME cv => cv |
|
132 | _ => Thm.cterm_of ctxt (Var ((Name.uu, Thm.maxidx_of_cterm ct + 1), T))) |
|
133 fun dec (i, v) = if i = 0 then NONE else SOME (i-1, v) |
|
134 val vars' = map_filter dec vars |
|
135 in (Thm.apply (Old_SMT_Utils.instT' cv q) (Thm.lambda cv ct), vars') end |
|
136 |
|
137 fun quant name = |
|
138 Old_SMT_Utils.mk_const_pat @{theory} name (Old_SMT_Utils.destT1 o Old_SMT_Utils.destT1) |
|
139 val forall = quant @{const_name All} |
|
140 val exists = quant @{const_name Ex} |
|
141 in |
|
142 |
|
143 fun mk_quant is_forall ctxt = |
|
144 fold_rev (mk_quant1 ctxt (if is_forall then forall else exists)) |
|
145 |
|
146 end |
|
147 |
|
148 local |
|
149 fun prep (ct, vars) (maxidx, all_vars) = |
|
150 let |
|
151 val maxidx' = maxidx + Thm.maxidx_of_cterm ct + 1 |
|
152 |
|
153 fun part (i, cv) = |
|
154 (case AList.lookup (op =) all_vars i of |
|
155 SOME cu => apfst (if cu aconvc cv then I else cons (cv, cu)) |
|
156 | NONE => |
|
157 let val cv' = Thm.incr_indexes_cterm maxidx cv |
|
158 in apfst (cons (cv, cv')) #> apsnd (cons (i, cv')) end) |
|
159 |
|
160 val (inst, vars') = |
|
161 if null vars then ([], vars) |
|
162 else fold part vars ([], []) |
|
163 |
|
164 in |
|
165 (Thm.instantiate_cterm ([], map (apfst (dest_Var o Thm.term_of)) inst) ct, |
|
166 (maxidx', vars' @ all_vars)) |
|
167 end |
|
168 in |
|
169 fun mk_fun f ts = |
|
170 let val (cts, (_, vars)) = fold_map prep ts (0, []) |
|
171 in f cts |> Option.map (rpair vars) end |
|
172 end |
|
173 |
|
174 |
|
175 |
|
176 (* proof parser *) |
|
177 |
|
178 datatype proof_step = Proof_Step of { |
|
179 rule: rule, |
|
180 args: cterm list, |
|
181 prems: int list, |
|
182 prop: cterm } |
|
183 |
|
184 |
|
185 (** parser context **) |
|
186 |
|
187 val not_false = Thm.cterm_of @{context} (@{const Not} $ @{const False}) |
|
188 |
|
189 fun make_context ctxt typs terms = |
|
190 let |
|
191 val ctxt' = |
|
192 ctxt |
|
193 |> Symtab.fold (Variable.declare_typ o snd) typs |
|
194 |> Symtab.fold (Variable.declare_term o snd) terms |
|
195 |
|
196 fun cert @{const True} = not_false |
|
197 | cert t = Thm.cterm_of ctxt' t |
|
198 |
|
199 in (typs, Symtab.map (K cert) terms, Inttab.empty, [], [], ctxt') end |
|
200 |
|
201 fun fresh_name n (typs, terms, exprs, steps, vars, ctxt) = |
|
202 let val (n', ctxt') = yield_singleton Variable.variant_fixes n ctxt |
|
203 in (n', (typs, terms, exprs, steps, vars, ctxt')) end |
|
204 |
|
205 fun context_of (_, _, _, _, _, ctxt) = ctxt |
|
206 |
|
207 fun add_decl (n, T) (cx as (_, terms, _, _, _, _)) = |
|
208 (case Symtab.lookup terms n of |
|
209 SOME _ => cx |
|
210 | NONE => cx |> fresh_name (decl_prefix ^ n) |
|
211 |> (fn (m, (typs, terms, exprs, steps, vars, ctxt)) => |
|
212 let |
|
213 val upd = Symtab.update (n, Thm.cterm_of ctxt (Free (m, T))) |
|
214 in (typs, upd terms, exprs, steps, vars, ctxt) end)) |
|
215 |
|
216 fun mk_typ (typs, _, _, _, _, ctxt) (s as Old_Z3_Interface.Sym (n, _)) = |
|
217 (case Old_Z3_Interface.mk_builtin_typ ctxt s of |
|
218 SOME T => SOME T |
|
219 | NONE => Symtab.lookup typs n) |
|
220 |
|
221 fun mk_num (_, _, _, _, _, ctxt) (i, T) = |
|
222 mk_fun (K (Old_Z3_Interface.mk_builtin_num ctxt i T)) [] |
|
223 |
|
224 fun mk_app (_, terms, _, _, _, ctxt) (s as Old_Z3_Interface.Sym (n, _), es) = |
|
225 mk_fun (fn cts => |
|
226 (case Old_Z3_Interface.mk_builtin_fun ctxt s cts of |
|
227 SOME ct => SOME ct |
|
228 | NONE => |
|
229 Symtab.lookup terms n |> Option.map (Drule.list_comb o rpair cts))) es |
|
230 |
|
231 fun add_expr k t (typs, terms, exprs, steps, vars, ctxt) = |
|
232 (typs, terms, Inttab.update (k, t) exprs, steps, vars, ctxt) |
|
233 |
|
234 fun lookup_expr (_, _, exprs, _, _, _) = Inttab.lookup exprs |
|
235 |
|
236 fun add_proof_step k ((r, args), prop) cx = |
|
237 let |
|
238 val (typs, terms, exprs, steps, vars, ctxt) = cx |
|
239 val (ct, vs) = close ctxt prop |
|
240 fun part (SOME e, _) (cts, ps) = (close ctxt e :: cts, ps) |
|
241 | part (NONE, i) (cts, ps) = (cts, i :: ps) |
|
242 val (args', prems) = fold (part o `(lookup_expr cx)) args ([], []) |
|
243 val (cts, vss) = split_list args' |
|
244 val step = Proof_Step {rule=r, args=rev cts, prems=rev prems, |
|
245 prop = Old_SMT_Utils.mk_cprop ct} |
|
246 val vars' = fold (union (op =)) (vs :: vss) vars |
|
247 in (typs, terms, exprs, (k, step) :: steps, vars', ctxt) end |
|
248 |
|
249 fun finish (_, _, _, steps, vars, ctxt) = |
|
250 let |
|
251 fun coll (p as (k, Proof_Step {prems, rule, prop, ...})) (ars, ps, ids) = |
|
252 (case rule of |
|
253 Asserted => ((k, prop) :: ars, ps, ids) |
|
254 | Goal => ((k, prop) :: ars, ps, ids) |
|
255 | _ => |
|
256 if Inttab.defined ids k then |
|
257 (ars, p :: ps, fold (Inttab.update o rpair ()) prems ids) |
|
258 else (ars, ps, ids)) |
|
259 |
|
260 val (ars, steps', _) = fold coll steps ([], [], Inttab.make [(~1, ())]) |
|
261 in (ars, steps', vars, ctxt) end |
|
262 |
|
263 |
|
264 (** core parser **) |
|
265 |
|
266 fun parse_exn line_no msg = raise Old_SMT_Failure.SMT (Old_SMT_Failure.Other_Failure |
|
267 ("Z3 proof parser (line " ^ string_of_int line_no ^ "): " ^ msg)) |
|
268 |
|
269 fun scan_exn msg ((line_no, _), _) = parse_exn line_no msg |
|
270 |
|
271 fun with_info f cx = |
|
272 (case f ((NONE, 1), cx) of |
|
273 ((SOME _, _), cx') => cx' |
|
274 | ((_, line_no), _) => parse_exn line_no "bad proof") |
|
275 |
|
276 fun parse_line _ _ (st as ((SOME _, _), _)) = st |
|
277 | parse_line scan line ((_, line_no), cx) = |
|
278 let val st = ((line_no, cx), raw_explode line) |
|
279 in |
|
280 (case Scan.catch (Scan.finite' Symbol.stopper (Scan.option scan)) st of |
|
281 (SOME r, ((_, cx'), _)) => ((r, line_no+1), cx') |
|
282 | (NONE, _) => parse_exn line_no ("bad proof line: " ^ quote line)) |
|
283 end |
|
284 |
|
285 fun with_context f x ((line_no, cx), st) = |
|
286 let val (y, cx') = f x cx |
|
287 in (y, ((line_no, cx'), st)) end |
|
288 |
|
289 |
|
290 fun lookup_context f x (st as ((_, cx), _)) = (f cx x, st) |
|
291 |
|
292 |
|
293 (** parser combinators and parsers for basic entities **) |
|
294 |
|
295 fun $$ s = Scan.lift (Scan.$$ s) |
|
296 fun this s = Scan.lift (Scan.this_string s) |
|
297 val is_blank = Symbol.is_ascii_blank |
|
298 fun blank st = Scan.lift (Scan.many1 is_blank) st |
|
299 fun sep scan = blank |-- scan |
|
300 fun seps scan = Scan.repeat (sep scan) |
|
301 fun seps1 scan = Scan.repeat1 (sep scan) |
|
302 fun seps_by scan_sep scan = scan ::: Scan.repeat (scan_sep |-- scan) |
|
303 |
|
304 val lpar = "(" and rpar = ")" |
|
305 val lbra = "[" and rbra = "]" |
|
306 fun par scan = $$ lpar |-- scan --| $$ rpar |
|
307 fun bra scan = $$ lbra |-- scan --| $$ rbra |
|
308 |
|
309 val digit = (fn |
|
310 "0" => SOME 0 | "1" => SOME 1 | "2" => SOME 2 | "3" => SOME 3 | |
|
311 "4" => SOME 4 | "5" => SOME 5 | "6" => SOME 6 | "7" => SOME 7 | |
|
312 "8" => SOME 8 | "9" => SOME 9 | _ => NONE) |
|
313 |
|
314 fun digits st = (Scan.lift (Scan.many1 Symbol.is_ascii_digit) >> implode) st |
|
315 |
|
316 fun nat_num st = (Scan.lift (Scan.repeat1 (Scan.some digit)) >> (fn ds => |
|
317 fold (fn d => fn i => i * 10 + d) ds 0)) st |
|
318 |
|
319 fun int_num st = (Scan.optional ($$ "-" >> K (fn i => ~i)) I :|-- |
|
320 (fn sign => nat_num >> sign)) st |
|
321 |
|
322 val is_char = Symbol.is_ascii_letter orf Symbol.is_ascii_digit orf |
|
323 member (op =) (raw_explode "_+*-/%~=<>$&|?!.@^#") |
|
324 |
|
325 fun name st = (Scan.lift (Scan.many1 is_char) >> implode) st |
|
326 |
|
327 fun sym st = (name -- |
|
328 Scan.optional (bra (seps_by ($$ ":") sym)) [] >> Old_Z3_Interface.Sym) st |
|
329 |
|
330 fun id st = ($$ "#" |-- nat_num) st |
|
331 |
|
332 |
|
333 (** parsers for various parts of Z3 proofs **) |
|
334 |
|
335 fun sort st = Scan.first [ |
|
336 this "array" |-- bra (sort --| $$ ":" -- sort) >> (op -->), |
|
337 par (this "->" |-- seps1 sort) >> ((op --->) o split_last), |
|
338 sym :|-- (fn s as Old_Z3_Interface.Sym (n, _) => lookup_context mk_typ s :|-- (fn |
|
339 SOME T => Scan.succeed T |
|
340 | NONE => scan_exn ("unknown sort: " ^ quote n)))] st |
|
341 |
|
342 fun bound st = (par (this ":var" |-- sep nat_num -- sep sort) :|-- |
|
343 lookup_context (mk_bound o context_of)) st |
|
344 |
|
345 fun numb (n as (i, _)) = lookup_context mk_num n :|-- (fn |
|
346 SOME n' => Scan.succeed n' |
|
347 | NONE => scan_exn ("unknown number: " ^ quote (string_of_int i))) |
|
348 |
|
349 fun appl (app as (Old_Z3_Interface.Sym (n, _), _)) = |
|
350 lookup_context mk_app app :|-- (fn |
|
351 SOME app' => Scan.succeed app' |
|
352 | NONE => scan_exn ("unknown function symbol: " ^ quote n)) |
|
353 |
|
354 fun bv_size st = (digits >> (fn sz => |
|
355 Old_Z3_Interface.Sym ("bv", [Old_Z3_Interface.Sym (sz, [])]))) st |
|
356 |
|
357 fun bv_number_sort st = (bv_size :|-- lookup_context mk_typ :|-- (fn |
|
358 SOME cT => Scan.succeed cT |
|
359 | NONE => scan_exn ("unknown sort: " ^ quote "bv"))) st |
|
360 |
|
361 fun bv_number st = |
|
362 (this "bv" |-- bra (nat_num --| $$ ":" -- bv_number_sort) :|-- numb) st |
|
363 |
|
364 fun frac_number st = ( |
|
365 int_num --| $$ "/" -- int_num --| this "::" -- sort :|-- (fn ((i, j), T) => |
|
366 numb (i, T) -- numb (j, T) :|-- (fn (n, m) => |
|
367 appl (Old_Z3_Interface.Sym ("/", []), [n, m])))) st |
|
368 |
|
369 fun plain_number st = (int_num --| this "::" -- sort :|-- numb) st |
|
370 |
|
371 fun number st = Scan.first [bv_number, frac_number, plain_number] st |
|
372 |
|
373 fun constant st = ((sym >> rpair []) :|-- appl) st |
|
374 |
|
375 fun expr_id st = (id :|-- (fn i => lookup_context lookup_expr i :|-- (fn |
|
376 SOME e => Scan.succeed e |
|
377 | NONE => scan_exn ("unknown term id: " ^ quote (string_of_int i))))) st |
|
378 |
|
379 fun arg st = Scan.first [expr_id, number, constant] st |
|
380 |
|
381 fun application st = par ((sym -- Scan.repeat1 (sep arg)) :|-- appl) st |
|
382 |
|
383 fun variables st = par (this "vars" |-- seps1 (par (name |-- sep sort))) st |
|
384 |
|
385 fun pats st = seps (par ((this ":pat" || this ":nopat") |-- seps1 id)) st |
|
386 |
|
387 val ctrue = Thm.cterm_of @{context} @{const True} |
|
388 |
|
389 fun pattern st = par (this "pattern" |-- Scan.repeat1 (sep arg) >> |
|
390 (the o mk_fun (K (SOME ctrue)))) st |
|
391 |
|
392 fun quant_kind st = st |> ( |
|
393 this "forall" >> K (mk_quant true o context_of) || |
|
394 this "exists" >> K (mk_quant false o context_of)) |
|
395 |
|
396 fun quantifier st = |
|
397 (par (quant_kind -- sep variables --| pats -- sep arg) :|-- |
|
398 lookup_context (fn cx => fn ((mk_q, Ts), body) => mk_q cx Ts body)) st |
|
399 |
|
400 fun expr k = |
|
401 Scan.first [bound, quantifier, pattern, application, number, constant] :|-- |
|
402 with_context (pair NONE oo add_expr k) |
|
403 |
|
404 val rule_arg = id |
|
405 (* if this is modified, then 'th_lemma_arg' needs reviewing *) |
|
406 |
|
407 fun th_lemma_arg st = Scan.unless (sep rule_arg >> K "" || $$ rbra) (sep name) st |
|
408 |
|
409 fun rule_name st = ((name >> `(Symtab.lookup rule_names)) :|-- (fn |
|
410 (SOME (Th_Lemma _), _) => Scan.repeat th_lemma_arg >> Th_Lemma |
|
411 | (SOME r, _) => Scan.succeed r |
|
412 | (NONE, n) => scan_exn ("unknown proof rule: " ^ quote n))) st |
|
413 |
|
414 fun rule f k = |
|
415 bra (rule_name -- seps id) --| $$ ":" -- sep arg #-> |
|
416 with_context (pair (f k) oo add_proof_step k) |
|
417 |
|
418 fun decl st = (this "decl" |-- sep name --| sep (this "::") -- sep sort :|-- |
|
419 with_context (pair NONE oo add_decl)) st |
|
420 |
|
421 fun def st = (id --| sep (this ":=")) st |
|
422 |
|
423 fun node st = st |> ( |
|
424 decl || |
|
425 def :|-- (fn k => sep (expr k) || sep (rule (K NONE) k)) || |
|
426 rule SOME ~1) |
|
427 |
|
428 |
|
429 (** overall parser **) |
|
430 |
|
431 (* |
|
432 Currently, terms are parsed bottom-up (i.e., along with parsing the proof |
|
433 text line by line), but proofs are reconstructed top-down (i.e. by an |
|
434 in-order top-down traversal of the proof tree/graph). The latter approach |
|
435 was taken because some proof texts comprise irrelevant proof steps which |
|
436 will thus not be reconstructed. This approach might also be beneficial |
|
437 for constructing terms, but it would also increase the complexity of the |
|
438 (otherwise rather modular) code. |
|
439 *) |
|
440 |
|
441 fun parse ctxt typs terms proof_text = |
|
442 make_context ctxt typs terms |
|
443 |> with_info (fold (parse_line node) proof_text) |
|
444 |> finish |
|
445 |
|
446 end |
|