From db1375eccd1e6943b504cd54ed17eb8f4d19c25f Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Thu, 6 Feb 2020 17:35:54 +0000
Subject: Remove most reliance on types stored in Value

---
 dhall/src/semantics/tck/env.rs | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'dhall/src/semantics/tck/env.rs')

diff --git a/dhall/src/semantics/tck/env.rs b/dhall/src/semantics/tck/env.rs
index 1fc711c..b3e7895 100644
--- a/dhall/src/semantics/tck/env.rs
+++ b/dhall/src/semantics/tck/env.rs
@@ -104,16 +104,16 @@ impl TyEnv {
         &self.names
     }
 
-    pub fn insert_type(&self, x: &Label, t: Type) -> Self {
+    pub fn insert_type(&self, x: &Label, ty: Type) -> Self {
         TyEnv {
             names: self.names.insert(x),
-            items: self.items.insert_type(t),
+            items: self.items.insert_type(ty),
         }
     }
-    pub fn insert_value(&self, x: &Label, e: Value) -> Self {
+    pub fn insert_value(&self, x: &Label, e: Value, ty: Type) -> Self {
         TyEnv {
             names: self.names.insert(x),
-            items: self.items.insert_value(e),
+            items: self.items.insert_value(e, ty),
         }
     }
     pub fn lookup(&self, var: &V) -> Option<(AlphaVar, Type)> {
-- 
cgit v1.2.3


From 6c90d356c9a4a5bbeb88f25ad0ab499ba1503eae Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 9 Feb 2020 11:53:55 +0000
Subject: Remove most TyExpr from normalization

---
 dhall/src/semantics/tck/env.rs | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'dhall/src/semantics/tck/env.rs')

diff --git a/dhall/src/semantics/tck/env.rs b/dhall/src/semantics/tck/env.rs
index b3e7895..af955f4 100644
--- a/dhall/src/semantics/tck/env.rs
+++ b/dhall/src/semantics/tck/env.rs
@@ -21,9 +21,9 @@ pub(crate) struct TyEnv {
 }
 
 impl VarEnv {
-    pub fn new() -> Self {
-        VarEnv { size: 0 }
-    }
+    // pub fn new() -> Self {
+    //     VarEnv { size: 0 }
+    // }
     pub fn size(&self) -> usize {
         self.size
     }
-- 
cgit v1.2.3


From 21db63d3e614554f258526182c7ed89a2c244b65 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 9 Feb 2020 21:58:28 +0000
Subject: Take Hir for typecheck

---
 dhall/src/semantics/tck/env.rs | 12 +++++-------
 1 file changed, 5 insertions(+), 7 deletions(-)

(limited to 'dhall/src/semantics/tck/env.rs')

diff --git a/dhall/src/semantics/tck/env.rs b/dhall/src/semantics/tck/env.rs
index af955f4..3b02074 100644
--- a/dhall/src/semantics/tck/env.rs
+++ b/dhall/src/semantics/tck/env.rs
@@ -21,9 +21,9 @@ pub(crate) struct TyEnv {
 }
 
 impl VarEnv {
-    // pub fn new() -> Self {
-    //     VarEnv { size: 0 }
-    // }
+    pub fn new() -> Self {
+        VarEnv { size: 0 }
+    }
     pub fn size(&self) -> usize {
         self.size
     }
@@ -116,9 +116,7 @@ impl TyEnv {
             items: self.items.insert_value(e, ty),
         }
     }
-    pub fn lookup(&self, var: &V) -> Option<(AlphaVar, Type)> {
-        let var = self.names.unlabel_var(var)?;
-        let ty = self.items.lookup_ty(&var);
-        Some((var, ty))
+    pub fn lookup(&self, var: &AlphaVar) -> Type {
+        self.items.lookup_ty(&var)
     }
 }
-- 
cgit v1.2.3


From f6732982c522dd579d378ab4820001d5ae107c43 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 9 Feb 2020 22:18:32 +0000
Subject: Automate conversion between envs

---
 dhall/src/semantics/tck/env.rs | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'dhall/src/semantics/tck/env.rs')

diff --git a/dhall/src/semantics/tck/env.rs b/dhall/src/semantics/tck/env.rs
index 3b02074..ba7fb73 100644
--- a/dhall/src/semantics/tck/env.rs
+++ b/dhall/src/semantics/tck/env.rs
@@ -120,3 +120,9 @@ impl TyEnv {
         self.items.lookup_ty(&var)
     }
 }
+
+impl<'a> From<&'a TyEnv> for &'a NzEnv {
+    fn from(x: &'a TyEnv) -> Self {
+        x.as_nzenv()
+    }
+}
-- 
cgit v1.2.3


From 35cc98dc767247f4881866de40c7d8dd82eba8a5 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 9 Feb 2020 22:30:32 +0000
Subject: Remove types from NzEnv

---
 dhall/src/semantics/tck/env.rs | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

(limited to 'dhall/src/semantics/tck/env.rs')

diff --git a/dhall/src/semantics/tck/env.rs b/dhall/src/semantics/tck/env.rs
index ba7fb73..7990059 100644
--- a/dhall/src/semantics/tck/env.rs
+++ b/dhall/src/semantics/tck/env.rs
@@ -1,4 +1,4 @@
-use crate::semantics::{AlphaVar, NzEnv, NzVar, Type, Value};
+use crate::semantics::{AlphaVar, NzEnv, NzVar, Type, ValEnv, Value};
 use crate::syntax::{Label, V};
 
 /// Environment for indexing variables.
