# HG changeset patch # User boehmes # Date 1292504057 -3600 # Node ID aa627a799e8e9bbc375ae133f288ee7c56dbbd50 # Parent edab1efe0a7086d1668ab9d107f123b273248e70# Parent 9796e5e01b61e2aa6bacc32a4073ceda7070de4c merged diff -r 9796e5e01b61 -r aa627a799e8e src/HOL/Tools/SMT/smt_translate.ML --- a/src/HOL/Tools/SMT/smt_translate.ML Thu Dec 16 12:19:00 2010 +0000 +++ b/src/HOL/Tools/SMT/smt_translate.ML Thu Dec 16 13:54:17 2010 +0100 @@ -202,7 +202,12 @@ fun expf t i T ts = let val Ts = U.dest_funT i T |> fst |> drop (length ts) - in Term.list_comb (t, ts) |> fold_rev eta Ts end + in + Term.list_comb (t, ts) + |> Term.incr_boundvars (length Ts) + |> fold_index (fn (i, _) => fn u => u $ Bound i) Ts + |> fold_rev (fn T => fn u => Abs (Name.uu, T, u)) Ts + end fun expand ((q as Const (@{const_name All}, _)) $ Abs a) = q $ abs_expand a | expand ((q as Const (@{const_name All}, T)) $ t) = q $ exp T t @@ -249,16 +254,18 @@ val T = Term.fastype_of1 (Us @ Ts, t) val lev = length Us val bs = sort int_ord (Term.add_loose_bnos (t, lev, [])) - val bss = map_index (fn (i, j) => (j, Integer.add lev i)) bs + val bss = map_index (fn (i, j) => (j + lev, i + lev)) bs val norm = perhaps (AList.lookup (op =) bss) val t' = Term.map_aterms (fn Bound i => Bound (norm i) | t => t) t val Ts' = map (nth Ts) bs fun mk_abs U u = Abs (Name.uu, U, u) val abs_rhs = fold mk_abs Ts' (fold mk_abs Us t') + + fun app f = Term.list_comb (f, map Bound bs) in (case Termtab.lookup defs abs_rhs of - SOME (f, _) => (Term.list_comb (f, map Bound bs), cx) + SOME (f, _) => (app f, cx) | NONE => let val (n, ctxt') = @@ -270,7 +277,7 @@ |> fold_rev (mk_bapp o snd) bss |> fold_rev mk_bapp (0 upto (length Us - 1)) val def = mk_def (Us @ Ts') T lhs t' - in (f, (Termtab.update (abs_rhs, (f, def)) defs, ctxt')) end) + in (app f, (Termtab.update (abs_rhs, (f, def)) defs, ctxt')) end) end fun dest_abs Ts (Abs (_, T, t)) = dest_abs (T :: Ts) t @@ -356,7 +363,7 @@ | (u as Bound i, ts) => appl0 (nth arities i) (map (traverse env) ts) (u, nth Ts i) | (Abs (n, T, u), ts) => - let val env' = (get_arities 0 u [] :: arities, T :: Ts) + let val env' = (get_arities 0 u [0] :: arities, T :: Ts) in traverses env (Abs (n, T, traverse env' u)) ts end | (u, ts) => traverses env u ts) and traverses env t ts = Term.list_comb (t, map (traverse env) ts)