3 files changed, 32 insertions, 30 deletions

diff --git a/dhall/src/semantics/nze/env.rs b/dhall/src/semantics/nze/env.rs
index ff52343..5b036f0 100644
--- a/dhall/src/semantics/nze/env.rs
+++ b/dhall/src/semantics/nze/env.rs
@@ -1,4 +1,4 @@
-use crate::semantics::{AlphaVar, Type, Value, ValueKind};
+use crate::semantics::{AlphaVar, Value, ValueKind};
 
 #[derive(Debug, Clone, Copy, PartialEq, Eq)]
 pub(crate) enum NzVar {
@@ -9,7 +9,7 @@ pub(crate) enum NzVar {
 }
 
 #[derive(Debug, Clone)]
-enum NzEnvItem {
+enum EnvItem<Type> {
     // Variable is bound with given type
     Kept(Type),
     // Variable has been replaced by corresponding value
@@ -17,10 +17,12 @@ enum NzEnvItem {
 }
 
 #[derive(Debug, Clone)]
-pub(crate) struct NzEnv {
-    items: Vec<NzEnvItem>,
+pub(crate) struct ValEnv<Type> {
+    items: Vec<EnvItem<Type>>,
 }
 
+pub(crate) type NzEnv = ValEnv<()>;
+
 impl NzVar {
     pub fn new(idx: usize) -> Self {
         NzVar::Bound(idx)
@@ -44,37 +46,43 @@ impl NzVar {
     }
 }
 
-impl NzEnv {
+impl<Type: Clone> ValEnv<Type> {
     pub fn new() -> Self {
-        NzEnv { items: Vec::new() }
+        ValEnv { items: Vec::new() }
+    }
+    pub fn discard_types(&self) -> ValEnv<()> {
+        let items = self
+            .items
+            .iter()
+            .map(|i| match i {
+                EnvItem::Kept(_) => EnvItem::Kept(()),
+                EnvItem::Replaced(val, _) => EnvItem::Replaced(val.clone(), ()),
+            })
+            .collect();
+        ValEnv { items }
     }
 
     pub fn insert_type(&self, ty: Type) -> Self {
         let mut env = self.clone();
-        env.items.push(NzEnvItem::Kept(ty));
+        env.items.push(EnvItem::Kept(ty));
         env
     }
     pub fn insert_value(&self, e: Value, ty: Type) -> Self {
         let mut env = self.clone();
-        env.items.push(NzEnvItem::Replaced(e, ty));
+        env.items.push(EnvItem::Replaced(e, ty));
         env
     }
-    pub fn insert_value_noty(&self, e: Value) -> Self {
-        // TODO
-        let ty = Value::const_sort();
-        self.insert_value(e, ty)
-    }
     pub fn lookup_val(&self, var: &AlphaVar) -> ValueKind {
         let idx = self.items.len() - 1 - var.idx();
         match &self.items[idx] {
-            NzEnvItem::Kept(_) => ValueKind::Var(NzVar::new(idx)),
-            NzEnvItem::Replaced(x, _) => x.kind().clone(),
+            EnvItem::Kept(_) => ValueKind::Var(NzVar::new(idx)),
+            EnvItem::Replaced(x, _) => x.kind().clone(),
         }
     }
-    pub fn lookup_ty(&self, var: &AlphaVar) -> Value {
+    pub fn lookup_ty(&self, var: &AlphaVar) -> Type {
         let idx = self.items.len() - 1 - var.idx();
         match &self.items[idx] {
-            NzEnvItem::Kept(ty) | NzEnvItem::Replaced(_, ty) => ty.clone(),
+            EnvItem::Kept(ty) | EnvItem::Replaced(_, ty) => ty.clone(),
         }
     }
 }
diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs
index 981d894..d12146a 100644
--- a/dhall/src/semantics/nze/normalize.rs
+++ b/dhall/src/semantics/nze/normalize.rs
@@ -473,7 +473,7 @@ pub(crate) fn normalize_hir_whnf(env: &NzEnv, hir: &Hir) -> ValueKind {
         }
         HirKind::Expr(ExprKind::Let(_, None, val, body)) => {
             let val = val.eval(env);
-            body.eval(&env.insert_value_noty(val)).kind().clone()
+            body.eval(&env.insert_value(val, ())).kind().clone()
         }
         HirKind::Expr(e) => {
             let e = e.map_ref(|hir| hir.eval(env));
diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs
index 5a7b558..a60be9d 100644
--- a/dhall/src/semantics/nze/value.rs
+++ b/dhall/src/semantics/nze/value.rs
@@ -100,11 +100,8 @@ pub(crate) enum ValueKind {
 }
 
 impl Value {
-    pub(crate) fn const_sort() -> Value {
-        Value::from_const(Const::Sort)
-    }
     /// Construct a Value from a completely unnormalized expression.
-    pub(crate) fn new_thunk(env: &NzEnv, hir: Hir) -> Value {
+    pub(crate) fn new_thunk(env: NzEnv, hir: Hir) -> Value {
         let span = hir.span();
         ValueInternal::from_thunk(Thunk::new(env, hir), span).into_value()
     }
@@ -158,8 +155,8 @@ impl Value {
 
         self.to_tyexpr_noenv().to_expr(opts)
     }
-    pub(crate) fn to_expr_tyenv(&self, env: &TyEnv) -> NormalizedExpr {
-        self.to_hir(env.as_varenv()).to_expr_tyenv(env)
+    pub(crate) fn to_expr_tyenv(&self, tyenv: &TyEnv) -> NormalizedExpr {
+        self.to_hir(tyenv.as_varenv()).to_expr_tyenv(tyenv)
     }
 
     pub(crate) fn normalize(&self) {
@@ -389,11 +386,8 @@ impl ValueKind {
 }
 
 impl Thunk {
-    fn new(env: &NzEnv, body: Hir) -> Self {
-        Thunk::Thunk {
-            env: env.clone(),
-            body,
-        }
+    fn new(env: NzEnv, body: Hir) -> Self {
+        Thunk::Thunk { env, body }
     }
     fn from_partial_expr(
         env: NzEnv,
@@ -424,7 +418,7 @@ impl Closure {
     pub fn apply(&self, val: Value) -> Value {
         match self {
             Closure::Closure { env, body, .. } => {
-                body.eval(&env.insert_value_noty(val))
+                body.eval(&env.insert_value(val, ()))
             }
             Closure::ConstantClosure { body, .. } => body.clone(),
         }