diff options
Diffstat (limited to 'dhall/src/semantics/nze')
-rw-r--r-- | dhall/src/semantics/nze/nzexpr.rs | 24 |
1 files changed, 17 insertions, 7 deletions
diff --git a/dhall/src/semantics/nze/nzexpr.rs b/dhall/src/semantics/nze/nzexpr.rs index 49aa704..33fdde3 100644 --- a/dhall/src/semantics/nze/nzexpr.rs +++ b/dhall/src/semantics/nze/nzexpr.rs @@ -82,16 +82,16 @@ pub(crate) struct QuoteEnv { } // Reverse-debruijn index: counts number of binders from the bottom of the stack. -#[derive(Debug, Clone, Copy, Eq)] +#[derive(Debug, Clone, Copy, PartialEq, Eq)] pub(crate) struct NzVar { idx: usize, } // TODO: temporary hopefully -impl std::cmp::PartialEq for NzVar { - fn eq(&self, _other: &Self) -> bool { - true - } -} +// impl std::cmp::PartialEq for NzVar { +// fn eq(&self, _other: &Self) -> bool { +// true +// } +// } impl TyEnv { pub fn new() -> Self { @@ -144,6 +144,9 @@ impl NameEnv { size: self.names.len(), } } + pub fn names(&self) -> &[Binder] { + &self.names + } pub fn insert(&self, x: &Binder) -> Self { let mut env = self.clone(); @@ -220,13 +223,20 @@ impl QuoteEnv { pub fn construct(size: usize) -> Self { QuoteEnv { size } } + pub fn size(&self) -> usize { + self.size + } pub fn insert(&self) -> Self { QuoteEnv { size: self.size + 1, } } pub fn lookup(&self, var: &NzVar) -> AlphaVar { - AlphaVar::new(V((), self.size - var.idx - 1)) + self.lookup_fallible(var).unwrap() + } + pub fn lookup_fallible(&self, var: &NzVar) -> Option<AlphaVar> { + let idx = self.size.checked_sub(var.idx + 1)?; + Some(AlphaVar::new(V((), idx))) } } |