diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2008-09-11 19:59:31 -0400 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2008-09-11 19:59:31 -0400 |
| commit | a12b7d5677662153dd69c14945c0d88f447425a3 (patch) | |
| tree | 6a16a83ce73b7c035f67e6d51c982e3bf79115ad /src | |
| parent | a1c9eb584060bb6fac219f53540324777a7fa5b4 (diff) | |
Fixed a mind-numbing De Bruijn bug
Diffstat (limited to 'src')
| -rw-r--r-- | src/elab_env.sml | 3 | ||||
| -rw-r--r-- | src/elab_ops.sml | 8 | ||||
| -rw-r--r-- | src/elaborate.sml | 13 |
3 files changed, 17 insertions, 7 deletions
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), |