diff options
author | Nadrieril | 2020-12-06 23:55:21 +0000 |
---|---|---|
committer | Nadrieril | 2020-12-07 19:34:38 +0000 |
commit | c785b7c0c6cd8b3b1cc15eb79caf982a757020ba (patch) | |
tree | 6d38e68385814073b8b22ee8a8956435546892dc /dhall/src/semantics/tck/env.rs | |
parent | 6287b7a7f9e421877ee13fefa586395fec844c99 (diff) |
Thread cx through normalization
Diffstat (limited to 'dhall/src/semantics/tck/env.rs')
-rw-r--r-- | dhall/src/semantics/tck/env.rs | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/dhall/src/semantics/tck/env.rs b/dhall/src/semantics/tck/env.rs index fc0ce9f..fdcc62d 100644 --- a/dhall/src/semantics/tck/env.rs +++ b/dhall/src/semantics/tck/env.rs @@ -13,7 +13,7 @@ pub struct VarEnv { pub struct TyEnv<'cx> { cx: Ctxt<'cx>, names: NameEnv, - items: ValEnv<Type>, + items: ValEnv<'cx, Type<'cx>>, } impl VarEnv { @@ -45,7 +45,7 @@ impl<'cx> TyEnv<'cx> { TyEnv { cx, names: NameEnv::new(), - items: ValEnv::new(), + items: ValEnv::new(cx), } } pub fn cx(&self) -> Ctxt<'cx> { @@ -54,34 +54,34 @@ impl<'cx> TyEnv<'cx> { pub fn as_varenv(&self) -> VarEnv { self.names.as_varenv() } - pub fn to_nzenv(&self) -> NzEnv { + pub fn to_nzenv(&self) -> NzEnv<'cx> { self.items.discard_types() } pub fn as_nameenv(&self) -> &NameEnv { &self.names } - pub fn insert_type(&self, x: &Label, ty: Type) -> Self { + pub fn insert_type(&self, x: &Label, ty: Type<'cx>) -> Self { TyEnv { cx: self.cx, names: self.names.insert(x), items: self.items.insert_type(ty), } } - pub fn insert_value(&self, x: &Label, e: Nir, ty: Type) -> Self { + pub fn insert_value(&self, x: &Label, e: Nir<'cx>, ty: Type<'cx>) -> Self { TyEnv { cx: self.cx, names: self.names.insert(x), items: self.items.insert_value(e, ty), } } - pub fn lookup(&self, var: AlphaVar) -> Type { + pub fn lookup(&self, var: AlphaVar) -> Type<'cx> { self.items.lookup_ty(var) } } -impl<'a, 'cx> From<&'a TyEnv<'cx>> for NzEnv { - fn from(x: &'a TyEnv) -> Self { +impl<'a, 'cx> From<&'a TyEnv<'cx>> for NzEnv<'cx> { + fn from(x: &'a TyEnv<'cx>) -> Self { x.to_nzenv() } } |