Rename Value to Nir

5 files changed, 239 insertions, 257 deletions

diff --git a/dhall/src/semantics/nze/env.rs b/dhall/src/semantics/nze/env.rs
index 241af40..55050ed 100644
--- a/dhall/src/semantics/nze/env.rs
+++ b/dhall/src/semantics/nze/env.rs
@@ -1,4 +1,4 @@
-use crate::semantics::{AlphaVar, Value, ValueKind};
+use crate::semantics::{AlphaVar, Nir, NirKind};
 
 #[derive(Debug, Clone, Copy, PartialEq, Eq)]
 pub(crate) enum NzVar {
@@ -13,7 +13,7 @@ enum EnvItem<Type> {
     // Variable is bound with given type
     Kept(Type),
     // Variable has been replaced by corresponding value
-    Replaced(Value, Type),
+    Replaced(Nir, Type),
 }
 
 #[derive(Debug, Clone)]
@@ -67,15 +67,15 @@ impl<Type: Clone> ValEnv<Type> {
         env.items.push(EnvItem::Kept(ty));
         env
     }
-    pub fn insert_value(&self, e: Value, ty: Type) -> Self {
+    pub fn insert_value(&self, e: Nir, ty: Type) -> Self {
         let mut env = self.clone();
         env.items.push(EnvItem::Replaced(e, ty));
         env
     }
-    pub fn lookup_val(&self, var: &AlphaVar) -> ValueKind {
+    pub fn lookup_val(&self, var: &AlphaVar) -> NirKind {
         let idx = self.items.len() - 1 - var.idx();
         match &self.items[idx] {
-            EnvItem::Kept(_) => ValueKind::Var(NzVar::new(idx)),
+            EnvItem::Kept(_) => NirKind::Var(NzVar::new(idx)),
             EnvItem::Replaced(x, _) => x.kind().clone(),
         }
     }
diff --git a/dhall/src/semantics/nze/mod.rs b/dhall/src/semantics/nze/mod.rs
index 2c8d907..2648339 100644
--- a/dhall/src/semantics/nze/mod.rs
+++ b/dhall/src/semantics/nze/mod.rs
@@ -1,9 +1,9 @@
 pub mod env;
 pub mod lazy;
+pub mod nir;
 pub mod normalize;
-pub mod value;
 pub mod var;
 pub(crate) use env::*;
+pub(crate) use nir::*;
 pub(crate) use normalize::*;
-pub(crate) use value::*;
 pub(crate) use var::*;
diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/nir.rs
index 7084af6..a6dafa2 100644
--- a/dhall/src/semantics/nze/value.rs
+++ b/dhall/src/semantics/nze/nir.rs
@@ -14,15 +14,16 @@ use crate::{NormalizedExpr, ToExprOptions};
 
 /// Stores a possibly unevaluated value. Gets (partially) normalized on-demand, sharing computation
 /// automatically. Uses a Rc<RefCell> to share computation.
-/// If you compare for equality two `Value`s, then equality will be up to alpha-equivalence
+/// If you compare for equality two `Nir`s, then equality will be up to alpha-equivalence
 /// (renaming of bound variables) and beta-equivalence (normalization). It will recursively
 /// normalize as needed.
+/// Stands for "Normalized intermediate representation"
 #[derive(Clone)]
-pub(crate) struct Value(Rc<ValueInternal>);
+pub(crate) struct Nir(Rc<NirInternal>);
 
 #[derive(Debug)]
-struct ValueInternal {
-    kind: lazy::Lazy<Thunk, ValueKind>,
+struct NirInternal {
+    kind: lazy::Lazy<Thunk, NirKind>,
     span: Span,
 }
 
@@ -32,7 +33,7 @@ pub(crate) enum Thunk {
     /// A completely unnormalized expression.
     Thunk { env: NzEnv, body: Hir },
     /// A partially normalized expression that may need to go through `normalize_one_layer`.
-    PartialExpr { env: NzEnv, expr: ExprKind<Value> },
+    PartialExpr { env: NzEnv, expr: ExprKind<Nir> },
 }
 
 /// An unevaluated subexpression that takes an argument.
@@ -41,101 +42,99 @@ pub(crate) enum Closure {
     /// Normal closure
     Closure { env: NzEnv, body: Hir },
     /// Closure that ignores the argument passed
-    ConstantClosure { body: Value },
+    ConstantClosure { body: Nir },
 }
 
 /// A text literal with interpolations.
 // Invariant: this must not contain interpolations that are themselves TextLits, and contiguous
 // text values must be merged.
 #[derive(Debug, Clone, PartialEq, Eq)]
-pub(crate) struct TextLit(Vec<InterpolatedTextContents<Value>>);
+pub(crate) struct TextLit(Vec<InterpolatedTextContents<Nir>>);
 
 /// This represents a value in Weak Head Normal Form (WHNF). This means that the value is
 /// normalized up to the first constructor, but subexpressions may not be fully normalized.
-/// When all the Values in a ValueKind are in WHNF, and recursively so, then the ValueKind is in
+/// When all the Nirs in a NirKind are in WHNF, and recursively so, then the NirKind is in
 /// Normal Form (NF). This is because WHNF ensures that we have the first constructor of the NF; so
 /// if we have the first constructor of the NF at all levels, we actually have the NF.
-/// In particular, this means that once we get a `ValueKind`, it can be considered immutable, and
-/// we only need to recursively normalize its sub-`Value`s to get to the NF.
+/// In particular, this means that once we get a `NirKind`, it can be considered immutable, and
+/// we only need to recursively normalize its sub-`Nir`s to get to the NF.
 #[derive(Debug, Clone, PartialEq, Eq)]
-pub(crate) enum ValueKind {
+pub(crate) enum NirKind {
     /// Closures
     LamClosure {
         binder: Binder,
-        annot: Value,
+        annot: Nir,
         closure: Closure,
     },
     PiClosure {
         binder: Binder,
-        annot: Value,
+        annot: Nir,
         closure: Closure,
     },
-    AppliedBuiltin(BuiltinClosure<Value>),
+    AppliedBuiltin(BuiltinClosure<Nir>),
 
     Var(NzVar),
     Const(Const),
     Lit(LitKind),
-    EmptyOptionalLit(Value),
-    NEOptionalLit(Value),
+    EmptyOptionalLit(Nir),
+    NEOptionalLit(Nir),
     // EmptyListLit(t) means `[] : List t`, not `[] : t`
-    EmptyListLit(Value),
-    NEListLit(Vec<Value>),
-    RecordType(HashMap<Label, Value>),
-    RecordLit(HashMap<Label, Value>),
-    UnionType(HashMap<Label, Option<Value>>),
-    UnionConstructor(Label, HashMap<Label, Option<Value>>),
-    UnionLit(Label, Value, HashMap<Label, Option<Value>>),
+    EmptyListLit(Nir),
+    NEListLit(Vec<Nir>),
+    RecordType(HashMap<Label, Nir>),
+    RecordLit(HashMap<Label, Nir>),
+    UnionType(HashMap<Label, Option<Nir>>),
+    UnionConstructor(Label, HashMap<Label, Option<Nir>>),
+    UnionLit(Label, Nir, HashMap<Label, Option<Nir>>),
     TextLit(TextLit),
-    Equivalence(Value, Value),
+    Equivalence(Nir, Nir),
     /// Invariant: evaluation must not be able to progress with `normalize_one_layer`.
-    PartialExpr(ExprKind<Value>),
+    PartialExpr(ExprKind<Nir>),
 }
 
-impl Value {
-    /// Construct a Value from a completely unnormalized expression.
-    pub(crate) fn new_thunk(env: NzEnv, hir: Hir) -> Value {
+impl Nir {
+    /// Construct a Nir from a completely unnormalized expression.
+    pub(crate) fn new_thunk(env: NzEnv, hir: Hir) -> Nir {
         let span = hir.span();
-        ValueInternal::from_thunk(Thunk::new(env, hir), span).into_value()
+        NirInternal::from_thunk(Thunk::new(env, hir), span).into_nir()
     }
-    /// Construct a Value from a partially normalized expression that's not in WHNF.
-    pub(crate) fn from_partial_expr(e: ExprKind<Value>) -> Value {
+    /// Construct a Nir from a partially normalized expression that's not in WHNF.
+    pub(crate) fn from_partial_expr(e: ExprKind<Nir>) -> Nir {
         // TODO: env
         let env = NzEnv::new();
-        ValueInternal::from_thunk(
+        NirInternal::from_thunk(
             Thunk::from_partial_expr(env, e),
             Span::Artificial,
         )
-        .into_value()
+        .into_nir()
     }
-    /// Make a Value from a ValueKind
-    pub(crate) fn from_kind(v: ValueKind) -> Value {
-        ValueInternal::from_whnf(v, Span::Artificial).into_value()
+    /// Make a Nir from a NirKind
+    pub(crate) fn from_kind(v: NirKind) -> Nir {
+        NirInternal::from_whnf(v, Span::Artificial).into_nir()
     }
     pub(crate) fn from_const(c: Const) -> Self {
-        let v = ValueKind::Const(c);
-        ValueInternal::from_whnf(v, Span::Artificial).into_value()
+        let v = NirKind::Const(c);
+        NirInternal::from_whnf(v, Span::Artificial).into_nir()
     }
     pub(crate) fn from_builtin(b: Builtin) -> Self {
         Self::from_builtin_env(b, &NzEnv::new())
     }
     pub(crate) fn from_builtin_env(b: Builtin, env: &NzEnv) -> Self {
-        Value::from_kind(ValueKind::from_builtin_env(b, env.clone()))
+        Nir::from_kind(NirKind::from_builtin_env(b, env.clone()))
     }
     pub(crate) fn from_text(txt: impl ToString) -> Self {
-        Value::from_kind(ValueKind::TextLit(TextLit::from_text(
-            txt.to_string(),
-        )))
+        Nir::from_kind(NirKind::TextLit(TextLit::from_text(txt.to_string())))
     }
 
     pub(crate) fn as_const(&self) -> Option<Const> {
         match &*self.kind() {
-            ValueKind::Const(c) => Some(*c),
+            NirKind::Const(c) => Some(*c),
             _ => None,
         }
     }
 
     /// This is what you want if you want to pattern-match on the value.
-    pub(crate) fn kind(&self) -> &ValueKind {
+    pub(crate) fn kind(&self) -> &NirKind {
         self.0.kind()
     }
 
@@ -157,12 +156,12 @@ impl Value {
         self.0.normalize()
     }
 
-    pub(crate) fn app(&self, v: Value) -> Value {
-        Value::from_kind(apply_any(self.clone(), v))
+    pub(crate) fn app(&self, v: Nir) -> Nir {
+        Nir::from_kind(apply_any(self.clone(), v))
     }
 
     pub fn to_hir(&self, venv: VarEnv) -> Hir {
-        let map_uniontype = |kts: &HashMap<Label, Option<Value>>| {
+        let map_uniontype = |kts: &HashMap<Label, Option<Nir>>| {
             ExprKind::UnionType(
                 kts.iter()
                     .map(|(k, v)| {
@@ -173,13 +172,13 @@ impl Value {
         };
 
         let hir = match &*self.kind() {
-            ValueKind::Var(v) => HirKind::Var(venv.lookup(v)),
-            ValueKind::AppliedBuiltin(closure) => closure.to_hirkind(venv),
+            NirKind::Var(v) => HirKind::Var(venv.lookup(v)),
+            NirKind::AppliedBuiltin(closure) => closure.to_hirkind(venv),
             self_kind => HirKind::Expr(match self_kind {
-                ValueKind::Var(..) | ValueKind::AppliedBuiltin(..) => {
+                NirKind::Var(..) | NirKind::AppliedBuiltin(..) => {
                     unreachable!()
                 }
-                ValueKind::LamClosure {
+                NirKind::LamClosure {
                     binder,
                     annot,
                     closure,
@@ -188,7 +187,7 @@ impl Value {
                     annot.to_hir(venv),
                     closure.to_hir(venv),
                 ),
-                ValueKind::PiClosure {
+                NirKind::PiClosure {
                     binder,
                     annot,
                     closure,
@@ -197,49 +196,47 @@ impl Value {
                     annot.to_hir(venv),
                     closure.to_hir(venv),
                 ),
-                ValueKind::Const(c) => ExprKind::Const(*c),
-                ValueKind::Lit(l) => ExprKind::Lit(l.clone()),
-                ValueKind::EmptyOptionalLit(n) => ExprKind::App(
-                    Value::from_builtin(Builtin::OptionalNone).to_hir(venv),
+                NirKind::Const(c) => ExprKind::Const(*c),
+                NirKind::Lit(l) => ExprKind::Lit(l.clone()),
+                NirKind::EmptyOptionalLit(n) => ExprKind::App(
+                    Nir::from_builtin(Builtin::OptionalNone).to_hir(venv),
                     n.to_hir(venv),
                 ),
-                ValueKind::NEOptionalLit(n) => {
-                    ExprKind::SomeLit(n.to_hir(venv))
-                }
-                ValueKind::EmptyListLit(n) => ExprKind::EmptyListLit(Hir::new(
+                NirKind::NEOptionalLit(n) => ExprKind::SomeLit(n.to_hir(venv)),
+                NirKind::EmptyListLit(n) => ExprKind::EmptyListLit(Hir::new(
                     HirKind::Expr(ExprKind::App(
-                        Value::from_builtin(Builtin::List).to_hir(venv),
+                        Nir::from_builtin(Builtin::List).to_hir(venv),
                         n.to_hir(venv),
                     )),
                     Span::Artificial,
                 )),
-                ValueKind::NEListLit(elts) => ExprKind::NEListLit(
+                NirKind::NEListLit(elts) => ExprKind::NEListLit(
                     elts.iter().map(|v| v.to_hir(venv)).collect(),
                 ),
-                ValueKind::TextLit(elts) => ExprKind::TextLit(
+                NirKind::TextLit(elts) => ExprKind::TextLit(
                     elts.iter()
                         .map(|t| t.map_ref(|v| v.to_hir(venv)))
                         .collect(),
                 ),
-                ValueKind::RecordLit(kvs) => ExprKind::RecordLit(
+                NirKind::RecordLit(kvs) => ExprKind::RecordLit(
                     kvs.iter()
                         .map(|(k, v)| (k.clone(), v.to_hir(venv)))
                         .collect(),
                 ),
-                ValueKind::RecordType(kts) => ExprKind::RecordType(
+                NirKind::RecordType(kts) => ExprKind::RecordType(
                     kts.iter()
                         .map(|(k, v)| (k.clone(), v.to_hir(venv)))
                         .collect(),
                 ),
-                ValueKind::UnionType(kts) => map_uniontype(kts),
-                ValueKind::UnionConstructor(l, kts) => ExprKind::Field(
+                NirKind::UnionType(kts) => map_uniontype(kts),
+                NirKind::UnionConstructor(l, kts) => ExprKind::Field(
                     Hir::new(
                         HirKind::Expr(map_uniontype(kts)),
                         Span::Artificial,
                     ),
                     l.clone(),
                 ),
-                ValueKind::UnionLit(l, v, kts) => ExprKind::App(
+                NirKind::UnionLit(l, v, kts) => ExprKind::App(
                     Hir::new(
                         HirKind::Expr(ExprKind::Field(
                             Hir::new(
@@ -252,12 +249,12 @@ impl Value {
                     ),
                     v.to_hir(venv),
                 ),
-                ValueKind::Equivalence(x, y) => ExprKind::BinOp(
+                NirKind::Equivalence(x, y) => ExprKind::BinOp(
                     BinOp::Equivalence,
                     x.to_hir(venv),
                     y.to_hir(venv),
                 ),
-                ValueKind::PartialExpr(e) => e.map_ref(|v| v.to_hir(venv)),
+                NirKind::PartialExpr(e) => e.map_ref(|v| v.to_hir(venv)),
             }),
         };
 
@@ -268,24 +265,24 @@ impl Value {
     }
 }
 
-impl ValueInternal {
-    fn from_whnf(k: ValueKind, span: Span) -> Self {
-        ValueInternal {
+impl NirInternal {
+    fn from_whnf(k: NirKind, span: Span) -> Self {
+        NirInternal {
             kind: lazy::Lazy::new_completed(k),
             span,
         }
     }
     fn from_thunk(th: Thunk, span: Span) -> Self {
-        ValueInternal {
+        NirInternal {
             kind: lazy::Lazy::new(th),
             span,
         }
     }
-    fn into_value(self) -> Value {
-        Value(Rc::new(self))
+    fn into_nir(self) -> Nir {
+        Nir(Rc::new(self))
     }
 
-    fn kind(&self) -> &ValueKind {
+    fn kind(&self) -> &NirKind {
         &self.kind
     }
     fn normalize(&self) {
@@ -293,70 +290,70 @@ impl ValueInternal {
     }
 }
 
-impl ValueKind {
-    pub(crate) fn into_value(self) -> Value {
-        Value::from_kind(self)
+impl NirKind {
+    pub(crate) fn into_nir(self) -> Nir {
+        Nir::from_kind(self)
     }
 
     pub(crate) fn normalize(&self) {
         match self {
-            ValueKind::Var(..) | ValueKind::Const(_) | ValueKind::Lit(_) => {}
+            NirKind::Var(..) | NirKind::Const(_) | NirKind::Lit(_) => {}
 
-            ValueKind::EmptyOptionalLit(tth) | ValueKind::EmptyListLit(tth) => {
+            NirKind::EmptyOptionalLit(tth) | NirKind::EmptyListLit(tth) => {
                 tth.normalize();
             }
 
-            ValueKind::NEOptionalLit(th) => {
+            NirKind::NEOptionalLit(th) => {
                 th.normalize();
             }
-            ValueKind::LamClosure { annot, closure, .. }
-            | ValueKind::PiClosure { annot, closure, .. } => {
+            NirKind::LamClosure { annot, closure, .. }
+            | NirKind::PiClosure { annot, closure, .. } => {
                 annot.normalize();
                 closure.normalize();
             }
-            ValueKind::AppliedBuiltin(closure) => closure.normalize(),
-            ValueKind::NEListLit(elts) => {
+            NirKind::AppliedBuiltin(closure) => closure.normalize(),
+            NirKind::NEListLit(elts) => {
                 for x in elts.iter() {
                     x.normalize();
                 }
             }
-            ValueKind::RecordLit(kvs) => {
+            NirKind::RecordLit(kvs) => {
                 for x in kvs.values() {
                     x.normalize();
                 }
             }
-            ValueKind::RecordType(kvs) => {
+            NirKind::RecordType(kvs) => {
                 for x in kvs.values() {
                     x.normalize();
                 }
             }
-            ValueKind::UnionType(kts) | ValueKind::UnionConstructor(_, kts) => {
+            NirKind::UnionType(kts) | NirKind::UnionConstructor(_, kts) => {
                 for x in kts.values().flat_map(|opt| opt) {
                     x.normalize();
                 }
             }
-            ValueKind::UnionLit(_, v, kts) => {
+            NirKind::UnionLit(_, v, kts) => {
                 v.normalize();
                 for x in kts.values().flat_map(|opt| opt) {
                     x.normalize();
                 }
             }
-            ValueKind::TextLit(tlit) => tlit.normalize(),
-            ValueKind::Equivalence(x, y) => {
+            NirKind::TextLit(tlit) => tlit.normalize(),
+            NirKind::Equivalence(x, y) => {
                 x.normalize();
                 y.normalize();
             }
-            ValueKind::PartialExpr(e) => {
-                e.map_ref(Value::normalize);
+            NirKind::PartialExpr(e) => {
+                e.map_ref(Nir::normalize);
             }
         }
     }
 
-    pub(crate) fn from_builtin(b: Builtin) -> ValueKind {
-        ValueKind::from_builtin_env(b, NzEnv::new())
+    pub(crate) fn from_builtin(b: Builtin) -> NirKind {
+        NirKind::from_builtin_env(b, NzEnv::new())
     }
-    pub(crate) fn from_builtin_env(b: Builtin, env: NzEnv) -> ValueKind {
-        ValueKind::AppliedBuiltin(BuiltinClosure::new(b, env))
+    pub(crate) fn from_builtin_env(b: Builtin, env: NzEnv) -> NirKind {
+        NirKind::AppliedBuiltin(BuiltinClosure::new(b, env))
     }
 }
 
@@ -364,10 +361,10 @@ impl Thunk {
     fn new(env: NzEnv, body: Hir) -> Self {
         Thunk::Thunk { env, body }
     }
-    fn from_partial_expr(env: NzEnv, expr: ExprKind<Value>) -> Self {
+    fn from_partial_expr(env: NzEnv, expr: ExprKind<Nir>) -> Self {
         Thunk::PartialExpr { env, expr }
     }
-    fn eval(self) -> ValueKind {
+    fn eval(self) -> NirKind {
         match self {
             Thunk::Thunk { env, body } => normalize_hir_whnf(&env, &body),
             Thunk::PartialExpr { env, expr } => normalize_one_layer(expr, &env),
@@ -383,11 +380,11 @@ impl Closure {
         }
     }
     /// New closure that ignores its argument
-    pub fn new_constant(body: Value) -> Self {
+    pub fn new_constant(body: Nir) -> Self {
         Closure::ConstantClosure { body }
     }
 
-    pub fn apply(&self, val: Value) -> Value {
+    pub fn apply(&self, val: Nir) -> Nir {
         match self {
             Closure::Closure { env, body, .. } => {
                 body.eval(env.insert_value(val, ()))
@@ -395,10 +392,10 @@ impl Closure {
             Closure::ConstantClosure { body, .. } => body.clone(),
         }
     }
-    fn apply_var(&self, var: NzVar) -> Value {
+    fn apply_var(&self, var: NzVar) -> Nir {
         match self {
             Closure::Closure { .. } => {
-                self.apply(Value::from_kind(ValueKind::Var(var)))
+                self.apply(Nir::from_kind(NirKind::Var(var)))
             }
             Closure::ConstantClosure { body, .. } => body.clone(),
         }
@@ -414,7 +411,7 @@ impl Closure {
     }
     /// If the closure variable is free in the closure, return Err. Otherwise, return the value
     /// with that free variable remove.
-    pub fn remove_binder(&self) -> Result<Value, ()> {
+    pub fn remove_binder(&self) -> Result<Nir, ()> {
         match self {
             Closure::Closure { .. } => {
                 let v = NzVar::fresh();
@@ -429,11 +426,11 @@ impl Closure {
 
 impl TextLit {
     pub fn new(
-        elts: impl Iterator<Item = InterpolatedTextContents<Value>>,
+        elts: impl Iterator<Item = InterpolatedTextContents<Nir>>,
     ) -> Self {
         TextLit(squash_textlit(elts))
     }
-    pub fn interpolate(v: Value) -> TextLit {
+    pub fn interpolate(v: Nir) -> TextLit {
         TextLit(vec![InterpolatedTextContents::Expr(v)])
     }
     pub fn from_text(s: String) -> TextLit {
@@ -448,7 +445,7 @@ impl TextLit {
     }
     /// If the literal consists of only one interpolation and not text, return the interpolated
     /// value.
-    pub fn as_single_expr(&self) -> Option<&Value> {
+    pub fn as_single_expr(&self) -> Option<&Nir> {
         use InterpolatedTextContents::Expr;
         if let [Expr(v)] = self.0.as_slice() {
             Some(v)
@@ -467,33 +464,31 @@ impl TextLit {
             None
         }
     }
-    pub fn iter(
-        &self,
-    ) -> impl Iterator<Item = &InterpolatedTextContents<Value>> {
+    pub fn iter(&self) -> impl Iterator<Item = &InterpolatedTextContents<Nir>> {
         self.0.iter()
     }
     /// Normalize the contained values. This does not break the invariant because we have already
     /// ensured that no contained values normalize to a TextLit.
     pub fn normalize(&self) {
         for x in self.0.iter() {
-            x.map_ref(Value::normalize);
+            x.map_ref(Nir::normalize);
         }
     }
 }
 
-impl lazy::Eval<ValueKind> for Thunk {
-    fn eval(self) -> ValueKind {
+impl lazy::Eval<NirKind> for Thunk {
+    fn eval(self) -> NirKind {
         self.eval()
     }
 }
 
 /// Compare two values for equality modulo alpha/beta-equivalence.
-impl std::cmp::PartialEq for Value {
+impl std::cmp::PartialEq for Nir {
     fn eq(&self, other: &Self) -> bool {
         Rc::ptr_eq(&self.0, &other.0) || self.kind() == other.kind()
     }
 }
-impl std::cmp::Eq for Value {}
+impl std::cmp::Eq for Nir {}
 
 impl std::cmp::PartialEq for Thunk {
     fn eq(&self, _other: &Self) -> bool {
@@ -512,14 +507,14 @@ impl std::cmp::PartialEq for Closure {
 }
 impl std::cmp::Eq for Closure {}
 
-impl std::fmt::Debug for Value {
+impl std::fmt::Debug for Nir {
     fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
-        let vint: &ValueInternal = &self.0;
+        let vint: &NirInternal = &self.0;
         let kind = vint.kind();
-        if let ValueKind::Const(c) = kind {
+        if let NirKind::Const(c) = kind {
             return write!(fmt, "{:?}", c);
         }
-        let mut x = fmt.debug_struct(&format!("Value@WHNF"));
+        let mut x = fmt.debug_struct(&format!("Nir@WHNF"));
         x.field("kind", kind);
         x.finish()
     }
diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs
index c2d2dc2..4c2aa33 100644
--- a/dhall/src/semantics/nze/normalize.rs
+++ b/dhall/src/semantics/nze/normalize.rs
@@ -3,41 +3,39 @@ use std::collections::HashMap;
 
 use crate::semantics::NzEnv;
 use crate::semantics::{
-    Binder, BuiltinClosure, Closure, Hir, HirKind, TextLit, Value, ValueKind,
+    Binder, BuiltinClosure, Closure, Hir, HirKind, Nir, NirKind, TextLit,
 };
 use crate::syntax::{
     BinOp, Builtin, ExprKind, InterpolatedTextContents, LitKind,
 };
 
-pub(crate) fn apply_any(f: Value, a: Value) -> ValueKind {
+pub(crate) fn apply_any(f: Nir, a: Nir) -> NirKind {
     match f.kind() {
-        ValueKind::LamClosure { closure, .. } => {
-            closure.apply(a).kind().clone()
+        NirKind::LamClosure { closure, .. } => closure.apply(a).kind().clone(),
+        NirKind::AppliedBuiltin(closure) => closure.apply(a),
+        NirKind::UnionConstructor(l, kts) => {
+            NirKind::UnionLit(l.clone(), a, kts.clone())
         }
-        ValueKind::AppliedBuiltin(closure) => closure.apply(a),
-        ValueKind::UnionConstructor(l, kts) => {
-            ValueKind::UnionLit(l.clone(), a, kts.clone())
-        }
-        _ => ValueKind::PartialExpr(ExprKind::App(f, a)),
+        _ => NirKind::PartialExpr(ExprKind::App(f, a)),
     }
 }
 
 pub(crate) fn squash_textlit(
-    elts: impl Iterator<Item = InterpolatedTextContents<Value>>,
-) -> Vec<InterpolatedTextContents<Value>> {
+    elts: impl Iterator<Item = InterpolatedTextContents<Nir>>,
+) -> Vec<InterpolatedTextContents<Nir>> {
     use std::mem::replace;
     use InterpolatedTextContents::{Expr, Text};
 
     fn inner(
-        elts: impl Iterator<Item = InterpolatedTextContents<Value>>,
+        elts: impl Iterator<Item = InterpolatedTextContents<Nir>>,
         crnt_str: &mut String,
-        ret: &mut Vec<InterpolatedTextContents<Value>>,
+        ret: &mut Vec<InterpolatedTextContents<Nir>>,
     ) {
         for contents in elts {
             match contents {
                 Text(s) => crnt_str.push_str(&s),
                 Expr(e) => match e.kind() {
-                    ValueKind::TextLit(elts2) => {
+                    NirKind::TextLit(elts2) => {
                         inner(elts2.iter().cloned(), crnt_str, ret)
                     }
                     _ => {
@@ -88,85 +86,77 @@ where
 
 // Small helper enum to avoid repetition
 enum Ret<'a> {
-    ValueKind(ValueKind),
-    Value(Value),
-    ValueRef(&'a Value),
-    Expr(ExprKind<Value>),
+    NirKind(NirKind),
+    Nir(Nir),
+    NirRef(&'a Nir),
+    Expr(ExprKind<Nir>),
 }
 
-fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option<Ret<'a>> {
+fn apply_binop<'a>(o: BinOp, x: &'a Nir, y: &'a Nir) -> Option<Ret<'a>> {
     use BinOp::{
         BoolAnd, BoolEQ, BoolNE, BoolOr, Equivalence, ListAppend, NaturalPlus,
         NaturalTimes, RecursiveRecordMerge, RecursiveRecordTypeMerge,
         RightBiasedRecordMerge, TextAppend,
     };
     use LitKind::{Bool, Natural};
-    use ValueKind::{EmptyListLit, Lit, NEListLit, RecordLit, RecordType};
+    use NirKind::{EmptyListLit, Lit, NEListLit, RecordLit, RecordType};
 
     Some(match (o, x.kind(), y.kind()) {
-        (BoolAnd, Lit(Bool(true)), _) => Ret::ValueRef(y),
-        (BoolAnd, _, Lit(Bool(true))) => Ret::ValueRef(x),
-        (BoolAnd, Lit(Bool(false)), _) => Ret::ValueKind(Lit(Bool(false))),
-        (BoolAnd, _, Lit(Bool(false))) => Ret::ValueKind(Lit(Bool(false))),
-        (BoolAnd, _, _) if x == y => Ret::ValueRef(x),
-        (BoolOr, Lit(Bool(true)), _) => Ret::ValueKind(Lit(Bool(true))),
-        (BoolOr, _, Lit(Bool(true))) => Ret::ValueKind(Lit(Bool(true))),
-        (BoolOr, Lit(Bool(false)), _) => Ret::ValueRef(y),
-        (BoolOr, _, Lit(Bool(false))) => Ret::ValueRef(x),
-        (BoolOr, _, _) if x == y => Ret::ValueRef(x),
-        (BoolEQ, Lit(Bool(true)), _) => Ret::ValueRef(y),
-        (BoolEQ, _, Lit(Bool(true))) => Ret::ValueRef(x),
-        (BoolEQ, Lit(Bool(x)), Lit(Bool(y))) => {
-            Ret::ValueKind(Lit(Bool(x == y)))
-        }
-        (BoolEQ, _, _) if x == y => Ret::ValueKind(Lit(Bool(true))),
-        (BoolNE, Lit(Bool(false)), _) => Ret::ValueRef(y),
-        (BoolNE, _, Lit(Bool(false))) => Ret::ValueRef(x),
-        (BoolNE, Lit(Bool(x)), Lit(Bool(y))) => {
-            Ret::ValueKind(Lit(Bool(x != y)))
-        }
-        (BoolNE, _, _) if x == y => Ret::ValueKind(Lit(Bool(false))),
+        (BoolAnd, Lit(Bool(true)), _) => Ret::NirRef(y),
+        (BoolAnd, _, Lit(Bool(true))) => Ret::NirRef(x),
+        (BoolAnd, Lit(Bool(false)), _) => Ret::NirKind(Lit(Bool(false))),
+        (BoolAnd, _, Lit(Bool(false))) => Ret::NirKind(Lit(Bool(false))),
+        (BoolAnd, _, _) if x == y => Ret::NirRef(x),
+        (BoolOr, Lit(Bool(true)), _) => Ret::NirKind(Lit(Bool(true))),
+        (BoolOr, _, Lit(Bool(true))) => Ret::NirKind(Lit(Bool(true))),
+        (BoolOr, Lit(Bool(false)), _) => Ret::NirRef(y),
+        (BoolOr, _, Lit(Bool(false))) => Ret::NirRef(x),
+        (BoolOr, _, _) if x == y => Ret::NirRef(x),
+        (BoolEQ, Lit(Bool(true)), _) => Ret::NirRef(y),
+        (BoolEQ, _, Lit(Bool(true))) => Ret::NirRef(x),
+        (BoolEQ, Lit(Bool(x)), Lit(Bool(y))) => Ret::NirKind(Lit(Bool(x == y))),
+        (BoolEQ, _, _) if x == y => Ret::NirKind(Lit(Bool(true))),
+        (BoolNE, Lit(Bool(false)), _) => Ret::NirRef(y),
+        (BoolNE, _, Lit(Bool(false))) => Ret::NirRef(x),
+        (BoolNE, Lit(Bool(x)), Lit(Bool(y))) => Ret::NirKind(Lit(Bool(x != y))),
+        (BoolNE, _, _) if x == y => Ret::NirKind(Lit(Bool(false))),
 
-        (NaturalPlus, Lit(Natural(0)), _) => Ret::ValueRef(y),
-        (NaturalPlus, _, Lit(Natural(0))) => Ret::ValueRef(x),
+        (NaturalPlus, Lit(Natural(0)), _) => Ret::NirRef(y),
+        (NaturalPlus, _, Lit(Natural(0))) => Ret::NirRef(x),
         (NaturalPlus, Lit(Natural(x)), Lit(Natural(y))) => {
-            Ret::ValueKind(Lit(Natural(x + y)))
+            Ret::NirKind(Lit(Natural(x + y)))
         }
-        (NaturalTimes, Lit(Natural(0)), _) => Ret::ValueKind(Lit(Natural(0))),
-        (NaturalTimes, _, Lit(Natural(0))) => Ret::ValueKind(Lit(Natural(0))),
-        (NaturalTimes, Lit(Natural(1)), _) => Ret::ValueRef(y),
-        (NaturalTimes, _, Lit(Natural(1))) => Ret::ValueRef(x),
+        (NaturalTimes, Lit(Natural(0)), _) => Ret::NirKind(Lit(Natural(0))),
+        (NaturalTimes, _, Lit(Natural(0))) => Ret::NirKind(Lit(Natural(0))),
+        (NaturalTimes, Lit(Natural(1)), _) => Ret::NirRef(y),
+        (NaturalTimes, _, Lit(Natural(1))) => Ret::NirRef(x),
         (NaturalTimes, Lit(Natural(x)), Lit(Natural(y))) => {
-            Ret::ValueKind(Lit(Natural(x * y)))
+            Ret::NirKind(Lit(Natural(x * y)))
         }
 
-        (ListAppend, EmptyListLit(_), _) => Ret::ValueRef(y),
-        (ListAppend, _, EmptyListLit(_)) => Ret::ValueRef(x),
-        (ListAppend, NEListLit(xs), NEListLit(ys)) => Ret::ValueKind(
-            NEListLit(xs.iter().chain(ys.iter()).cloned().collect()),
-        ),
+        (ListAppend, EmptyListLit(_), _) => Ret::NirRef(y),
+        (ListAppend, _, EmptyListLit(_)) => Ret::NirRef(x),
+        (ListAppend, NEListLit(xs), NEListLit(ys)) => Ret::NirKind(NEListLit(
+            xs.iter().chain(ys.iter()).cloned().collect(),
+        )),
 
-        (TextAppend, ValueKind::TextLit(x), _) if x.is_empty() => {
-            Ret::ValueRef(y)
-        }
-        (TextAppend, _, ValueKind::TextLit(y)) if y.is_empty() => {
-            Ret::ValueRef(x)
-        }
-        (TextAppend, ValueKind::TextLit(x), ValueKind::TextLit(y)) => {
-            Ret::ValueKind(ValueKind::TextLit(x.concat(y)))
-        }
-        (TextAppend, ValueKind::TextLit(x), _) => Ret::ValueKind(
-            ValueKind::TextLit(x.concat(&TextLit::interpolate(y.clone()))),
-        ),
-        (TextAppend, _, ValueKind::TextLit(y)) => Ret::ValueKind(
-            ValueKind::TextLit(TextLit::interpolate(x.clone()).concat(y)),
-        ),
+        (TextAppend, NirKind::TextLit(x), _) if x.is_empty() => Ret::NirRef(y),
+        (TextAppend, _, NirKind::TextLit(y)) if y.is_empty() => Ret::NirRef(x),
+        (TextAppend, NirKind::TextLit(x), NirKind::TextLit(y)) => {
+            Ret::NirKind(NirKind::TextLit(x.concat(y)))
+        }
+        (TextAppend, NirKind::TextLit(x), _) => Ret::NirKind(NirKind::TextLit(
+            x.concat(&TextLit::interpolate(y.clone())),
+        )),
+        (TextAppend, _, NirKind::TextLit(y)) => Ret::NirKind(NirKind::TextLit(
+            TextLit::interpolate(x.clone()).concat(y),
+        )),
 
         (RightBiasedRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => {
-            Ret::ValueRef(x)
+            Ret::NirRef(x)
         }
         (RightBiasedRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => {
-            Ret::ValueRef(y)
+            Ret::NirRef(y)
         }
         (RightBiasedRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => {
             let mut kvs = kvs2.clone();
@@ -174,25 +164,25 @@ fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option<Ret<'a>> {
                 // Insert only if key not already present
                 kvs.entry(x.clone()).or_insert_with(|| v.clone());
             }
-            Ret::ValueKind(RecordLit(kvs))
+            Ret::NirKind(RecordLit(kvs))
         }
-        (RightBiasedRecordMerge, _, _) if x == y => Ret::ValueRef(y),
+        (RightBiasedRecordMerge, _, _) if x == y => Ret::NirRef(y),
 
         (RecursiveRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => {
-            Ret::ValueRef(x)
+            Ret::NirRef(x)
         }
         (RecursiveRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => {
-            Ret::ValueRef(y)
+            Ret::NirRef(y)
         }
         (RecursiveRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => {
             let kvs = merge_maps::<_, _, _, !>(kvs1, kvs2, |_, v1, v2| {
-                Ok(Value::from_partial_expr(ExprKind::BinOp(
+                Ok(Nir::from_partial_expr(ExprKind::BinOp(
                     RecursiveRecordMerge,
                     v1.clone(),
                     v2.clone(),
                 )))
             })?;
-            Ret::ValueKind(RecordLit(kvs))
+            Ret::NirKind(RecordLit(kvs))
         }
 
         (RecursiveRecordTypeMerge, RecordType(kts_x), RecordType(kts_y)) => {
@@ -200,31 +190,28 @@ fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option<Ret<'a>> {
                 kts_x,
                 kts_y,
                 // If the Label exists for both records, then we hit the recursive case.
-                |_, l: &Value, r: &Value| {
-                    Ok(Value::from_partial_expr(ExprKind::BinOp(
+                |_, l: &Nir, r: &Nir| {
+                    Ok(Nir::from_partial_expr(ExprKind::BinOp(
                         RecursiveRecordTypeMerge,
                         l.clone(),
                         r.clone(),
                     )))
                 },
             )?;
-            Ret::ValueKind(RecordType(kts))
+            Ret::NirKind(RecordType(kts))
         }
 
         (Equivalence, _, _) => {
-            Ret::ValueKind(ValueKind::Equivalence(x.clone(), y.clone()))
+            Ret::NirKind(NirKind::Equivalence(x.clone(), y.clone()))
         }
 
         _ => return None,
     })
 }
 
-pub(crate) fn normalize_one_layer(
-    expr: ExprKind<Value>,
-    env: &NzEnv,
-) -> ValueKind {
+pub(crate) fn normalize_one_layer(expr: ExprKind<Nir>, env: &NzEnv) -> NirKind {
     use LitKind::Bool;
-    use ValueKind::{
+    use NirKind::{
         EmptyListLit, EmptyOptionalLit, Lit, NEListLit, NEOptionalLit,
         PartialExpr, RecordLit, RecordType, UnionConstructor, UnionLit,
         UnionType,
@@ -241,54 +228,54 @@ pub(crate) fn normalize_one_layer(
             "This case should have been handled in normalize_hir_whnf"
         ),
 
-        ExprKind::Annot(x, _) => Ret::Value(x),
-        ExprKind::Const(c) => Ret::Value(Value::from_const(c)),
-        ExprKind::Builtin(b) => Ret::Value(Value::from_builtin_env(b, env)),
+        ExprKind::Annot(x, _) => Ret::Nir(x),
+        ExprKind::Const(c) => Ret::Nir(Nir::from_const(c)),
+        ExprKind::Builtin(b) => Ret::Nir(Nir::from_builtin_env(b, env)),
         ExprKind::Assert(_) => Ret::Expr(expr),
-        ExprKind::App(v, a) => Ret::Value(v.app(a)),
-        ExprKind::Lit(l) => Ret::ValueKind(Lit(l.clone())),
-        ExprKind::SomeLit(e) => Ret::ValueKind(NEOptionalLit(e)),
+        ExprKind::App(v, a) => Ret::Nir(v.app(a)),
+        ExprKind::Lit(l) => Ret::NirKind(Lit(l.clone())),
+        ExprKind::SomeLit(e) => Ret::NirKind(NEOptionalLit(e)),
         ExprKind::EmptyListLit(t) => {
             let arg = match t.kind() {
-                ValueKind::AppliedBuiltin(BuiltinClosure {
+                NirKind::AppliedBuiltin(BuiltinClosure {
                     b: Builtin::List,
                     args,
                     ..
                 }) if args.len() == 1 => args[0].clone(),
                 _ => panic!("internal type error"),
             };
-            Ret::ValueKind(ValueKind::EmptyListLit(arg))
+            Ret::NirKind(NirKind::EmptyListLit(arg))
         }
         ExprKind::NEListLit(elts) => {
-            Ret::ValueKind(NEListLit(elts.into_iter().collect()))
+            Ret::NirKind(NEListLit(elts.into_iter().collect()))
         }
         ExprKind::RecordLit(kvs) => {
-            Ret::ValueKind(RecordLit(kvs.into_iter().collect()))
+            Ret::NirKind(RecordLit(kvs.into_iter().collect()))
         }
         ExprKind::RecordType(kvs) => {
-            Ret::ValueKind(RecordType(kvs.into_iter().collect()))
+            Ret::NirKind(RecordType(kvs.into_iter().collect()))
         }
         ExprKind::UnionType(kvs) => {
-            Ret::ValueKind(UnionType(kvs.into_iter().collect()))
+            Ret::NirKind(UnionType(kvs.into_iter().collect()))
         }
         ExprKind::TextLit(elts) => {
             let tlit = TextLit::new(elts.into_iter());
             // Simplify bare interpolation
             if let Some(v) = tlit.as_single_expr() {
-                Ret::Value(v.clone())
+                Ret::Nir(v.clone())
             } else {
-                Ret::ValueKind(ValueKind::TextLit(tlit))
+                Ret::NirKind(NirKind::TextLit(tlit))
             }
         }
         ExprKind::BoolIf(ref b, ref e1, ref e2) => {
             match b.kind() {
-                Lit(Bool(true)) => Ret::ValueRef(e1),
-                Lit(Bool(false)) => Ret::ValueRef(e2),
+                Lit(Bool(true)) => Ret::NirRef(e1),
+                Lit(Bool(false)) => Ret::NirRef(e2),
                 _ => {
                     match (e1.kind(), e2.kind()) {
                         // Simplify `if b then True else False`
-                        (Lit(Bool(true)), Lit(Bool(false))) => Ret::ValueRef(b),
-                        _ if e1 == e2 => Ret::ValueRef(e1),
+                        (Lit(Bool(true)), Lit(Bool(false))) => Ret::NirRef(b),
+                        _ if e1 == e2 => Ret::NirRef(e1),
                         _ => Ret::Expr(expr),
                     }
                 }
@@ -300,10 +287,10 @@ pub(crate) fn normalize_one_layer(
         },
 
         ExprKind::Projection(_, ref ls) if ls.is_empty() => {
-            Ret::ValueKind(RecordLit(HashMap::new()))
+            Ret::NirKind(RecordLit(HashMap::new()))
         }
         ExprKind::Projection(ref v, ref ls) => match v.kind() {
-            RecordLit(kvs) => Ret::ValueKind(RecordLit(
+            RecordLit(kvs) => Ret::NirKind(RecordLit(
                 ls.iter()
                     .filter_map(|l| kvs.get(l).map(|x| (l.clone(), x.clone())))
                     .collect(),
@@ -318,11 +305,11 @@ pub(crate) fn normalize_one_layer(
         },
         ExprKind::Field(ref v, ref l) => match v.kind() {
             RecordLit(kvs) => match kvs.get(l) {
-                Some(r) => Ret::Value(r.clone()),
+                Some(r) => Ret::Nir(r.clone()),
                 None => Ret::Expr(expr),
             },
             UnionType(kts) => {
-                Ret::ValueKind(UnionConstructor(l.clone(), kts.clone()))
+                Ret::NirKind(UnionConstructor(l.clone(), kts.clone()))
             }
             PartialExpr(ExprKind::BinOp(
                 BinOp::RightBiasedRecordMerge,
@@ -330,7 +317,7 @@ pub(crate) fn normalize_one_layer(
                 y,
             )) => match (x.kind(), y.kind()) {
                 (_, RecordLit(kvs)) => match kvs.get(l) {
-                    Some(r) => Ret::Value(r.clone()),
+                    Some(r) => Ret::Nir(r.clone()),
                     None => {
                         return normalize_one_layer(
                             ExprKind::Field(x.clone(), l.clone()),
@@ -340,9 +327,9 @@ pub(crate) fn normalize_one_layer(
                 },
                 (RecordLit(kvs), _) => match kvs.get(l) {
                     Some(r) => Ret::Expr(ExprKind::Field(
-                        Value::from_kind(PartialExpr(ExprKind::BinOp(
+                        Nir::from_kind(PartialExpr(ExprKind::BinOp(
                             BinOp::RightBiasedRecordMerge,
-                            Value::from_kind(RecordLit({
+                            Nir::from_kind(RecordLit({
                                 let mut kvs = HashMap::new();
                                 kvs.insert(l.clone(), r.clone());
                                 kvs
@@ -395,19 +382,19 @@ pub(crate) fn normalize_one_layer(
             match handlers.kind() {
                 RecordLit(kvs) => match variant.kind() {
                     UnionConstructor(l, _) => match kvs.get(l) {
-                        Some(h) => Ret::Value(h.clone()),
+                        Some(h) => Ret::Nir(h.clone()),
                         None => Ret::Expr(expr),
                     },
                     UnionLit(l, v, _) => match kvs.get(l) {
-                        Some(h) => Ret::Value(h.app(v.clone())),
+                        Some(h) => Ret::Nir(h.app(v.clone())),
                         None => Ret::Expr(expr),
                     },
                     EmptyOptionalLit(_) => match kvs.get(&"None".into()) {
-                        Some(h) => Ret::Value(h.clone()),
+                        Some(h) => Ret::Nir(h.clone()),
                         None => Ret::Expr(expr),
                     },
                     NEOptionalLit(v) => match kvs.get(&"Some".into()) {
-                        Some(h) => Ret::Value(h.app(v.clone())),
+                        Some(h) => Ret::Nir(h.app(v.clone())),
                         None => Ret::Expr(expr),
                     },
                     _ => Ret::Expr(expr),
@@ -418,24 +405,24 @@ pub(crate) fn normalize_one_layer(
         ExprKind::ToMap(ref v, ref annot) => match v.kind() {
             RecordLit(kvs) if kvs.is_empty() => {
                 match annot.as_ref().map(|v| v.kind()) {
-                    Some(ValueKind::AppliedBuiltin(BuiltinClosure {
+                    Some(NirKind::AppliedBuiltin(BuiltinClosure {
                         b: Builtin::List,
                         args,
                         ..
                     })) if args.len() == 1 => {
-                        Ret::ValueKind(EmptyListLit(args[0].clone()))
+                        Ret::NirKind(EmptyListLit(args[0].clone()))
                     }
                     _ => Ret::Expr(expr),
                 }
             }
-            RecordLit(kvs) => Ret::ValueKind(NEListLit(
+            RecordLit(kvs) => Ret::NirKind(NEListLit(
                 kvs.iter()
                     .sorted_by_key(|(k, _)| k.clone())
                     .map(|(k, v)| {
                         let mut rec = HashMap::new();
-                        rec.insert("mapKey".into(), Value::from_text(k));
+                        rec.insert("mapKey".into(), Nir::from_text(k));
                         rec.insert("mapValue".into(), v.clone());
-                        Value::from_kind(ValueKind::RecordLit(rec))
+                        Nir::from_kind(NirKind::RecordLit(rec))
                     })
                     .collect(),
             )),
@@ -444,20 +431,20 @@ pub(crate) fn normalize_one_layer(
     };
 
     match ret {
-        Ret::ValueKind(v) => v,
-        Ret::Value(v) => v.kind().clone(),
-        Ret::ValueRef(v) => v.kind().clone(),
-        Ret::Expr(expr) => ValueKind::PartialExpr(expr),
+        Ret::NirKind(v) => v,
+        Ret::Nir(v) => v.kind().clone(),
+        Ret::NirRef(v) => v.kind().clone(),
+        Ret::Expr(expr) => NirKind::PartialExpr(expr),
     }
 }
 
 /// Normalize Hir into WHNF
-pub(crate) fn normalize_hir_whnf(env: &NzEnv, hir: &Hir) -> ValueKind {
+pub(crate) fn normalize_hir_whnf(env: &NzEnv, hir: &Hir) -> NirKind {
     match hir.kind() {
         HirKind::Var(var) => env.lookup_val(var),
         HirKind::Expr(ExprKind::Lam(binder, annot, body)) => {
             let annot = annot.eval(env);
-            ValueKind::LamClosure {
+            NirKind::LamClosure {
                 binder: Binder::new(binder.clone()),
                 annot: annot,
                 closure: Closure::new(env, body.clone()),
@@ -465,7 +452,7 @@ pub(crate) fn normalize_hir_whnf(env: &NzEnv, hir: &Hir) -> ValueKind {
         }
         HirKind::Expr(ExprKind::Pi(binder, annot, body)) => {
             let annot = annot.eval(env);
-            ValueKind::PiClosure {
+            NirKind::PiClosure {
                 binder: Binder::new(binder.clone()),
                 annot,
                 closure: Closure::new(env, body.clone()),
diff --git a/dhall/src/semantics/nze/var.rs b/dhall/src/semantics/nze/var.rs
index 264b81d..413c759 100644
--- a/dhall/src/semantics/nze/var.rs
+++ b/dhall/src/semantics/nze/var.rs
@@ -1,7 +1,7 @@
 use crate::syntax::Label;
 
 // Exactly like a Label, but equality returns always true.
-// This is so that ValueKind equality is exactly alpha-equivalence.
+// This is so that NirKind equality is exactly alpha-equivalence.
 #[derive(Clone, Eq)]
 pub struct Binder {
     name: Label,