author | boehmes |
Wed, 15 Dec 2010 08:39:24 +0100 | |
changeset 41123 | 3bb9be510a9d |
parent 41059 | d2b1fc1b8e19 |
child 41127 | 2ea84c8535c6 |
permissions | -rw-r--r-- |
36898 | 1 |
(* Title: HOL/Tools/SMT/smt_translate.ML |
2 |
Author: Sascha Boehme, TU Muenchen |
|
3 |
||
4 |
Translate theorems into an SMT intermediate format and serialize them. |
|
5 |
*) |
|
6 |
||
7 |
signature SMT_TRANSLATE = |
|
8 |
sig |
|
41123 | 9 |
(*intermediate term structure*) |
36898 | 10 |
datatype squant = SForall | SExists |
11 |
datatype 'a spattern = SPat of 'a list | SNoPat of 'a list |
|
12 |
datatype sterm = |
|
13 |
SVar of int | |
|
14 |
SApp of string * sterm list | |
|
15 |
SLet of string * sterm * sterm | |
|
40664 | 16 |
SQua of squant * string list * sterm spattern list * int option * sterm |
36898 | 17 |
|
41123 | 18 |
(*configuration options*) |
36898 | 19 |
type prefixes = {sort_prefix: string, func_prefix: string} |
20 |
type sign = { |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
21 |
header: string list, |
36898 | 22 |
sorts: string list, |
39298
5aefb5bc8a93
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents:
37124
diff
changeset
|
23 |
dtyps: (string * (string * (string * string) list) list) list list, |
36898 | 24 |
funcs: (string * (string list * string)) list } |
25 |
type config = { |
|
26 |
prefixes: prefixes, |
|
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
27 |
header: Proof.context -> term list -> string list, |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
28 |
is_fol: bool, |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
29 |
has_datatypes: bool, |
36898 | 30 |
serialize: string list -> sign -> sterm list -> string } |
31 |
type recon = { |
|
32 |
typs: typ Symtab.table, |
|
33 |
terms: term Symtab.table, |
|
34 |
unfolds: thm list, |
|
40161
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39535
diff
changeset
|
35 |
assms: (int * thm) list } |
36898 | 36 |
|
40161
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39535
diff
changeset
|
37 |
val translate: config -> Proof.context -> string list -> (int * thm) list -> |
36898 | 38 |
string * recon |
39 |
end |
|
40 |
||
41 |
structure SMT_Translate: SMT_TRANSLATE = |
|
42 |
struct |
|
43 |
||
40663 | 44 |
structure U = SMT_Utils |
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
45 |
structure B = SMT_Builtin |
40663 | 46 |
|
47 |
||
36898 | 48 |
(* intermediate term structure *) |
49 |
||
50 |
datatype squant = SForall | SExists |
|
51 |
||
52 |
datatype 'a spattern = SPat of 'a list | SNoPat of 'a list |
|
53 |
||
54 |
datatype sterm = |
|
55 |
SVar of int | |
|
56 |
SApp of string * sterm list | |
|
57 |
SLet of string * sterm * sterm | |
|
40664 | 58 |
SQua of squant * string list * sterm spattern list * int option * sterm |
36898 | 59 |
|
60 |
||
61 |
||
62 |
(* configuration options *) |
|
63 |
||
64 |
type prefixes = {sort_prefix: string, func_prefix: string} |
|
65 |
||
66 |
type sign = { |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
67 |
header: string list, |
36898 | 68 |
sorts: string list, |
39298
5aefb5bc8a93
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents:
37124
diff
changeset
|
69 |
dtyps: (string * (string * (string * string) list) list) list list, |
36898 | 70 |
funcs: (string * (string list * string)) list } |
71 |
||
72 |
type config = { |
|
73 |
prefixes: prefixes, |
|
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
74 |
header: Proof.context -> term list -> string list, |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
75 |
is_fol: bool, |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
76 |
has_datatypes: bool, |
36898 | 77 |
serialize: string list -> sign -> sterm list -> string } |
78 |
||
79 |
type recon = { |
|
80 |
typs: typ Symtab.table, |
|
81 |
terms: term Symtab.table, |
|
82 |
unfolds: thm list, |
|
40161
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39535
diff
changeset
|
83 |
assms: (int * thm) list } |
36898 | 84 |
|
85 |
||
86 |
||
87 |
(* utility functions *) |
|
88 |
||
89 |
val quantifier = (fn |
|
90 |
@{const_name All} => SOME SForall |
|
91 |
| @{const_name Ex} => SOME SExists |
|
92 |
| _ => NONE) |
|
93 |
||
94 |
fun group_quant qname Ts (t as Const (q, _) $ Abs (_, T, u)) = |
|
95 |
if q = qname then group_quant qname (T :: Ts) u else (Ts, t) |
|
96 |
| group_quant _ Ts t = (Ts, t) |
|
97 |
||
40664 | 98 |
fun dest_weight (@{const SMT.weight} $ w $ t) = |
99 |
(SOME (snd (HOLogic.dest_number w)), t) |
|
100 |
| dest_weight t = (NONE, t) |
|
101 |
||
37124 | 102 |
fun dest_pat (Const (@{const_name pat}, _) $ t) = (t, true) |
103 |
| dest_pat (Const (@{const_name nopat}, _) $ t) = (t, false) |
|
104 |
| dest_pat t = raise TERM ("dest_pat", [t]) |
|
105 |
||
106 |
fun dest_pats [] = I |
|
107 |
| dest_pats ts = |
|
108 |
(case map dest_pat ts |> split_list ||> distinct (op =) of |
|
109 |
(ps, [true]) => cons (SPat ps) |
|
110 |
| (ps, [false]) => cons (SNoPat ps) |
|
111 |
| _ => raise TERM ("dest_pats", ts)) |
|
36898 | 112 |
|
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:
40274
diff
changeset
|
113 |
fun dest_trigger (@{const trigger} $ tl $ t) = |
37124 | 114 |
(rev (fold (dest_pats o HOLogic.dest_list) (HOLogic.dest_list tl) []), t) |
36898 | 115 |
| dest_trigger t = ([], t) |
116 |
||
117 |
fun dest_quant qn T t = quantifier qn |> Option.map (fn q => |
|
118 |
let |
|
119 |
val (Ts, u) = group_quant qn [T] t |
|
40664 | 120 |
val (ps, p) = dest_trigger u |
121 |
val (w, b) = dest_weight p |
|
122 |
in (q, rev Ts, ps, w, b) end) |
|
36898 | 123 |
|
124 |
fun fold_map_pat f (SPat ts) = fold_map f ts #>> SPat |
|
125 |
| fold_map_pat f (SNoPat ts) = fold_map f ts #>> SNoPat |
|
126 |
||
127 |
fun prop_of thm = HOLogic.dest_Trueprop (Thm.prop_of thm) |
|
128 |
||
129 |
||
130 |
||
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
131 |
(* map HOL formulas to FOL formulas (i.e., separate formulas froms terms) *) |
36898 | 132 |
|
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
133 |
val tboolT = @{typ SMT.term_bool} |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
134 |
val term_true = Const (@{const_name True}, tboolT) |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
135 |
val term_false = Const (@{const_name False}, tboolT) |
36898 | 136 |
|
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
137 |
val term_bool = @{lemma "True ~= False" by simp} |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
138 |
val term_bool_prop = |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
139 |
let |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
140 |
fun replace @{const HOL.eq (bool)} = @{const HOL.eq (SMT.term_bool)} |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
141 |
| replace @{const True} = term_true |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
142 |
| replace @{const False} = term_false |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
143 |
| replace t = t |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
144 |
in Term.map_aterms replace (prop_of term_bool) end |
36898 | 145 |
|
146 |
val needs_rewrite = Thm.prop_of #> Term.exists_subterm (fn |
|
147 |
Const (@{const_name Let}, _) => 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:
40274
diff
changeset
|
148 |
| @{const HOL.eq (bool)} $ _ $ @{const True} => 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:
40274
diff
changeset
|
149 |
| Const (@{const_name If}, _) $ _ $ @{const True} $ @{const False} => true |
36898 | 150 |
| _ => false) |
151 |
||
152 |
val rewrite_rules = [ |
|
153 |
Let_def, |
|
154 |
@{lemma "P = True == P" by (rule eq_reflection) simp}, |
|
155 |
@{lemma "if P then True else False == P" by (rule eq_reflection) simp}] |
|
156 |
||
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
157 |
fun rewrite ctxt ct = |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
158 |
Conv.top_sweep_conv (fn ctxt' => |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
159 |
Conv.rewrs_conv rewrite_rules then_conv rewrite ctxt') ctxt ct |
36898 | 160 |
|
161 |
fun normalize ctxt thm = |
|
162 |
if needs_rewrite thm then Conv.fconv_rule (rewrite ctxt) thm else thm |
|
163 |
||
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
164 |
fun revert_typ @{typ SMT.term_bool} = @{typ bool} |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
165 |
| revert_typ (Type (n, Ts)) = Type (n, map revert_typ Ts) |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
166 |
| revert_typ T = T |
36898 | 167 |
|
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
168 |
val revert_types = Term.map_types revert_typ |
36898 | 169 |
|
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
170 |
fun folify ctxt = |
36898 | 171 |
let |
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
172 |
fun is_builtin_conn (@{const_name True}, _) _ = false |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
173 |
| is_builtin_conn (@{const_name False}, _) _ = false |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
174 |
| is_builtin_conn c ts = B.is_builtin_conn ctxt c ts |
36898 | 175 |
|
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
176 |
fun as_term t = @{const HOL.eq (SMT.term_bool)} $ t $ term_true |
40681
872b08416fb4
be more precise: only treat constant 'distinct' applied to an explicit list as built-in
boehmes
parents:
40664
diff
changeset
|
177 |
|
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
178 |
fun as_tbool @{typ bool} = tboolT |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
179 |
| as_tbool (Type (n, Ts)) = Type (n, map as_tbool Ts) |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
180 |
| as_tbool T = T |
36898 | 181 |
fun mapTs f g = Term.strip_type #> (fn (Ts, T) => map f Ts ---> g T) |
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
182 |
fun predT T = mapTs as_tbool I T |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
183 |
fun funcT T = mapTs as_tbool as_tbool T |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
184 |
fun func (n, T) = Const (n, funcT T) |
36898 | 185 |
|
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
186 |
fun map_ifT T = T |> Term.dest_funT ||> funcT |> (op -->) |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
187 |
val if_term = @{const If (bool)} |> Term.dest_Const ||> map_ifT |> Const |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
188 |
fun wrap_in_if t = if_term $ t $ term_true $ term_false |
36898 | 189 |
|
190 |
fun in_list T f t = HOLogic.mk_list T (map f (HOLogic.dest_list t)) |
|
191 |
||
192 |
fun in_term t = |
|
193 |
(case Term.strip_comb t of |
|
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
194 |
(Const (c as @{const_name If}, T), [t1, t2, t3]) => |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
195 |
Const (c, map_ifT T) $ in_form t1 $ in_term t2 $ in_term t3 |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
196 |
| (Const c, ts) => |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
197 |
if is_builtin_conn c ts orelse B.is_builtin_pred ctxt c ts |
36898 | 198 |
then wrap_in_if (in_form t) |
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
199 |
else Term.list_comb (func c, map in_term ts) |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
200 |
| (Free (n, T), ts) => Term.list_comb (Free (n, funcT T), map in_term ts) |
36898 | 201 |
| _ => t) |
202 |
||
40664 | 203 |
and in_weight ((c as @{const SMT.weight}) $ w $ t) = c $ w $ in_form t |
204 |
| in_weight t = in_form t |
|
205 |
||
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
206 |
and in_pat (Const (c as (@{const_name pat}, _)) $ t) = func c $ in_term t |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
207 |
| in_pat (Const (c as (@{const_name nopat}, _)) $ t) = func c $ in_term t |
36898 | 208 |
| in_pat t = raise TERM ("in_pat", [t]) |
209 |
||
37124 | 210 |
and in_pats ps = |
211 |
in_list @{typ "pattern list"} (in_list @{typ pattern} in_pat) ps |
|
36898 | 212 |
|
40664 | 213 |
and in_trig ((c as @{const trigger}) $ p $ t) = c $ in_pats p $ in_weight t |
214 |
| in_trig t = in_weight t |
|
36898 | 215 |
|
216 |
and in_form t = |
|
217 |
(case Term.strip_comb t of |
|
218 |
(q as Const (qn, _), [Abs (n, T, t')]) => |
|
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
219 |
if is_some (quantifier qn) then q $ Abs (n, as_tbool T, in_trig t') |
36898 | 220 |
else as_term (in_term t) |
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
221 |
| (Const (c as (n as @{const_name distinct}, T)), [t']) => |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
222 |
if B.is_builtin_fun ctxt c [t'] then |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
223 |
Const (n, predT T) $ in_list T in_term t' |
36898 | 224 |
else as_term (in_term t) |
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
225 |
| (Const (c as (n, T)), ts) => |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
226 |
if B.is_builtin_conn ctxt c ts |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
227 |
then Term.list_comb (Const c, map in_form ts) |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
228 |
else if B.is_builtin_pred ctxt c ts |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
229 |
then Term.list_comb (Const (n, predT T), map in_term ts) |
36898 | 230 |
else as_term (in_term t) |
231 |
| _ => as_term (in_term t)) |
|
232 |
in |
|
40161
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39535
diff
changeset
|
233 |
map (apsnd (normalize ctxt)) #> (fn irules => |
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
234 |
((rewrite_rules, (~1, term_bool) :: irules), |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
235 |
term_bool_prop :: map (in_form o prop_of o snd) irules)) |
36898 | 236 |
end |
237 |
||
238 |
||
239 |
||
240 |
(* translation from Isabelle terms into SMT intermediate terms *) |
|
241 |
||
39298
5aefb5bc8a93
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents:
37124
diff
changeset
|
242 |
val empty_context = (1, Typtab.empty, [], 1, Termtab.empty) |
36898 | 243 |
|
39298
5aefb5bc8a93
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents:
37124
diff
changeset
|
244 |
fun make_sign header (_, typs, dtyps, _, terms) = { |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
245 |
header = header, |
39298
5aefb5bc8a93
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents:
37124
diff
changeset
|
246 |
sorts = Typtab.fold (fn (_, (n, true)) => cons n | _ => I) typs [], |
5aefb5bc8a93
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents:
37124
diff
changeset
|
247 |
funcs = Termtab.fold (fn (_, (n, SOME ss)) => cons (n,ss) | _ => I) terms [], |
39435
5d18f4c00c07
reverse order of datatype declarations so that declarations only depend on already declared datatypes
boehmes
parents:
39298
diff
changeset
|
248 |
dtyps = rev dtyps } |
36898 | 249 |
|
39298
5aefb5bc8a93
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents:
37124
diff
changeset
|
250 |
fun make_recon (unfolds, assms) (_, typs, _, _, terms) = { |
5aefb5bc8a93
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents:
37124
diff
changeset
|
251 |
typs = Symtab.make (map (apfst fst o swap) (Typtab.dest typs)), |
5aefb5bc8a93
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents:
37124
diff
changeset
|
252 |
(*FIXME: don't drop the datatype information! *) |
36898 | 253 |
terms = Symtab.make (map (fn (t, (n, _)) => (n, t)) (Termtab.dest terms)), |
254 |
unfolds = unfolds, |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
255 |
assms = assms } |
36898 | 256 |
|
257 |
fun string_of_index pre i = pre ^ string_of_int i |
|
258 |
||
39298
5aefb5bc8a93
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents:
37124
diff
changeset
|
259 |
fun new_typ sort_prefix proper T (Tidx, typs, dtyps, idx, terms) = |
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
260 |
let |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
261 |
val s = string_of_index sort_prefix Tidx |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
262 |
val U = revert_typ T |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
263 |
in (s, (Tidx+1, Typtab.update (U, (s, proper)) typs, dtyps, idx, terms)) end |
39298
5aefb5bc8a93
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents:
37124
diff
changeset
|
264 |
|
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
265 |
fun lookup_typ (_, typs, _, _, _) = Typtab.lookup typs o revert_typ |
36898 | 266 |
|
39298
5aefb5bc8a93
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents:
37124
diff
changeset
|
267 |
fun fresh_typ T f cx = |
5aefb5bc8a93
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents:
37124
diff
changeset
|
268 |
(case lookup_typ cx T of |
5aefb5bc8a93
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents:
37124
diff
changeset
|
269 |
SOME (s, _) => (s, cx) |
5aefb5bc8a93
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents:
37124
diff
changeset
|
270 |
| NONE => f T cx) |
5aefb5bc8a93
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents:
37124
diff
changeset
|
271 |
|
5aefb5bc8a93
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents:
37124
diff
changeset
|
272 |
fun new_fun func_prefix t ss (Tidx, typs, dtyps, idx, terms) = |
5aefb5bc8a93
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents:
37124
diff
changeset
|
273 |
let |
5aefb5bc8a93
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents:
37124
diff
changeset
|
274 |
val f = string_of_index func_prefix idx |
5aefb5bc8a93
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents:
37124
diff
changeset
|
275 |
val terms' = Termtab.update (revert_types t, (f, ss)) terms |
5aefb5bc8a93
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents:
37124
diff
changeset
|
276 |
in (f, (Tidx, typs, dtyps, idx+1, terms')) end |
5aefb5bc8a93
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents:
37124
diff
changeset
|
277 |
|
5aefb5bc8a93
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents:
37124
diff
changeset
|
278 |
fun fresh_fun func_prefix t ss (cx as (_, _, _, _, terms)) = |
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
279 |
(case Termtab.lookup terms (revert_types t) of |
36898 | 280 |
SOME (f, _) => (f, cx) |
39298
5aefb5bc8a93
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents:
37124
diff
changeset
|
281 |
| NONE => new_fun func_prefix t ss cx) |
5aefb5bc8a93
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents:
37124
diff
changeset
|
282 |
|
39483
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
39435
diff
changeset
|
283 |
fun mk_type (_, Tfs) (d as Datatype.DtTFree _) = the (AList.lookup (op =) Tfs d) |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
39435
diff
changeset
|
284 |
| mk_type Ts (Datatype.DtType (n, ds)) = Type (n, map (mk_type Ts) ds) |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
39435
diff
changeset
|
285 |
| mk_type (Tds, _) (Datatype.DtRec i) = nth Tds i |
39298
5aefb5bc8a93
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents:
37124
diff
changeset
|
286 |
|
39483
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
39435
diff
changeset
|
287 |
fun mk_selector ctxt Ts T n (i, d) = |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
39435
diff
changeset
|
288 |
(case Datatype_Selectors.lookup_selector ctxt (n, i+1) of |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
39435
diff
changeset
|
289 |
NONE => raise Fail ("missing selector for datatype constructor " ^ quote n) |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
39435
diff
changeset
|
290 |
| SOME m => mk_type Ts d |> (fn U => (Const (m, T --> U), U))) |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
39435
diff
changeset
|
291 |
|
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
39435
diff
changeset
|
292 |
fun mk_constructor ctxt Ts T (n, args) = |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
39435
diff
changeset
|
293 |
let val (sels, Us) = split_list (map_index (mk_selector ctxt Ts T n) args) |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
39435
diff
changeset
|
294 |
in (Const (n, Us ---> T), sels) end |
39298
5aefb5bc8a93
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents:
37124
diff
changeset
|
295 |
|
39535
cd1bb7125d8a
do not treat natural numbers as a datatype (natural numbers are considered an abstract type with a coercion to integers)
boehmes
parents:
39483
diff
changeset
|
296 |
fun lookup_datatype ctxt n Ts = |
cd1bb7125d8a
do not treat natural numbers as a datatype (natural numbers are considered an abstract type with a coercion to integers)
boehmes
parents:
39483
diff
changeset
|
297 |
if member (op =) [@{type_name bool}, @{type_name nat}] n then NONE |
cd1bb7125d8a
do not treat natural numbers as a datatype (natural numbers are considered an abstract type with a coercion to integers)
boehmes
parents:
39483
diff
changeset
|
298 |
else |
cd1bb7125d8a
do not treat natural numbers as a datatype (natural numbers are considered an abstract type with a coercion to integers)
boehmes
parents:
39483
diff
changeset
|
299 |
Datatype.get_info (ProofContext.theory_of ctxt) n |
cd1bb7125d8a
do not treat natural numbers as a datatype (natural numbers are considered an abstract type with a coercion to integers)
boehmes
parents:
39483
diff
changeset
|
300 |
|> Option.map (fn {descr, ...} => |
cd1bb7125d8a
do not treat natural numbers as a datatype (natural numbers are considered an abstract type with a coercion to integers)
boehmes
parents:
39483
diff
changeset
|
301 |
let |
cd1bb7125d8a
do not treat natural numbers as a datatype (natural numbers are considered an abstract type with a coercion to integers)
boehmes
parents:
39483
diff
changeset
|
302 |
val Tds = map (fn (_, (tn, _, _)) => Type (tn, Ts)) |
cd1bb7125d8a
do not treat natural numbers as a datatype (natural numbers are considered an abstract type with a coercion to integers)
boehmes
parents:
39483
diff
changeset
|
303 |
(sort (int_ord o pairself fst) descr) |
cd1bb7125d8a
do not treat natural numbers as a datatype (natural numbers are considered an abstract type with a coercion to integers)
boehmes
parents:
39483
diff
changeset
|
304 |
val Tfs = (case hd descr of (_, (_, tfs, _)) => tfs ~~ Ts) |
cd1bb7125d8a
do not treat natural numbers as a datatype (natural numbers are considered an abstract type with a coercion to integers)
boehmes
parents:
39483
diff
changeset
|
305 |
in |
cd1bb7125d8a
do not treat natural numbers as a datatype (natural numbers are considered an abstract type with a coercion to integers)
boehmes
parents:
39483
diff
changeset
|
306 |
descr |> map (fn (i, (_, _, cs)) => |
cd1bb7125d8a
do not treat natural numbers as a datatype (natural numbers are considered an abstract type with a coercion to integers)
boehmes
parents:
39483
diff
changeset
|
307 |
(nth Tds i, map (mk_constructor ctxt (Tds, Tfs) (nth Tds i)) cs)) |
cd1bb7125d8a
do not treat natural numbers as a datatype (natural numbers are considered an abstract type with a coercion to integers)
boehmes
parents:
39483
diff
changeset
|
308 |
end) |
36898 | 309 |
|
40161
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39535
diff
changeset
|
310 |
fun relaxed irules = (([], irules), map (prop_of o snd) irules) |
36898 | 311 |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
312 |
fun with_context header f (ths, ts) = |
36898 | 313 |
let val (us, context) = fold_map f ts empty_context |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
314 |
in ((make_sign (header ts) context, us), make_recon ths context) end |
36898 | 315 |
|
316 |
||
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
317 |
fun translate config ctxt comments = |
36898 | 318 |
let |
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
319 |
val {prefixes, is_fol, header, has_datatypes, serialize} = config |
36898 | 320 |
val {sort_prefix, func_prefix} = prefixes |
39298
5aefb5bc8a93
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents:
37124
diff
changeset
|
321 |
|
5aefb5bc8a93
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents:
37124
diff
changeset
|
322 |
fun transT (T as TFree _) = fresh_typ T (new_typ sort_prefix true) |
5aefb5bc8a93
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents:
37124
diff
changeset
|
323 |
| transT (T as TVar _) = (fn _ => raise TYPE ("smt_translate", [T], [])) |
5aefb5bc8a93
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents:
37124
diff
changeset
|
324 |
| transT (T as Type (n, Ts)) = |
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
325 |
(case B.builtin_typ ctxt T of |
39298
5aefb5bc8a93
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents:
37124
diff
changeset
|
326 |
SOME n => pair n |
5aefb5bc8a93
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents:
37124
diff
changeset
|
327 |
| NONE => fresh_typ T (fn _ => fn cx => |
5aefb5bc8a93
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents:
37124
diff
changeset
|
328 |
if not has_datatypes then new_typ sort_prefix true T cx |
5aefb5bc8a93
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents:
37124
diff
changeset
|
329 |
else |
5aefb5bc8a93
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents:
37124
diff
changeset
|
330 |
(case lookup_datatype ctxt n Ts of |
5aefb5bc8a93
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents:
37124
diff
changeset
|
331 |
NONE => new_typ sort_prefix true T cx |
5aefb5bc8a93
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents:
37124
diff
changeset
|
332 |
| SOME dts => |
5aefb5bc8a93
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents:
37124
diff
changeset
|
333 |
let val cx' = new_dtyps dts cx |
5aefb5bc8a93
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents:
37124
diff
changeset
|
334 |
in (fst (the (lookup_typ cx' T)), cx') end))) |
36898 | 335 |
|
39298
5aefb5bc8a93
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents:
37124
diff
changeset
|
336 |
and new_dtyps dts cx = |
5aefb5bc8a93
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents:
37124
diff
changeset
|
337 |
let |
5aefb5bc8a93
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents:
37124
diff
changeset
|
338 |
fun new_decl i t = |
40663 | 339 |
let val (Ts, T) = U.dest_funT i (Term.fastype_of t) |
39298
5aefb5bc8a93
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents:
37124
diff
changeset
|
340 |
in |
5aefb5bc8a93
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents:
37124
diff
changeset
|
341 |
fold_map transT Ts ##>> transT T ##>> |
5aefb5bc8a93
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents:
37124
diff
changeset
|
342 |
new_fun func_prefix t NONE #>> swap |
5aefb5bc8a93
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents:
37124
diff
changeset
|
343 |
end |
5aefb5bc8a93
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents:
37124
diff
changeset
|
344 |
fun new_dtyp_decl (con, sels) = |
5aefb5bc8a93
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents:
37124
diff
changeset
|
345 |
new_decl (length sels) con ##>> fold_map (new_decl 1) sels #>> |
5aefb5bc8a93
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents:
37124
diff
changeset
|
346 |
(fn ((con', _), sels') => (con', map (apsnd snd) sels')) |
5aefb5bc8a93
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents:
37124
diff
changeset
|
347 |
in |
5aefb5bc8a93
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents:
37124
diff
changeset
|
348 |
cx |
5aefb5bc8a93
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents:
37124
diff
changeset
|
349 |
|> fold_map (new_typ sort_prefix false o fst) dts |
5aefb5bc8a93
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents:
37124
diff
changeset
|
350 |
||>> fold_map (fold_map new_dtyp_decl o snd) dts |
5aefb5bc8a93
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents:
37124
diff
changeset
|
351 |
|-> (fn (ss, decls) => fn (Tidx, typs, dtyps, idx, terms) => |
5aefb5bc8a93
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents:
37124
diff
changeset
|
352 |
(Tidx, typs, (ss ~~ decls) :: dtyps, idx, terms)) |
5aefb5bc8a93
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents:
37124
diff
changeset
|
353 |
end |
36898 | 354 |
|
355 |
fun app n ts = SApp (n, ts) |
|
356 |
||
357 |
fun trans t = |
|
358 |
(case Term.strip_comb t of |
|
359 |
(Const (qn, _), [Abs (_, T, t1)]) => |
|
360 |
(case dest_quant qn T t1 of |
|
40664 | 361 |
SOME (q, Ts, ps, w, b) => |
36898 | 362 |
fold_map transT Ts ##>> fold_map (fold_map_pat trans) ps ##>> |
40664 | 363 |
trans b #>> (fn ((Ts', ps'), b') => SQua (q, Ts', ps', w, b')) |
36898 | 364 |
| NONE => raise TERM ("intermediate", [t])) |
365 |
| (Const (@{const_name Let}, _), [t1, Abs (_, T, t2)]) => |
|
366 |
transT T ##>> trans t1 ##>> trans t2 #>> |
|
367 |
(fn ((U, u1), u2) => SLet (U, u1, u2)) |
|
40681
872b08416fb4
be more precise: only treat constant 'distinct' applied to an explicit list as built-in
boehmes
parents:
40664
diff
changeset
|
368 |
| (h as Const (c as (@{const_name distinct}, T)), ts) => |
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
369 |
(case B.builtin_fun ctxt c ts of |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
370 |
SOME (n, ts) => fold_map trans ts #>> app n |
40681
872b08416fb4
be more precise: only treat constant 'distinct' applied to an explicit list as built-in
boehmes
parents:
40664
diff
changeset
|
371 |
| NONE => transs h T ts) |
36898 | 372 |
| (h as Const (c as (_, T)), ts) => |
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
373 |
(case B.builtin_num ctxt t of |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
374 |
SOME n => pair (SApp (n, [])) |
36898 | 375 |
| NONE => |
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
376 |
(case B.builtin_fun ctxt c ts of |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
377 |
SOME (n, ts') => fold_map trans ts' #>> app n |
36898 | 378 |
| NONE => transs h T ts)) |
379 |
| (h as Free (_, T), ts) => transs h T ts |
|
380 |
| (Bound i, []) => pair (SVar i) |
|
40697 | 381 |
| (Abs (_, _, t1 $ Bound 0), []) => |
382 |
if not (loose_bvar1 (t1, 0)) then trans t1 (* eta-reduce on the fly *) |
|
383 |
else raise TERM ("smt_translate", [t]) |
|
39298
5aefb5bc8a93
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents:
37124
diff
changeset
|
384 |
| _ => raise TERM ("smt_translate", [t])) |
36898 | 385 |
|
386 |
and transs t T ts = |
|
40663 | 387 |
let val (Us, U) = U.dest_funT (length ts) T |
36898 | 388 |
in |
389 |
fold_map transT Us ##>> transT U #-> (fn Up => |
|
39298
5aefb5bc8a93
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents:
37124
diff
changeset
|
390 |
fresh_fun func_prefix t (SOME Up) ##>> fold_map trans ts #>> SApp) |
36898 | 391 |
end |
392 |
in |
|
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
393 |
(if is_fol then folify ctxt else relaxed) #> |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
394 |
with_context (header ctxt) trans #>> uncurry (serialize comments) |
36898 | 395 |
end |
396 |
||
397 |
end |