1 (* Title: HOL/SMT/Tools/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 = TrueAxiom | Asserted | Goal | ModusPonens | Reflexivity | |
|
11 Symmetry | Transitivity | TransitivityStar | Monotonicity | QuantIntro | |
|
12 Distributivity | AndElim | NotOrElim | Rewrite | RewriteStar | PullQuant | |
|
13 PullQuantStar | PushQuant | ElimUnusedVars | DestEqRes | QuantInst | |
|
14 Hypothesis | Lemma | UnitResolution | IffTrue | IffFalse | Commutativity | |
|
15 DefAxiom | IntroDef | ApplyDef | IffOeq | NnfPos | NnfNeg | NnfStar | |
|
16 CnfStar | Skolemize | ModusPonensOeq | ThLemma |
|
17 val string_of_rule: rule -> string |
|
18 |
|
19 (* proof parser *) |
|
20 datatype proof_step = Proof_Step of { |
|
21 rule: rule, |
|
22 prems: int list, |
|
23 prop: cterm } |
|
24 val parse: Proof.context -> typ Symtab.table -> term Symtab.table -> |
|
25 string list -> |
|
26 int * (proof_step Inttab.table * string list * Proof.context) |
|
27 end |
|
28 |
|
29 structure Z3_Proof_Parser: Z3_PROOF_PARSER = |
|
30 struct |
|
31 |
|
32 (** proof rules **) |
|
33 |
|
34 datatype rule = TrueAxiom | Asserted | Goal | ModusPonens | Reflexivity | |
|
35 Symmetry | Transitivity | TransitivityStar | Monotonicity | QuantIntro | |
|
36 Distributivity | AndElim | NotOrElim | Rewrite | RewriteStar | PullQuant | |
|
37 PullQuantStar | PushQuant | ElimUnusedVars | DestEqRes | QuantInst | |
|
38 Hypothesis | Lemma | UnitResolution | IffTrue | IffFalse | Commutativity | |
|
39 DefAxiom | IntroDef | ApplyDef | IffOeq | NnfPos | NnfNeg | NnfStar | |
|
40 CnfStar | Skolemize | ModusPonensOeq | ThLemma |
|
41 |
|
42 val rule_names = Symtab.make [ |
|
43 ("true-axiom", TrueAxiom), |
|
44 ("asserted", Asserted), |
|
45 ("goal", Goal), |
|
46 ("mp", ModusPonens), |
|
47 ("refl", Reflexivity), |
|
48 ("symm", Symmetry), |
|
49 ("trans", Transitivity), |
|
50 ("trans*", TransitivityStar), |
|
51 ("monotonicity", Monotonicity), |
|
52 ("quant-intro", QuantIntro), |
|
53 ("distributivity", Distributivity), |
|
54 ("and-elim", AndElim), |
|
55 ("not-or-elim", NotOrElim), |
|
56 ("rewrite", Rewrite), |
|
57 ("rewrite*", RewriteStar), |
|
58 ("pull-quant", PullQuant), |
|
59 ("pull-quant*", PullQuantStar), |
|
60 ("push-quant", PushQuant), |
|
61 ("elim-unused", ElimUnusedVars), |
|
62 ("der", DestEqRes), |
|
63 ("quant-inst", QuantInst), |
|
64 ("hypothesis", Hypothesis), |
|
65 ("lemma", Lemma), |
|
66 ("unit-resolution", UnitResolution), |
|
67 ("iff-true", IffTrue), |
|
68 ("iff-false", IffFalse), |
|
69 ("commutativity", Commutativity), |
|
70 ("def-axiom", DefAxiom), |
|
71 ("intro-def", IntroDef), |
|
72 ("apply-def", ApplyDef), |
|
73 ("iff~", IffOeq), |
|
74 ("nnf-pos", NnfPos), |
|
75 ("nnf-neg", NnfNeg), |
|
76 ("nnf*", NnfStar), |
|
77 ("cnf*", CnfStar), |
|
78 ("sk", Skolemize), |
|
79 ("mp~", ModusPonensOeq), |
|
80 ("th-lemma", ThLemma)] |
|
81 |
|
82 fun string_of_rule r = |
|
83 let fun eq_rule (s, r') = if r = r' then SOME s else NONE |
|
84 in the (Symtab.get_first eq_rule rule_names) end |
|
85 |
|
86 |
|
87 |
|
88 (** certified terms and variables **) |
|
89 |
|
90 val (var_prefix, decl_prefix) = ("v", "sk") (* must be distinct *) |
|
91 |
|
92 fun instTs cUs (cTs, ct) = Thm.instantiate_cterm (cTs ~~ cUs, []) ct |
|
93 fun instT cU (cT, ct) = instTs [cU] ([cT], ct) |
|
94 fun mk_inst_pair destT cpat = (destT (Thm.ctyp_of_term cpat), cpat) |
|
95 val destT1 = hd o Thm.dest_ctyp |
|
96 val destT2 = hd o tl o Thm.dest_ctyp |
|
97 |
|
98 fun ctyp_of (ct, _) = Thm.ctyp_of_term ct |
|
99 fun instT' t = instT (ctyp_of t) |
|
100 |
|
101 fun certify ctxt = Thm.cterm_of (ProofContext.theory_of ctxt) |
|
102 |
|
103 val maxidx_of = #maxidx o Thm.rep_cterm |
|
104 |
|
105 fun mk_inst ctxt vars = |
|
106 let |
|
107 val max = fold (Integer.max o fst) vars 0 |
|
108 val ns = fst (Variable.variant_fixes (replicate (max + 1) var_prefix) ctxt) |
|
109 fun mk (i, v) = (v, certify ctxt (Free (nth ns i, #T (Thm.rep_cterm v)))) |
|
110 in map mk vars end |
|
111 |
|
112 fun close ctxt (ct, vars) = |
|
113 let |
|
114 val inst = mk_inst ctxt vars |
|
115 val mk_prop = Thm.capply @{cterm Trueprop} |
|
116 val names = fold (Term.add_free_names o Thm.term_of o snd) inst [] |
|
117 in (mk_prop (Thm.instantiate_cterm ([], inst) ct), names) end |
|
118 |
|
119 |
|
120 fun mk_bound thy (i, T) = |
|
121 let val ct = Thm.cterm_of thy (Var ((Name.uu, 0), T)) |
|
122 in (ct, [(i, ct)]) end |
|
123 |
|
124 local |
|
125 fun mk_quant thy q T (ct, vars) = |
|
126 let |
|
127 val cv = |
|
128 (case AList.lookup (op =) vars 0 of |
|
129 SOME cv => cv |
|
130 | _ => Thm.cterm_of thy (Var ((Name.uu, maxidx_of ct + 1), T))) |
|
131 val cq = instT (Thm.ctyp_of_term cv) q |
|
132 fun dec (i, v) = if i = 0 then NONE else SOME (i-1, v) |
|
133 in (Thm.capply cq (Thm.cabs cv ct), map_filter dec vars) end |
|
134 |
|
135 val forall = mk_inst_pair (destT1 o destT1) @{cpat All} |
|
136 val exists = mk_inst_pair (destT1 o destT1) @{cpat Ex} |
|
137 in |
|
138 fun mk_forall thy = fold_rev (mk_quant thy forall) |
|
139 fun mk_exists thy = fold_rev (mk_quant thy exists) |
|
140 end |
|
141 |
|
142 |
|
143 local |
|
144 fun equal_var cv (_, cu) = (cv aconvc cu) |
|
145 |
|
146 fun apply (ct2, vars2) (ct1, vars1) = |
|
147 let |
|
148 val incr = Thm.incr_indexes_cterm (maxidx_of ct1 + maxidx_of ct2 + 2) |
|
149 |
|
150 fun part (v as (i, cv)) = |
|
151 (case AList.lookup (op =) vars1 i of |
|
152 SOME cu => apfst (if cu aconvc cv then I else cons (cv, cu)) |
|
153 | NONE => |
|
154 if not (exists (equal_var cv) vars1) then apsnd (cons v) |
|
155 else |
|
156 let val cv' = incr cv |
|
157 in apfst (cons (cv, cv')) #> apsnd (cons (i, cv')) end) |
|
158 |
|
159 val (ct2', vars2') = |
|
160 if null vars1 then (ct2, vars2) |
|
161 else fold part vars2 ([], []) |
|
162 |>> (fn inst => Thm.instantiate_cterm ([], inst) ct2) |
|
163 |
|
164 in (Thm.capply ct1 ct2', vars1 @ vars2') end |
|
165 in |
|
166 fun mk_fun ct ts = fold apply ts (ct, []) |
|
167 fun mk_binop f t u = mk_fun f [t, u] |
|
168 fun mk_nary _ e [] = e |
|
169 | mk_nary ct _ es = uncurry (fold_rev (mk_binop ct)) (split_last es) |
|
170 end |
|
171 |
|
172 |
|
173 val mk_true = mk_fun @{cterm "~False"} [] |
|
174 val mk_false = mk_fun @{cterm "False"} [] |
|
175 fun mk_not t = mk_fun @{cterm Not} [t] |
|
176 val mk_imp = mk_binop @{cterm "op -->"} |
|
177 val mk_iff = mk_binop @{cterm "op = :: bool => _"} |
|
178 |
|
179 val eq = mk_inst_pair destT1 @{cpat "op ="} |
|
180 fun mk_eq t u = mk_binop (instT' t eq) t u |
|
181 |
|
182 val if_term = mk_inst_pair (destT1 o destT2) @{cpat If} |
|
183 fun mk_if c t u = mk_fun (instT' t if_term) [c, t, u] |
|
184 |
|
185 val nil_term = mk_inst_pair destT1 @{cpat Nil} |
|
186 val cons_term = mk_inst_pair destT1 @{cpat Cons} |
|
187 fun mk_list cT es = |
|
188 fold_rev (mk_binop (instT cT cons_term)) es (mk_fun (instT cT nil_term) []) |
|
189 |
|
190 val distinct = mk_inst_pair (destT1 o destT1) @{cpat distinct} |
|
191 fun mk_distinct [] = mk_true |
|
192 | mk_distinct (es as (e :: _)) = |
|
193 mk_fun (instT' e distinct) [mk_list (ctyp_of e) es] |
|
194 |
|
195 |
|
196 (* arithmetic *) |
|
197 |
|
198 fun mk_int_num i = mk_fun (Numeral.mk_cnumber @{ctyp int} i) [] |
|
199 fun mk_real_num i = mk_fun (Numeral.mk_cnumber @{ctyp real} i) [] |
|
200 fun mk_real_frac_num (e, NONE) = mk_real_num e |
|
201 | mk_real_frac_num (e, SOME d) = |
|
202 mk_binop @{cterm "op / :: real => _"} (mk_real_num e) (mk_real_num d) |
|
203 |
|
204 fun has_int_type e = (Thm.typ_of (ctyp_of e) = @{typ int}) |
|
205 fun choose e i r = if has_int_type e then i else r |
|
206 |
|
207 val uminus_i = @{cterm "uminus :: int => _"} |
|
208 val uminus_r = @{cterm "uminus :: real => _"} |
|
209 fun mk_uminus e = mk_fun (choose e uminus_i uminus_r) [e] |
|
210 |
|
211 fun arith_op int_op real_op t u = mk_binop (choose t int_op real_op) t u |
|
212 |
|
213 val mk_add = arith_op @{cterm "op + :: int => _"} @{cterm "op + :: real => _"} |
|
214 val mk_sub = arith_op @{cterm "op - :: int => _"} @{cterm "op - :: real => _"} |
|
215 val mk_mul = arith_op @{cterm "op * :: int => _"} @{cterm "op * :: real => _"} |
|
216 val mk_int_div = mk_binop @{cterm "op div :: int => _"} |
|
217 val mk_real_div = mk_binop @{cterm "op / :: real => _"} |
|
218 val mk_mod = mk_binop @{cterm "op mod :: int => _"} |
|
219 val mk_lt = arith_op @{cterm "op < :: int => _"} @{cterm "op < :: real => _"} |
|
220 val mk_le = arith_op @{cterm "op <= :: int => _"} @{cterm "op <= :: real => _"} |
|
221 |
|
222 |
|
223 (* arrays *) |
|
224 |
|
225 val access = mk_inst_pair (Thm.dest_ctyp o destT1) @{cpat apply} |
|
226 fun mk_access array index = |
|
227 let val cTs = Thm.dest_ctyp (ctyp_of array) |
|
228 in mk_fun (instTs cTs access) [array, index] end |
|
229 |
|
230 val update = mk_inst_pair (Thm.dest_ctyp o destT1) @{cpat fun_upd} |
|
231 fun mk_update array index value = |
|
232 let val cTs = Thm.dest_ctyp (ctyp_of array) |
|
233 in mk_fun (instTs cTs update) [array, index, value] end |
|
234 |
|
235 |
|
236 (* bitvectors *) |
|
237 |
|
238 fun mk_binT size = |
|
239 let |
|
240 fun bitT i T = |
|
241 if i = 0 |
|
242 then Type (@{type_name "Numeral_Type.bit0"}, [T]) |
|
243 else Type (@{type_name "Numeral_Type.bit1"}, [T]) |
|
244 |
|
245 fun binT i = |
|
246 if i = 0 then @{typ "Numeral_Type.num0"} |
|
247 else if i = 1 then @{typ "Numeral_Type.num1"} |
|
248 else let val (q, r) = Integer.div_mod i 2 in bitT r (binT q) end |
|
249 in |
|
250 if size >= 0 then binT size |
|
251 else raise TYPE ("mk_binT: " ^ string_of_int size, [], []) |
|
252 end |
|
253 |
|
254 fun mk_wordT size = Type (@{type_name "word"}, [mk_binT size]) |
|
255 |
|
256 fun mk_bv_num thy (num, size) = |
|
257 mk_fun (Numeral.mk_cnumber (Thm.ctyp_of thy (mk_wordT size)) num) [] |
|
258 |
|
259 |
|
260 |
|
261 (** proof parser **) |
|
262 |
|
263 datatype proof_step = Proof_Step of { |
|
264 rule: rule, |
|
265 prems: int list, |
|
266 prop: cterm } |
|
267 |
|
268 |
|
269 (* parser context *) |
|
270 |
|
271 fun make_context ctxt typs terms = |
|
272 let |
|
273 val ctxt' = |
|
274 ctxt |
|
275 |> Symtab.fold (Variable.declare_typ o snd) typs |
|
276 |> Symtab.fold (Variable.declare_term o snd) terms |
|
277 |
|
278 fun cert @{term True} = @{cterm "~False"} |
|
279 | cert t = certify ctxt' t |
|
280 in (typs, Symtab.map cert terms, Inttab.empty, Inttab.empty, [], ctxt') end |
|
281 |
|
282 fun fresh_name n (typs, terms, exprs, steps, vars, ctxt) = |
|
283 let val (n', ctxt') = yield_singleton Variable.variant_fixes n ctxt |
|
284 in (n', (typs, terms, exprs, steps, vars, ctxt')) end |
|
285 |
|
286 fun theory_of (_, _, _, _, _, ctxt) = ProofContext.theory_of ctxt |
|
287 |
|
288 fun typ_of_sort n (cx as (typs, _, _, _, _, _)) = |
|
289 (case Symtab.lookup typs n of |
|
290 SOME T => (T, cx) |
|
291 | NONE => cx |
|
292 |> fresh_name ("'" ^ n) |>> TFree o rpair @{sort type} |
|
293 |> (fn (T, (typs, terms, exprs, steps, vars, ctxt)) => |
|
294 (T, (Symtab.update (n, T) typs, terms, exprs, steps, vars, ctxt)))) |
|
295 |
|
296 fun add_decl (n, T) (cx as (_, terms, _, _, _, _)) = |
|
297 (case Symtab.lookup terms n of |
|
298 SOME _ => cx |
|
299 | NONE => cx |> fresh_name (decl_prefix ^ n) |
|
300 |> (fn (m, (typs, terms, exprs, steps, vars, ctxt)) => |
|
301 let val upd = Symtab.update (n, certify ctxt (Free (m, T))) |
|
302 in (typs, upd terms, exprs, steps, vars, ctxt) end)) |
|
303 |
|
304 datatype sym = Sym of string * sym list |
|
305 |
|
306 fun mk_app _ (Sym ("true", _), _) = SOME mk_true |
|
307 | mk_app _ (Sym ("false", _), _) = SOME mk_false |
|
308 | mk_app _ (Sym ("=", _), [t, u]) = SOME (mk_eq t u) |
|
309 | mk_app _ (Sym ("distinct", _), ts) = SOME (mk_distinct ts) |
|
310 | mk_app _ (Sym ("ite", _), [s, t, u]) = SOME (mk_if s t u) |
|
311 | mk_app _ (Sym ("and", _), ts) = SOME (mk_nary @{cterm "op &"} mk_true ts) |
|
312 | mk_app _ (Sym ("or", _), ts) = SOME (mk_nary @{cterm "op |"} mk_false ts) |
|
313 | mk_app _ (Sym ("iff", _), [t, u]) = SOME (mk_iff t u) |
|
314 | mk_app _ (Sym ("xor", _), [t, u]) = SOME (mk_not (mk_iff t u)) |
|
315 | mk_app _ (Sym ("not", _), [t]) = SOME (mk_not t) |
|
316 | mk_app _ (Sym ("implies", _), [t, u]) = SOME (mk_imp t u) |
|
317 | mk_app _ (Sym ("~", _), [t, u]) = SOME (mk_iff t u) |
|
318 | mk_app _ (Sym ("<", _), [t, u]) = SOME (mk_lt t u) |
|
319 | mk_app _ (Sym ("<=", _), [t, u]) = SOME (mk_le t u) |
|
320 | mk_app _ (Sym (">", _), [t, u]) = SOME (mk_lt u t) |
|
321 | mk_app _ (Sym (">=", _), [t, u]) = SOME (mk_le u t) |
|
322 | mk_app _ (Sym ("+", _), [t, u]) = SOME (mk_add t u) |
|
323 | mk_app _ (Sym ("-", _), [t, u]) = SOME (mk_sub t u) |
|
324 | mk_app _ (Sym ("-", _), [t]) = SOME (mk_uminus t) |
|
325 | mk_app _ (Sym ("*", _), [t, u]) = SOME (mk_mul t u) |
|
326 | mk_app _ (Sym ("/", _), [t, u]) = SOME (mk_real_div t u) |
|
327 | mk_app _ (Sym ("div", _), [t, u]) = SOME (mk_int_div t u) |
|
328 | mk_app _ (Sym ("mod", _), [t, u]) = SOME (mk_mod t u) |
|
329 | mk_app _ (Sym ("select", _), [m, k]) = SOME (mk_access m k) |
|
330 | mk_app _ (Sym ("store", _), [m, k, v]) = SOME (mk_update m k v) |
|
331 | mk_app _ (Sym ("pattern", _), _) = SOME mk_true |
|
332 | mk_app (_, terms, _, _, _, _) (Sym (n, _), ts) = |
|
333 Symtab.lookup terms n |> Option.map (fn ct => mk_fun ct ts) |
|
334 |
|
335 fun add_expr k t (typs, terms, exprs, steps, vars, ctxt) = |
|
336 (typs, terms, Inttab.update (k, t) exprs, steps, vars, ctxt) |
|
337 |
|
338 fun lookup_expr (_, _, exprs, _, _, _) = Inttab.lookup exprs |
|
339 |
|
340 fun add_proof_step k ((r, prems), prop) cx = |
|
341 let |
|
342 val (typs, terms, exprs, steps, vars, ctxt) = cx |
|
343 val (ct, vs) = close ctxt prop |
|
344 val step = Proof_Step {rule=r, prems=prems, prop=ct} |
|
345 val vars' = union (op =) vs vars |
|
346 in (typs, terms, exprs, Inttab.update (k, step) steps, vars', ctxt) end |
|
347 |
|
348 fun finish (_, _, _, steps, vars, ctxt) = (steps, vars, ctxt) |
|
349 |
|
350 |
|
351 (* core parser *) |
|
352 |
|
353 fun parse_exn line_no msg = raise SMT_Solver.SMT ("Z3 proof parser (line " ^ |
|
354 string_of_int line_no ^ "): " ^ msg) |
|
355 |
|
356 fun scan_exn msg ((line_no, _), _) = parse_exn line_no msg |
|
357 |
|
358 fun with_info f cx = |
|
359 (case f ((NONE, 1), cx) of |
|
360 ((SOME root, _), cx') => (root, cx') |
|
361 | ((_, line_no), _) => parse_exn line_no "bad proof") |
|
362 |
|
363 fun parse_line _ _ (st as ((SOME _, _), _)) = st |
|
364 | parse_line scan line ((_, line_no), cx) = |
|
365 let val st = ((line_no, cx), explode line) |
|
366 in |
|
367 (case Scan.catch (Scan.finite' Symbol.stopper (Scan.option scan)) st of |
|
368 (SOME r, ((_, cx'), _)) => ((r, line_no+1), cx') |
|
369 | (NONE, _) => parse_exn line_no ("bad proof line: " ^ quote line)) |
|
370 end |
|
371 |
|
372 fun with_context f x ((line_no, cx), st) = |
|
373 let val (y, cx') = f x cx |
|
374 in (y, ((line_no, cx'), st)) end |
|
375 |
|
376 |
|
377 fun lookup_context f x (st as ((_, cx), _)) = (f cx x, st) |
|
378 |
|
379 |
|
380 (* parser combinators and parsers for basic entities *) |
|
381 |
|
382 fun $$ s = Scan.lift (Scan.$$ s) |
|
383 fun this s = Scan.lift (Scan.this_string s) |
|
384 fun blank st = Scan.lift (Scan.many1 Symbol.is_ascii_blank) st |
|
385 fun sep scan = blank |-- scan |
|
386 fun seps scan = Scan.repeat (sep scan) |
|
387 fun seps1 scan = Scan.repeat1 (sep scan) |
|
388 fun seps_by scan_sep scan = scan ::: Scan.repeat (scan_sep |-- scan) |
|
389 |
|
390 fun par scan = $$ "(" |-- scan --| $$ ")" |
|
391 fun bra scan = $$ "[" |-- scan --| $$ "]" |
|
392 |
|
393 val digit = (fn |
|
394 "0" => SOME 0 | "1" => SOME 1 | "2" => SOME 2 | "3" => SOME 3 | |
|
395 "4" => SOME 4 | "5" => SOME 5 | "6" => SOME 6 | "7" => SOME 7 | |
|
396 "8" => SOME 8 | "9" => SOME 9 | _ => NONE) |
|
397 |
|
398 fun mk_num ds = fold (fn d => fn i => i * 10 + d) ds 0 |
|
399 val nat_num = Scan.lift (Scan.repeat1 (Scan.some digit)) >> mk_num |
|
400 val int_num = Scan.optional ($$ "-" >> K (fn i => ~i)) I :|-- |
|
401 (fn sign => nat_num >> sign) |
|
402 |
|
403 val is_char = Symbol.is_ascii_letter orf Symbol.is_ascii_digit orf |
|
404 member (op =) (explode "_+*-/%~=<>$&|?!.@^#") |
|
405 val name = Scan.lift (Scan.many1 is_char) >> implode |
|
406 |
|
407 fun sym st = (name -- Scan.optional (bra (seps_by ($$ ":") sym)) [] >> Sym) st |
|
408 |
|
409 fun id st = ($$ "#" |-- nat_num) st |
|
410 |
|
411 |
|
412 (* parsers for various parts of Z3 proofs *) |
|
413 |
|
414 fun sort st = Scan.first [ |
|
415 this "bool" >> K @{typ bool}, |
|
416 this "int" >> K @{typ int}, |
|
417 this "real" >> K @{typ real}, |
|
418 this "bv" |-- bra nat_num >> mk_wordT, |
|
419 this "array" |-- bra (sort --| $$ ":" -- sort) >> (op -->), |
|
420 par (this "->" |-- seps1 sort) >> ((op --->) o split_last), |
|
421 name :|-- with_context typ_of_sort] st |
|
422 |
|
423 fun bound st = (par (this ":var" |-- sep nat_num -- sep sort) :|-- |
|
424 lookup_context (mk_bound o theory_of)) st |
|
425 |
|
426 fun number st = st |> ( |
|
427 int_num -- Scan.option ($$ "/" |-- int_num) --| this "::" :|-- |
|
428 (fn num as (n, _) => |
|
429 this "int" >> K (mk_int_num n) || |
|
430 this "real" >> K (mk_real_frac_num num))) |
|
431 |
|
432 fun bv_number st = (this "bv" |-- bra (nat_num --| $$ ":" -- nat_num) :|-- |
|
433 lookup_context (mk_bv_num o theory_of)) st |
|
434 |
|
435 fun appl (app as (Sym (n, _), _)) = lookup_context mk_app app :|-- (fn |
|
436 SOME app' => Scan.succeed app' |
|
437 | NONE => scan_exn ("unknown function: " ^ quote n)) |
|
438 |
|
439 fun constant st = ((sym >> rpair []) :|-- appl) st |
|
440 |
|
441 fun expr_id st = (id :|-- (fn i => lookup_context lookup_expr i :|-- (fn |
|
442 SOME e => Scan.succeed e |
|
443 | NONE => scan_exn ("unknown term id: " ^ quote (string_of_int i))))) st |
|
444 |
|
445 fun arg st = Scan.first [expr_id, number, bv_number, constant] st |
|
446 |
|
447 fun application st = par ((sym -- Scan.repeat1 (sep arg)) :|-- appl) st |
|
448 |
|
449 fun variables st = par (this "vars" |-- seps1 (par (name |-- sep sort))) st |
|
450 |
|
451 fun patterns st = seps (par ((this ":pat" || this ":nopat") |-- seps1 id)) st |
|
452 |
|
453 fun quant_kind st = st |> ( |
|
454 this "forall" >> K (mk_forall o theory_of) || |
|
455 this "exists" >> K (mk_exists o theory_of)) |
|
456 |
|
457 fun quantifier st = |
|
458 (par (quant_kind -- sep variables --| patterns -- sep arg) :|-- |
|
459 lookup_context (fn cx => fn ((mk_q, Ts), body) => mk_q cx Ts body)) st |
|
460 |
|
461 fun expr k = |
|
462 Scan.first [bound, quantifier, application, number, bv_number, constant] :|-- |
|
463 with_context (pair NONE oo add_expr k) |
|
464 |
|
465 fun rule_name st = ((name >> `(Symtab.lookup rule_names)) :|-- (fn |
|
466 (SOME r, _) => Scan.succeed r |
|
467 | (NONE, n) => scan_exn ("unknown proof rule: " ^ quote n))) st |
|
468 |
|
469 fun rule f k = |
|
470 bra (rule_name -- seps id) --| $$ ":" -- sep arg #-> |
|
471 with_context (pair (f k) oo add_proof_step k) |
|
472 |
|
473 fun decl st = (this "decl" |-- sep name --| sep (this "::") -- sep sort :|-- |
|
474 with_context (pair NONE oo add_decl)) st |
|
475 |
|
476 fun def st = (id --| sep (this ":=")) st |
|
477 |
|
478 fun node st = st |> ( |
|
479 decl || |
|
480 def :|-- (fn k => sep (expr k) || sep (rule (K NONE) k)) || |
|
481 rule SOME ~1) |
|
482 |
|
483 |
|
484 (* overall parser *) |
|
485 |
|
486 (* Currently, terms are parsed bottom-up (i.e., along with parsing the proof |
|
487 text line by line), but proofs are reconstructed top-down (i.e. by an |
|
488 in-order top-down traversal of the proof tree/graph). The latter approach |
|
489 was taken because some proof texts comprise irrelevant proof steps which |
|
490 will thus not be reconstructed. This approach might also be beneficial |
|
491 for constructing terms, but it would also increase the complexity of the |
|
492 (otherwise rather modular) code. *) |
|
493 |
|
494 fun parse ctxt typs terms proof_text = |
|
495 make_context ctxt typs terms |
|
496 |> with_info (fold (parse_line node) proof_text) |
|
497 ||> finish |
|
498 |
|
499 end |
|