summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-09-11 19:59:31 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-09-11 19:59:31 -0400
commita12b7d5677662153dd69c14945c0d88f447425a3 (patch)
tree6a16a83ce73b7c035f67e6d51c982e3bf79115ad
parenta1c9eb584060bb6fac219f53540324777a7fa5b4 (diff)
Fixed a mind-numbing De Bruijn bug
-rw-r--r--lib/top.ur10
-rw-r--r--src/elab_env.sml3
-rw-r--r--src/elab_ops.sml8
-rw-r--r--src/elaborate.sml13
4 files changed, 27 insertions, 7 deletions
diff --git a/lib/top.ur b/lib/top.ur
index 16d2ed42..ec0e58af 100644
--- a/lib/top.ur
+++ b/lib/top.ur
@@ -4,3 +4,13 @@ con mapTT (f :: Type -> Type) = fold (fn nm t acc => [nm] ~ acc =>
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 --git a/src/elab_env.sml b/src/elab_env.sml
index 1b9de129..6c3d7802 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -241,7 +241,8 @@ fun pushCRel (env : env) x k =
})
(#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 --git a/src/elab_ops.sml b/src/elab_ops.sml
index 6c75768b..3cdc37c1 100644
--- a/src/elab_ops.sml
+++ b/src/elab_ops.sml
@@ -92,10 +92,10 @@ fun hnormCon env (cAll as (c, loc)) =
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 --git a/src/elaborate.sml b/src/elaborate.sml
index 223c10e6..7e4ff670 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -1609,19 +1609,26 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
| 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 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
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),