@@ -17,7 +17,7 @@ pub(crate) struct NameEnv {
 #[derive(Debug, Clone)]
 pub(crate) struct TyEnv {
     names: NameEnv,
-    items: NzEnv,
+    items: ValEnv<Type>,
 }
 
 impl VarEnv {
@@ -91,14 +91,14 @@ impl TyEnv {
     pub fn new() -> Self {
         TyEnv {
             names: NameEnv::new(),
-            items: NzEnv::new(),
+            items: ValEnv::new(),
         }
     }
     pub fn as_varenv(&self) -> VarEnv {
         self.names.as_varenv()
     }
-    pub fn as_nzenv(&self) -> &NzEnv {
-        &self.items
+    pub fn to_nzenv(&self) -> NzEnv {
+        self.items.discard_types()
     }
     pub fn as_nameenv(&self) -> &NameEnv {
         &self.names
@@ -121,8 +121,8 @@ impl TyEnv {
     }
 }
 
-impl<'a> From<&'a TyEnv> for &'a NzEnv {
+impl<'a> From<&'a TyEnv> for NzEnv {
     fn from(x: &'a TyEnv) -> Self {
-        x.as_nzenv()
+        x.to_nzenv()
     }
 }
-- 
cgit v1.2.3


From 8da4445e6d06cf79d43112042b69c798f86884f3 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Mon, 17 Feb 2020 17:58:03 +0000
Subject: Extract resolve-relevant envs together

---
 dhall/src/semantics/tck/env.rs | 59 ++++--------------------------------------
 1 file changed, 5 insertions(+), 54 deletions(-)

(limited to 'dhall/src/semantics/tck/env.rs')

diff --git a/dhall/src/semantics/tck/env.rs b/dhall/src/semantics/tck/env.rs
index 7990059..f290c02 100644
--- a/dhall/src/semantics/tck/env.rs
+++ b/dhall/src/semantics/tck/env.rs
@@ -1,5 +1,5 @@
-use crate::semantics::{AlphaVar, NzEnv, NzVar, Type, ValEnv, Value};
-use crate::syntax::{Label, V};
+use crate::semantics::{AlphaVar, NameEnv, NzEnv, NzVar, Type, ValEnv, Value};
+use crate::syntax::Label;
 
 /// Environment for indexing variables.
 #[derive(Debug, Clone, Copy)]
@@ -7,12 +7,6 @@ pub(crate) struct VarEnv {
     size: usize,
 }
 
-/// Environment for resolving names.
-#[derive(Debug, Clone)]
-pub(crate) struct NameEnv {
-    names: Vec<Label>,
-}
-
 /// Environment for typing expressions.
 #[derive(Debug, Clone)]
 pub(crate) struct TyEnv {
@@ -24,6 +18,9 @@ impl VarEnv {
     pub fn new() -> Self {
         VarEnv { size: 0 }
     }
+    pub fn from_size(size: usize) -> Self {
+        VarEnv { size }
+    }
     pub fn size(&self) -> usize {
         self.size
     }
@@ -41,52 +38,6 @@ impl VarEnv {
     }
 }
 
-impl NameEnv {
-    pub fn new() -> Self {
-        NameEnv { names: Vec::new() }
-    }
-    pub fn as_varenv(&self) -> VarEnv {
-        VarEnv {
-            size: self.names.len(),
-        }
-    }
-
-    pub fn insert(&self, x: &Label) -> Self {
-        let mut env = self.clone();
-        env.insert_mut(x);
-        env
-    }
-    pub fn insert_mut(&mut self, x: &Label) {
-        self.names.push(x.clone())
-    }
-    pub fn remove_mut(&mut self) {
-        self.names.pop();
-    }
-
-    pub fn unlabel_var(&self, var: &V) -> Option<AlphaVar> {
-        let V(name, idx) = var;
-        let (idx, _) = self
-            .names
-            .iter()
-            .rev()
-            .enumerate()
-            .filter(|(_, n)| *n == name)
-            .nth(*idx)?;
-        Some(AlphaVar::new(idx))
-    }
-    pub fn label_var(&self, var: &AlphaVar) -> V {
-        let name = &self.names[self.names.len() - 1 - var.idx()];
-        let idx = self
-            .names
-            .iter()
-            .rev()
-            .take(var.idx())
-            .filter(|n| *n == name)
-            .count();
-        V(name.clone(), idx)
-    }
-}
-
 impl TyEnv {
     pub fn new() -> Self {
         TyEnv {
-- 
cgit v1.2.3


From cd5e172002ce724be7bdd52883e121efa8817f20 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Mon, 17 Feb 2020 18:22:06 +0000
Subject: Rename Value to Nir

---
 dhall/src/semantics/tck/env.rs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'dhall/src/semantics/tck/env.rs')

diff --git a/dhall/src/semantics/tck/env.rs b/dhall/src/semantics/tck/env.rs
index f290c02..17b3cfe 100644
--- a/dhall/src/semantics/tck/env.rs
+++ b/dhall/src/semantics/tck/env.rs
@@ -1,4 +1,4 @@
-use crate::semantics::{AlphaVar, NameEnv, NzEnv, NzVar, Type, ValEnv, Value};
+use crate::semantics::{AlphaVar, NameEnv, Nir, NzEnv, NzVar, Type, ValEnv};
 use crate::syntax::Label;
 
 /// Environment for indexing variables.
@@ -61,7 +61,7 @@ impl TyEnv {
             items: self.items.insert_type(ty),
         }
     }
-    pub fn insert_value(&self, x: &Label, e: Value, ty: Type) -> Self {
+    pub fn insert_value(&self, x: &Label, e: Nir, ty: Type) -> Self {
         TyEnv {
             names: self.names.insert(x),
             items: self.items.insert_value(e, ty),
-- 
cgit v1.2.3