1 (* Title: HOL/Tools/SMT2/smt2_translate.ML |
|
2 Author: Sascha Boehme, TU Muenchen |
|
3 |
|
4 Translate theorems into an SMT intermediate format and serialize them. |
|
5 *) |
|
6 |
|
7 signature SMT2_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 * sterm |
|
17 |
|
18 (*translation configuration*) |
|
19 type sign = { |
|
20 logic: string, |
|
21 sorts: string list, |
|
22 dtyps: (string * (string * (string * string) list) list) list list, |
|
23 funcs: (string * (string list * string)) list } |
|
24 type config = { |
|
25 logic: term list -> string, |
|
26 has_datatypes: bool, |
|
27 serialize: (string * string) list -> string list -> sign -> sterm list -> string } |
|
28 type replay_data = { |
|
29 context: Proof.context, |
|
30 typs: typ Symtab.table, |
|
31 terms: term Symtab.table, |
|
32 ll_defs: term list, |
|
33 rewrite_rules: thm list, |
|
34 assms: (int * thm) list } |
|
35 |
|
36 (*translation*) |
|
37 val add_config: SMT2_Util.class * (Proof.context -> config) -> Context.generic -> Context.generic |
|
38 val translate: Proof.context -> (string * string) list -> string list -> (int * thm) list -> |
|
39 string * replay_data |
|
40 end; |
|
41 |
|
42 structure SMT2_Translate: SMT2_TRANSLATE = |
|
43 struct |
|
44 |
|
45 |
|
46 (* intermediate term structure *) |
|
47 |
|
48 datatype squant = SForall | SExists |
|
49 |
|
50 datatype 'a spattern = SPat of 'a list | SNoPat of 'a list |
|
51 |
|
52 datatype sterm = |
|
53 SVar of int | |
|
54 SApp of string * sterm list | |
|
55 SLet of string * sterm * sterm | |
|
56 SQua of squant * string list * sterm spattern list * sterm |
|
57 |
|
58 |
|
59 (* translation configuration *) |
|
60 |
|
61 type sign = { |
|
62 logic: string, |
|
63 sorts: string list, |
|
64 dtyps: (string * (string * (string * string) list) list) list list, |
|
65 funcs: (string * (string list * string)) list } |
|
66 |
|
67 type config = { |
|
68 logic: term list -> string, |
|
69 has_datatypes: bool, |
|
70 serialize: (string * string) list -> string list -> sign -> sterm list -> string } |
|
71 |
|
72 type replay_data = { |
|
73 context: Proof.context, |
|
74 typs: typ Symtab.table, |
|
75 terms: term Symtab.table, |
|
76 ll_defs: term list, |
|
77 rewrite_rules: thm list, |
|
78 assms: (int * thm) list } |
|
79 |
|
80 |
|
81 (* translation context *) |
|
82 |
|
83 fun add_components_of_typ (Type (s, Ts)) = |
|
84 cons (Long_Name.base_name s) #> fold_rev add_components_of_typ Ts |
|
85 | add_components_of_typ (TFree (s, _)) = cons (perhaps (try (unprefix "'")) s) |
|
86 | add_components_of_typ _ = I; |
|
87 |
|
88 fun suggested_name_of_typ T = space_implode "_" (add_components_of_typ T []); |
|
89 |
|
90 fun suggested_name_of_term (Const (s, _)) = Long_Name.base_name s |
|
91 | suggested_name_of_term (Free (s, _)) = s |
|
92 | suggested_name_of_term _ = Name.uu |
|
93 |
|
94 val empty_tr_context = (Name.context, Typtab.empty, Termtab.empty) |
|
95 val safe_suffix = "$" |
|
96 |
|
97 fun add_typ T proper (cx as (names, typs, terms)) = |
|
98 (case Typtab.lookup typs T of |
|
99 SOME (name, _) => (name, cx) |
|
100 | NONE => |
|
101 let |
|
102 val sugg = Name.desymbolize (SOME true) (suggested_name_of_typ T) ^ safe_suffix |
|
103 val (name, names') = Name.variant sugg names |
|
104 val typs' = Typtab.update (T, (name, proper)) typs |
|
105 in (name, (names', typs', terms)) end) |
|
106 |
|
107 fun add_fun t sort (cx as (names, typs, terms)) = |
|
108 (case Termtab.lookup terms t of |
|
109 SOME (name, _) => (name, cx) |
|
110 | NONE => |
|
111 let |
|
112 val sugg = Name.desymbolize (SOME false) (suggested_name_of_term t) ^ safe_suffix |
|
113 val (name, names') = Name.variant sugg names |
|
114 val terms' = Termtab.update (t, (name, sort)) terms |
|
115 in (name, (names', typs, terms')) end) |
|
116 |
|
117 fun sign_of logic dtyps (_, typs, terms) = { |
|
118 logic = logic, |
|
119 sorts = Typtab.fold (fn (_, (n, true)) => cons n | _ => I) typs [], |
|
120 dtyps = dtyps, |
|
121 funcs = Termtab.fold (fn (_, (n, SOME ss)) => cons (n,ss) | _ => I) terms []} |
|
122 |
|
123 fun replay_data_of ctxt ll_defs rules assms (_, typs, terms) = |
|
124 let |
|
125 fun add_typ (T, (n, _)) = Symtab.update (n, T) |
|
126 val typs' = Typtab.fold add_typ typs Symtab.empty |
|
127 |
|
128 fun add_fun (t, (n, _)) = Symtab.update (n, t) |
|
129 val terms' = Termtab.fold add_fun terms Symtab.empty |
|
130 in |
|
131 {context = ctxt, typs = typs', terms = terms', ll_defs = ll_defs, rewrite_rules = rules, |
|
132 assms = assms} |
|
133 end |
|
134 |
|
135 |
|
136 (* preprocessing *) |
|
137 |
|
138 (** datatype declarations **) |
|
139 |
|
140 fun collect_datatypes_and_records (tr_context, ctxt) ts = |
|
141 let |
|
142 val (declss, ctxt') = fold (Term.fold_types SMT2_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 SMT2_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 expf k i T t = |
|
179 let val Ts = drop i (fst (SMT2_Util.dest_funT k T)) |
|
180 in |
|
181 Term.incr_boundvars (length Ts) t |
|
182 |> fold_rev (fn i => fn u => u $ Bound i) (0 upto length Ts - 1) |
|
183 |> fold_rev (fn T => fn u => Abs (Name.uu, T, u)) Ts |
|
184 end |
|
185 in |
|
186 |
|
187 fun eta_expand ctxt funcs = |
|
188 let |
|
189 fun exp_func t T ts = |
|
190 (case Termtab.lookup funcs t of |
|
191 SOME k => Term.list_comb (t, ts) |> k <> length ts ? expf k (length ts) T |
|
192 | NONE => Term.list_comb (t, ts)) |
|
193 |
|
194 fun expand ((q as Const (@{const_name All}, _)) $ Abs a) = q $ abs_expand a |
|
195 | expand ((q as Const (@{const_name All}, T)) $ t) = q $ exp expand T t |
|
196 | expand (q as Const (@{const_name All}, T)) = exp2 T q |
|
197 | expand ((q as Const (@{const_name Ex}, _)) $ Abs a) = q $ abs_expand a |
|
198 | expand ((q as Const (@{const_name Ex}, T)) $ t) = q $ exp expand T t |
|
199 | expand (q as Const (@{const_name Ex}, T)) = exp2 T q |
|
200 | expand (Const (@{const_name Let}, _) $ t $ u) = expand (Term.betapply (u, t)) |
|
201 | expand (Const (@{const_name Let}, T) $ t) = |
|
202 let val U = Term.domain_type (Term.range_type T) |
|
203 in Abs (Name.uu, U, Bound 0 $ Term.incr_boundvars 1 t) end |
|
204 | expand (Const (@{const_name Let}, T)) = |
|
205 let val U = Term.domain_type (Term.range_type T) |
|
206 in Abs (Name.uu, Term.domain_type T, Abs (Name.uu, U, Bound 0 $ Bound 1)) end |
|
207 | expand t = |
|
208 (case Term.strip_comb t of |
|
209 (u as Const (c as (_, T)), ts) => |
|
210 (case SMT2_Builtin.dest_builtin ctxt c ts of |
|
211 SOME (_, k, us, mk) => |
|
212 if k = length us then mk (map expand us) |
|
213 else if k < length us then chop k (map expand us) |>> mk |> Term.list_comb |
|
214 else expf k (length ts) T (mk (map expand us)) |
|
215 | NONE => exp_func u T (map expand ts)) |
|
216 | (u as Free (_, T), ts) => exp_func u T (map expand ts) |
|
217 | (Abs a, ts) => Term.list_comb (abs_expand a, map expand ts) |
|
218 | (u, ts) => Term.list_comb (u, map expand ts)) |
|
219 |
|
220 and abs_expand (n, T, t) = Abs (n, T, expand t) |
|
221 |
|
222 in map expand end |
|
223 |
|
224 end |
|
225 |
|
226 |
|
227 (** introduce explicit applications **) |
|
228 |
|
229 local |
|
230 (* |
|
231 Make application explicit for functions with varying number of arguments. |
|
232 *) |
|
233 |
|
234 fun add t i = apfst (Termtab.map_default (t, i) (Integer.min i)) |
|
235 fun add_type T = apsnd (Typtab.update (T, ())) |
|
236 |
|
237 fun min_arities t = |
|
238 (case Term.strip_comb t of |
|
239 (u as Const _, ts) => add u (length ts) #> fold min_arities ts |
|
240 | (u as Free _, ts) => add u (length ts) #> fold min_arities ts |
|
241 | (Abs (_, T, u), ts) => (can dest_funT T ? add_type T) #> min_arities u #> fold min_arities ts |
|
242 | (_, ts) => fold min_arities ts) |
|
243 |
|
244 fun minimize types t i = |
|
245 let |
|
246 fun find_min j [] _ = j |
|
247 | find_min j (U :: Us) T = |
|
248 if Typtab.defined types T then j else find_min (j + 1) Us (U --> T) |
|
249 |
|
250 val (Ts, T) = Term.strip_type (Term.type_of t) |
|
251 in find_min 0 (take i (rev Ts)) T end |
|
252 |
|
253 fun app u (t, T) = (Const (@{const_name fun_app}, T --> T) $ t $ u, Term.range_type T) |
|
254 |
|
255 fun apply i t T ts = |
|
256 let |
|
257 val (ts1, ts2) = chop i ts |
|
258 val (_, U) = SMT2_Util.dest_funT i T |
|
259 in fst (fold app ts2 (Term.list_comb (t, ts1), U)) end |
|
260 in |
|
261 |
|
262 fun intro_explicit_application ctxt funcs ts = |
|
263 let |
|
264 val (arities, types) = fold min_arities ts (Termtab.empty, Typtab.empty) |
|
265 val arities' = Termtab.map (minimize types) arities (* FIXME: highly suspicious *) |
|
266 |
|
267 fun app_func t T ts = |
|
268 if is_some (Termtab.lookup funcs t) then Term.list_comb (t, ts) |
|
269 else apply (the (Termtab.lookup arities' t)) t T ts |
|
270 |
|
271 fun in_list T f t = SMT2_Util.mk_symb_list T (map f (SMT2_Util.dest_symb_list t)) |
|
272 |
|
273 fun traverse Ts t = |
|
274 (case Term.strip_comb t of |
|
275 (q as Const (@{const_name All}, _), [Abs (x, T, u)]) => |
|
276 q $ Abs (x, T, in_trigger (T :: Ts) u) |
|
277 | (q as Const (@{const_name Ex}, _), [Abs (x, T, u)]) => |
|
278 q $ Abs (x, T, in_trigger (T :: Ts) u) |
|
279 | (q as Const (@{const_name Let}, _), [u1, u2 as Abs _]) => |
|
280 q $ traverse Ts u1 $ traverse Ts u2 |
|
281 | (u as Const (c as (_, T)), ts) => |
|
282 (case SMT2_Builtin.dest_builtin ctxt c ts of |
|
283 SOME (_, k, us, mk) => |
|
284 let |
|
285 val (ts1, ts2) = chop k (map (traverse Ts) us) |
|
286 val U = Term.strip_type T |>> snd o chop k |> (op --->) |
|
287 in apply 0 (mk ts1) U ts2 end |
|
288 | NONE => app_func u T (map (traverse Ts) ts)) |
|
289 | (u as Free (_, T), ts) => app_func u T (map (traverse Ts) ts) |
|
290 | (u as Bound i, ts) => apply 0 u (nth Ts i) (map (traverse Ts) ts) |
|
291 | (Abs (n, T, u), ts) => traverses Ts (Abs (n, T, traverse (T::Ts) u)) ts |
|
292 | (u, ts) => traverses Ts u ts) |
|
293 and in_trigger Ts ((c as @{const trigger}) $ p $ t) = c $ in_pats Ts p $ traverse Ts t |
|
294 | in_trigger Ts t = traverse Ts t |
|
295 and in_pats Ts ps = |
|
296 in_list @{typ "pattern symb_list"} (in_list @{typ pattern} (in_pat Ts)) ps |
|
297 and in_pat Ts ((p as Const (@{const_name pat}, _)) $ t) = p $ traverse Ts t |
|
298 | in_pat Ts ((p as Const (@{const_name nopat}, _)) $ t) = p $ traverse Ts t |
|
299 | in_pat _ t = raise TERM ("bad pattern", [t]) |
|
300 and traverses Ts t ts = Term.list_comb (t, map (traverse Ts) ts) |
|
301 in map (traverse []) ts end |
|
302 |
|
303 val fun_app_eq = mk_meta_eq @{thm fun_app_def} |
|
304 |
|
305 end |
|
306 |
|
307 |
|
308 (** map HOL formulas to FOL formulas (i.e., separate formulas froms terms) **) |
|
309 |
|
310 local |
|
311 val is_quant = member (op =) [@{const_name All}, @{const_name Ex}] |
|
312 |
|
313 val fol_rules = [ |
|
314 Let_def, |
|
315 @{lemma "P = True == P" by (rule eq_reflection) simp}, |
|
316 @{lemma "if P then True else False == P" by (rule eq_reflection) simp}] |
|
317 |
|
318 exception BAD_PATTERN of unit |
|
319 |
|
320 fun wrap_in_if pat t = |
|
321 if pat then raise BAD_PATTERN () else @{const If (bool)} $ t $ @{const True} $ @{const False} |
|
322 |
|
323 fun is_builtin_conn_or_pred ctxt c ts = |
|
324 is_some (SMT2_Builtin.dest_builtin_conn ctxt c ts) orelse |
|
325 is_some (SMT2_Builtin.dest_builtin_pred ctxt c ts) |
|
326 in |
|
327 |
|
328 fun folify ctxt = |
|
329 let |
|
330 fun in_list T f t = SMT2_Util.mk_symb_list T (map_filter f (SMT2_Util.dest_symb_list t)) |
|
331 |
|
332 fun in_term pat t = |
|
333 (case Term.strip_comb t of |
|
334 (@{const True}, []) => t |
|
335 | (@{const False}, []) => t |
|
336 | (u as Const (@{const_name If}, _), [t1, t2, t3]) => |
|
337 if pat then raise BAD_PATTERN () else u $ in_form t1 $ in_term pat t2 $ in_term pat t3 |
|
338 | (Const (c as (n, _)), ts) => |
|
339 if is_builtin_conn_or_pred ctxt c ts then wrap_in_if pat (in_form t) |
|
340 else if is_quant n then wrap_in_if pat (in_form t) |
|
341 else Term.list_comb (Const c, map (in_term pat) ts) |
|
342 | (Free c, ts) => Term.list_comb (Free c, map (in_term pat) ts) |
|
343 | _ => t) |
|
344 |
|
345 and in_pat ((p as Const (@{const_name pat}, _)) $ t) = |
|
346 p $ in_term true t |
|
347 | in_pat ((p as Const (@{const_name nopat}, _)) $ t) = |
|
348 p $ in_term true t |
|
349 | in_pat t = raise TERM ("bad pattern", [t]) |
|
350 |
|
351 and in_pats ps = |
|
352 in_list @{typ "pattern symb_list"} (SOME o in_list @{typ pattern} (try in_pat)) ps |
|
353 |
|
354 and in_trigger ((c as @{const trigger}) $ p $ t) = c $ in_pats p $ in_form t |
|
355 | in_trigger t = in_form t |
|
356 |
|
357 and in_form t = |
|
358 (case Term.strip_comb t of |
|
359 (q as Const (qn, _), [Abs (n, T, u)]) => |
|
360 if is_quant qn then q $ Abs (n, T, in_trigger u) |
|
361 else in_term false t |
|
362 | (Const c, ts) => |
|
363 (case SMT2_Builtin.dest_builtin_conn ctxt c ts of |
|
364 SOME (_, _, us, mk) => mk (map in_form us) |
|
365 | NONE => |
|
366 (case SMT2_Builtin.dest_builtin_pred ctxt c ts of |
|
367 SOME (_, _, us, mk) => mk (map (in_term false) us) |
|
368 | NONE => in_term false t)) |
|
369 | _ => in_term false t) |
|
370 in |
|
371 map in_form #> |
|
372 pair (fol_rules, I) |
|
373 end |
|
374 |
|
375 end |
|
376 |
|
377 |
|
378 (* translation into intermediate format *) |
|
379 |
|
380 (** utility functions **) |
|
381 |
|
382 val quantifier = (fn |
|
383 @{const_name All} => SOME SForall |
|
384 | @{const_name Ex} => SOME SExists |
|
385 | _ => NONE) |
|
386 |
|
387 fun group_quant qname Ts (t as Const (q, _) $ Abs (_, T, u)) = |
|
388 if q = qname then group_quant qname (T :: Ts) u else (Ts, t) |
|
389 | group_quant _ Ts t = (Ts, t) |
|
390 |
|
391 fun dest_pat (Const (@{const_name pat}, _) $ t) = (t, true) |
|
392 | dest_pat (Const (@{const_name nopat}, _) $ t) = (t, false) |
|
393 | dest_pat t = raise TERM ("bad pattern", [t]) |
|
394 |
|
395 fun dest_pats [] = I |
|
396 | dest_pats ts = |
|
397 (case map dest_pat ts |> split_list ||> distinct (op =) of |
|
398 (ps, [true]) => cons (SPat ps) |
|
399 | (ps, [false]) => cons (SNoPat ps) |
|
400 | _ => raise TERM ("bad multi-pattern", ts)) |
|
401 |
|
402 fun dest_trigger (@{const trigger} $ tl $ t) = |
|
403 (rev (fold (dest_pats o SMT2_Util.dest_symb_list) (SMT2_Util.dest_symb_list tl) []), t) |
|
404 | dest_trigger t = ([], t) |
|
405 |
|
406 fun dest_quant qn T t = quantifier qn |> Option.map (fn q => |
|
407 let |
|
408 val (Ts, u) = group_quant qn [T] t |
|
409 val (ps, p) = dest_trigger u |
|
410 in (q, rev Ts, ps, p) end) |
|
411 |
|
412 fun fold_map_pat f (SPat ts) = fold_map f ts #>> SPat |
|
413 | fold_map_pat f (SNoPat ts) = fold_map f ts #>> SNoPat |
|
414 |
|
415 |
|
416 (** translation from Isabelle terms into SMT intermediate terms **) |
|
417 |
|
418 fun intermediate logic dtyps builtin ctxt ts trx = |
|
419 let |
|
420 fun transT (T as TFree _) = add_typ T true |
|
421 | transT (T as TVar _) = (fn _ => raise TYPE ("bad SMT type", [T], [])) |
|
422 | transT (T as Type _) = |
|
423 (case SMT2_Builtin.dest_builtin_typ ctxt T of |
|
424 SOME n => pair n |
|
425 | NONE => add_typ T true) |
|
426 |
|
427 fun app n ts = SApp (n, ts) |
|
428 |
|
429 fun trans t = |
|
430 (case Term.strip_comb t of |
|
431 (Const (qn, _), [Abs (_, T, t1)]) => |
|
432 (case dest_quant qn T t1 of |
|
433 SOME (q, Ts, ps, b) => |
|
434 fold_map transT Ts ##>> fold_map (fold_map_pat trans) ps ##>> |
|
435 trans b #>> (fn ((Ts', ps'), b') => SQua (q, Ts', ps', b')) |
|
436 | NONE => raise TERM ("unsupported quantifier", [t])) |
|
437 | (Const (@{const_name Let}, _), [t1, Abs (_, T, t2)]) => |
|
438 transT T ##>> trans t1 ##>> trans t2 #>> (fn ((U, u1), u2) => SLet (U, u1, u2)) |
|
439 | (u as Const (c as (_, T)), ts) => |
|
440 (case builtin ctxt c ts of |
|
441 SOME (n, _, us, _) => fold_map trans us #>> app n |
|
442 | NONE => transs u T ts) |
|
443 | (u as Free (_, T), ts) => transs u T ts |
|
444 | (Bound i, []) => pair (SVar i) |
|
445 | _ => raise TERM ("bad SMT term", [t])) |
|
446 |
|
447 and transs t T ts = |
|
448 let val (Us, U) = SMT2_Util.dest_funT (length ts) T |
|
449 in |
|
450 fold_map transT Us ##>> transT U #-> (fn Up => |
|
451 add_fun t (SOME Up) ##>> fold_map trans ts #>> SApp) |
|
452 end |
|
453 |
|
454 val (us, trx') = fold_map trans ts trx |
|
455 in ((sign_of (logic ts) dtyps trx', us), trx') end |
|
456 |
|
457 |
|
458 (* translation *) |
|
459 |
|
460 structure Configs = Generic_Data |
|
461 ( |
|
462 type T = (Proof.context -> config) SMT2_Util.dict |
|
463 val empty = [] |
|
464 val extend = I |
|
465 fun merge data = SMT2_Util.dict_merge fst data |
|
466 ) |
|
467 |
|
468 fun add_config (cs, cfg) = Configs.map (SMT2_Util.dict_update (cs, cfg)) |
|
469 |
|
470 fun get_config ctxt = |
|
471 let val cs = SMT2_Config.solver_class_of ctxt |
|
472 in |
|
473 (case SMT2_Util.dict_get (Configs.get (Context.Proof ctxt)) cs of |
|
474 SOME cfg => cfg ctxt |
|
475 | NONE => error ("SMT: no translation configuration found " ^ |
|
476 "for solver class " ^ quote (SMT2_Util.string_of_class cs))) |
|
477 end |
|
478 |
|
479 fun translate ctxt smt_options comments ithms = |
|
480 let |
|
481 val {logic, has_datatypes, serialize} = get_config ctxt |
|
482 |
|
483 fun no_dtyps (tr_context, ctxt) ts = |
|
484 ((Termtab.empty, [], tr_context, ctxt), ts) |
|
485 |
|
486 val ts1 = map (Envir.beta_eta_contract o SMT2_Util.prop_of o snd) ithms |
|
487 |
|
488 val ((funcs, dtyps, tr_context, ctxt1), ts2) = |
|
489 ((empty_tr_context, ctxt), ts1) |
|
490 |-> (if has_datatypes then collect_datatypes_and_records else no_dtyps) |
|
491 |
|
492 fun is_binder (Const (@{const_name Let}, _) $ _) = true |
|
493 | is_binder t = Lambda_Lifting.is_quantifier t |
|
494 |
|
495 fun mk_trigger ((q as Const (@{const_name All}, _)) $ Abs (n, T, t)) = |
|
496 q $ Abs (n, T, mk_trigger t) |
|
497 | mk_trigger (eq as (Const (@{const_name HOL.eq}, T) $ lhs $ _)) = |
|
498 Term.domain_type T --> @{typ pattern} |
|
499 |> (fn T => Const (@{const_name pat}, T) $ lhs) |
|
500 |> SMT2_Util.mk_symb_list @{typ pattern} o single |
|
501 |> SMT2_Util.mk_symb_list @{typ "pattern symb_list"} o single |
|
502 |> (fn t => @{const trigger} $ t $ eq) |
|
503 | mk_trigger t = t |
|
504 |
|
505 val (ctxt2, (ts3, ll_defs)) = |
|
506 ts2 |
|
507 |> eta_expand ctxt1 funcs |
|
508 |> rpair ctxt1 |
|
509 |-> Lambda_Lifting.lift_lambdas NONE is_binder |
|
510 |-> (fn (ts', ll_defs) => fn ctxt' => |
|
511 (ctxt', (intro_explicit_application ctxt' funcs (map mk_trigger ll_defs @ ts'), ll_defs))) |
|
512 |
|
513 val ((rewrite_rules, builtin), ts4) = folify ctxt2 ts3 |
|
514 |>> apfst (cons fun_app_eq) |
|
515 in |
|
516 (ts4, tr_context) |
|
517 |-> intermediate logic dtyps (builtin SMT2_Builtin.dest_builtin) ctxt2 |
|
518 |>> uncurry (serialize smt_options comments) |
|
519 ||> replay_data_of ctxt2 ll_defs rewrite_rules ithms |
|
520 end |
|
521 |
|
522 end; |
|