Rename Value to Nir

1 files changed, 115 insertions, 128 deletions

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()),