69 dtyps: (string * (string * (string * string) list) list) list list, |
73 dtyps: (string * (string * (string * string) list) list) list list, |
70 funcs: (string * (string list * string)) list } |
74 funcs: (string * (string list * string)) list } |
71 |
75 |
72 type config = { |
76 type config = { |
73 prefixes: prefixes, |
77 prefixes: prefixes, |
74 header: Proof.context -> term list -> string list, |
78 header: term list -> string list, |
75 is_fol: bool, |
79 is_fol: bool, |
76 has_datatypes: bool, |
80 has_datatypes: bool, |
77 serialize: string list -> sign -> sterm list -> string } |
81 serialize: string list -> sign -> sterm list -> string } |
78 |
82 |
79 type recon = { |
83 type recon = { |
|
84 context: Proof.context, |
80 typs: typ Symtab.table, |
85 typs: typ Symtab.table, |
81 terms: term Symtab.table, |
86 terms: term Symtab.table, |
82 unfolds: thm list, |
87 rewrite_rules: thm list, |
83 assms: (int * thm) list } |
88 assms: (int * thm) list } |
84 |
89 |
85 |
90 |
86 |
91 |
87 (* utility functions *) |
92 (* translation context *) |
|
93 |
|
94 fun make_tr_context {sort_prefix, func_prefix} = |
|
95 (sort_prefix, 1, Typtab.empty, func_prefix, 1, Termtab.empty) |
|
96 |
|
97 fun string_of_index pre i = pre ^ string_of_int i |
|
98 |
|
99 fun add_typ T proper (cx as (sp, Tidx, typs, fp, idx, terms)) = |
|
100 (case Typtab.lookup typs T of |
|
101 SOME (n, _) => (n, cx) |
|
102 | NONE => |
|
103 let |
|
104 val n = string_of_index sp Tidx |
|
105 val typs' = Typtab.update (T, (n, proper)) typs |
|
106 in (n, (sp, Tidx+1, typs', fp, idx, terms)) end) |
|
107 |
|
108 fun add_fun t sort (cx as (sp, Tidx, typs, fp, idx, terms)) = |
|
109 (case Termtab.lookup terms t of |
|
110 SOME (n, _) => (n, cx) |
|
111 | NONE => |
|
112 let |
|
113 val n = string_of_index fp idx |
|
114 val terms' = Termtab.update (t, (n, sort)) terms |
|
115 in (n, (sp, Tidx, typs, fp, idx+1, terms')) end) |
|
116 |
|
117 fun sign_of header dtyps (_, _, typs, _, _, terms) = { |
|
118 header = header, |
|
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 recon_of ctxt rules thms ithms revertT revert (_, _, typs, _, _, terms) = |
|
124 let |
|
125 fun add_typ (T, (n, _)) = Symtab.update (n, revertT T) |
|
126 val typs' = Typtab.fold add_typ typs Symtab.empty |
|
127 |
|
128 fun add_fun (t, (n, _)) = Symtab.update (n, revert t) |
|
129 val terms' = Termtab.fold add_fun terms Symtab.empty |
|
130 |
|
131 val assms = map (pair ~1) thms @ ithms |
|
132 in |
|
133 {context=ctxt, typs=typs', terms=terms', rewrite_rules=rules, assms=assms} |
|
134 end |
|
135 |
|
136 |
|
137 |
|
138 (* preprocessing *) |
|
139 |
|
140 (** mark built-in constants as Var **) |
|
141 |
|
142 fun mark_builtins ctxt = |
|
143 let |
|
144 (* |
|
145 Note: schematic terms cannot occur anymore in terms at this stage. |
|
146 *) |
|
147 fun mark t = |
|
148 (case Term.strip_comb t of |
|
149 (u as Const (@{const_name If}, _), ts) => marks u ts |
|
150 | (u as Const c, ts) => |
|
151 (case B.builtin_num ctxt t of |
|
152 SOME (n, T) => |
|
153 let val v = ((n, 0), T) |
|
154 in Vartab.update v #> pair (Var v) end |
|
155 | NONE => |
|
156 (case B.builtin_fun ctxt c ts of |
|
157 SOME ((ni, T), us, U) => |
|
158 Vartab.update (ni, U) #> marks (Var (ni, T)) us |
|
159 | NONE => marks u ts)) |
|
160 | (Abs (n, T, u), ts) => mark u #-> (fn u' => marks (Abs (n, T, u')) ts) |
|
161 | (u, ts) => marks u ts) |
|
162 |
|
163 and marks t ts = fold_map mark ts #>> Term.list_comb o pair t |
|
164 |
|
165 in (fn ts => swap (fold_map mark ts Vartab.empty)) end |
|
166 |
|
167 fun mark_builtins' ctxt t = hd (snd (mark_builtins ctxt [t])) |
|
168 |
|
169 |
|
170 (** FIXME **) |
|
171 |
|
172 local |
|
173 (* |
|
174 mark constructors and selectors as Vars (forcing eta-expansion), |
|
175 add missing datatype selectors via hypothetical definitions, |
|
176 also return necessary datatype and record theorems |
|
177 *) |
|
178 in |
|
179 |
|
180 fun collect_datatypes_and_records (tr_context, ctxt) ts = |
|
181 (([], tr_context, ctxt), ts) |
|
182 |
|
183 end |
|
184 |
|
185 |
|
186 (** eta-expand quantifiers, let expressions and built-ins *) |
|
187 |
|
188 local |
|
189 fun eta T t = Abs (Name.uu, T, Term.incr_boundvars 1 t $ Bound 0) |
|
190 |
|
191 fun exp T = eta (Term.domain_type (Term.domain_type T)) |
|
192 |
|
193 fun exp2 T q = |
|
194 let val U = Term.domain_type T |
|
195 in Abs (Name.uu, U, q $ eta (Term.domain_type U) (Bound 0)) end |
|
196 |
|
197 fun exp2' T l = |
|
198 let val (U1, U2) = Term.dest_funT T ||> Term.domain_type |
|
199 in Abs (Name.uu, U1, eta U2 (l $ Bound 0)) end |
|
200 |
|
201 fun expf t i T ts = |
|
202 let val Ts = U.dest_funT i T |> fst |> drop (length ts) |
|
203 in Term.list_comb (t, ts) |> fold_rev eta Ts end |
|
204 |
|
205 fun expand ((q as Const (@{const_name All}, _)) $ Abs a) = q $ abs_expand a |
|
206 | expand ((q as Const (@{const_name All}, T)) $ t) = q $ exp T t |
|
207 | expand (q as Const (@{const_name All}, T)) = exp2 T q |
|
208 | expand ((q as Const (@{const_name Ex}, _)) $ Abs a) = q $ abs_expand a |
|
209 | expand ((q as Const (@{const_name Ex}, T)) $ t) = q $ exp T t |
|
210 | expand (q as Const (@{const_name Ex}, T)) = exp2 T q |
|
211 | expand ((l as Const (@{const_name Let}, _)) $ t $ Abs a) = |
|
212 l $ expand t $ abs_expand a |
|
213 | expand ((l as Const (@{const_name Let}, T)) $ t $ u) = |
|
214 l $ expand t $ exp (Term.range_type T) u |
|
215 | expand ((l as Const (@{const_name Let}, T)) $ t) = exp2 T (l $ expand t) |
|
216 | expand (l as Const (@{const_name Let}, T)) = exp2' T l |
|
217 | expand (Abs a) = abs_expand a |
|
218 | expand t = |
|
219 (case Term.strip_comb t of |
|
220 (u as Const (@{const_name If}, T), ts) => expf u 3 T (map expand ts) |
|
221 | (u as Var ((_, i), T), ts) => expf u i T (map expand ts) |
|
222 | (u, ts) => Term.list_comb (u, map expand ts)) |
|
223 |
|
224 and abs_expand (n, T, t) = Abs (n, T, expand t) |
|
225 in |
|
226 |
|
227 val eta_expand = map expand |
|
228 |
|
229 end |
|
230 |
|
231 |
|
232 (** lambda-lifting **) |
|
233 |
|
234 local |
|
235 fun mk_def Ts T lhs rhs = |
|
236 let |
|
237 val eq = HOLogic.eq_const T $ lhs $ rhs |
|
238 val trigger = |
|
239 [[Const (@{const_name SMT.pat}, T --> @{typ SMT.pattern}) $ lhs]] |
|
240 |> map (HOLogic.mk_list @{typ SMT.pattern}) |
|
241 |> HOLogic.mk_list @{typ "SMT.pattern list"} |
|
242 fun mk_all T t = HOLogic.all_const T $ Abs (Name.uu, T, t) |
|
243 in fold mk_all Ts (@{const SMT.trigger} $ trigger $ eq) end |
|
244 |
|
245 fun replace_lambda Us Ts t (cx as (defs, ctxt)) = |
|
246 let |
|
247 val T = Term.fastype_of1 (Us @ Ts, t) |
|
248 val lev = length Us |
|
249 val bs = sort int_ord (Term.add_loose_bnos (t, lev, [])) |
|
250 val bss = map_index (fn (i, j) => (j, Integer.add lev i)) bs |
|
251 val norm = perhaps (AList.lookup (op =) bss) |
|
252 val t' = Term.map_aterms (fn Bound i => Bound (norm i) | t => t) t |
|
253 val Ts' = map (nth Ts) bs |
|
254 |
|
255 fun mk_abs U u = Abs (Name.uu, U, u) |
|
256 val abs_rhs = fold mk_abs Ts' (fold mk_abs Us t') |
|
257 in |
|
258 (case Termtab.lookup defs abs_rhs of |
|
259 SOME (f, _) => (Term.list_comb (f, map Bound bs), cx) |
|
260 | NONE => |
|
261 let |
|
262 val (n, ctxt') = |
|
263 yield_singleton Variable.variant_fixes Name.uu ctxt |
|
264 val f = Free (n, rev Ts' ---> (rev Us ---> T)) |
|
265 fun mk_bapp i t = t $ Bound i |
|
266 val lhs = |
|
267 f |
|
268 |> fold_rev (mk_bapp o snd) bss |
|
269 |> fold_rev mk_bapp (0 upto (length Us - 1)) |
|
270 val def = mk_def (Us @ Ts') T lhs t' |
|
271 in (f, (Termtab.update (abs_rhs, (f, def)) defs, ctxt')) end) |
|
272 end |
|
273 |
|
274 fun dest_abs Ts (Abs (_, T, t)) = dest_abs (T :: Ts) t |
|
275 | dest_abs Ts t = (Ts, t) |
|
276 |
|
277 fun traverse Ts t = |
|
278 (case t of |
|
279 (q as Const (@{const_name All}, _)) $ Abs a => |
|
280 abs_traverse Ts a #>> (fn a' => q $ Abs a') |
|
281 | (q as Const (@{const_name Ex}, _)) $ Abs a => |
|
282 abs_traverse Ts a #>> (fn a' => q $ Abs a') |
|
283 | (l as Const (@{const_name Let}, _)) $ u $ Abs a => |
|
284 traverse Ts u ##>> abs_traverse Ts a #>> |
|
285 (fn (u', a') => l $ u' $ Abs a') |
|
286 | Abs _ => |
|
287 let val (Us, u) = dest_abs [] t |
|
288 in traverse (Us @ Ts) u #-> replace_lambda Us Ts end |
|
289 | u1 $ u2 => traverse Ts u1 ##>> traverse Ts u2 #>> (op $) |
|
290 | _ => pair t) |
|
291 |
|
292 and abs_traverse Ts (n, T, t) = traverse (T::Ts) t #>> (fn t' => (n, T, t')) |
|
293 in |
|
294 |
|
295 fun lift_lambdas ctxt ts = |
|
296 (Termtab.empty, ctxt) |
|
297 |> fold_map (traverse []) ts |
|
298 |> (fn (us, (defs, ctxt')) => |
|
299 (ctxt', Termtab.fold (cons o snd o snd) defs us)) |
|
300 |
|
301 end |
|
302 |
|
303 |
|
304 (** introduce explicit applications **) |
|
305 |
|
306 local |
|
307 (* |
|
308 Make application explicit for functions with varying number of arguments. |
|
309 *) |
|
310 |
|
311 fun add t ts = |
|
312 Termtab.map_default (t, []) (Ord_List.insert int_ord (length ts)) |
|
313 |
|
314 fun collect t = |
|
315 (case Term.strip_comb t of |
|
316 (u as Const _, ts) => add u ts #> fold collect ts |
|
317 | (u as Free _, ts) => add u ts #> fold collect ts |
|
318 | (Abs (_, _, u), ts) => collect u #> fold collect ts |
|
319 | (_, ts) => fold collect ts) |
|
320 |
|
321 fun app ts (t, T) = |
|
322 let val f = Const (@{const_name SMT.fun_app}, T --> T) |
|
323 in (Term.list_comb (f $ t, ts), snd (U.dest_funT (length ts) T)) end |
|
324 |
|
325 fun appl _ _ [] = fst |
|
326 | appl _ [] ts = fst o app ts |
|
327 | appl i (k :: ks) ts = |
|
328 let val (ts1, ts2) = chop (k - i) ts |
|
329 in appl k ks ts2 o app ts1 end |
|
330 |
|
331 fun appl0 [_] ts (t, _) = Term.list_comb (t, ts) |
|
332 | appl0 (0 :: ks) ts tT = appl 0 ks ts tT |
|
333 | appl0 ks ts tT = appl 0 ks ts tT |
|
334 |
|
335 fun apply terms T t ts = appl0 (Termtab.lookup_list terms t) ts (t, T) |
|
336 |
|
337 fun get_arities i t = |
|
338 (case Term.strip_comb t of |
|
339 (Bound j, ts) => |
|
340 (if i = j then Ord_List.insert int_ord (length ts) else I) #> |
|
341 fold (get_arities i) ts |
|
342 | (Abs (_, _, u), ts) => get_arities (i+1) u #> fold (get_arities i) ts |
|
343 | (_, ts) => fold (get_arities i) ts) |
|
344 in |
|
345 |
|
346 fun intro_explicit_application ts = |
|
347 let |
|
348 val terms = fold collect ts Termtab.empty |
|
349 |
|
350 fun traverse (env as (arities, Ts)) t = |
|
351 (case Term.strip_comb t of |
|
352 (u as Const (_, T), ts) => apply terms T u (map (traverse env) ts) |
|
353 | (u as Free (_, T), ts) => apply terms T u (map (traverse env) ts) |
|
354 | (u as Bound i, ts) => |
|
355 appl0 (nth arities i) (map (traverse env) ts) (u, nth Ts i) |
|
356 | (Abs (n, T, u), ts) => |
|
357 let val env' = (get_arities 0 u [] :: arities, T :: Ts) |
|
358 in traverses env (Abs (n, T, traverse env' u)) ts end |
|
359 | (u, ts) => traverses env u ts) |
|
360 and traverses env t ts = Term.list_comb (t, map (traverse env) ts) |
|
361 in map (traverse ([], [])) ts end |
|
362 |
|
363 val fun_app_eq = mk_meta_eq @{thm SMT.fun_app_def} |
|
364 |
|
365 end |
|
366 |
|
367 |
|
368 (** map HOL formulas to FOL formulas (i.e., separate formulas froms terms) **) |
|
369 |
|
370 val tboolT = @{typ SMT.term_bool} |
|
371 val term_true = Const (@{const_name True}, tboolT) |
|
372 val term_false = Const (@{const_name False}, tboolT) |
|
373 |
|
374 val term_bool = @{lemma "True ~= False" by simp} |
|
375 val term_bool_prop = |
|
376 let |
|
377 fun replace @{const HOL.eq (bool)} = @{const HOL.eq (SMT.term_bool)} |
|
378 | replace @{const True} = term_true |
|
379 | replace @{const False} = term_false |
|
380 | replace t = t |
|
381 in |
|
382 Term.map_aterms replace (HOLogic.dest_Trueprop (Thm.prop_of term_bool)) |
|
383 end |
|
384 |
|
385 val fol_rules = [ |
|
386 Let_def, |
|
387 @{lemma "P = True == P" by (rule eq_reflection) simp}, |
|
388 @{lemma "if P then True else False == P" by (rule eq_reflection) simp}] |
|
389 |
|
390 fun reduce_let (Const (@{const_name Let}, _) $ t $ u) = |
|
391 reduce_let (Term.betapply (u, t)) |
|
392 | reduce_let (t $ u) = reduce_let t $ reduce_let u |
|
393 | reduce_let (Abs (n, T, t)) = Abs (n, T, reduce_let t) |
|
394 | reduce_let t = t |
|
395 |
|
396 fun is_pred_type NONE = false |
|
397 | is_pred_type (SOME T) = (Term.body_type T = @{typ bool}) |
|
398 |
|
399 fun is_conn_type NONE = false |
|
400 | is_conn_type (SOME T) = |
|
401 forall (equal @{typ bool}) (Term.body_type T :: Term.binder_types T) |
|
402 |
|
403 fun revert_typ @{typ SMT.term_bool} = @{typ bool} |
|
404 | revert_typ (Type (n, Ts)) = Type (n, map revert_typ Ts) |
|
405 | revert_typ T = T |
|
406 |
|
407 val revert_types = Term.map_types revert_typ |
|
408 |
|
409 fun folify ctxt builtins = |
|
410 let |
|
411 fun as_term t = @{const HOL.eq (SMT.term_bool)} $ t $ term_true |
|
412 |
|
413 fun as_tbool @{typ bool} = tboolT |
|
414 | as_tbool (Type (n, Ts)) = Type (n, map as_tbool Ts) |
|
415 | as_tbool T = T |
|
416 fun mapTs f g i = U.dest_funT i #> (fn (Ts, T) => map f Ts ---> g T) |
|
417 fun predT i = mapTs as_tbool I i |
|
418 fun funcT i = mapTs as_tbool as_tbool i |
|
419 fun func i (n, T) = (n, funcT i T) |
|
420 |
|
421 fun map_ifT T = T |> Term.dest_funT ||> funcT 2 |> (op -->) |
|
422 val if_term = @{const If (bool)} |> Term.dest_Const ||> map_ifT |> Const |
|
423 fun wrap_in_if t = if_term $ t $ term_true $ term_false |
|
424 |
|
425 fun in_list T f t = HOLogic.mk_list T (map f (HOLogic.dest_list t)) |
|
426 |
|
427 fun in_term t = |
|
428 (case Term.strip_comb t of |
|
429 (Const (n as @{const_name If}, T), [t1, t2, t3]) => |
|
430 Const (n, map_ifT T) $ in_form t1 $ in_term t2 $ in_term t3 |
|
431 | (Const (@{const_name HOL.eq}, _), _) => wrap_in_if (in_form t) |
|
432 | (Var (ni as (_, i), T), ts) => |
|
433 let val U = Vartab.lookup builtins ni |
|
434 in |
|
435 if is_conn_type U orelse is_pred_type U then wrap_in_if (in_form t) |
|
436 else Term.list_comb (Var (ni, funcT i T), map in_term ts) |
|
437 end |
|
438 | (Const c, ts) => |
|
439 Term.list_comb (Const (func (length ts) c), map in_term ts) |
|
440 | (Free c, ts) => |
|
441 Term.list_comb (Free (func (length ts) c), map in_term ts) |
|
442 | _ => t) |
|
443 |
|
444 and in_weight ((c as @{const SMT.weight}) $ w $ t) = c $ w $ in_form t |
|
445 | in_weight t = in_form t |
|
446 |
|
447 and in_pat (Const (c as (@{const_name pat}, _)) $ t) = |
|
448 Const (func 1 c) $ in_term t |
|
449 | in_pat (Const (c as (@{const_name nopat}, _)) $ t) = |
|
450 Const (func 1 c) $ in_term t |
|
451 | in_pat t = raise TERM ("bad pattern", [t]) |
|
452 |
|
453 and in_pats ps = |
|
454 in_list @{typ "pattern list"} (in_list @{typ pattern} in_pat) ps |
|
455 |
|
456 and in_trig ((c as @{const trigger}) $ p $ t) = c $ in_pats p $ in_weight t |
|
457 | in_trig t = in_weight t |
|
458 |
|
459 and in_form t = |
|
460 (case Term.strip_comb t of |
|
461 (q as Const (qn, _), [Abs (n, T, u)]) => |
|
462 if member (op =) [@{const_name All}, @{const_name Ex}] qn then |
|
463 q $ Abs (n, as_tbool T, in_trig u) |
|
464 else as_term (in_term t) |
|
465 | (u as Const (@{const_name If}, _), ts) => |
|
466 Term.list_comb (u, map in_form ts) |
|
467 | (b as @{const HOL.eq (bool)}, ts) => Term.list_comb (b, map in_form ts) |
|
468 | (Const (n as @{const_name HOL.eq}, T), ts) => |
|
469 Term.list_comb (Const (n, predT 2 T), map in_term ts) |
|
470 | (b as Var (ni as (_, i), T), ts) => |
|
471 if is_conn_type (Vartab.lookup builtins ni) then |
|
472 Term.list_comb (b, map in_form ts) |
|
473 else if is_pred_type (Vartab.lookup builtins ni) then |
|
474 Term.list_comb (Var (ni, predT i T), map in_term ts) |
|
475 else as_term (in_term t) |
|
476 | _ => as_term (in_term t)) |
|
477 in |
|
478 map (reduce_let #> in_form) #> |
|
479 cons (mark_builtins' ctxt term_bool_prop) #> |
|
480 pair (fol_rules, [term_bool]) |
|
481 end |
|
482 |
|
483 |
|
484 |
|
485 (* translation into intermediate format *) |
|
486 |
|
487 (** utility functions **) |
88 |
488 |
89 val quantifier = (fn |
489 val quantifier = (fn |
90 @{const_name All} => SOME SForall |
490 @{const_name All} => SOME SForall |
91 | @{const_name Ex} => SOME SExists |
491 | @{const_name Ex} => SOME SExists |
92 | _ => NONE) |
492 | _ => NONE) |
122 in (q, rev Ts, ps, w, b) end) |
522 in (q, rev Ts, ps, w, b) end) |
123 |
523 |
124 fun fold_map_pat f (SPat ts) = fold_map f ts #>> SPat |
524 fun fold_map_pat f (SPat ts) = fold_map f ts #>> SPat |
125 | fold_map_pat f (SNoPat ts) = fold_map f ts #>> SNoPat |
525 | fold_map_pat f (SNoPat ts) = fold_map f ts #>> SNoPat |
126 |
526 |
127 fun prop_of thm = HOLogic.dest_Trueprop (Thm.prop_of thm) |
527 |
128 |
528 (** translation from Isabelle terms into SMT intermediate terms **) |
129 |
529 |
130 |
530 fun intermediate header dtyps ctxt ts trx = |
131 (* map HOL formulas to FOL formulas (i.e., separate formulas froms terms) *) |
531 let |
132 |
532 fun transT (T as TFree _) = add_typ T true |
133 val tboolT = @{typ SMT.term_bool} |
533 | transT (T as TVar _) = (fn _ => raise TYPE ("bad SMT type", [T], [])) |
134 val term_true = Const (@{const_name True}, tboolT) |
534 | transT (T as Type _) = |
135 val term_false = Const (@{const_name False}, tboolT) |
|
136 |
|
137 val term_bool = @{lemma "True ~= False" by simp} |
|
138 val term_bool_prop = |
|
139 let |
|
140 fun replace @{const HOL.eq (bool)} = @{const HOL.eq (SMT.term_bool)} |
|
141 | replace @{const True} = term_true |
|
142 | replace @{const False} = term_false |
|
143 | replace t = t |
|
144 in Term.map_aterms replace (prop_of term_bool) end |
|
145 |
|
146 val needs_rewrite = Thm.prop_of #> Term.exists_subterm (fn |
|
147 Const (@{const_name Let}, _) => true |
|
148 | @{const HOL.eq (bool)} $ _ $ @{const True} => true |
|
149 | Const (@{const_name If}, _) $ _ $ @{const True} $ @{const False} => true |
|
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 |
|
157 fun rewrite ctxt ct = |
|
158 Conv.top_sweep_conv (fn ctxt' => |
|
159 Conv.rewrs_conv rewrite_rules then_conv rewrite ctxt') ctxt ct |
|
160 |
|
161 fun normalize ctxt thm = |
|
162 if needs_rewrite thm then Conv.fconv_rule (rewrite ctxt) thm else thm |
|
163 |
|
164 fun revert_typ @{typ SMT.term_bool} = @{typ bool} |
|
165 | revert_typ (Type (n, Ts)) = Type (n, map revert_typ Ts) |
|
166 | revert_typ T = T |
|
167 |
|
168 val revert_types = Term.map_types revert_typ |
|
169 |
|
170 fun folify ctxt = |
|
171 let |
|
172 fun is_builtin_conn (@{const_name True}, _) _ = false |
|
173 | is_builtin_conn (@{const_name False}, _) _ = false |
|
174 | is_builtin_conn c ts = B.is_builtin_conn ctxt c ts |
|
175 |
|
176 fun as_term t = @{const HOL.eq (SMT.term_bool)} $ t $ term_true |
|
177 |
|
178 fun as_tbool @{typ bool} = tboolT |
|
179 | as_tbool (Type (n, Ts)) = Type (n, map as_tbool Ts) |
|
180 | as_tbool T = T |
|
181 fun mapTs f g = Term.strip_type #> (fn (Ts, T) => map f Ts ---> g T) |
|
182 fun predT T = mapTs as_tbool I T |
|
183 fun funcT T = mapTs as_tbool as_tbool T |
|
184 fun func (n, T) = Const (n, funcT T) |
|
185 |
|
186 fun map_ifT T = T |> Term.dest_funT ||> funcT |> (op -->) |
|
187 val if_term = @{const If (bool)} |> Term.dest_Const ||> map_ifT |> Const |
|
188 fun wrap_in_if t = if_term $ t $ term_true $ term_false |
|
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 |
|
194 (Const (c as @{const_name If}, T), [t1, t2, t3]) => |
|
195 Const (c, map_ifT T) $ in_form t1 $ in_term t2 $ in_term t3 |
|
196 | (Const c, ts) => |
|
197 if is_builtin_conn c ts orelse B.is_builtin_pred ctxt c ts |
|
198 then wrap_in_if (in_form t) |
|
199 else Term.list_comb (func c, map in_term ts) |
|
200 | (Free (n, T), ts) => Term.list_comb (Free (n, funcT T), map in_term ts) |
|
201 | _ => t) |
|
202 |
|
203 and in_weight ((c as @{const SMT.weight}) $ w $ t) = c $ w $ in_form t |
|
204 | in_weight t = in_form t |
|
205 |
|
206 and in_pat (Const (c as (@{const_name pat}, _)) $ t) = func c $ in_term t |
|
207 | in_pat (Const (c as (@{const_name nopat}, _)) $ t) = func c $ in_term t |
|
208 | in_pat t = raise TERM ("in_pat", [t]) |
|
209 |
|
210 and in_pats ps = |
|
211 in_list @{typ "pattern list"} (in_list @{typ pattern} in_pat) ps |
|
212 |
|
213 and in_trig ((c as @{const trigger}) $ p $ t) = c $ in_pats p $ in_weight t |
|
214 | in_trig t = in_weight t |
|
215 |
|
216 and in_form t = |
|
217 (case Term.strip_comb t of |
|
218 (q as Const (qn, _), [Abs (n, T, t')]) => |
|
219 if is_some (quantifier qn) then q $ Abs (n, as_tbool T, in_trig t') |
|
220 else as_term (in_term t) |
|
221 | (Const (c as (n as @{const_name distinct}, T)), [t']) => |
|
222 if B.is_builtin_fun ctxt c [t'] then |
|
223 Const (n, predT T) $ in_list T in_term t' |
|
224 else as_term (in_term t) |
|
225 | (Const (c as (n, T)), ts) => |
|
226 if B.is_builtin_conn ctxt c ts |
|
227 then Term.list_comb (Const c, map in_form ts) |
|
228 else if B.is_builtin_pred ctxt c ts |
|
229 then Term.list_comb (Const (n, predT T), map in_term ts) |
|
230 else as_term (in_term t) |
|
231 | _ => as_term (in_term t)) |
|
232 in |
|
233 map (apsnd (normalize ctxt)) #> (fn irules => |
|
234 ((rewrite_rules, (~1, term_bool) :: irules), |
|
235 term_bool_prop :: map (in_form o prop_of o snd) irules)) |
|
236 end |
|
237 |
|
238 |
|
239 |
|
240 (* translation from Isabelle terms into SMT intermediate terms *) |
|
241 |
|
242 val empty_context = (1, Typtab.empty, [], 1, Termtab.empty) |
|
243 |
|
244 fun make_sign header (_, typs, dtyps, _, terms) = { |
|
245 header = header, |
|
246 sorts = Typtab.fold (fn (_, (n, true)) => cons n | _ => I) typs [], |
|
247 funcs = Termtab.fold (fn (_, (n, SOME ss)) => cons (n,ss) | _ => I) terms [], |
|
248 dtyps = rev dtyps } |
|
249 |
|
250 fun make_recon (unfolds, assms) (_, typs, _, _, terms) = { |
|
251 typs = Symtab.make (map (apfst fst o swap) (Typtab.dest typs)), |
|
252 (*FIXME: don't drop the datatype information! *) |
|
253 terms = Symtab.make (map (fn (t, (n, _)) => (n, t)) (Termtab.dest terms)), |
|
254 unfolds = unfolds, |
|
255 assms = assms } |
|
256 |
|
257 fun string_of_index pre i = pre ^ string_of_int i |
|
258 |
|
259 fun new_typ sort_prefix proper T (Tidx, typs, dtyps, idx, terms) = |
|
260 let |
|
261 val s = string_of_index sort_prefix Tidx |
|
262 val U = revert_typ T |
|
263 in (s, (Tidx+1, Typtab.update (U, (s, proper)) typs, dtyps, idx, terms)) end |
|
264 |
|
265 fun lookup_typ (_, typs, _, _, _) = Typtab.lookup typs o revert_typ |
|
266 |
|
267 fun fresh_typ T f cx = |
|
268 (case lookup_typ cx T of |
|
269 SOME (s, _) => (s, cx) |
|
270 | NONE => f T cx) |
|
271 |
|
272 fun new_fun func_prefix t ss (Tidx, typs, dtyps, idx, terms) = |
|
273 let |
|
274 val f = string_of_index func_prefix idx |
|
275 val terms' = Termtab.update (revert_types t, (f, ss)) terms |
|
276 in (f, (Tidx, typs, dtyps, idx+1, terms')) end |
|
277 |
|
278 fun fresh_fun func_prefix t ss (cx as (_, _, _, _, terms)) = |
|
279 (case Termtab.lookup terms (revert_types t) of |
|
280 SOME (f, _) => (f, cx) |
|
281 | NONE => new_fun func_prefix t ss cx) |
|
282 |
|
283 fun mk_type (_, Tfs) (d as Datatype.DtTFree _) = the (AList.lookup (op =) Tfs d) |
|
284 | mk_type Ts (Datatype.DtType (n, ds)) = Type (n, map (mk_type Ts) ds) |
|
285 | mk_type (Tds, _) (Datatype.DtRec i) = nth Tds i |
|
286 |
|
287 fun mk_selector ctxt Ts T n (i, d) = |
|
288 (case Datatype_Selectors.lookup_selector ctxt (n, i+1) of |
|
289 NONE => raise Fail ("missing selector for datatype constructor " ^ quote n) |
|
290 | SOME m => mk_type Ts d |> (fn U => (Const (m, T --> U), U))) |
|
291 |
|
292 fun mk_constructor ctxt Ts T (n, args) = |
|
293 let val (sels, Us) = split_list (map_index (mk_selector ctxt Ts T n) args) |
|
294 in (Const (n, Us ---> T), sels) end |
|
295 |
|
296 fun lookup_datatype ctxt n Ts = |
|
297 if member (op =) [@{type_name bool}, @{type_name nat}] n then NONE |
|
298 else |
|
299 Datatype.get_info (ProofContext.theory_of ctxt) n |
|
300 |> Option.map (fn {descr, ...} => |
|
301 let |
|
302 val Tds = map (fn (_, (tn, _, _)) => Type (tn, Ts)) |
|
303 (sort (int_ord o pairself fst) descr) |
|
304 val Tfs = (case hd descr of (_, (_, tfs, _)) => tfs ~~ Ts) |
|
305 in |
|
306 descr |> map (fn (i, (_, _, cs)) => |
|
307 (nth Tds i, map (mk_constructor ctxt (Tds, Tfs) (nth Tds i)) cs)) |
|
308 end) |
|
309 |
|
310 fun relaxed irules = (([], irules), map (prop_of o snd) irules) |
|
311 |
|
312 fun with_context header f (ths, ts) = |
|
313 let val (us, context) = fold_map f ts empty_context |
|
314 in ((make_sign (header ts) context, us), make_recon ths context) end |
|
315 |
|
316 |
|
317 fun translate config ctxt comments = |
|
318 let |
|
319 val {prefixes, is_fol, header, has_datatypes, serialize} = config |
|
320 val {sort_prefix, func_prefix} = prefixes |
|
321 |
|
322 fun transT (T as TFree _) = fresh_typ T (new_typ sort_prefix true) |
|
323 | transT (T as TVar _) = (fn _ => raise TYPE ("smt_translate", [T], [])) |
|
324 | transT (T as Type (n, Ts)) = |
|
325 (case B.builtin_typ ctxt T of |
535 (case B.builtin_typ ctxt T of |
326 SOME n => pair n |
536 SOME n => pair n |
327 | NONE => fresh_typ T (fn _ => fn cx => |
537 | NONE => add_typ T true) |
328 if not has_datatypes then new_typ sort_prefix true T cx |
538 |
329 else |
539 val unmarked_builtins = [@{const_name If}, @{const_name HOL.eq}] |
330 (case lookup_datatype ctxt n Ts of |
|
331 NONE => new_typ sort_prefix true T cx |
|
332 | SOME dts => |
|
333 let val cx' = new_dtyps dts cx |
|
334 in (fst (the (lookup_typ cx' T)), cx') end))) |
|
335 |
|
336 and new_dtyps dts cx = |
|
337 let |
|
338 fun new_decl i t = |
|
339 let val (Ts, T) = U.dest_funT i (Term.fastype_of t) |
|
340 in |
|
341 fold_map transT Ts ##>> transT T ##>> |
|
342 new_fun func_prefix t NONE #>> swap |
|
343 end |
|
344 fun new_dtyp_decl (con, sels) = |
|
345 new_decl (length sels) con ##>> fold_map (new_decl 1) sels #>> |
|
346 (fn ((con', _), sels') => (con', map (apsnd snd) sels')) |
|
347 in |
|
348 cx |
|
349 |> fold_map (new_typ sort_prefix false o fst) dts |
|
350 ||>> fold_map (fold_map new_dtyp_decl o snd) dts |
|
351 |-> (fn (ss, decls) => fn (Tidx, typs, dtyps, idx, terms) => |
|
352 (Tidx, typs, (ss ~~ decls) :: dtyps, idx, terms)) |
|
353 end |
|
354 |
540 |
355 fun app n ts = SApp (n, ts) |
541 fun app n ts = SApp (n, ts) |
356 |
542 |
357 fun trans t = |
543 fun trans t = |
358 (case Term.strip_comb t of |
544 (case Term.strip_comb t of |
359 (Const (qn, _), [Abs (_, T, t1)]) => |
545 (Const (qn, _), [Abs (_, T, t1)]) => |
360 (case dest_quant qn T t1 of |
546 (case dest_quant qn T t1 of |
361 SOME (q, Ts, ps, w, b) => |
547 SOME (q, Ts, ps, w, b) => |
362 fold_map transT Ts ##>> fold_map (fold_map_pat trans) ps ##>> |
548 fold_map transT Ts ##>> fold_map (fold_map_pat trans) ps ##>> |
363 trans b #>> (fn ((Ts', ps'), b') => SQua (q, Ts', ps', w, b')) |
549 trans b #>> (fn ((Ts', ps'), b') => SQua (q, Ts', ps', w, b')) |
364 | NONE => raise TERM ("intermediate", [t])) |
550 | NONE => raise TERM ("unsupported quantifier", [t])) |
365 | (Const (@{const_name Let}, _), [t1, Abs (_, T, t2)]) => |
551 | (Const (@{const_name Let}, _), [t1, Abs (_, T, t2)]) => |
366 transT T ##>> trans t1 ##>> trans t2 #>> |
552 transT T ##>> trans t1 ##>> trans t2 #>> |
367 (fn ((U, u1), u2) => SLet (U, u1, u2)) |
553 (fn ((U, u1), u2) => SLet (U, u1, u2)) |
368 | (h as Const (c as (@{const_name distinct}, T)), ts) => |
554 | (Var ((n, _), _), ts) => fold_map trans ts #>> app n |
369 (case B.builtin_fun ctxt c ts of |
555 | (u as Const (c as (n, T)), ts) => |
370 SOME (n, ts) => fold_map trans ts #>> app n |
556 if member (op =) unmarked_builtins n then |
371 | NONE => transs h T ts) |
557 (case B.builtin_fun ctxt c ts of |
372 | (h as Const (c as (_, T)), ts) => |
558 SOME (((m, _), _), us, _) => fold_map trans us #>> app m |
373 (case B.builtin_num ctxt t of |
559 | NONE => raise TERM ("not a built-in symbol", [t])) |
374 SOME n => pair (SApp (n, [])) |
560 else transs u T ts |
375 | NONE => |
561 | (u as Free (_, T), ts) => transs u T ts |
376 (case B.builtin_fun ctxt c ts of |
|
377 SOME (n, ts') => fold_map trans ts' #>> app n |
|
378 | NONE => transs h T ts)) |
|
379 | (h as Free (_, T), ts) => transs h T ts |
|
380 | (Bound i, []) => pair (SVar i) |
562 | (Bound i, []) => pair (SVar i) |
381 | (Abs (_, _, t1 $ Bound 0), []) => |
563 | _ => raise TERM ("bad SMT term", [t])) |
382 if not (loose_bvar1 (t1, 0)) then trans t1 (* eta-reduce on the fly *) |
564 |
383 else raise TERM ("smt_translate", [t]) |
|
384 | _ => raise TERM ("smt_translate", [t])) |
|
385 |
|
386 and transs t T ts = |
565 and transs t T ts = |
387 let val (Us, U) = U.dest_funT (length ts) T |
566 let val (Us, U) = U.dest_funT (length ts) T |
388 in |
567 in |
389 fold_map transT Us ##>> transT U #-> (fn Up => |
568 fold_map transT Us ##>> transT U #-> (fn Up => |
390 fresh_fun func_prefix t (SOME Up) ##>> fold_map trans ts #>> SApp) |
569 add_fun t (SOME Up) ##>> fold_map trans ts #>> SApp) |
391 end |
570 end |
|
571 |
|
572 val (us, trx') = fold_map trans ts trx |
|
573 in ((sign_of (header ts) dtyps trx', us), trx') end |
|
574 |
|
575 |
|
576 |
|
577 (* translation *) |
|
578 |
|
579 structure Configs = Generic_Data |
|
580 ( |
|
581 type T = (Proof.context -> config) U.dict |
|
582 val empty = [] |
|
583 val extend = I |
|
584 val merge = U.dict_merge fst |
|
585 ) |
|
586 |
|
587 fun add_config (cs, cfg) = Configs.map (U.dict_update (cs, cfg)) |
|
588 |
|
589 fun translate ctxt comments ithms = |
|
590 let |
|
591 val cs = SMT_Config.solver_class_of ctxt |
|
592 val {prefixes, is_fol, header, has_datatypes, serialize} = |
|
593 (case U.dict_get (Configs.get (Context.Proof ctxt)) cs of |
|
594 SOME cfg => cfg ctxt |
|
595 | NONE => error ("SMT: no translation configuration found " ^ |
|
596 "for solver class " ^ quote (U.string_of_class cs))) |
|
597 |
|
598 val with_datatypes = |
|
599 has_datatypes andalso Config.get ctxt SMT_Config.datatypes |
|
600 |
|
601 fun no_dtyps (tr_context, ctxt) ts = (([], tr_context, ctxt), ts) |
|
602 |
|
603 val (builtins, ts1) = |
|
604 ithms |
|
605 |> map (HOLogic.dest_Trueprop o Thm.prop_of o snd) |
|
606 |> map (Envir.eta_contract o Envir.beta_norm) |
|
607 |> mark_builtins ctxt |
|
608 |
|
609 val ((dtyps, tr_context, ctxt1), ts2) = |
|
610 ((make_tr_context prefixes, ctxt), ts1) |
|
611 |-> (if with_datatypes then collect_datatypes_and_records else no_dtyps) |
|
612 |
|
613 val (ctxt2, ts3) = |
|
614 ts2 |
|
615 |> eta_expand |
|
616 |> lift_lambdas ctxt1 |
|
617 ||> intro_explicit_application |
|
618 |
|
619 val ((rewrite_rules, extra_thms), ts4) = |
|
620 (if is_fol then folify ctxt2 builtins else pair ([], [])) ts3 |
|
621 |
|
622 val rewrite_rules' = fun_app_eq :: rewrite_rules |
392 in |
623 in |
393 (if is_fol then folify ctxt else relaxed) #> |
624 (ts4, tr_context) |
394 with_context (header ctxt) trans #>> uncurry (serialize comments) |
625 |-> intermediate header dtyps ctxt2 |
|
626 |>> uncurry (serialize comments) |
|
627 ||> recon_of ctxt2 rewrite_rules' extra_thms ithms revert_typ revert_types |
395 end |
628 end |
396 |
629 |
397 end |
630 end |