diff options
| -rw-r--r-- | lib/top.ur | 10 | ||||
| -rw-r--r-- | src/elab_env.sml | 3 | ||||
| -rw-r--r-- | src/elab_ops.sml | 8 | ||||
| -rw-r--r-- | src/elaborate.sml | 13 |
4 files changed, 27 insertions, 7 deletions
@@ -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), |