# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1221177571 14400
# Node ID 58f1260f293ffc650f046d52e043636305dd2c54
# Parent  3a57f3b3a3f8de6550b73da951b0116da191c65d
Fixed a mind-numbing De Bruijn bug

diff -r 3a57f3b3a3f8 -r 58f1260f293f lib/top.ur
--- a/lib/top.ur	Thu Sep 11 18:36:20 2008 -0400
+++ b/lib/top.ur	Thu Sep 11 19:59:31 2008 -0400
@@ -4,3 +4,13 @@
 fun compose (t1 ::: Type) (t2 ::: Type) (t3 ::: Type) (f1 : t2 -> t3) (f2 : t1 -> t2) (x : t1) = f1 (f2 x)
 
 fun txt (t ::: Type) (ctx ::: {Unit}) (use ::: {Type}) (sh : show t) (v : t) = cdata (show sh v)
+
+fun foldTR2 (tf1 :: Type -> Type) (tf2 :: Type -> Type) (tr :: {Type} -> Type)
+        (f : nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest
+                -> tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
+        (i : tr []) =
+        fold [fn r :: {Type} => $(mapTT tf1 r) -> $(mapTT tf2 r) -> tr r]
+                (fn (nm :: Name) (t :: Type) (rest :: {Type}) (acc : _ -> _ -> tr rest) =>
+                        [[nm] ~ rest] =>
+                        fn r1 r2 => f [nm] [t] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm)))
+                (fn _ _ => i)
diff -r 3a57f3b3a3f8 -r 58f1260f293f src/elab_env.sml
--- a/src/elab_env.sml	Thu Sep 11 18:36:20 2008 -0400
+++ b/src/elab_env.sml	Thu Sep 11 19:59:31 2008 -0400
@@ -241,7 +241,8 @@
                           })
                           (#classes env),
 
-         renameE = #renameE env,
+         renameE = SM.map (fn Rel' (n, c) => Rel' (n, lift c)
+                            | Named' (n, c) => Named' (n, lift c)) (#renameE env),
          relE = map (fn (x, c) => (x, lift c)) (#relE env),
          namedE = IM.map (fn (x, c) => (x, lift c)) (#namedE env),
 
diff -r 3a57f3b3a3f8 -r 58f1260f293f src/elab_ops.sml
--- a/src/elab_ops.sml	Thu Sep 11 18:36:20 2008 -0400
+++ b/src/elab_ops.sml	Thu Sep 11 19:59:31 2008 -0400
@@ -92,10 +92,10 @@
                      handle SynUnif => cAll
                  (*val env' = E.pushCRel env x k*)
              in
-                 (*eprefaces "Subst" [("x", Print.PD.string x),
-                                    ("cb", p_con env' cb),
-                                    ("c2", p_con env c2),
-                                    ("sc", p_con env sc)];*)
+                 (*Print.eprefaces "Subst" [("x", Print.PD.string x),
+                                          ("cb", ElabPrint.p_con env' cb),
+                                          ("c2", ElabPrint.p_con env c2),
+                                          ("sc", ElabPrint.p_con env sc)];*)
                  sc
              end
            | c1' as CApp (c', i) =>
diff -r 3a57f3b3a3f8 -r 58f1260f293f src/elaborate.sml
--- a/src/elaborate.sml	Thu Sep 11 18:36:20 2008 -0400
+++ b/src/elaborate.sml	Thu Sep 11 19:59:31 2008 -0400
@@ -1609,19 +1609,26 @@
           | L.ECApp (e, c) =>
             let
                 val (e', et, gs1) = elabExp (env, denv) e
+                val oldEt = et
                 val (e', et, gs2) = elabHead (env, denv) e' et
                 val (c', ck, gs3) = elabCon (env, denv) c
                 val ((et', _), gs4) = hnormCon (env, denv) et
             in
                 case et' of
                     L'.CError => (eerror, cerror, [])
-                  | L'.TCFun (_, _, k, eb) =>
+                  | L'.TCFun (_, x, k, eb) =>
                     let
                         val () = checkKind env c' ck k
                         val eb' = subConInCon (0, c') eb
                             handle SynUnif => (expError env (Unif ("substitution", eb));
                                                cerror)
                     in
+                        (*prefaces "Elab ECApp" [("e", SourcePrint.p_exp eAll),
+                                               ("et", p_con env oldEt),
+                                               ("x", PD.string x),
+                                               ("eb", p_con (E.pushCRel env x k) eb),
+                                               ("c", p_con env c'),
+                                               ("eb'", p_con env eb')];*)
                         ((L'.ECApp (e', c'), loc), eb', gs1 @ gs2 @ enD gs3 @ enD gs4)
                     end
 
@@ -1637,7 +1644,9 @@
             let
                 val expl' = elabExplicitness expl
                 val k' = elabKind k
-                val (e', et, gs) = elabExp (E.pushCRel env x k', D.enter denv) e
+
+                val env' = E.pushCRel env x k'
+                val (e', et, gs) = elabExp (env', D.enter denv) e
             in
                 ((L'.ECAbs (expl', x, k', e'), loc),
                  (L'.TCFun (expl', x, k', et), loc),