author | wenzelm |
Thu, 02 Sep 2010 16:31:50 +0200 | |
changeset 39046 | 5b38730f3e12 |
parent 39020 | ac0f24f850c9 |
child 40162 | 7f58a9a843c2 |
permissions | -rw-r--r-- |
36898 | 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 = 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 |
||
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
32 |
structure I = Z3_Interface |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
33 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
34 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
35 |
|
36898 | 36 |
(** proof rules **) |
37 |
||
38 |
datatype rule = TrueAxiom | Asserted | Goal | ModusPonens | Reflexivity | |
|
39 |
Symmetry | Transitivity | TransitivityStar | Monotonicity | QuantIntro | |
|
40 |
Distributivity | AndElim | NotOrElim | Rewrite | RewriteStar | PullQuant | |
|
41 |
PullQuantStar | PushQuant | ElimUnusedVars | DestEqRes | QuantInst | |
|
42 |
Hypothesis | Lemma | UnitResolution | IffTrue | IffFalse | Commutativity | |
|
43 |
DefAxiom | IntroDef | ApplyDef | IffOeq | NnfPos | NnfNeg | NnfStar | |
|
44 |
CnfStar | Skolemize | ModusPonensOeq | ThLemma |
|
45 |
||
46 |
val rule_names = Symtab.make [ |
|
47 |
("true-axiom", TrueAxiom), |
|
48 |
("asserted", Asserted), |
|
49 |
("goal", Goal), |
|
50 |
("mp", ModusPonens), |
|
51 |
("refl", Reflexivity), |
|
52 |
("symm", Symmetry), |
|
53 |
("trans", Transitivity), |
|
54 |
("trans*", TransitivityStar), |
|
55 |
("monotonicity", Monotonicity), |
|
56 |
("quant-intro", QuantIntro), |
|
57 |
("distributivity", Distributivity), |
|
58 |
("and-elim", AndElim), |
|
59 |
("not-or-elim", NotOrElim), |
|
60 |
("rewrite", Rewrite), |
|
61 |
("rewrite*", RewriteStar), |
|
62 |
("pull-quant", PullQuant), |
|
63 |
("pull-quant*", PullQuantStar), |
|
64 |
("push-quant", PushQuant), |
|
65 |
("elim-unused", ElimUnusedVars), |
|
66 |
("der", DestEqRes), |
|
67 |
("quant-inst", QuantInst), |
|
68 |
("hypothesis", Hypothesis), |
|
69 |
("lemma", Lemma), |
|
70 |
("unit-resolution", UnitResolution), |
|
71 |
("iff-true", IffTrue), |
|
72 |
("iff-false", IffFalse), |
|
73 |
("commutativity", Commutativity), |
|
74 |
("def-axiom", DefAxiom), |
|
75 |
("intro-def", IntroDef), |
|
76 |
("apply-def", ApplyDef), |
|
77 |
("iff~", IffOeq), |
|
78 |
("nnf-pos", NnfPos), |
|
79 |
("nnf-neg", NnfNeg), |
|
80 |
("nnf*", NnfStar), |
|
81 |
("cnf*", CnfStar), |
|
82 |
("sk", Skolemize), |
|
83 |
("mp~", ModusPonensOeq), |
|
84 |
("th-lemma", ThLemma)] |
|
85 |
||
86 |
fun string_of_rule r = |
|
87 |
let fun eq_rule (s, r') = if r = r' then SOME s else NONE |
|
88 |
in the (Symtab.get_first eq_rule rule_names) end |
|
89 |
||
90 |
||
91 |
||
92 |
(** certified terms and variables **) |
|
93 |
||
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
94 |
val (var_prefix, decl_prefix) = ("v", "sk") |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
95 |
(* "decl_prefix" is for skolem constants (represented by free variables) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
96 |
"var_prefix" is for pseudo-schematic variables (schematic with respect |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
97 |
to the Z3 proof, but represented by free variables) |
36898 | 98 |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
99 |
Both prefixes must be distinct to avoid name interferences. |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
100 |
More precisely, the naming of pseudo-schematic variables must be |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
101 |
context-independent modulo the current proof context to be able to |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
102 |
use fast inference kernel rules during proof reconstruction. *) |
36898 | 103 |
|
104 |
fun certify ctxt = Thm.cterm_of (ProofContext.theory_of ctxt) |
|
105 |
||
106 |
val maxidx_of = #maxidx o Thm.rep_cterm |
|
107 |
||
108 |
fun mk_inst ctxt vars = |
|
109 |
let |
|
110 |
val max = fold (Integer.max o fst) vars 0 |
|
111 |
val ns = fst (Variable.variant_fixes (replicate (max + 1) var_prefix) ctxt) |
|
112 |
fun mk (i, v) = (v, certify ctxt (Free (nth ns i, #T (Thm.rep_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 mk_prop = Thm.capply @{cterm Trueprop} |
|
119 |
val names = fold (Term.add_free_names o Thm.term_of o snd) inst [] |
|
120 |
in (mk_prop (Thm.instantiate_cterm ([], inst) ct), names) end |
|
121 |
||
122 |
||
123 |
fun mk_bound thy (i, T) = |
|
124 |
let val ct = Thm.cterm_of thy (Var ((Name.uu, 0), T)) |
|
125 |
in (ct, [(i, ct)]) end |
|
126 |
||
127 |
local |
|
128 |
fun mk_quant thy q T (ct, vars) = |
|
129 |
let |
|
130 |
val cv = |
|
131 |
(case AList.lookup (op =) vars 0 of |
|
132 |
SOME cv => cv |
|
133 |
| _ => Thm.cterm_of thy (Var ((Name.uu, maxidx_of ct + 1), T))) |
|
134 |
fun dec (i, v) = if i = 0 then NONE else SOME (i-1, v) |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
135 |
in (Thm.capply (I.instT' cv q) (Thm.cabs cv ct), map_filter dec vars) end |
36898 | 136 |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
137 |
val forall = I.mk_inst_pair (I.destT1 o I.destT1) @{cpat All} |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
138 |
val exists = I.mk_inst_pair (I.destT1 o I.destT1) @{cpat Ex} |
36898 | 139 |
in |
140 |
fun mk_forall thy = fold_rev (mk_quant thy forall) |
|
141 |
fun mk_exists thy = fold_rev (mk_quant thy exists) |
|
142 |
end |
|
143 |
||
144 |
||
145 |
local |
|
146 |
fun equal_var cv (_, cu) = (cv aconvc cu) |
|
147 |
||
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
148 |
fun prep (ct, vars) (maxidx, all_vars) = |
36898 | 149 |
let |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
150 |
val maxidx' = maxidx_of ct + maxidx + 1 |
36898 | 151 |
|
152 |
fun part (v as (i, cv)) = |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
153 |
(case AList.lookup (op =) all_vars i of |
36898 | 154 |
SOME cu => apfst (if cu aconvc cv then I else cons (cv, cu)) |
155 |
| NONE => |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
156 |
if not (exists (equal_var cv) all_vars) then apsnd (cons v) |
36898 | 157 |
else |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
158 |
let val cv' = Thm.incr_indexes_cterm maxidx' cv |
36898 | 159 |
in apfst (cons (cv, cv')) #> apsnd (cons (i, cv')) end) |
160 |
||
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
161 |
val (inst, vars') = |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
162 |
if null vars then ([], vars) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
163 |
else fold part vars ([], []) |
36898 | 164 |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
165 |
in (Thm.instantiate_cterm ([], inst) ct, (maxidx', vars' @ all_vars)) end |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
166 |
in |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
167 |
fun mk_fun f ts = |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
168 |
let val (cts, (_, vars)) = fold_map prep ts (~1, []) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
169 |
in f cts |> Option.map (rpair vars) end |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
170 |
end |
36898 | 171 |
|
172 |
||
173 |
||
174 |
(** proof parser **) |
|
175 |
||
176 |
datatype proof_step = Proof_Step of { |
|
177 |
rule: rule, |
|
178 |
prems: int list, |
|
179 |
prop: cterm } |
|
180 |
||
181 |
||
182 |
(* parser context *) |
|
183 |
||
184 |
fun make_context ctxt typs terms = |
|
185 |
let |
|
186 |
val ctxt' = |
|
187 |
ctxt |
|
188 |
|> Symtab.fold (Variable.declare_typ o snd) typs |
|
189 |
|> Symtab.fold (Variable.declare_term o snd) terms |
|
190 |
||
191 |
fun cert @{term True} = @{cterm "~False"} |
|
192 |
| cert t = certify ctxt' t |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
193 |
|
39020 | 194 |
in (typs, Symtab.map (K cert) terms, Inttab.empty, Inttab.empty, [], ctxt') end |
36898 | 195 |
|
196 |
fun fresh_name n (typs, terms, exprs, steps, vars, ctxt) = |
|
197 |
let val (n', ctxt') = yield_singleton Variable.variant_fixes n ctxt |
|
198 |
in (n', (typs, terms, exprs, steps, vars, ctxt')) end |
|
199 |
||
200 |
fun theory_of (_, _, _, _, _, ctxt) = ProofContext.theory_of ctxt |
|
201 |
||
202 |
fun add_decl (n, T) (cx as (_, terms, _, _, _, _)) = |
|
203 |
(case Symtab.lookup terms n of |
|
204 |
SOME _ => cx |
|
205 |
| NONE => cx |> fresh_name (decl_prefix ^ n) |
|
206 |
|> (fn (m, (typs, terms, exprs, steps, vars, ctxt)) => |
|
207 |
let val upd = Symtab.update (n, certify ctxt (Free (m, T))) |
|
208 |
in (typs, upd terms, exprs, steps, vars, ctxt) end)) |
|
209 |
||
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
210 |
fun mk_typ (typs, _, _, _, _, ctxt) (s as I.Sym (n, _)) = |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
211 |
(case I.mk_builtin_typ ctxt s of |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
212 |
SOME T => SOME T |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
213 |
| NONE => Symtab.lookup typs n) |
36898 | 214 |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
215 |
fun mk_num (_, _, _, _, _, ctxt) (i, T) = |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
216 |
mk_fun (K (I.mk_builtin_num ctxt i T)) [] |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
217 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
218 |
fun mk_app (_, terms, _, _, _, ctxt) (s as I.Sym (n, _), es) = |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
219 |
mk_fun (fn cts => |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
220 |
(case I.mk_builtin_fun ctxt s cts of |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
221 |
SOME ct => SOME ct |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
222 |
| NONE => |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
223 |
Symtab.lookup terms n |> Option.map (Drule.list_comb o rpair cts))) es |
36898 | 224 |
|
225 |
fun add_expr k t (typs, terms, exprs, steps, vars, ctxt) = |
|
226 |
(typs, terms, Inttab.update (k, t) exprs, steps, vars, ctxt) |
|
227 |
||
228 |
fun lookup_expr (_, _, exprs, _, _, _) = Inttab.lookup exprs |
|
229 |
||
230 |
fun add_proof_step k ((r, prems), prop) cx = |
|
231 |
let |
|
232 |
val (typs, terms, exprs, steps, vars, ctxt) = cx |
|
233 |
val (ct, vs) = close ctxt prop |
|
234 |
val step = Proof_Step {rule=r, prems=prems, prop=ct} |
|
235 |
val vars' = union (op =) vs vars |
|
236 |
in (typs, terms, exprs, Inttab.update (k, step) steps, vars', ctxt) end |
|
237 |
||
238 |
fun finish (_, _, _, steps, vars, ctxt) = (steps, vars, ctxt) |
|
239 |
||
240 |
||
241 |
(* core parser *) |
|
242 |
||
243 |
fun parse_exn line_no msg = raise SMT_Solver.SMT ("Z3 proof parser (line " ^ |
|
244 |
string_of_int line_no ^ "): " ^ msg) |
|
245 |
||
246 |
fun scan_exn msg ((line_no, _), _) = parse_exn line_no msg |
|
247 |
||
248 |
fun with_info f cx = |
|
249 |
(case f ((NONE, 1), cx) of |
|
250 |
((SOME root, _), cx') => (root, cx') |
|
251 |
| ((_, line_no), _) => parse_exn line_no "bad proof") |
|
252 |
||
253 |
fun parse_line _ _ (st as ((SOME _, _), _)) = st |
|
254 |
| parse_line scan line ((_, line_no), cx) = |
|
255 |
let val st = ((line_no, cx), explode line) |
|
256 |
in |
|
257 |
(case Scan.catch (Scan.finite' Symbol.stopper (Scan.option scan)) st of |
|
258 |
(SOME r, ((_, cx'), _)) => ((r, line_no+1), cx') |
|
259 |
| (NONE, _) => parse_exn line_no ("bad proof line: " ^ quote line)) |
|
260 |
end |
|
261 |
||
262 |
fun with_context f x ((line_no, cx), st) = |
|
263 |
let val (y, cx') = f x cx |
|
264 |
in (y, ((line_no, cx'), st)) end |
|
265 |
||
266 |
||
267 |
fun lookup_context f x (st as ((_, cx), _)) = (f cx x, st) |
|
268 |
||
269 |
||
270 |
(* parser combinators and parsers for basic entities *) |
|
271 |
||
272 |
fun $$ s = Scan.lift (Scan.$$ s) |
|
273 |
fun this s = Scan.lift (Scan.this_string s) |
|
274 |
fun blank st = Scan.lift (Scan.many1 Symbol.is_ascii_blank) st |
|
275 |
fun sep scan = blank |-- scan |
|
276 |
fun seps scan = Scan.repeat (sep scan) |
|
277 |
fun seps1 scan = Scan.repeat1 (sep scan) |
|
278 |
fun seps_by scan_sep scan = scan ::: Scan.repeat (scan_sep |-- scan) |
|
279 |
||
280 |
fun par scan = $$ "(" |-- scan --| $$ ")" |
|
281 |
fun bra scan = $$ "[" |-- scan --| $$ "]" |
|
282 |
||
283 |
val digit = (fn |
|
284 |
"0" => SOME 0 | "1" => SOME 1 | "2" => SOME 2 | "3" => SOME 3 | |
|
285 |
"4" => SOME 4 | "5" => SOME 5 | "6" => SOME 6 | "7" => SOME 7 | |
|
286 |
"8" => SOME 8 | "9" => SOME 9 | _ => NONE) |
|
287 |
||
36940 | 288 |
fun digits st = (Scan.lift (Scan.many1 Symbol.is_ascii_digit) >> implode) st |
289 |
fun nat_num st = (Scan.lift (Scan.repeat1 (Scan.some digit)) >> (fn ds => |
|
290 |
fold (fn d => fn i => i * 10 + d) ds 0)) st |
|
291 |
fun int_num st = (Scan.optional ($$ "-" >> K (fn i => ~i)) I :|-- |
|
292 |
(fn sign => nat_num >> sign)) st |
|
36898 | 293 |
|
294 |
val is_char = Symbol.is_ascii_letter orf Symbol.is_ascii_digit orf |
|
295 |
member (op =) (explode "_+*-/%~=<>$&|?!.@^#") |
|
36940 | 296 |
fun name st = (Scan.lift (Scan.many1 is_char) >> implode) st |
36898 | 297 |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
298 |
fun sym st = |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
299 |
(name -- Scan.optional (bra (seps_by ($$ ":") sym)) [] >> I.Sym) st |
36898 | 300 |
|
301 |
fun id st = ($$ "#" |-- nat_num) st |
|
302 |
||
303 |
||
304 |
(* parsers for various parts of Z3 proofs *) |
|
305 |
||
306 |
fun sort st = Scan.first [ |
|
307 |
this "array" |-- bra (sort --| $$ ":" -- sort) >> (op -->), |
|
308 |
par (this "->" |-- seps1 sort) >> ((op --->) o split_last), |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
309 |
sym :|-- (fn s as I.Sym (n, _) => lookup_context mk_typ s :|-- (fn |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
310 |
SOME T => Scan.succeed T |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
311 |
| NONE => scan_exn ("unknown sort: " ^ quote n)))] st |
36898 | 312 |
|
313 |
fun bound st = (par (this ":var" |-- sep nat_num -- sep sort) :|-- |
|
314 |
lookup_context (mk_bound o theory_of)) st |
|
315 |
||
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
316 |
fun numb (n as (i, _)) = lookup_context mk_num n :|-- (fn |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
317 |
SOME n' => Scan.succeed n' |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
318 |
| NONE => scan_exn ("unknown number: " ^ quote (string_of_int i))) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
319 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
320 |
fun appl (app as (I.Sym (n, _), _)) = lookup_context mk_app app :|-- (fn |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
321 |
SOME app' => Scan.succeed app' |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
322 |
| NONE => scan_exn ("unknown function symbol: " ^ quote n)) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
323 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
324 |
fun bv_size st = (digits >> (fn sz => I.Sym ("bv", [I.Sym (sz, [])]))) st |
36898 | 325 |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
326 |
fun bv_number_sort st = (bv_size :|-- lookup_context mk_typ :|-- (fn |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
327 |
SOME cT => Scan.succeed cT |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
328 |
| NONE => scan_exn ("unknown sort: " ^ quote "bv"))) st |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
329 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
330 |
fun bv_number st = |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
331 |
(this "bv" |-- bra (nat_num --| $$ ":" -- bv_number_sort) :|-- numb) st |
36898 | 332 |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
333 |
fun frac_number st = ( |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
334 |
int_num --| $$ "/" -- int_num --| this "::" -- sort :|-- (fn ((i, j), T) => |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
335 |
numb (i, T) -- numb (j, T) :|-- (fn (n, m) => |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
336 |
appl (I.Sym ("/", []), [n, m])))) st |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
337 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
338 |
fun plain_number st = (int_num --| this "::" -- sort :|-- numb) st |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
339 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
340 |
fun number st = Scan.first [bv_number, frac_number, plain_number] st |
36898 | 341 |
|
342 |
fun constant st = ((sym >> rpair []) :|-- appl) st |
|
343 |
||
344 |
fun expr_id st = (id :|-- (fn i => lookup_context lookup_expr i :|-- (fn |
|
345 |
SOME e => Scan.succeed e |
|
346 |
| NONE => scan_exn ("unknown term id: " ^ quote (string_of_int i))))) st |
|
347 |
||
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
348 |
fun arg st = Scan.first [expr_id, number, constant] st |
36898 | 349 |
|
350 |
fun application st = par ((sym -- Scan.repeat1 (sep arg)) :|-- appl) st |
|
351 |
||
352 |
fun variables st = par (this "vars" |-- seps1 (par (name |-- sep sort))) st |
|
353 |
||
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
354 |
fun pats st = seps (par ((this ":pat" || this ":nopat") |-- seps1 id)) st |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
355 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
356 |
fun pattern st = par (this "pattern" |-- Scan.repeat1 (sep arg) >> |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
357 |
(the o mk_fun (K (SOME @{cterm True})))) st |
36898 | 358 |
|
359 |
fun quant_kind st = st |> ( |
|
360 |
this "forall" >> K (mk_forall o theory_of) || |
|
361 |
this "exists" >> K (mk_exists o theory_of)) |
|
362 |
||
363 |
fun quantifier st = |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
364 |
(par (quant_kind -- sep variables --| pats -- sep arg) :|-- |
36898 | 365 |
lookup_context (fn cx => fn ((mk_q, Ts), body) => mk_q cx Ts body)) st |
366 |
||
367 |
fun expr k = |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
368 |
Scan.first [bound, quantifier, pattern, application, number, constant] :|-- |
36898 | 369 |
with_context (pair NONE oo add_expr k) |
370 |
||
371 |
fun rule_name st = ((name >> `(Symtab.lookup rule_names)) :|-- (fn |
|
372 |
(SOME r, _) => Scan.succeed r |
|
373 |
| (NONE, n) => scan_exn ("unknown proof rule: " ^ quote n))) st |
|
374 |
||
375 |
fun rule f k = |
|
376 |
bra (rule_name -- seps id) --| $$ ":" -- sep arg #-> |
|
377 |
with_context (pair (f k) oo add_proof_step k) |
|
378 |
||
379 |
fun decl st = (this "decl" |-- sep name --| sep (this "::") -- sep sort :|-- |
|
380 |
with_context (pair NONE oo add_decl)) st |
|
381 |
||
382 |
fun def st = (id --| sep (this ":=")) st |
|
383 |
||
384 |
fun node st = st |> ( |
|
385 |
decl || |
|
386 |
def :|-- (fn k => sep (expr k) || sep (rule (K NONE) k)) || |
|
387 |
rule SOME ~1) |
|
388 |
||
389 |
||
390 |
(* overall parser *) |
|
391 |
||
392 |
(* Currently, terms are parsed bottom-up (i.e., along with parsing the proof |
|
393 |
text line by line), but proofs are reconstructed top-down (i.e. by an |
|
394 |
in-order top-down traversal of the proof tree/graph). The latter approach |
|
395 |
was taken because some proof texts comprise irrelevant proof steps which |
|
396 |
will thus not be reconstructed. This approach might also be beneficial |
|
397 |
for constructing terms, but it would also increase the complexity of the |
|
398 |
(otherwise rather modular) code. *) |
|
399 |
||
400 |
fun parse ctxt typs terms proof_text = |
|
401 |
make_context ctxt typs terms |
|
402 |
|> with_info (fold (parse_line node) proof_text) |
|
403 |
||> finish |
|
404 |
||
405 |
end |