From 5a835d9db35bf76858e178e1bd66e60128879629 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Mon, 27 Jan 2020 18:45:09 +0000
Subject: Fix a bunch of bugs and more tck

---
 dhall/src/semantics/nze/nzexpr.rs | 24 +++++++++++++++++-------
 1 file changed, 17 insertions(+), 7 deletions(-)

(limited to 'dhall/src/semantics/nze')

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)))
     }
 }
 
-- 
cgit v1.2.3