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