5 files changed, 25 insertions, 25 deletions

diff --git a/dhall/src/semantics/nze/env.rs b/dhall/src/semantics/nze/env.rs
index 073886e..0b22a8b 100644
--- a/dhall/src/semantics/nze/env.rs
+++ b/dhall/src/semantics/nze/env.rs
@@ -59,14 +59,18 @@ impl NzEnv {
         env.items.push(NzEnvItem::Replaced(e));
         env
     }
-    pub fn lookup_val(&self, var: &AlphaVar) -> Value {
+    pub fn lookup_val(&self, var: &AlphaVar) -> ValueKind {
         let idx = self.items.len() - 1 - var.idx();
         match &self.items[idx] {
-            NzEnvItem::Kept(ty) => Value::from_kind_and_type(
-                ValueKind::Var(NzVar::new(idx)),
-                ty.clone(),
-            ),
-            NzEnvItem::Replaced(x) => x.clone(),
+            NzEnvItem::Kept(_) => ValueKind::Var(NzVar::new(idx)),
+            NzEnvItem::Replaced(x) => x.kind().clone(),
+        }
+    }
+    pub fn lookup_ty(&self, var: &AlphaVar) -> Value {
+        let idx = self.items.len() - 1 - var.idx();
+        match &self.items[idx] {
+            NzEnvItem::Kept(ty) => ty.clone(),
+            NzEnvItem::Replaced(x) => x.get_type().unwrap(),
         }
     }
 }
diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs
index 7632d12..e677f78 100644
--- a/dhall/src/semantics/nze/normalize.rs
+++ b/dhall/src/semantics/nze/normalize.rs
@@ -445,14 +445,9 @@ pub(crate) fn normalize_one_layer(
 }
 
 /// Normalize a TyExpr into WHNF
-pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> Value {
-    let ty = match tye.get_type() {
-        Ok(ty) => ty,
-        Err(_) => return Value::from_const(Const::Sort),
-    };
-
-    let kind = match tye.kind() {
-        TyExprKind::Var(var) => return env.lookup_val(var),
+pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> ValueKind {
+    match tye.kind() {
+        TyExprKind::Var(var) => env.lookup_val(var),
         TyExprKind::Expr(ExprKind::Lam(binder, annot, body)) => {
             let annot = annot.eval(env);
             ValueKind::LamClosure {
@@ -472,13 +467,15 @@ pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> Value {
         }
         TyExprKind::Expr(ExprKind::Let(_, None, val, body)) => {
             let val = val.eval(env);
-            return body.eval(&env.insert_value(val));
+            body.eval(&env.insert_value(val)).kind().clone()
         }
         TyExprKind::Expr(e) => {
+            let ty = match tye.get_type() {
+                Ok(ty) => ty,
+                Err(_) => return ValueKind::Const(Const::Sort),
+            };
             let e = e.map_ref(|tye| tye.eval(env));
             normalize_one_layer(e, &ty, env)
         }
-    };
-
-    Value::from_kind_and_type(kind, ty)
+    }
 }
diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs
index 108dc9c..ff0ca42 100644
--- a/dhall/src/semantics/nze/value.rs
+++ b/dhall/src/semantics/nze/value.rs
@@ -405,7 +405,7 @@ impl ValueInternal {
         use std::mem::replace;
         let dummy = Form::PartialExpr(ExprKind::Const(Const::Type));
         self.form = match replace(&mut self.form, dummy) {
-            Form::Thunk(th) => Form::WHNF(th.eval().kind().clone()),
+            Form::Thunk(th) => Form::WHNF(th.eval()),
             Form::PartialExpr(e) => {
                 Form::WHNF(match &self.ty {
                     // TODO: env
@@ -516,9 +516,7 @@ impl Thunk {
             body,
         }
     }
-
-    // TODO: maybe return a ValueKind ?
-    pub fn eval(&self) -> Value {
+    pub fn eval(&self) -> ValueKind {
         normalize_tyexpr_whnf(&self.body, &self.env)
     }
 }
diff --git a/dhall/src/semantics/tck/env.rs b/dhall/src/semantics/tck/env.rs
index d4cc37d..812ca7a 100644
--- a/dhall/src/semantics/tck/env.rs
+++ b/dhall/src/semantics/tck/env.rs
@@ -118,7 +118,7 @@ impl TyEnv {
     }
     pub fn lookup(&self, var: &V) -> Option<(TyExprKind, Type)> {
         let var = self.names.unlabel_var(var)?;
-        let ty = self.items.lookup_val(&var).get_type().unwrap();
+        let ty = self.items.lookup_ty(&var);
         Some((TyExprKind::Var(var), ty))
     }
 }
diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index 4b88048..1a048f9 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -1,5 +1,4 @@
 use crate::error::{TypeError, TypeMessage};
-use crate::semantics::normalize_tyexpr_whnf;
 use crate::semantics::{rc, NameEnv, NzEnv, TyEnv, Value};
 use crate::syntax::{ExprKind, Span, V};
 use crate::Normalized;
@@ -83,7 +82,9 @@ impl TyExpr {
     }
     /// Eval a closed TyExpr fully and recursively;
     pub fn rec_eval_closed_expr(&self) -> Value {
-        normalize_tyexpr_whnf(self, &NzEnv::new())
+        let mut val = self.eval_closed_expr();
+        val.normalize_mut();
+        val
     }
 }