Mercurial > urweb
changeset 328:58f1260f293f
Fixed a mind-numbing De Bruijn bug
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Thu, 11 Sep 2008 19:59:31 -0400 (2008-09-11) |
parents | 3a57f3b3a3f8 |
children | eec65c11d3e2 |
files | lib/top.ur src/elab_env.sml src/elab_ops.sml src/elaborate.sml |
diffstat | 4 files changed, 27 insertions(+), 7 deletions(-) [+] |
line wrap: on
line diff
--- 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)
--- 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),
--- 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) =>
--- 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),