|
1 (* Title: HOL/Library/Old_SMT/old_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 OLD_SMT_TRANSLATE = |
|
8 sig |
|
9 (*intermediate term structure*) |
|
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 | |
|
16 SQua of squant * string list * sterm spattern list * int option * sterm |
|
17 |
|
18 (*translation configuration*) |
|
19 type prefixes = {sort_prefix: string, func_prefix: string} |
|
20 type sign = { |
|
21 header: string list, |
|
22 sorts: string list, |
|
23 dtyps: (string * (string * (string * string) list) list) list list, |
|
24 funcs: (string * (string list * string)) list } |
|
25 type config = { |
|
26 prefixes: prefixes, |
|
27 header: term list -> string list, |
|
28 is_fol: bool, |
|
29 has_datatypes: bool, |
|
30 serialize: string list -> sign -> sterm list -> string } |
|
31 type recon = { |
|
32 context: Proof.context, |
|
33 typs: typ Symtab.table, |
|
34 terms: term Symtab.table, |
|
35 rewrite_rules: thm list, |
|
36 assms: (int * thm) list } |
|
37 |
|
38 (*translation*) |
|
39 val add_config: Old_SMT_Utils.class * (Proof.context -> config) -> |
|
40 Context.generic -> Context.generic |
|
41 val translate: Proof.context -> string list -> (int * thm) list -> |
|
42 string * recon |
|
43 end |
|
44 |
|
45 structure Old_SMT_Translate: OLD_SMT_TRANSLATE = |
|
46 struct |
|
47 |
|
48 |
|
49 (* intermediate term structure *) |
|
50 |
|
51 datatype squant = SForall | SExists |
|
52 |
|
53 datatype 'a spattern = SPat of 'a list | SNoPat of 'a list |
|
54 |
|
55 datatype sterm = |
|
56 SVar of int | |
|
57 SApp of string * sterm list | |
|
58 SLet of string * sterm * sterm | |
|
59 SQua of squant * string list * sterm spattern list * int option * sterm |
|
60 |
|
61 |
|
62 |
|
63 (* translation configuration *) |
|
64 |
|
65 type prefixes = {sort_prefix: string, func_prefix: string} |
|
66 |
|
67 type sign = { |
|
68 header: string list, |
|
69 sorts: string list, |
|
70 dtyps: (string * (string * (string * string) list) list) list list, |
|
71 funcs: (string * (string list * string)) list } |
|
72 |
|
73 type config = { |
|
74 prefixes: prefixes, |
|
75 header: term list -> string list, |
|
76 is_fol: bool, |
|
77 has_datatypes: bool, |
|
78 serialize: string list -> sign -> sterm list -> string } |
|
79 |
|
80 type recon = { |
|
81 context: Proof.context, |
|
82 typs: typ Symtab.table, |
|
83 terms: term Symtab.table, |
|
84 rewrite_rules: thm list, |
|
85 assms: (int * thm) list } |
|
86 |
|
87 |
|
88 |
|
89 (* translation context *) |
|
90 |
|
91 fun make_tr_context {sort_prefix, func_prefix} = |
|
92 (sort_prefix, 1, Typtab.empty, func_prefix, 1, Termtab.empty) |
|
93 |
|
94 fun string_of_index pre i = pre ^ string_of_int i |
|
95 |
|
96 fun add_typ T proper (cx as (sp, Tidx, typs, fp, idx, terms)) = |
|
97 (case Typtab.lookup typs T of |
|
98 SOME (n, _) => (n, cx) |
|
99 | NONE => |
|
100 let |
|
101 val n = string_of_index sp Tidx |
|
102 val typs' = Typtab.update (T, (n, proper)) typs |
|
103 in (n, (sp, Tidx+1, typs', fp, idx, terms)) end) |
|
104 |
|
105 fun add_fun t sort (cx as (sp, Tidx, typs, fp, idx, terms)) = |
|
106 (case Termtab.lookup terms t of |
|
107 SOME (n, _) => (n, cx) |
|
108 | NONE => |
|
109 let |
|
110 val n = string_of_index fp idx |
|
111 val terms' = Termtab.update (t, (n, sort)) terms |
|
112 in (n, (sp, Tidx, typs, fp, idx+1, terms')) end) |
|
113 |
|
114 fun sign_of header dtyps (_, _, typs, _, _, terms) = { |
|
115 header = header, |
|
116 sorts = Typtab.fold (fn (_, (n, true)) => cons n | _ => I) typs [], |
|
117 dtyps = dtyps, |
|
118 funcs = Termtab.fold (fn (_, (n, SOME ss)) => cons (n,ss) | _ => I) terms []} |
|
119 |
|
120 fun recon_of ctxt rules thms ithms (_, _, typs, _, _, terms) = |
|
121 let |
|
122 fun add_typ (T, (n, _)) = Symtab.update (n, T) |
|
123 val typs' = Typtab.fold add_typ typs Symtab.empty |
|
124 |
|
125 fun add_fun (t, (n, _)) = Symtab.update (n, t) |
|
126 val terms' = Termtab.fold add_fun terms Symtab.empty |
|
127 |
|
128 val assms = map (pair ~1) thms @ ithms |
|
129 in |
|
130 {context=ctxt, typs=typs', terms=terms', rewrite_rules=rules, assms=assms} |
|
131 end |
|
132 |
|
133 |
|
134 |
|
135 (* preprocessing *) |
|
136 |
|
137 (** datatype declarations **) |
|
138 |
|
139 fun collect_datatypes_and_records (tr_context, ctxt) ts = |
|
140 let |
|
141 val (declss, ctxt') = |
|
142 fold (Term.fold_types Old_SMT_Datatypes.add_decls) ts ([], ctxt) |
|
143 |
|
144 fun is_decl_typ T = exists (exists (equal T o fst)) declss |
|
145 |
|
146 fun add_typ' T proper = |
|
147 (case Old_SMT_Builtin.dest_builtin_typ ctxt' T of |
|
148 SOME n => pair n |
|
149 | NONE => add_typ T proper) |
|
150 |
|
151 fun tr_select sel = |
|
152 let val T = Term.range_type (Term.fastype_of sel) |
|
153 in add_fun sel NONE ##>> add_typ' T (not (is_decl_typ T)) end |
|
154 fun tr_constr (constr, selects) = |
|
155 add_fun constr NONE ##>> fold_map tr_select selects |
|
156 fun tr_typ (T, cases) = add_typ' T false ##>> fold_map tr_constr cases |
|
157 val (declss', tr_context') = fold_map (fold_map tr_typ) declss tr_context |
|
158 |
|
159 fun add (constr, selects) = |
|
160 Termtab.update (constr, length selects) #> |
|
161 fold (Termtab.update o rpair 1) selects |
|
162 val funcs = fold (fold (fold add o snd)) declss Termtab.empty |
|
163 in ((funcs, declss', tr_context', ctxt'), ts) end |
|
164 (* FIXME: also return necessary datatype and record theorems *) |
|
165 |
|
166 |
|
167 (** eta-expand quantifiers, let expressions and built-ins *) |
|
168 |
|
169 local |
|
170 fun eta f T t = Abs (Name.uu, T, f (Term.incr_boundvars 1 t $ Bound 0)) |
|
171 |
|
172 fun exp f T = eta f (Term.domain_type (Term.domain_type T)) |
|
173 |
|
174 fun exp2 T q = |
|
175 let val U = Term.domain_type T |
|
176 in Abs (Name.uu, U, q $ eta I (Term.domain_type U) (Bound 0)) end |
|
177 |
|
178 fun exp2' T l = |
|
179 let val (U1, U2) = Term.dest_funT T ||> Term.domain_type |
|
180 in Abs (Name.uu, U1, eta I U2 (l $ Bound 0)) end |
|
181 |
|
182 fun expf k i T t = |
|
183 let val Ts = drop i (fst (Old_SMT_Utils.dest_funT k T)) |
|
184 in |
|
185 Term.incr_boundvars (length Ts) t |
|
186 |> fold_rev (fn i => fn u => u $ Bound i) (0 upto length Ts - 1) |
|
187 |> fold_rev (fn T => fn u => Abs (Name.uu, T, u)) Ts |
|
188 end |
|
189 in |
|
190 |
|
191 fun eta_expand ctxt is_fol funcs = |
|
192 let |
|
193 fun exp_func t T ts = |
|
194 (case Termtab.lookup funcs t of |
|
195 SOME k => |
|
196 Term.list_comb (t, ts) |
|
197 |> k <> length ts ? expf k (length ts) T |
|
198 | NONE => Term.list_comb (t, ts)) |
|
199 |
|
200 fun expand ((q as Const (@{const_name All}, _)) $ Abs a) = q $ abs_expand a |
|
201 | expand ((q as Const (@{const_name All}, T)) $ t) = q $ exp expand T t |
|
202 | expand (q as Const (@{const_name All}, T)) = exp2 T q |
|
203 | expand ((q as Const (@{const_name Ex}, _)) $ Abs a) = q $ abs_expand a |
|
204 | expand ((q as Const (@{const_name Ex}, T)) $ t) = q $ exp expand T t |
|
205 | expand (q as Const (@{const_name Ex}, T)) = exp2 T q |
|
206 | expand ((l as Const (@{const_name Let}, _)) $ t $ Abs a) = |
|
207 if is_fol then expand (Term.betapply (Abs a, t)) |
|
208 else l $ expand t $ abs_expand a |
|
209 | expand ((l as Const (@{const_name Let}, T)) $ t $ u) = |
|
210 if is_fol then expand (u $ t) |
|
211 else l $ expand t $ exp expand (Term.range_type T) u |
|
212 | expand ((l as Const (@{const_name Let}, T)) $ t) = |
|
213 if is_fol then |
|
214 let val U = Term.domain_type (Term.range_type T) |
|
215 in Abs (Name.uu, U, Bound 0 $ Term.incr_boundvars 1 t) end |
|
216 else exp2 T (l $ expand t) |
|
217 | expand (l as Const (@{const_name Let}, T)) = |
|
218 if is_fol then |
|
219 let val U = Term.domain_type (Term.range_type T) |
|
220 in |
|
221 Abs (Name.uu, Term.domain_type T, Abs (Name.uu, U, |
|
222 Bound 0 $ Bound 1)) |
|
223 end |
|
224 else exp2' T l |
|
225 | expand t = |
|
226 (case Term.strip_comb t of |
|
227 (u as Const (c as (_, T)), ts) => |
|
228 (case Old_SMT_Builtin.dest_builtin ctxt c ts of |
|
229 SOME (_, k, us, mk) => |
|
230 if k = length us then mk (map expand us) |
|
231 else if k < length us then |
|
232 chop k (map expand us) |>> mk |> Term.list_comb |
|
233 else expf k (length ts) T (mk (map expand us)) |
|
234 | NONE => exp_func u T (map expand ts)) |
|
235 | (u as Free (_, T), ts) => exp_func u T (map expand ts) |
|
236 | (Abs a, ts) => Term.list_comb (abs_expand a, map expand ts) |
|
237 | (u, ts) => Term.list_comb (u, map expand ts)) |
|
238 |
|
239 and abs_expand (n, T, t) = Abs (n, T, expand t) |
|
240 |
|
241 in map expand end |
|
242 |
|
243 end |
|
244 |
|
245 |
|
246 (** introduce explicit applications **) |
|
247 |
|
248 local |
|
249 (* |
|
250 Make application explicit for functions with varying number of arguments. |
|
251 *) |
|
252 |
|
253 fun add t i = apfst (Termtab.map_default (t, i) (Integer.min i)) |
|
254 fun add_type T = apsnd (Typtab.update (T, ())) |
|
255 |
|
256 fun min_arities t = |
|
257 (case Term.strip_comb t of |
|
258 (u as Const _, ts) => add u (length ts) #> fold min_arities ts |
|
259 | (u as Free _, ts) => add u (length ts) #> fold min_arities ts |
|
260 | (Abs (_, T, u), ts) => add_type T #> min_arities u #> fold min_arities ts |
|
261 | (_, ts) => fold min_arities ts) |
|
262 |
|
263 fun minimize types t i = |
|
264 let |
|
265 fun find_min j [] _ = j |
|
266 | find_min j (U :: Us) T = |
|
267 if Typtab.defined types T then j |
|
268 else find_min (j + 1) Us (U --> T) |
|
269 |
|
270 val (Ts, T) = Term.strip_type (Term.type_of t) |
|
271 in find_min 0 (take i (rev Ts)) T end |
|
272 |
|
273 fun app u (t, T) = |
|
274 (Const (@{const_name fun_app}, T --> T) $ t $ u, Term.range_type T) |
|
275 |
|
276 fun apply i t T ts = |
|
277 let |
|
278 val (ts1, ts2) = chop i ts |
|
279 val (_, U) = Old_SMT_Utils.dest_funT i T |
|
280 in fst (fold app ts2 (Term.list_comb (t, ts1), U)) end |
|
281 in |
|
282 |
|
283 fun intro_explicit_application ctxt funcs ts = |
|
284 let |
|
285 val (arities, types) = fold min_arities ts (Termtab.empty, Typtab.empty) |
|
286 val arities' = Termtab.map (minimize types) arities |
|
287 |
|
288 fun app_func t T ts = |
|
289 if is_some (Termtab.lookup funcs t) then Term.list_comb (t, ts) |
|
290 else apply (the (Termtab.lookup arities' t)) t T ts |
|
291 |
|
292 fun in_list T f t = HOLogic.mk_list T (map f (HOLogic.dest_list t)) |
|
293 |
|
294 fun traverse Ts t = |
|
295 (case Term.strip_comb t of |
|
296 (q as Const (@{const_name All}, _), [Abs (x, T, u)]) => |
|
297 q $ Abs (x, T, in_trigger (T :: Ts) u) |
|
298 | (q as Const (@{const_name Ex}, _), [Abs (x, T, u)]) => |
|
299 q $ Abs (x, T, in_trigger (T :: Ts) u) |
|
300 | (q as Const (@{const_name Let}, _), [u1, u2 as Abs _]) => |
|
301 q $ traverse Ts u1 $ traverse Ts u2 |
|
302 | (u as Const (c as (_, T)), ts) => |
|
303 (case Old_SMT_Builtin.dest_builtin ctxt c ts of |
|
304 SOME (_, k, us, mk) => |
|
305 let |
|
306 val (ts1, ts2) = chop k (map (traverse Ts) us) |
|
307 val U = Term.strip_type T |>> snd o chop k |> (op --->) |
|
308 in apply 0 (mk ts1) U ts2 end |
|
309 | NONE => app_func u T (map (traverse Ts) ts)) |
|
310 | (u as Free (_, T), ts) => app_func u T (map (traverse Ts) ts) |
|
311 | (u as Bound i, ts) => apply 0 u (nth Ts i) (map (traverse Ts) ts) |
|
312 | (Abs (n, T, u), ts) => traverses Ts (Abs (n, T, traverse (T::Ts) u)) ts |
|
313 | (u, ts) => traverses Ts u ts) |
|
314 and in_trigger Ts ((c as @{const trigger}) $ p $ t) = |
|
315 c $ in_pats Ts p $ in_weight Ts t |
|
316 | in_trigger Ts t = in_weight Ts t |
|
317 and in_pats Ts ps = |
|
318 in_list @{typ "pattern list"} |
|
319 (in_list @{typ pattern} (in_pat Ts)) ps |
|
320 and in_pat Ts ((p as Const (@{const_name pat}, _)) $ t) = |
|
321 p $ traverse Ts t |
|
322 | in_pat Ts ((p as Const (@{const_name nopat}, _)) $ t) = |
|
323 p $ traverse Ts t |
|
324 | in_pat _ t = raise TERM ("bad pattern", [t]) |
|
325 and in_weight Ts ((c as @{const weight}) $ w $ t) = |
|
326 c $ w $ traverse Ts t |
|
327 | in_weight Ts t = traverse Ts t |
|
328 and traverses Ts t ts = Term.list_comb (t, map (traverse Ts) ts) |
|
329 in map (traverse []) ts end |
|
330 |
|
331 val fun_app_eq = mk_meta_eq @{thm fun_app_def} |
|
332 |
|
333 end |
|
334 |
|
335 |
|
336 (** map HOL formulas to FOL formulas (i.e., separate formulas froms terms) **) |
|
337 |
|
338 local |
|
339 val term_bool = @{lemma "term_true ~= term_false" |
|
340 by (simp add: term_true_def term_false_def)} |
|
341 |
|
342 val is_quant = member (op =) [@{const_name All}, @{const_name Ex}] |
|
343 |
|
344 val fol_rules = [ |
|
345 Let_def, |
|
346 mk_meta_eq @{thm term_true_def}, |
|
347 mk_meta_eq @{thm term_false_def}, |
|
348 @{lemma "P = True == P" by (rule eq_reflection) simp}, |
|
349 @{lemma "if P then True else False == P" by (rule eq_reflection) simp}] |
|
350 |
|
351 fun as_term t = @{const HOL.eq (bool)} $ t $ @{const term_true} |
|
352 |
|
353 exception BAD_PATTERN of unit |
|
354 |
|
355 fun wrap_in_if pat t = |
|
356 if pat then |
|
357 raise BAD_PATTERN () |
|
358 else |
|
359 @{const If (bool)} $ t $ @{const term_true} $ @{const term_false} |
|
360 |
|
361 fun is_builtin_conn_or_pred ctxt c ts = |
|
362 is_some (Old_SMT_Builtin.dest_builtin_conn ctxt c ts) orelse |
|
363 is_some (Old_SMT_Builtin.dest_builtin_pred ctxt c ts) |
|
364 |
|
365 fun builtin b ctxt c ts = |
|
366 (case (Const c, ts) of |
|
367 (@{const HOL.eq (bool)}, [t, u]) => |
|
368 if t = @{const term_true} orelse u = @{const term_true} then |
|
369 Old_SMT_Builtin.dest_builtin_eq ctxt t u |
|
370 else b ctxt c ts |
|
371 | _ => b ctxt c ts) |
|
372 in |
|
373 |
|
374 fun folify ctxt = |
|
375 let |
|
376 fun in_list T f t = HOLogic.mk_list T (map_filter f (HOLogic.dest_list t)) |
|
377 |
|
378 fun in_term pat t = |
|
379 (case Term.strip_comb t of |
|
380 (@{const True}, []) => @{const term_true} |
|
381 | (@{const False}, []) => @{const term_false} |
|
382 | (u as Const (@{const_name If}, _), [t1, t2, t3]) => |
|
383 if pat then raise BAD_PATTERN () |
|
384 else u $ in_form t1 $ in_term pat t2 $ in_term pat t3 |
|
385 | (Const (c as (n, _)), ts) => |
|
386 if is_builtin_conn_or_pred ctxt c ts then wrap_in_if pat (in_form t) |
|
387 else if is_quant n then wrap_in_if pat (in_form t) |
|
388 else Term.list_comb (Const c, map (in_term pat) ts) |
|
389 | (Free c, ts) => Term.list_comb (Free c, map (in_term pat) ts) |
|
390 | _ => t) |
|
391 |
|
392 and in_weight ((c as @{const weight}) $ w $ t) = c $ w $ in_form t |
|
393 | in_weight t = in_form t |
|
394 |
|
395 and in_pat ((p as Const (@{const_name pat}, _)) $ t) = |
|
396 p $ in_term true t |
|
397 | in_pat ((p as Const (@{const_name nopat}, _)) $ t) = |
|
398 p $ in_term true t |
|
399 | in_pat t = raise TERM ("bad pattern", [t]) |
|
400 |
|
401 and in_pats ps = |
|
402 in_list @{typ "pattern list"} |
|
403 (SOME o in_list @{typ pattern} (try in_pat)) ps |
|
404 |
|
405 and in_trigger ((c as @{const trigger}) $ p $ t) = |
|
406 c $ in_pats p $ in_weight t |
|
407 | in_trigger t = in_weight t |
|
408 |
|
409 and in_form t = |
|
410 (case Term.strip_comb t of |
|
411 (q as Const (qn, _), [Abs (n, T, u)]) => |
|
412 if is_quant qn then q $ Abs (n, T, in_trigger u) |
|
413 else as_term (in_term false t) |
|
414 | (Const c, ts) => |
|
415 (case Old_SMT_Builtin.dest_builtin_conn ctxt c ts of |
|
416 SOME (_, _, us, mk) => mk (map in_form us) |
|
417 | NONE => |
|
418 (case Old_SMT_Builtin.dest_builtin_pred ctxt c ts of |
|
419 SOME (_, _, us, mk) => mk (map (in_term false) us) |
|
420 | NONE => as_term (in_term false t))) |
|
421 | _ => as_term (in_term false t)) |
|
422 in |
|
423 map in_form #> |
|
424 cons (Old_SMT_Utils.prop_of term_bool) #> |
|
425 pair (fol_rules, [term_bool], builtin) |
|
426 end |
|
427 |
|
428 end |
|
429 |
|
430 |
|
431 (* translation into intermediate format *) |
|
432 |
|
433 (** utility functions **) |
|
434 |
|
435 val quantifier = (fn |
|
436 @{const_name All} => SOME SForall |
|
437 | @{const_name Ex} => SOME SExists |
|
438 | _ => NONE) |
|
439 |
|
440 fun group_quant qname Ts (t as Const (q, _) $ Abs (_, T, u)) = |
|
441 if q = qname then group_quant qname (T :: Ts) u else (Ts, t) |
|
442 | group_quant _ Ts t = (Ts, t) |
|
443 |
|
444 fun dest_weight (@{const weight} $ w $ t) = |
|
445 (SOME (snd (HOLogic.dest_number w)), t) |
|
446 | dest_weight t = (NONE, t) |
|
447 |
|
448 fun dest_pat (Const (@{const_name pat}, _) $ t) = (t, true) |
|
449 | dest_pat (Const (@{const_name nopat}, _) $ t) = (t, false) |
|
450 | dest_pat t = raise TERM ("bad pattern", [t]) |
|
451 |
|
452 fun dest_pats [] = I |
|
453 | dest_pats ts = |
|
454 (case map dest_pat ts |> split_list ||> distinct (op =) of |
|
455 (ps, [true]) => cons (SPat ps) |
|
456 | (ps, [false]) => cons (SNoPat ps) |
|
457 | _ => raise TERM ("bad multi-pattern", ts)) |
|
458 |
|
459 fun dest_trigger (@{const trigger} $ tl $ t) = |
|
460 (rev (fold (dest_pats o HOLogic.dest_list) (HOLogic.dest_list tl) []), t) |
|
461 | dest_trigger t = ([], t) |
|
462 |
|
463 fun dest_quant qn T t = quantifier qn |> Option.map (fn q => |
|
464 let |
|
465 val (Ts, u) = group_quant qn [T] t |
|
466 val (ps, p) = dest_trigger u |
|
467 val (w, b) = dest_weight p |
|
468 in (q, rev Ts, ps, w, b) end) |
|
469 |
|
470 fun fold_map_pat f (SPat ts) = fold_map f ts #>> SPat |
|
471 | fold_map_pat f (SNoPat ts) = fold_map f ts #>> SNoPat |
|
472 |
|
473 |
|
474 (** translation from Isabelle terms into SMT intermediate terms **) |
|
475 |
|
476 fun intermediate header dtyps builtin ctxt ts trx = |
|
477 let |
|
478 fun transT (T as TFree _) = add_typ T true |
|
479 | transT (T as TVar _) = (fn _ => raise TYPE ("bad SMT type", [T], [])) |
|
480 | transT (T as Type _) = |
|
481 (case Old_SMT_Builtin.dest_builtin_typ ctxt T of |
|
482 SOME n => pair n |
|
483 | NONE => add_typ T true) |
|
484 |
|
485 fun app n ts = SApp (n, ts) |
|
486 |
|
487 fun trans t = |
|
488 (case Term.strip_comb t of |
|
489 (Const (qn, _), [Abs (_, T, t1)]) => |
|
490 (case dest_quant qn T t1 of |
|
491 SOME (q, Ts, ps, w, b) => |
|
492 fold_map transT Ts ##>> fold_map (fold_map_pat trans) ps ##>> |
|
493 trans b #>> (fn ((Ts', ps'), b') => SQua (q, Ts', ps', w, b')) |
|
494 | NONE => raise TERM ("unsupported quantifier", [t])) |
|
495 | (Const (@{const_name Let}, _), [t1, Abs (_, T, t2)]) => |
|
496 transT T ##>> trans t1 ##>> trans t2 #>> |
|
497 (fn ((U, u1), u2) => SLet (U, u1, u2)) |
|
498 | (u as Const (c as (_, T)), ts) => |
|
499 (case builtin ctxt c ts of |
|
500 SOME (n, _, us, _) => fold_map trans us #>> app n |
|
501 | NONE => transs u T ts) |
|
502 | (u as Free (_, T), ts) => transs u T ts |
|
503 | (Bound i, []) => pair (SVar i) |
|
504 | _ => raise TERM ("bad SMT term", [t])) |
|
505 |
|
506 and transs t T ts = |
|
507 let val (Us, U) = Old_SMT_Utils.dest_funT (length ts) T |
|
508 in |
|
509 fold_map transT Us ##>> transT U #-> (fn Up => |
|
510 add_fun t (SOME Up) ##>> fold_map trans ts #>> SApp) |
|
511 end |
|
512 |
|
513 val (us, trx') = fold_map trans ts trx |
|
514 in ((sign_of (header ts) dtyps trx', us), trx') end |
|
515 |
|
516 |
|
517 |
|
518 (* translation *) |
|
519 |
|
520 structure Configs = Generic_Data |
|
521 ( |
|
522 type T = (Proof.context -> config) Old_SMT_Utils.dict |
|
523 val empty = [] |
|
524 val extend = I |
|
525 fun merge data = Old_SMT_Utils.dict_merge fst data |
|
526 ) |
|
527 |
|
528 fun add_config (cs, cfg) = Configs.map (Old_SMT_Utils.dict_update (cs, cfg)) |
|
529 |
|
530 fun get_config ctxt = |
|
531 let val cs = Old_SMT_Config.solver_class_of ctxt |
|
532 in |
|
533 (case Old_SMT_Utils.dict_get (Configs.get (Context.Proof ctxt)) cs of |
|
534 SOME cfg => cfg ctxt |
|
535 | NONE => error ("SMT: no translation configuration found " ^ |
|
536 "for solver class " ^ quote (Old_SMT_Utils.string_of_class cs))) |
|
537 end |
|
538 |
|
539 fun translate ctxt comments ithms = |
|
540 let |
|
541 val {prefixes, is_fol, header, has_datatypes, serialize} = get_config ctxt |
|
542 |
|
543 val with_datatypes = |
|
544 has_datatypes andalso Config.get ctxt Old_SMT_Config.datatypes |
|
545 |
|
546 fun no_dtyps (tr_context, ctxt) ts = |
|
547 ((Termtab.empty, [], tr_context, ctxt), ts) |
|
548 |
|
549 val ts1 = map (Envir.beta_eta_contract o Old_SMT_Utils.prop_of o snd) ithms |
|
550 |
|
551 val ((funcs, dtyps, tr_context, ctxt1), ts2) = |
|
552 ((make_tr_context prefixes, ctxt), ts1) |
|
553 |-> (if with_datatypes then collect_datatypes_and_records else no_dtyps) |
|
554 |
|
555 fun is_binder (Const (@{const_name Let}, _) $ _) = true |
|
556 | is_binder t = Lambda_Lifting.is_quantifier t |
|
557 |
|
558 fun mk_trigger ((q as Const (@{const_name All}, _)) $ Abs (n, T, t)) = |
|
559 q $ Abs (n, T, mk_trigger t) |
|
560 | mk_trigger (eq as (Const (@{const_name HOL.eq}, T) $ lhs $ _)) = |
|
561 Term.domain_type T --> @{typ pattern} |
|
562 |> (fn T => Const (@{const_name pat}, T) $ lhs) |
|
563 |> HOLogic.mk_list @{typ pattern} o single |
|
564 |> HOLogic.mk_list @{typ "pattern list"} o single |
|
565 |> (fn t => @{const trigger} $ t $ eq) |
|
566 | mk_trigger t = t |
|
567 |
|
568 val (ctxt2, ts3) = |
|
569 ts2 |
|
570 |> eta_expand ctxt1 is_fol funcs |
|
571 |> rpair ctxt1 |
|
572 |-> Lambda_Lifting.lift_lambdas NONE is_binder |
|
573 |-> (fn (ts', defs) => fn ctxt' => |
|
574 map mk_trigger defs @ ts' |
|
575 |> intro_explicit_application ctxt' funcs |
|
576 |> pair ctxt') |
|
577 |
|
578 val ((rewrite_rules, extra_thms, builtin), ts4) = |
|
579 (if is_fol then folify ctxt2 else pair ([], [], I)) ts3 |
|
580 |
|
581 val rewrite_rules' = fun_app_eq :: rewrite_rules |
|
582 in |
|
583 (ts4, tr_context) |
|
584 |-> intermediate header dtyps (builtin Old_SMT_Builtin.dest_builtin) ctxt2 |
|
585 |>> uncurry (serialize comments) |
|
586 ||> recon_of ctxt2 rewrite_rules' extra_thms ithms |
|
587 end |
|
588 |
|
589 end |