diff options
author | Nadrieril | 2020-12-06 21:41:03 +0000 |
---|---|---|
committer | Nadrieril | 2020-12-07 19:34:38 +0000 |
commit | 6287b7a7f9e421877ee13fefa586395fec844c99 (patch) | |
tree | 65129001dbd7e56561df656dc8eee8f441a05b25 /dhall/src/semantics/tck/env.rs | |
parent | 9991bd4891774c4dd598decae02ee860554d2ab7 (diff) |
Thread cx through typecheck
Diffstat (limited to 'dhall/src/semantics/tck/env.rs')
-rw-r--r-- | dhall/src/semantics/tck/env.rs | 16 |
1 files changed, 12 insertions, 4 deletions
diff --git a/dhall/src/semantics/tck/env.rs b/dhall/src/semantics/tck/env.rs index 1fa66f0..fc0ce9f 100644 --- a/dhall/src/semantics/tck/env.rs +++ b/dhall/src/semantics/tck/env.rs @@ -1,5 +1,6 @@ use crate::semantics::{AlphaVar, NameEnv, Nir, NzEnv, NzVar, Type, ValEnv}; use crate::syntax::Label; +use crate::Ctxt; /// Environment for indexing variables. #[derive(Debug, Clone, Copy, Default)] @@ -9,7 +10,8 @@ pub struct VarEnv { /// Environment for typing expressions. #[derive(Debug, Clone)] -pub struct TyEnv { +pub struct TyEnv<'cx> { + cx: Ctxt<'cx>, names: NameEnv, items: ValEnv<Type>, } @@ -38,13 +40,17 @@ impl VarEnv { } } -impl TyEnv { - pub fn new() -> Self { +impl<'cx> TyEnv<'cx> { + pub fn new(cx: Ctxt<'cx>) -> Self { TyEnv { + cx, names: NameEnv::new(), items: ValEnv::new(), } } + pub fn cx(&self) -> Ctxt<'cx> { + self.cx + } pub fn as_varenv(&self) -> VarEnv { self.names.as_varenv() } @@ -57,12 +63,14 @@ impl TyEnv { pub fn insert_type(&self, x: &Label, ty: Type) -> 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 { TyEnv { + cx: self.cx, names: self.names.insert(x), items: self.items.insert_value(e, ty), } @@ -72,7 +80,7 @@ impl TyEnv { } } -impl<'a> From<&'a TyEnv> for NzEnv { +impl<'a, 'cx> From<&'a TyEnv<'cx>> for NzEnv { fn from(x: &'a TyEnv) -> Self { x.to_nzenv() } |