summaryrefslogtreecommitdiff
path: root/dhall/src/semantics/nze
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src/semantics/nze')
-rw-r--r--dhall/src/semantics/nze/nzexpr.rs24
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)))
}
}