diff options
author | Nadrieril | 2020-12-08 18:47:41 +0000 |
---|---|---|
committer | GitHub | 2020-12-08 18:47:41 +0000 |
commit | 109dcf894e759bce1c28f9ae94f3fdaa6e08feb5 (patch) | |
tree | 9ce374d02ea15966c7bb2dfb39d5d81720a63687 /dhall/src/semantics/nze/env.rs | |
parent | 35ed301e8de5a2b1102e370e638564d3c3d204a8 (diff) | |
parent | d0a61179addf838d33e7e7a4c6a13f06e871e9c5 (diff) |
Merge pull request #204 from Nadrieril/source-id
Diffstat (limited to 'dhall/src/semantics/nze/env.rs')
-rw-r--r-- | dhall/src/semantics/nze/env.rs | 42 |
1 files changed, 25 insertions, 17 deletions
diff --git a/dhall/src/semantics/nze/env.rs b/dhall/src/semantics/nze/env.rs index ec99dbe..30fa8af 100644 --- a/dhall/src/semantics/nze/env.rs +++ b/dhall/src/semantics/nze/env.rs @@ -1,4 +1,5 @@ use crate::semantics::{AlphaVar, Nir, NirKind}; +use crate::Ctxt; #[derive(Debug, Clone, Copy, PartialEq, Eq)] pub enum NzVar { @@ -9,19 +10,20 @@ pub enum NzVar { } #[derive(Debug, Clone)] -enum EnvItem<Type> { +enum EnvItem<'cx, T> { // Variable is bound with given type - Kept(Type), + Kept(T), // Variable has been replaced by corresponding value - Replaced(Nir, Type), + Replaced(Nir<'cx>, T), } #[derive(Debug, Clone)] -pub struct ValEnv<Type> { - items: Vec<EnvItem<Type>>, +pub struct ValEnv<'cx, T> { + cx: Ctxt<'cx>, + items: Vec<EnvItem<'cx, T>>, } -pub type NzEnv = ValEnv<()>; +pub type NzEnv<'cx> = ValEnv<'cx, ()>; impl NzVar { pub fn new(idx: usize) -> Self { @@ -46,11 +48,17 @@ impl NzVar { } } -impl<Type: Clone> ValEnv<Type> { - pub fn new() -> Self { - ValEnv { items: Vec::new() } +impl<'cx, T: Clone> ValEnv<'cx, T> { + pub fn new(cx: Ctxt<'cx>) -> Self { + ValEnv { + cx, + items: Vec::new(), + } + } + pub fn cx(&self) -> Ctxt<'cx> { + self.cx } - pub fn discard_types(&self) -> ValEnv<()> { + pub fn discard_types(&self) -> ValEnv<'cx, ()> { let items = self .items .iter() @@ -59,27 +67,27 @@ impl<Type: Clone> ValEnv<Type> { EnvItem::Replaced(val, _) => EnvItem::Replaced(val.clone(), ()), }) .collect(); - ValEnv { items } + ValEnv { cx: self.cx, items } } - pub fn insert_type(&self, ty: Type) -> Self { + pub fn insert_type(&self, ty: T) -> Self { let mut env = self.clone(); env.items.push(EnvItem::Kept(ty)); env } - pub fn insert_value(&self, e: Nir, ty: Type) -> Self { + pub fn insert_value(&self, e: Nir<'cx>, ty: T) -> Self { let mut env = self.clone(); env.items.push(EnvItem::Replaced(e, ty)); env } - pub fn lookup_val(&self, var: AlphaVar) -> NirKind { + pub fn lookup_val(&self, var: AlphaVar) -> NirKind<'cx> { let idx = self.items.len() - 1 - var.idx(); match &self.items[idx] { EnvItem::Kept(_) => NirKind::Var(NzVar::new(idx)), EnvItem::Replaced(x, _) => x.kind().clone(), } } - pub fn lookup_ty(&self, var: AlphaVar) -> Type { + pub fn lookup_ty(&self, var: AlphaVar) -> T { let idx = self.items.len() - 1 - var.idx(); match &self.items[idx] { EnvItem::Kept(ty) | EnvItem::Replaced(_, ty) => ty.clone(), @@ -87,8 +95,8 @@ impl<Type: Clone> ValEnv<Type> { } } -impl<'a> From<&'a NzEnv> for NzEnv { - fn from(x: &'a NzEnv) -> Self { +impl<'cx, 'a> From<&'a NzEnv<'cx>> for NzEnv<'cx> { + fn from(x: &'a NzEnv<'cx>) -> Self { x.clone() } } |