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