Remove types from NzEnv

7 files changed, 47 insertions, 42 deletions

diff --git a/dhall/src/semantics/builtins.rs b/dhall/src/semantics/builtins.rs
index 9d4f8a2..d9a3599 100644
--- a/dhall/src/semantics/builtins.rs
+++ b/dhall/src/semantics/builtins.rs
@@ -265,8 +265,11 @@ fn apply_builtin(b: Builtin, args: Vec<Value>, env: NzEnv) -> ValueKind {
         Value(Value),
         DoneAsIs,
     }
-    let make_closure =
-        |e| typecheck(&skip_resolve(&e).unwrap()).unwrap().eval(&env);
+    let make_closure = |e| {
+        typecheck(&skip_resolve(&e).unwrap())
+            .unwrap()
+            .eval(env.clone())
+    };
 
     let ret = match (b, args.as_slice()) {
         (OptionalNone, [t]) => Ret::ValueKind(EmptyOptionalLit(t.clone())),
diff --git a/dhall/src/semantics/hir.rs b/dhall/src/semantics/hir.rs
index 28b38e3..9ad7374 100644
--- a/dhall/src/semantics/hir.rs
+++ b/dhall/src/semantics/hir.rs
@@ -70,7 +70,7 @@ impl Hir {
 
     /// Eval the Hir. It will actually get evaluated only as needed on demand.
     pub fn eval(&self, env: &NzEnv) -> Value {
-        Value::new_thunk(env, self.clone())
+        Value::new_thunk(env.clone(), self.clone())
     }
     /// Eval a closed Hir (i.e. without free variables). It will actually get evaluated only as
     /// needed on demand.
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(),
         }
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()
     }
 }
diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index edba477..a1666a4 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -56,13 +56,13 @@ impl TyExpr {
     }
 
     /// Eval the TyExpr. It will actually get evaluated only as needed on demand.
-    pub fn eval<'e>(&self, env: impl Into<&'e NzEnv>) -> Value {
+    pub fn eval(&self, env: impl Into<NzEnv>) -> Value {
         Value::new_thunk(env.into(), self.to_hir())
     }
     /// Eval a closed TyExpr (i.e. without free variables). It will actually get evaluated only as
     /// needed on demand.
     pub fn eval_closed_expr(&self) -> Value {
-        self.eval(&NzEnv::new())
+        self.eval(NzEnv::new())
     }
     /// Eval a closed TyExpr fully and recursively;
     pub fn rec_eval_closed_expr(&self) -> Value {