From db1375eccd1e6943b504cd54ed17eb8f4d19c25f Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Thu, 6 Feb 2020 17:35:54 +0000
Subject: Remove most reliance on types stored in Value

---
 dhall/src/semantics/nze/env.rs       | 23 ++++++++------
 dhall/src/semantics/nze/normalize.rs |  8 ++---
 dhall/src/semantics/nze/value.rs     | 60 +++++++++++++++++++++---------------
 3 files changed, 53 insertions(+), 38 deletions(-)

(limited to 'dhall/src/semantics/nze')

diff --git a/dhall/src/semantics/nze/env.rs b/dhall/src/semantics/nze/env.rs
index 0b22a8b..261e0b6 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, Type, Value, ValueKind};
 
 #[derive(Debug, Clone, Copy, PartialEq, Eq)]
 pub(crate) enum NzVar {
@@ -11,9 +11,9 @@ pub(crate) enum NzVar {
 #[derive(Debug, Clone)]
 enum NzEnvItem {
     // Variable is bound with given type
-    Kept(Value),
+    Kept(Type),
     // Variable has been replaced by corresponding value
-    Replaced(Value),
+    Replaced(Value, Type),
 }
 
 #[derive(Debug, Clone)]
@@ -49,28 +49,31 @@ impl NzEnv {
         NzEnv { items: Vec::new() }
     }
 
-    pub fn insert_type(&self, t: Value) -> Self {
+    pub fn insert_type(&self, ty: Type) -> Self {
         let mut env = self.clone();
-        env.items.push(NzEnvItem::Kept(t));
+        env.items.push(NzEnvItem::Kept(ty));
         env
     }
-    pub fn insert_value(&self, e: Value) -> Self {
+    pub fn insert_value(&self, e: Value, ty: Type) -> Self {
         let mut env = self.clone();
-        env.items.push(NzEnvItem::Replaced(e));
+        env.items.push(NzEnvItem::Replaced(e, ty));
         env
     }
+    pub fn insert_value_noty(&self, e: Value) -> Self {
+        let ty = e.get_type_not_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(),
+            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(),
+            NzEnvItem::Kept(ty) | NzEnvItem::Replaced(_, ty) => ty.clone(),
         }
     }
 }
diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs
index a00b7ff..3a981f4 100644
--- a/dhall/src/semantics/nze/normalize.rs
+++ b/dhall/src/semantics/nze/normalize.rs
@@ -17,14 +17,14 @@ pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind {
             closure.apply(a).to_whnf_check_type(ty)
         }
         ValueKind::AppliedBuiltin(closure) => {
-            closure.apply(a, f.get_type().unwrap(), ty)
+            closure.apply(a, f.get_type_not_sort(), ty)
         }
         ValueKind::UnionConstructor(l, kts, uniont) => ValueKind::UnionLit(
             l.clone(),
             a,
             kts.clone(),
             uniont.clone(),
-            f.get_type().unwrap(),
+            f.get_type_not_sort(),
         ),
         _ => ValueKind::PartialExpr(ExprKind::App(f, a)),
     }
@@ -349,7 +349,7 @@ pub(crate) fn normalize_one_layer(
             UnionType(kts) => Ret::ValueKind(UnionConstructor(
                 l.clone(),
                 kts.clone(),
-                v.get_type().unwrap(),
+                v.get_type_not_sort(),
             )),
             PartialExpr(ExprKind::BinOp(
                 BinOp::RightBiasedRecordMerge,
@@ -536,7 +536,7 @@ pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> ValueKind {
         }
         TyExprKind::Expr(ExprKind::Let(_, None, val, body)) => {
             let val = val.eval(env);
-            body.eval(&env.insert_value(val)).kind().clone()
+            body.eval(&env.insert_value_noty(val)).kind().clone()
         }
         TyExprKind::Expr(e) => {
             let ty = match tye.get_type() {
diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs
index 607aa0d..203b479 100644
--- a/dhall/src/semantics/nze/value.rs
+++ b/dhall/src/semantics/nze/value.rs
@@ -3,13 +3,11 @@ use std::rc::Rc;
 
 use crate::error::{TypeError, TypeMessage};
 use crate::semantics::nze::lazy;
-use crate::semantics::Binder;
 use crate::semantics::{
     apply_any, normalize_one_layer, normalize_tyexpr_whnf, squash_textlit,
-    TyEnv,
+    type_of_builtin, type_with, typecheck, Binder, BuiltinClosure, NzEnv,
+    NzVar, TyEnv, TyExpr, TyExprKind, VarEnv,
 };
-use crate::semantics::{type_of_builtin, typecheck, TyExpr, TyExprKind};
-use crate::semantics::{BuiltinClosure, NzEnv, NzVar, VarEnv};
 use crate::syntax::{
     BinOp, Builtin, Const, ExprKind, Integer, InterpolatedTextContents, Label,
     NaiveDouble, Natural, Span,
@@ -119,11 +117,14 @@ impl Value {
         )
         .into_value()
     }
+    pub(crate) fn const_kind() -> Value {
+        Value::from_const(Const::Kind)
+    }
     /// Construct a Value from a completely unnormalized expression.
     pub(crate) fn new_thunk(env: &NzEnv, tye: TyExpr) -> Value {
         ValueInternal::from_thunk(
             Thunk::new(env, tye.clone()),
-            tye.get_type().ok(),
+            Some(Value::const_kind()),
             tye.span().clone(),
         )
         .into_value()
@@ -137,24 +138,31 @@ impl Value {
         let env = NzEnv::new();
         ValueInternal::from_thunk(
             Thunk::from_partial_expr(env, e, ty.clone()),
-            Some(ty),
+            Some(Value::const_kind()),
             Span::Artificial,
         )
         .into_value()
     }
     /// Make a Value from a ValueKind
     pub(crate) fn from_kind_and_type(v: ValueKind, t: Value) -> Value {
-        ValueInternal::from_whnf(v, Some(t), Span::Artificial).into_value()
+        ValueInternal::from_whnf(v, Some(Value::const_kind()), Span::Artificial)
+            .into_value()
     }
     pub(crate) fn from_const(c: Const) -> Self {
         let v = ValueKind::Const(c);
         match c {
-            Const::Type => {
-                Value::from_kind_and_type(v, Value::from_const(Const::Kind))
-            }
-            Const::Kind => {
-                Value::from_kind_and_type(v, Value::from_const(Const::Sort))
-            }
+            Const::Type => ValueInternal::from_whnf(
+                v,
+                Some(Value::from_const(Const::Kind)),
+                Span::Artificial,
+            )
+            .into_value(),
+            Const::Kind => ValueInternal::from_whnf(
+                v,
+                Some(Value::const_sort()),
+                Span::Artificial,
+            )
+            .into_value(),
             Const::Sort => Value::const_sort(),
         }
     }
@@ -226,14 +234,10 @@ impl Value {
     }
 
     pub(crate) fn app(&self, v: Value) -> Value {
-        let body_t = match &*self.get_type_not_sort().kind() {
-            ValueKind::PiClosure { annot, closure, .. } => {
-                v.check_type(annot);
-                closure.apply(v.clone())
-            }
-            _ => unreachable!("Internal type error"),
-        };
-        Value::from_kind_and_type(apply_any(self.clone(), v, &body_t), body_t)
+        Value::from_kind_and_type(
+            apply_any(self.clone(), v, &Value::const_kind()),
+            Value::const_kind(),
+        )
     }
 
     /// In debug mode, panic if the provided type doesn't match the value's type.
@@ -246,12 +250,16 @@ impl Value {
         //     "Internal type error"
         // );
     }
-    pub(crate) fn get_type(&self) -> Result<Value, TypeError> {
+    pub(crate) fn get_type(&self, tyenv: &TyEnv) -> Result<Value, TypeError> {
+        let expr = self.to_tyexpr(tyenv.as_varenv()).to_expr_tyenv(tyenv);
+        type_with(tyenv, &expr).unwrap().get_type()
+    }
+    pub(crate) fn get_type_noenv(&self) -> Result<Value, TypeError> {
         Ok(self.0.get_type()?.clone())
     }
     /// When we know the value isn't `Sort`, this gets the type directly
     pub(crate) fn get_type_not_sort(&self) -> Value {
-        self.get_type()
+        self.get_type_noenv()
             .expect("Internal type error: value is `Sort` but shouldn't be")
     }
 
@@ -366,6 +374,10 @@ impl Value {
 
         TyExpr::new(tye, self.0.ty.clone(), self.0.span.clone())
     }
+    pub fn to_tyexpr_tyenv(&self, tyenv: &TyEnv) -> TyExpr {
+        let expr = self.to_tyexpr(tyenv.as_varenv()).to_expr_tyenv(tyenv);
+        type_with(tyenv, &expr).unwrap()
+    }
     pub fn to_tyexpr_noenv(&self) -> TyExpr {
         self.to_tyexpr(VarEnv::new())
     }
@@ -522,7 +534,7 @@ impl Closure {
     pub fn apply(&self, val: Value) -> Value {
         match self {
             Closure::Closure { env, body, .. } => {
-                body.eval(&env.insert_value(val))
+                body.eval(&env.insert_value_noty(val))
             }
             Closure::ConstantClosure { body, .. } => body.clone(),
         }
-- 
cgit v1.2.3


From 5870a46d5ab5810901198f03ed461d5c3bb5aa8a Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Thu, 6 Feb 2020 17:58:48 +0000
Subject: Remove move type propagation through Value

---
 dhall/src/semantics/nze/normalize.rs | 124 ++++++++++-------------------------
 dhall/src/semantics/nze/value.rs     |  84 ++++++------------------
 2 files changed, 54 insertions(+), 154 deletions(-)

(limited to 'dhall/src/semantics/nze')

diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs
index 3a981f4..c660fce 100644
--- a/dhall/src/semantics/nze/normalize.rs
+++ b/dhall/src/semantics/nze/normalize.rs
@@ -6,18 +6,16 @@ use crate::semantics::{
     Binder, BuiltinClosure, Closure, TextLit, TyExpr, TyExprKind, Value,
     ValueKind,
 };
-use crate::syntax::{
-    BinOp, Builtin, Const, ExprKind, InterpolatedTextContents,
-};
+use crate::syntax::{BinOp, Builtin, ExprKind, InterpolatedTextContents};
 use crate::Normalized;
 
-pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind {
+pub(crate) fn apply_any(f: Value, a: Value) -> ValueKind {
     match f.kind() {
         ValueKind::LamClosure { closure, .. } => {
-            closure.apply(a).to_whnf_check_type(ty)
+            closure.apply(a).kind().clone()
         }
         ValueKind::AppliedBuiltin(closure) => {
-            closure.apply(a, f.get_type_not_sort(), ty)
+            closure.apply(a, f.get_type_not_sort())
         }
         ValueKind::UnionConstructor(l, kts, uniont) => ValueKind::UnionLit(
             l.clone(),
@@ -102,12 +100,7 @@ enum Ret<'a> {
     Expr(ExprKind<Value, Normalized>),
 }
 
-fn apply_binop<'a>(
-    o: BinOp,
-    x: &'a Value,
-    y: &'a Value,
-    ty: &Value,
-) -> Option<Ret<'a>> {
+fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option<Ret<'a>> {
     use BinOp::{
         BoolAnd, BoolEQ, BoolNE, BoolOr, Equivalence, ListAppend, NaturalPlus,
         NaturalTimes, RecursiveRecordMerge, RecursiveRecordTypeMerge,
@@ -194,19 +187,12 @@ fn apply_binop<'a>(
             Ret::ValueRef(y)
         }
         (RecursiveRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => {
-            let kts = match ty.kind() {
-                RecordType(kts) => kts,
-                _ => unreachable!("Internal type error"),
-            };
-            let kvs = merge_maps::<_, _, _, !>(kvs1, kvs2, |k, v1, v2| {
-                Ok(Value::from_partial_expr(
-                    ExprKind::BinOp(
-                        RecursiveRecordMerge,
-                        v1.clone(),
-                        v2.clone(),
-                    ),
-                    kts.get(k).expect("Internal type error").clone(),
-                ))
+            let kvs = merge_maps::<_, _, _, !>(kvs1, kvs2, |_, v1, v2| {
+                Ok(Value::from_partial_expr(ExprKind::BinOp(
+                    RecursiveRecordMerge,
+                    v1.clone(),
+                    v2.clone(),
+                )))
             })?;
             Ret::ValueKind(RecordLit(kvs))
         }
@@ -217,14 +203,11 @@ fn apply_binop<'a>(
                 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(
-                            RecursiveRecordTypeMerge,
-                            l.clone(),
-                            r.clone(),
-                        ),
-                        ty.clone(),
-                    ))
+                    Ok(Value::from_partial_expr(ExprKind::BinOp(
+                        RecursiveRecordTypeMerge,
+                        l.clone(),
+                        r.clone(),
+                    )))
                 },
             )?;
             Ret::ValueKind(RecordType(kts))
@@ -240,7 +223,6 @@ fn apply_binop<'a>(
 
 pub(crate) fn normalize_one_layer(
     expr: ExprKind<Value, Normalized>,
-    ty: &Value,
     env: &NzEnv,
 ) -> ValueKind {
     use ValueKind::{
@@ -318,7 +300,7 @@ pub(crate) fn normalize_one_layer(
                 }
             }
         }
-        ExprKind::BinOp(o, ref x, ref y) => match apply_binop(o, x, y, ty) {
+        ExprKind::BinOp(o, ref x, ref y) => match apply_binop(o, x, y) {
             Some(ret) => ret,
             None => Ret::Expr(expr),
         },
@@ -335,7 +317,6 @@ pub(crate) fn normalize_one_layer(
             PartialExpr(ExprKind::Projection(v2, _)) => {
                 return normalize_one_layer(
                     ExprKind::Projection(v2.clone(), ls.clone()),
-                    ty,
                     env,
                 )
             }
@@ -361,45 +342,26 @@ pub(crate) fn normalize_one_layer(
                     None => {
                         return normalize_one_layer(
                             ExprKind::Field(x.clone(), l.clone()),
-                            ty,
                             env,
                         )
                     }
                 },
                 (RecordLit(kvs), _) => match kvs.get(l) {
                     Some(r) => Ret::Expr(ExprKind::Field(
-                        Value::from_kind_and_type(
-                            PartialExpr(ExprKind::BinOp(
-                                BinOp::RightBiasedRecordMerge,
-                                Value::from_kind_and_type(
-                                    RecordLit({
-                                        let mut kvs = HashMap::new();
-                                        kvs.insert(l.clone(), r.clone());
-                                        kvs
-                                    }),
-                                    Value::from_kind_and_type(
-                                        RecordType({
-                                            let mut kvs = HashMap::new();
-                                            kvs.insert(
-                                                l.clone(),
-                                                r.get_type_not_sort(),
-                                            );
-                                            kvs
-                                        }),
-                                        r.get_type_not_sort()
-                                            .get_type_not_sort(),
-                                    ),
-                                ),
-                                y.clone(),
-                            )),
-                            v.get_type_not_sort(),
-                        ),
+                        Value::from_kind(PartialExpr(ExprKind::BinOp(
+                            BinOp::RightBiasedRecordMerge,
+                            Value::from_kind(RecordLit({
+                                let mut kvs = HashMap::new();
+                                kvs.insert(l.clone(), r.clone());
+                                kvs
+                            })),
+                            y.clone(),
+                        ))),
                         l.clone(),
                     )),
                     None => {
                         return normalize_one_layer(
                             ExprKind::Field(y.clone(), l.clone()),
-                            ty,
                             env,
                         )
                     }
@@ -416,7 +378,6 @@ pub(crate) fn normalize_one_layer(
                     None => {
                         return normalize_one_layer(
                             ExprKind::Field(y.clone(), l.clone()),
-                            ty,
                             env,
                         )
                     }
@@ -426,7 +387,6 @@ pub(crate) fn normalize_one_layer(
                     None => {
                         return normalize_one_layer(
                             ExprKind::Field(x.clone(), l.clone()),
-                            ty,
                             env,
                         )
                     }
@@ -482,22 +442,9 @@ pub(crate) fn normalize_one_layer(
                     .sorted_by_key(|(k, _)| k.clone())
                     .map(|(k, v)| {
                         let mut rec = HashMap::new();
-                        let mut rec_ty = HashMap::new();
                         rec.insert("mapKey".into(), Value::from_text(k));
                         rec.insert("mapValue".into(), v.clone());
-                        rec_ty.insert(
-                            "mapKey".into(),
-                            Value::from_builtin(Builtin::Text),
-                        );
-                        rec_ty.insert("mapValue".into(), v.get_type_not_sort());
-
-                        Value::from_kind_and_type(
-                            ValueKind::RecordLit(rec),
-                            Value::from_kind_and_type(
-                                ValueKind::RecordType(rec_ty),
-                                Value::from_const(Const::Type),
-                            ),
-                        )
+                        Value::from_kind(ValueKind::RecordLit(rec))
                     })
                     .collect(),
             )),
@@ -507,8 +454,8 @@ pub(crate) fn normalize_one_layer(
 
     match ret {
         Ret::ValueKind(v) => v,
-        Ret::Value(v) => v.to_whnf_check_type(ty),
-        Ret::ValueRef(v) => v.to_whnf_check_type(ty),
+        Ret::Value(v) => v.kind().clone(),
+        Ret::ValueRef(v) => v.kind().clone(),
         Ret::Expr(expr) => ValueKind::PartialExpr(expr),
     }
 }
@@ -521,17 +468,16 @@ pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> ValueKind {
             let annot = annot.eval(env);
             ValueKind::LamClosure {
                 binder: Binder::new(binder.clone()),
-                annot: annot.clone(),
-                closure: Closure::new(annot, env, body.clone()),
+                annot: annot,
+                closure: Closure::new(env, body.clone()),
             }
         }
         TyExprKind::Expr(ExprKind::Pi(binder, annot, body)) => {
             let annot = annot.eval(env);
-            let closure = Closure::new(annot.clone(), env, body.clone());
             ValueKind::PiClosure {
                 binder: Binder::new(binder.clone()),
                 annot,
-                closure,
+                closure: Closure::new(env, body.clone()),
             }
         }
         TyExprKind::Expr(ExprKind::Let(_, None, val, body)) => {
@@ -539,12 +485,8 @@ pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> ValueKind {
             body.eval(&env.insert_value_noty(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)
+            normalize_one_layer(e, env)
         }
     }
 }
diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs
index 203b479..47c50a4 100644
--- a/dhall/src/semantics/nze/value.rs
+++ b/dhall/src/semantics/nze/value.rs
@@ -5,8 +5,8 @@ use crate::error::{TypeError, TypeMessage};
 use crate::semantics::nze::lazy;
 use crate::semantics::{
     apply_any, normalize_one_layer, normalize_tyexpr_whnf, squash_textlit,
-    type_of_builtin, type_with, typecheck, Binder, BuiltinClosure, NzEnv,
-    NzVar, TyEnv, TyExpr, TyExprKind, VarEnv,
+    type_with, Binder, BuiltinClosure, NzEnv, NzVar, TyEnv, TyExpr, TyExprKind,
+    VarEnv,
 };
 use crate::syntax::{
     BinOp, Builtin, Const, ExprKind, Integer, InterpolatedTextContents, Label,
@@ -39,7 +39,6 @@ pub(crate) enum Thunk {
     PartialExpr {
         env: NzEnv,
         expr: ExprKind<Value, Normalized>,
-        ty: Value,
     },
 }
 
@@ -47,11 +46,7 @@ pub(crate) enum Thunk {
 #[derive(Debug, Clone)]
 pub(crate) enum Closure {
     /// Normal closure
-    Closure {
-        arg_ty: Value,
-        env: NzEnv,
-        body: TyExpr,
-    },
+    Closure { env: NzEnv, body: TyExpr },
     /// Closure that ignores the argument passed
     ConstantClosure { body: Value },
 }
@@ -130,21 +125,18 @@ impl Value {
         .into_value()
     }
     /// Construct a Value from a partially normalized expression that's not in WHNF.
-    pub(crate) fn from_partial_expr(
-        e: ExprKind<Value, Normalized>,
-        ty: Value,
-    ) -> Value {
+    pub(crate) fn from_partial_expr(e: ExprKind<Value, Normalized>) -> Value {
         // TODO: env
         let env = NzEnv::new();
         ValueInternal::from_thunk(
-            Thunk::from_partial_expr(env, e, ty.clone()),
+            Thunk::from_partial_expr(env, e),
             Some(Value::const_kind()),
             Span::Artificial,
         )
         .into_value()
     }
     /// Make a Value from a ValueKind
-    pub(crate) fn from_kind_and_type(v: ValueKind, t: Value) -> Value {
+    pub(crate) fn from_kind(v: ValueKind) -> Value {
         ValueInternal::from_whnf(v, Some(Value::const_kind()), Span::Artificial)
             .into_value()
     }
@@ -170,16 +162,12 @@ impl Value {
         Self::from_builtin_env(b, &NzEnv::new())
     }
     pub(crate) fn from_builtin_env(b: Builtin, env: &NzEnv) -> Self {
-        Value::from_kind_and_type(
-            ValueKind::from_builtin_env(b, env.clone()),
-            typecheck(&type_of_builtin(b)).unwrap().eval_closed_expr(),
-        )
+        Value::from_kind(ValueKind::from_builtin_env(b, env.clone()))
     }
     pub(crate) fn from_text(txt: impl ToString) -> Self {
-        Value::from_kind_and_type(
-            ValueKind::TextLit(TextLit::from_text(txt.to_string())),
-            Value::from_builtin(Builtin::Text),
-        )
+        Value::from_kind(ValueKind::TextLit(TextLit::from_text(
+            txt.to_string(),
+        )))
     }
 
     pub(crate) fn as_const(&self) -> Option<Const> {
@@ -210,14 +198,6 @@ impl Value {
     pub(crate) fn to_expr_tyenv(&self, env: &TyEnv) -> NormalizedExpr {
         self.to_tyexpr(env.as_varenv()).to_expr_tyenv(env)
     }
-    pub(crate) fn to_whnf_ignore_type(&self) -> ValueKind {
-        self.kind().clone()
-    }
-    /// Before discarding type information, check that it matches the expected return type.
-    pub(crate) fn to_whnf_check_type(&self, ty: &Value) -> ValueKind {
-        self.check_type(ty);
-        self.to_whnf_ignore_type()
-    }
 
     /// Normalizes contents to normal form; faster than `normalize` if
     /// no one else shares this.
@@ -234,33 +214,19 @@ impl Value {
     }
 
     pub(crate) fn app(&self, v: Value) -> Value {
-        Value::from_kind_and_type(
-            apply_any(self.clone(), v, &Value::const_kind()),
-            Value::const_kind(),
-        )
+        Value::from_kind(apply_any(self.clone(), v))
     }
 
-    /// In debug mode, panic if the provided type doesn't match the value's type.
-    /// Otherwise does nothing.
-    pub(crate) fn check_type(&self, _ty: &Value) {
-        // TODO: reenable
-        // debug_assert_eq!(
-        //     Some(ty),
-        //     self.get_type().ok().as_ref(),
-        //     "Internal type error"
-        // );
-    }
     pub(crate) fn get_type(&self, tyenv: &TyEnv) -> Result<Value, TypeError> {
         let expr = self.to_tyexpr(tyenv.as_varenv()).to_expr_tyenv(tyenv);
         type_with(tyenv, &expr).unwrap().get_type()
     }
-    pub(crate) fn get_type_noenv(&self) -> Result<Value, TypeError> {
-        Ok(self.0.get_type()?.clone())
-    }
     /// When we know the value isn't `Sort`, this gets the type directly
     pub(crate) fn get_type_not_sort(&self) -> Value {
-        self.get_type_noenv()
+        self.0
+            .get_type()
             .expect("Internal type error: value is `Sort` but shouldn't be")
+            .clone()
     }
 
     pub fn to_tyexpr(&self, venv: VarEnv) -> TyExpr {
@@ -422,8 +388,8 @@ impl ValueInternal {
 }
 
 impl ValueKind {
-    pub(crate) fn into_value_with_type(self, t: Value) -> Value {
-        Value::from_kind_and_type(self, t)
+    pub(crate) fn into_value(self) -> Value {
+        Value::from_kind(self)
     }
 
     pub(crate) fn normalize(&self) {
@@ -504,24 +470,20 @@ impl Thunk {
     pub fn from_partial_expr(
         env: NzEnv,
         expr: ExprKind<Value, Normalized>,
-        ty: Value,
     ) -> Self {
-        Thunk::PartialExpr { env, expr, ty }
+        Thunk::PartialExpr { env, expr }
     }
     pub fn eval(self) -> ValueKind {
         match self {
             Thunk::Thunk { env, body } => normalize_tyexpr_whnf(&body, &env),
-            Thunk::PartialExpr { env, expr, ty } => {
-                normalize_one_layer(expr, &ty, &env)
-            }
+            Thunk::PartialExpr { env, expr } => normalize_one_layer(expr, &env),
         }
     }
 }
 
 impl Closure {
-    pub fn new(arg_ty: Value, env: &NzEnv, body: TyExpr) -> Self {
+    pub fn new(env: &NzEnv, body: TyExpr) -> Self {
         Closure::Closure {
-            arg_ty,
             env: env.clone(),
             body,
         }
@@ -541,12 +503,8 @@ impl Closure {
     }
     fn apply_var(&self, var: NzVar) -> Value {
         match self {
-            Closure::Closure { arg_ty, .. } => {
-                let val = Value::from_kind_and_type(
-                    ValueKind::Var(var),
-                    arg_ty.clone(),
-                );
-                self.apply(val)
+            Closure::Closure { .. } => {
+                self.apply(Value::from_kind(ValueKind::Var(var)))
             }
             Closure::ConstantClosure { body, .. } => body.clone(),
         }
-- 
cgit v1.2.3


From 27031b3739ff9f2043e64130a4c5699d0f9233e8 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 9 Feb 2020 11:23:59 +0000
Subject: Add Hir as untyped alternative to TyExpr

---
 dhall/src/semantics/nze/normalize.rs |  4 ++--
 dhall/src/semantics/nze/value.rs     | 10 +++++-----
 2 files changed, 7 insertions(+), 7 deletions(-)

(limited to 'dhall/src/semantics/nze')

diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs
index c660fce..b5949f5 100644
--- a/dhall/src/semantics/nze/normalize.rs
+++ b/dhall/src/semantics/nze/normalize.rs
@@ -3,8 +3,8 @@ use std::collections::HashMap;
 
 use crate::semantics::NzEnv;
 use crate::semantics::{
-    Binder, BuiltinClosure, Closure, TextLit, TyExpr, TyExprKind, Value,
-    ValueKind,
+    Binder, BuiltinClosure, Closure, Hir, HirKind, TextLit, TyExpr, TyExprKind,
+    Value, ValueKind,
 };
 use crate::syntax::{BinOp, Builtin, ExprKind, InterpolatedTextContents};
 use crate::Normalized;
diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs
index 47c50a4..d4213bc 100644
--- a/dhall/src/semantics/nze/value.rs
+++ b/dhall/src/semantics/nze/value.rs
@@ -5,8 +5,8 @@ use crate::error::{TypeError, TypeMessage};
 use crate::semantics::nze::lazy;
 use crate::semantics::{
     apply_any, normalize_one_layer, normalize_tyexpr_whnf, squash_textlit,
-    type_with, Binder, BuiltinClosure, NzEnv, NzVar, TyEnv, TyExpr, TyExprKind,
-    VarEnv,
+    type_with, Binder, BuiltinClosure, Hir, NzEnv, NzVar, TyEnv, TyExpr,
+    TyExprKind, VarEnv,
 };
 use crate::syntax::{
     BinOp, Builtin, Const, ExprKind, Integer, InterpolatedTextContents, Label,
@@ -461,19 +461,19 @@ impl ValueKind {
 }
 
 impl Thunk {
-    pub fn new(env: &NzEnv, body: TyExpr) -> Self {
+    fn new(env: &NzEnv, body: TyExpr) -> Self {
         Thunk::Thunk {
             env: env.clone(),
             body,
         }
     }
-    pub fn from_partial_expr(
+    fn from_partial_expr(
         env: NzEnv,
         expr: ExprKind<Value, Normalized>,
     ) -> Self {
         Thunk::PartialExpr { env, expr }
     }
-    pub fn eval(self) -> ValueKind {
+    fn eval(self) -> ValueKind {
         match self {
             Thunk::Thunk { env, body } => normalize_tyexpr_whnf(&body, &env),
             Thunk::PartialExpr { env, expr } => normalize_one_layer(expr, &env),
-- 
cgit v1.2.3


From 6c90d356c9a4a5bbeb88f25ad0ab499ba1503eae Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 9 Feb 2020 11:53:55 +0000
Subject: Remove most TyExpr from normalization

---
 dhall/src/semantics/nze/normalize.rs |  21 +++---
 dhall/src/semantics/nze/value.rs     | 120 ++++++++++++++++-------------------
 2 files changed, 65 insertions(+), 76 deletions(-)

(limited to 'dhall/src/semantics/nze')

diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs
index b5949f5..acb2e51 100644
--- a/dhall/src/semantics/nze/normalize.rs
+++ b/dhall/src/semantics/nze/normalize.rs
@@ -3,8 +3,7 @@ use std::collections::HashMap;
 
 use crate::semantics::NzEnv;
 use crate::semantics::{
-    Binder, BuiltinClosure, Closure, Hir, HirKind, TextLit, TyExpr, TyExprKind,
-    Value, ValueKind,
+    Binder, BuiltinClosure, Closure, Hir, HirKind, TextLit, Value, ValueKind,
 };
 use crate::syntax::{BinOp, Builtin, ExprKind, InterpolatedTextContents};
 use crate::Normalized;
@@ -460,11 +459,11 @@ pub(crate) fn normalize_one_layer(
     }
 }
 
-/// Normalize a TyExpr into WHNF
-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)) => {
+/// Normalize Hir into WHNF
+pub(crate) fn normalize_hir_whnf(env: &NzEnv, hir: &Hir) -> ValueKind {
+    match hir.kind() {
+        HirKind::Var(var) => env.lookup_val(var),
+        HirKind::Expr(ExprKind::Lam(binder, annot, body)) => {
             let annot = annot.eval(env);
             ValueKind::LamClosure {
                 binder: Binder::new(binder.clone()),
@@ -472,7 +471,7 @@ pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> ValueKind {
                 closure: Closure::new(env, body.clone()),
             }
         }
-        TyExprKind::Expr(ExprKind::Pi(binder, annot, body)) => {
+        HirKind::Expr(ExprKind::Pi(binder, annot, body)) => {
             let annot = annot.eval(env);
             ValueKind::PiClosure {
                 binder: Binder::new(binder.clone()),
@@ -480,12 +479,12 @@ pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> ValueKind {
                 closure: Closure::new(env, body.clone()),
             }
         }
-        TyExprKind::Expr(ExprKind::Let(_, None, val, body)) => {
+        HirKind::Expr(ExprKind::Let(_, None, val, body)) => {
             let val = val.eval(env);
             body.eval(&env.insert_value_noty(val)).kind().clone()
         }
-        TyExprKind::Expr(e) => {
-            let e = e.map_ref(|tye| tye.eval(env));
+        HirKind::Expr(e) => {
+            let e = e.map_ref(|hir| hir.eval(env));
             normalize_one_layer(e, env)
         }
     }
diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs
index d4213bc..d05c545 100644
--- a/dhall/src/semantics/nze/value.rs
+++ b/dhall/src/semantics/nze/value.rs
@@ -4,9 +4,9 @@ use std::rc::Rc;
 use crate::error::{TypeError, TypeMessage};
 use crate::semantics::nze::lazy;
 use crate::semantics::{
-    apply_any, normalize_one_layer, normalize_tyexpr_whnf, squash_textlit,
-    type_with, Binder, BuiltinClosure, Hir, NzEnv, NzVar, TyEnv, TyExpr,
-    TyExprKind, VarEnv,
+    apply_any, normalize_hir_whnf, normalize_one_layer, squash_textlit,
+    type_with, Binder, BuiltinClosure, Hir, HirKind, NzEnv, NzVar, TyEnv,
+    TyExpr, VarEnv,
 };
 use crate::syntax::{
     BinOp, Builtin, Const, ExprKind, Integer, InterpolatedTextContents, Label,
@@ -34,7 +34,7 @@ struct ValueInternal {
 #[derive(Debug, Clone)]
 pub(crate) enum Thunk {
     /// A completely unnormalized expression.
-    Thunk { env: NzEnv, body: TyExpr },
+    Thunk { env: NzEnv, body: Hir },
     /// A partially normalized expression that may need to go through `normalize_one_layer`.
     PartialExpr {
         env: NzEnv,
@@ -46,7 +46,7 @@ pub(crate) enum Thunk {
 #[derive(Debug, Clone)]
 pub(crate) enum Closure {
     /// Normal closure
-    Closure { env: NzEnv, body: TyExpr },
+    Closure { env: NzEnv, body: Hir },
     /// Closure that ignores the argument passed
     ConstantClosure { body: Value },
 }
@@ -116,11 +116,12 @@ impl Value {
         Value::from_const(Const::Kind)
     }
     /// Construct a Value from a completely unnormalized expression.
-    pub(crate) fn new_thunk(env: &NzEnv, tye: TyExpr) -> Value {
+    pub(crate) fn new_thunk(env: &NzEnv, hir: Hir) -> Value {
+        let span = hir.span();
         ValueInternal::from_thunk(
-            Thunk::new(env, tye.clone()),
+            Thunk::new(env, hir),
             Some(Value::const_kind()),
-            tye.span().clone(),
+            span,
         )
         .into_value()
     }
@@ -176,13 +177,8 @@ impl Value {
             _ => None,
         }
     }
-    // pub(crate) fn span(&self) -> Span {
-    //     self.0.span.clone()
-    // }
 
     /// This is what you want if you want to pattern-match on the value.
-    /// WARNING: drop this ref before normalizing the same value or you will run into BorrowMut
-    /// panics.
     pub(crate) fn kind(&self) -> &ValueKind {
         self.0.kind()
     }
@@ -196,7 +192,7 @@ impl Value {
         self.to_tyexpr_noenv().to_expr(opts)
     }
     pub(crate) fn to_expr_tyenv(&self, env: &TyEnv) -> NormalizedExpr {
-        self.to_tyexpr(env.as_varenv()).to_expr_tyenv(env)
+        self.to_hir(env.as_varenv()).to_expr_tyenv(env)
     }
 
     /// Normalizes contents to normal form; faster than `normalize` if
@@ -218,8 +214,7 @@ impl Value {
     }
 
     pub(crate) fn get_type(&self, tyenv: &TyEnv) -> Result<Value, TypeError> {
-        let expr = self.to_tyexpr(tyenv.as_varenv()).to_expr_tyenv(tyenv);
-        type_with(tyenv, &expr).unwrap().get_type()
+        self.to_tyexpr_tyenv(tyenv).get_type()
     }
     /// When we know the value isn't `Sort`, this gets the type directly
     pub(crate) fn get_type_not_sort(&self) -> Value {
@@ -229,21 +224,21 @@ impl Value {
             .clone()
     }
 
-    pub fn to_tyexpr(&self, venv: VarEnv) -> TyExpr {
+    pub fn to_hir(&self, venv: VarEnv) -> Hir {
         let map_uniontype = |kts: &HashMap<Label, Option<Value>>| {
             ExprKind::UnionType(
                 kts.iter()
                     .map(|(k, v)| {
-                        (k.clone(), v.as_ref().map(|v| v.to_tyexpr(venv)))
+                        (k.clone(), v.as_ref().map(|v| v.to_hir(venv)))
                     })
                     .collect(),
             )
         };
 
-        let tye = match &*self.kind() {
-            ValueKind::Var(v) => TyExprKind::Var(venv.lookup(v)),
-            ValueKind::AppliedBuiltin(closure) => closure.to_tyexprkind(venv),
-            self_kind => TyExprKind::Expr(match self_kind {
+        let hir = match &*self.kind() {
+            ValueKind::Var(v) => HirKind::Var(venv.lookup(v)),
+            ValueKind::AppliedBuiltin(closure) => closure.to_hirkind(venv),
+            self_kind => HirKind::Expr(match self_kind {
                 ValueKind::Var(..) | ValueKind::AppliedBuiltin(..) => {
                     unreachable!()
                 }
@@ -253,8 +248,8 @@ impl Value {
                     closure,
                 } => ExprKind::Lam(
                     binder.to_label(),
-                    annot.to_tyexpr(venv),
-                    closure.to_tyexpr(venv),
+                    annot.to_hir(venv),
+                    closure.to_hir(venv),
                 ),
                 ValueKind::PiClosure {
                     binder,
@@ -262,8 +257,8 @@ impl Value {
                     closure,
                 } => ExprKind::Pi(
                     binder.to_label(),
-                    annot.to_tyexpr(venv),
-                    closure.to_tyexpr(venv),
+                    annot.to_hir(venv),
+                    closure.to_hir(venv),
                 ),
                 ValueKind::Const(c) => ExprKind::Const(*c),
                 ValueKind::BoolLit(b) => ExprKind::BoolLit(*b),
@@ -271,81 +266,75 @@ impl Value {
                 ValueKind::IntegerLit(n) => ExprKind::IntegerLit(*n),
                 ValueKind::DoubleLit(n) => ExprKind::DoubleLit(*n),
                 ValueKind::EmptyOptionalLit(n) => ExprKind::App(
-                    Value::from_builtin(Builtin::OptionalNone).to_tyexpr(venv),
-                    n.to_tyexpr(venv),
+                    Value::from_builtin(Builtin::OptionalNone).to_hir(venv),
+                    n.to_hir(venv),
                 ),
                 ValueKind::NEOptionalLit(n) => {
-                    ExprKind::SomeLit(n.to_tyexpr(venv))
-                }
-                ValueKind::EmptyListLit(n) => {
-                    ExprKind::EmptyListLit(TyExpr::new(
-                        TyExprKind::Expr(ExprKind::App(
-                            Value::from_builtin(Builtin::List).to_tyexpr(venv),
-                            n.to_tyexpr(venv),
-                        )),
-                        Some(Value::from_const(Const::Type)),
-                        Span::Artificial,
-                    ))
+                    ExprKind::SomeLit(n.to_hir(venv))
                 }
+                ValueKind::EmptyListLit(n) => ExprKind::EmptyListLit(Hir::new(
+                    HirKind::Expr(ExprKind::App(
+                        Value::from_builtin(Builtin::List).to_hir(venv),
+                        n.to_hir(venv),
+                    )),
+                    Span::Artificial,
+                )),
                 ValueKind::NEListLit(elts) => ExprKind::NEListLit(
-                    elts.iter().map(|v| v.to_tyexpr(venv)).collect(),
+                    elts.iter().map(|v| v.to_hir(venv)).collect(),
                 ),
                 ValueKind::TextLit(elts) => ExprKind::TextLit(
                     elts.iter()
-                        .map(|t| t.map_ref(|v| v.to_tyexpr(venv)))
+                        .map(|t| t.map_ref(|v| v.to_hir(venv)))
                         .collect(),
                 ),
                 ValueKind::RecordLit(kvs) => ExprKind::RecordLit(
                     kvs.iter()
-                        .map(|(k, v)| (k.clone(), v.to_tyexpr(venv)))
+                        .map(|(k, v)| (k.clone(), v.to_hir(venv)))
                         .collect(),
                 ),
                 ValueKind::RecordType(kts) => ExprKind::RecordType(
                     kts.iter()
-                        .map(|(k, v)| (k.clone(), v.to_tyexpr(venv)))
+                        .map(|(k, v)| (k.clone(), v.to_hir(venv)))
                         .collect(),
                 ),
                 ValueKind::UnionType(kts) => map_uniontype(kts),
                 ValueKind::UnionConstructor(l, kts, t) => ExprKind::Field(
-                    TyExpr::new(
-                        TyExprKind::Expr(map_uniontype(kts)),
-                        Some(t.clone()),
+                    Hir::new(
+                        HirKind::Expr(map_uniontype(kts)),
                         Span::Artificial,
                     ),
                     l.clone(),
                 ),
                 ValueKind::UnionLit(l, v, kts, uniont, ctort) => ExprKind::App(
-                    TyExpr::new(
-                        TyExprKind::Expr(ExprKind::Field(
-                            TyExpr::new(
-                                TyExprKind::Expr(map_uniontype(kts)),
-                                Some(uniont.clone()),
+                    Hir::new(
+                        HirKind::Expr(ExprKind::Field(
+                            Hir::new(
+                                HirKind::Expr(map_uniontype(kts)),
                                 Span::Artificial,
                             ),
                             l.clone(),
                         )),
-                        Some(ctort.clone()),
                         Span::Artificial,
                     ),
-                    v.to_tyexpr(venv),
+                    v.to_hir(venv),
                 ),
                 ValueKind::Equivalence(x, y) => ExprKind::BinOp(
                     BinOp::Equivalence,
-                    x.to_tyexpr(venv),
-                    y.to_tyexpr(venv),
+                    x.to_hir(venv),
+                    y.to_hir(venv),
                 ),
-                ValueKind::PartialExpr(e) => e.map_ref(|v| v.to_tyexpr(venv)),
+                ValueKind::PartialExpr(e) => e.map_ref(|v| v.to_hir(venv)),
             }),
         };
 
-        TyExpr::new(tye, self.0.ty.clone(), self.0.span.clone())
+        Hir::new(hir, self.0.span.clone())
     }
     pub fn to_tyexpr_tyenv(&self, tyenv: &TyEnv) -> TyExpr {
-        let expr = self.to_tyexpr(tyenv.as_varenv()).to_expr_tyenv(tyenv);
+        let expr = self.to_hir(tyenv.as_varenv()).to_expr_tyenv(tyenv);
         type_with(tyenv, &expr).unwrap()
     }
     pub fn to_tyexpr_noenv(&self) -> TyExpr {
-        self.to_tyexpr(VarEnv::new())
+        self.to_tyexpr_tyenv(&TyEnv::new())
     }
 }
 
@@ -461,7 +450,7 @@ impl ValueKind {
 }
 
 impl Thunk {
-    fn new(env: &NzEnv, body: TyExpr) -> Self {
+    fn new(env: &NzEnv, body: Hir) -> Self {
         Thunk::Thunk {
             env: env.clone(),
             body,
@@ -475,14 +464,14 @@ impl Thunk {
     }
     fn eval(self) -> ValueKind {
         match self {
-            Thunk::Thunk { env, body } => normalize_tyexpr_whnf(&body, &env),
+            Thunk::Thunk { env, body } => normalize_hir_whnf(&env, &body),
             Thunk::PartialExpr { env, expr } => normalize_one_layer(expr, &env),
         }
     }
 }
 
 impl Closure {
-    pub fn new(env: &NzEnv, body: TyExpr) -> Self {
+    pub fn new(env: &NzEnv, body: Hir) -> Self {
         Closure::Closure {
             env: env.clone(),
             body,
@@ -512,10 +501,11 @@ impl Closure {
 
     // TODO: somehow normalize the body. Might require to pass an env.
     pub fn normalize(&self) {}
-    /// Convert this closure to a TyExpr
-    pub fn to_tyexpr(&self, venv: VarEnv) -> TyExpr {
+
+    /// Convert this closure to a Hir expression
+    pub fn to_hir(&self, venv: VarEnv) -> Hir {
         self.apply_var(NzVar::new(venv.size()))
-            .to_tyexpr(venv.insert())
+            .to_hir(venv.insert())
     }
     /// If the closure variable is free in the closure, return Err. Otherwise, return the value
     /// with that free variable remove.
-- 
cgit v1.2.3


From 5688ed654eee258bf8ffc8761ce693c73a0242d5 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 9 Feb 2020 11:58:11 +0000
Subject: Remove extra types stored in Value

---
 dhall/src/semantics/nze/normalize.rs | 24 ++++++++----------------
 dhall/src/semantics/nze/value.rs     | 15 ++++++---------
 2 files changed, 14 insertions(+), 25 deletions(-)

(limited to 'dhall/src/semantics/nze')

diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs
index acb2e51..981d894 100644
--- a/dhall/src/semantics/nze/normalize.rs
+++ b/dhall/src/semantics/nze/normalize.rs
@@ -13,16 +13,10 @@ pub(crate) fn apply_any(f: Value, a: Value) -> ValueKind {
         ValueKind::LamClosure { closure, .. } => {
             closure.apply(a).kind().clone()
         }
-        ValueKind::AppliedBuiltin(closure) => {
-            closure.apply(a, f.get_type_not_sort())
+        ValueKind::AppliedBuiltin(closure) => closure.apply(a),
+        ValueKind::UnionConstructor(l, kts) => {
+            ValueKind::UnionLit(l.clone(), a, kts.clone())
         }
-        ValueKind::UnionConstructor(l, kts, uniont) => ValueKind::UnionLit(
-            l.clone(),
-            a,
-            kts.clone(),
-            uniont.clone(),
-            f.get_type_not_sort(),
-        ),
         _ => ValueKind::PartialExpr(ExprKind::App(f, a)),
     }
 }
@@ -326,11 +320,9 @@ pub(crate) fn normalize_one_layer(
                 Some(r) => Ret::Value(r.clone()),
                 None => Ret::Expr(expr),
             },
-            UnionType(kts) => Ret::ValueKind(UnionConstructor(
-                l.clone(),
-                kts.clone(),
-                v.get_type_not_sort(),
-            )),
+            UnionType(kts) => {
+                Ret::ValueKind(UnionConstructor(l.clone(), kts.clone()))
+            }
             PartialExpr(ExprKind::BinOp(
                 BinOp::RightBiasedRecordMerge,
                 x,
@@ -402,11 +394,11 @@ pub(crate) fn normalize_one_layer(
         ExprKind::Merge(ref handlers, ref variant, _) => {
             match handlers.kind() {
                 RecordLit(kvs) => match variant.kind() {
-                    UnionConstructor(l, _, _) => match kvs.get(l) {
+                    UnionConstructor(l, _) => match kvs.get(l) {
                         Some(h) => Ret::Value(h.clone()),
                         None => Ret::Expr(expr),
                     },
-                    UnionLit(l, v, _, _, _) => match kvs.get(l) {
+                    UnionLit(l, v, _) => match kvs.get(l) {
                         Some(h) => Ret::Value(h.app(v.clone())),
                         None => Ret::Expr(expr),
                     },
diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs
index d05c545..a771b91 100644
--- a/dhall/src/semantics/nze/value.rs
+++ b/dhall/src/semantics/nze/value.rs
@@ -93,10 +93,8 @@ pub(crate) enum ValueKind {
     RecordType(HashMap<Label, Value>),
     RecordLit(HashMap<Label, Value>),
     UnionType(HashMap<Label, Option<Value>>),
-    // Also keep the type of the uniontype around
-    UnionConstructor(Label, HashMap<Label, Option<Value>>, Value),
-    // Also keep the type of the uniontype and the constructor around
-    UnionLit(Label, Value, HashMap<Label, Option<Value>>, Value, Value),
+    UnionConstructor(Label, HashMap<Label, Option<Value>>),
+    UnionLit(Label, Value, HashMap<Label, Option<Value>>),
     TextLit(TextLit),
     Equivalence(Value, Value),
     /// Invariant: evaluation must not be able to progress with `normalize_one_layer`?
@@ -298,14 +296,14 @@ impl Value {
                         .collect(),
                 ),
                 ValueKind::UnionType(kts) => map_uniontype(kts),
-                ValueKind::UnionConstructor(l, kts, t) => ExprKind::Field(
+                ValueKind::UnionConstructor(l, kts) => ExprKind::Field(
                     Hir::new(
                         HirKind::Expr(map_uniontype(kts)),
                         Span::Artificial,
                     ),
                     l.clone(),
                 ),
-                ValueKind::UnionLit(l, v, kts, uniont, ctort) => ExprKind::App(
+                ValueKind::UnionLit(l, v, kts) => ExprKind::App(
                     Hir::new(
                         HirKind::Expr(ExprKind::Field(
                             Hir::new(
@@ -418,13 +416,12 @@ impl ValueKind {
                     x.normalize();
                 }
             }
-            ValueKind::UnionType(kts)
-            | ValueKind::UnionConstructor(_, kts, _) => {
+            ValueKind::UnionType(kts) | ValueKind::UnionConstructor(_, kts) => {
                 for x in kts.values().flat_map(|opt| opt) {
                     x.normalize();
                 }
             }
-            ValueKind::UnionLit(_, v, kts, _, _) => {
+            ValueKind::UnionLit(_, v, kts) => {
                 v.normalize();
                 for x in kts.values().flat_map(|opt| opt) {
                     x.normalize();
-- 
cgit v1.2.3


From 21db63d3e614554f258526182c7ed89a2c244b65 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 9 Feb 2020 21:58:28 +0000
Subject: Take Hir for typecheck

---
 dhall/src/semantics/nze/value.rs | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

(limited to 'dhall/src/semantics/nze')

diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs
index a771b91..48acdb5 100644
--- a/dhall/src/semantics/nze/value.rs
+++ b/dhall/src/semantics/nze/value.rs
@@ -327,9 +327,12 @@ impl Value {
 
         Hir::new(hir, self.0.span.clone())
     }
+    pub fn to_hir_noenv(&self) -> Hir {
+        self.to_hir(VarEnv::new())
+    }
     pub fn to_tyexpr_tyenv(&self, tyenv: &TyEnv) -> TyExpr {
-        let expr = self.to_hir(tyenv.as_varenv()).to_expr_tyenv(tyenv);
-        type_with(tyenv, &expr).unwrap()
+        let hir = self.to_hir(tyenv.as_varenv());
+        type_with(tyenv, &hir).unwrap()
     }
     pub fn to_tyexpr_noenv(&self) -> TyExpr {
         self.to_tyexpr_tyenv(&TyEnv::new())
-- 
cgit v1.2.3


From ad085a20bc257d03a52708d920cfc65f0e9051e6 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 9 Feb 2020 22:07:03 +0000
Subject: Remove all types from Value

---
 dhall/src/semantics/nze/env.rs   |  3 +-
 dhall/src/semantics/nze/value.rs | 80 ++++------------------------------------
 2 files changed, 9 insertions(+), 74 deletions(-)

(limited to 'dhall/src/semantics/nze')

diff --git a/dhall/src/semantics/nze/env.rs b/dhall/src/semantics/nze/env.rs
index 261e0b6..ff52343 100644
--- a/dhall/src/semantics/nze/env.rs
+++ b/dhall/src/semantics/nze/env.rs
@@ -60,7 +60,8 @@ impl NzEnv {
         env
     }
     pub fn insert_value_noty(&self, e: Value) -> Self {
-        let ty = e.get_type_not_sort();
+        // TODO
+        let ty = Value::const_sort();
         self.insert_value(e, ty)
     }
     pub fn lookup_val(&self, var: &AlphaVar) -> ValueKind {
diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs
index 48acdb5..5a7b558 100644
--- a/dhall/src/semantics/nze/value.rs
+++ b/dhall/src/semantics/nze/value.rs
@@ -1,7 +1,7 @@
 use std::collections::HashMap;
 use std::rc::Rc;
 
-use crate::error::{TypeError, TypeMessage};
+use crate::error::TypeError;
 use crate::semantics::nze::lazy;
 use crate::semantics::{
     apply_any, normalize_hir_whnf, normalize_one_layer, squash_textlit,
@@ -25,8 +25,6 @@ pub(crate) struct Value(Rc<ValueInternal>);
 #[derive(Debug)]
 struct ValueInternal {
     kind: lazy::Lazy<Thunk, ValueKind>,
-    /// This is None if and only if `form` is `Sort` (which doesn't have a type)
-    ty: Option<Value>,
     span: Span,
 }
 
@@ -103,25 +101,12 @@ pub(crate) enum ValueKind {
 
 impl Value {
     pub(crate) fn const_sort() -> Value {
-        ValueInternal::from_whnf(
-            ValueKind::Const(Const::Sort),
-            None,
-            Span::Artificial,
-        )
-        .into_value()
-    }
-    pub(crate) fn const_kind() -> Value {
-        Value::from_const(Const::Kind)
+        Value::from_const(Const::Sort)
     }
     /// Construct a Value from a completely unnormalized expression.
     pub(crate) fn new_thunk(env: &NzEnv, hir: Hir) -> Value {
         let span = hir.span();
-        ValueInternal::from_thunk(
-            Thunk::new(env, hir),
-            Some(Value::const_kind()),
-            span,
-        )
-        .into_value()
+        ValueInternal::from_thunk(Thunk::new(env, hir), span).into_value()
     }
     /// Construct a Value from a partially normalized expression that's not in WHNF.
     pub(crate) fn from_partial_expr(e: ExprKind<Value, Normalized>) -> Value {
@@ -129,33 +114,17 @@ impl Value {
         let env = NzEnv::new();
         ValueInternal::from_thunk(
             Thunk::from_partial_expr(env, e),
-            Some(Value::const_kind()),
             Span::Artificial,
         )
         .into_value()
     }
     /// Make a Value from a ValueKind
     pub(crate) fn from_kind(v: ValueKind) -> Value {
-        ValueInternal::from_whnf(v, Some(Value::const_kind()), Span::Artificial)
-            .into_value()
+        ValueInternal::from_whnf(v, Span::Artificial).into_value()
     }
     pub(crate) fn from_const(c: Const) -> Self {
         let v = ValueKind::Const(c);
-        match c {
-            Const::Type => ValueInternal::from_whnf(
-                v,
-                Some(Value::from_const(Const::Kind)),
-                Span::Artificial,
-            )
-            .into_value(),
-            Const::Kind => ValueInternal::from_whnf(
-                v,
-                Some(Value::const_sort()),
-                Span::Artificial,
-            )
-            .into_value(),
-            Const::Sort => Value::const_sort(),
-        }
+        ValueInternal::from_whnf(v, Span::Artificial).into_value()
     }
     pub(crate) fn from_builtin(b: Builtin) -> Self {
         Self::from_builtin_env(b, &NzEnv::new())
@@ -193,16 +162,6 @@ impl Value {
         self.to_hir(env.as_varenv()).to_expr_tyenv(env)
     }
 
-    /// Normalizes contents to normal form; faster than `normalize` if
-    /// no one else shares this.
-    pub(crate) fn normalize_mut(&mut self) {
-        match Rc::get_mut(&mut self.0) {
-            // Mutate directly if sole owner
-            Some(vint) => vint.normalize_mut(),
-            // Otherwise mutate through the refcell
-            None => self.normalize(),
-        }
-    }
     pub(crate) fn normalize(&self) {
         self.0.normalize()
     }
@@ -214,13 +173,6 @@ impl Value {
     pub(crate) fn get_type(&self, tyenv: &TyEnv) -> Result<Value, TypeError> {
         self.to_tyexpr_tyenv(tyenv).get_type()
     }
-    /// When we know the value isn't `Sort`, this gets the type directly
-    pub(crate) fn get_type_not_sort(&self) -> Value {
-        self.0
-            .get_type()
-            .expect("Internal type error: value is `Sort` but shouldn't be")
-            .clone()
-    }
 
     pub fn to_hir(&self, venv: VarEnv) -> Hir {
         let map_uniontype = |kts: &HashMap<Label, Option<Value>>| {
@@ -340,17 +292,15 @@ impl Value {
 }
 
 impl ValueInternal {
-    fn from_whnf(k: ValueKind, ty: Option<Value>, span: Span) -> Self {
+    fn from_whnf(k: ValueKind, span: Span) -> Self {
         ValueInternal {
             kind: lazy::Lazy::new_completed(k),
-            ty,
             span,
         }
     }
-    fn from_thunk(th: Thunk, ty: Option<Value>, span: Span) -> Self {
+    fn from_thunk(th: Thunk, span: Span) -> Self {
         ValueInternal {
             kind: lazy::Lazy::new(th),
-            ty,
             span,
         }
     }
@@ -364,17 +314,6 @@ impl ValueInternal {
     fn normalize(&self) {
         self.kind().normalize();
     }
-    // TODO: deprecated
-    fn normalize_mut(&mut self) {
-        self.normalize();
-    }
-
-    fn get_type(&self) -> Result<&Value, TypeError> {
-        match &self.ty {
-            Some(t) => Ok(t),
-            None => Err(TypeError::new(TypeMessage::Sort)),
-        }
-    }
 }
 
 impl ValueKind {
@@ -616,11 +555,6 @@ impl std::fmt::Debug for Value {
         }
         let mut x = fmt.debug_struct(&format!("Value@WHNF"));
         x.field("kind", kind);
-        if let Some(ty) = vint.ty.as_ref() {
-            x.field("type", &ty);
-        } else {
-            x.field("type", &None::<()>);
-        }
         x.finish()
     }
 }
-- 
cgit v1.2.3


From 35cc98dc767247f4881866de40c7d8dd82eba8a5 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 9 Feb 2020 22:30:32 +0000
Subject: Remove types from NzEnv

---
 dhall/src/semantics/nze/env.rs       | 42 +++++++++++++++++++++---------------
 dhall/src/semantics/nze/normalize.rs |  2 +-
 dhall/src/semantics/nze/value.rs     | 18 ++++++----------
 3 files changed, 32 insertions(+), 30 deletions(-)

(limited to 'dhall/src/semantics/nze')

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(),
         }
-- 
cgit v1.2.3


From c3ed75dc4b354becac0821e4288105dc2a300c4c Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Mon, 10 Feb 2020 19:14:07 +0000
Subject: Remove need for Embed

This was an archaic leftover from copying the Haskell datatypes anyway
---
 dhall/src/semantics/nze/env.rs | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'dhall/src/semantics/nze')

diff --git a/dhall/src/semantics/nze/env.rs b/dhall/src/semantics/nze/env.rs
index 5b036f0..241af40 100644
--- a/dhall/src/semantics/nze/env.rs
+++ b/dhall/src/semantics/nze/env.rs
@@ -86,3 +86,9 @@ impl<Type: Clone> ValEnv<Type> {
         }
     }
 }
+
+impl<'a> From<&'a NzEnv> for NzEnv {
+    fn from(x: &'a NzEnv) -> Self {
+        x.clone()
+    }
+}
-- 
cgit v1.2.3


From 5a2538d174fd36a8ed7f4fa344b9583fc48bd977 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 11 Feb 2020 13:12:13 +0000
Subject: Remove the Embed variant from ExprKind

---
 dhall/src/semantics/nze/normalize.rs |  6 ++----
 dhall/src/semantics/nze/value.rs     | 16 +++++-----------
 2 files changed, 7 insertions(+), 15 deletions(-)

(limited to 'dhall/src/semantics/nze')

diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs
index d12146a..03b91a5 100644
--- a/dhall/src/semantics/nze/normalize.rs
+++ b/dhall/src/semantics/nze/normalize.rs
@@ -6,7 +6,6 @@ use crate::semantics::{
     Binder, BuiltinClosure, Closure, Hir, HirKind, TextLit, Value, ValueKind,
 };
 use crate::syntax::{BinOp, Builtin, ExprKind, InterpolatedTextContents};
-use crate::Normalized;
 
 pub(crate) fn apply_any(f: Value, a: Value) -> ValueKind {
     match f.kind() {
@@ -90,7 +89,7 @@ enum Ret<'a> {
     ValueKind(ValueKind),
     Value(Value),
     ValueRef(&'a Value),
-    Expr(ExprKind<Value, Normalized>),
+    Expr(ExprKind<Value>),
 }
 
 fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option<Ret<'a>> {
@@ -215,7 +214,7 @@ fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option<Ret<'a>> {
 }
 
 pub(crate) fn normalize_one_layer(
-    expr: ExprKind<Value, Normalized>,
+    expr: ExprKind<Value>,
     env: &NzEnv,
 ) -> ValueKind {
     use ValueKind::{
@@ -233,7 +232,6 @@ pub(crate) fn normalize_one_layer(
         ExprKind::Lam(..)
         | ExprKind::Pi(..)
         | ExprKind::Let(..)
-        | ExprKind::Embed(_)
         | ExprKind::Var(_) => {
             unreachable!("This case should have been handled in typecheck")
         }
diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs
index a60be9d..0df3c74 100644
--- a/dhall/src/semantics/nze/value.rs
+++ b/dhall/src/semantics/nze/value.rs
@@ -12,7 +12,7 @@ use crate::syntax::{
     BinOp, Builtin, Const, ExprKind, Integer, InterpolatedTextContents, Label,
     NaiveDouble, Natural, Span,
 };
-use crate::{Normalized, NormalizedExpr, ToExprOptions};
+use crate::{NormalizedExpr, ToExprOptions};
 
 /// Stores a possibly unevaluated value. Gets (partially) normalized on-demand, sharing computation
 /// automatically. Uses a Rc<RefCell> to share computation.
@@ -34,10 +34,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, Normalized>,
-    },
+    PartialExpr { env: NzEnv, expr: ExprKind<Value> },
 }
 
 /// An unevaluated subexpression that takes an argument.
@@ -96,7 +93,7 @@ pub(crate) enum ValueKind {
     TextLit(TextLit),
     Equivalence(Value, Value),
     /// Invariant: evaluation must not be able to progress with `normalize_one_layer`?
-    PartialExpr(ExprKind<Value, Normalized>),
+    PartialExpr(ExprKind<Value>),
 }
 
 impl Value {
@@ -106,7 +103,7 @@ impl Value {
         ValueInternal::from_thunk(Thunk::new(env, hir), span).into_value()
     }
     /// Construct a Value from a partially normalized expression that's not in WHNF.
-    pub(crate) fn from_partial_expr(e: ExprKind<Value, Normalized>) -> Value {
+    pub(crate) fn from_partial_expr(e: ExprKind<Value>) -> Value {
         // TODO: env
         let env = NzEnv::new();
         ValueInternal::from_thunk(
@@ -389,10 +386,7 @@ impl Thunk {
     fn new(env: NzEnv, body: Hir) -> Self {
         Thunk::Thunk { env, body }
     }
-    fn from_partial_expr(
-        env: NzEnv,
-        expr: ExprKind<Value, Normalized>,
-    ) -> Self {
+    fn from_partial_expr(env: NzEnv, expr: ExprKind<Value>) -> Self {
         Thunk::PartialExpr { env, expr }
     }
     fn eval(self) -> ValueKind {
-- 
cgit v1.2.3


From 40bee3cdcb9ac0c76996feeceb6ca160a6bd8b42 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 11 Feb 2020 19:04:44 +0000
Subject: Introduce LitKind to factor out common enum nodes

---
 dhall/src/semantics/nze/normalize.rs | 86 +++++++++++++++++++-----------------
 dhall/src/semantics/nze/value.rs     | 21 +++------
 2 files changed, 50 insertions(+), 57 deletions(-)

(limited to 'dhall/src/semantics/nze')

diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs
index 03b91a5..4111190 100644
--- a/dhall/src/semantics/nze/normalize.rs
+++ b/dhall/src/semantics/nze/normalize.rs
@@ -5,7 +5,9 @@ use crate::semantics::NzEnv;
 use crate::semantics::{
     Binder, BuiltinClosure, Closure, Hir, HirKind, TextLit, Value, ValueKind,
 };
-use crate::syntax::{BinOp, Builtin, ExprKind, InterpolatedTextContents};
+use crate::syntax::{
+    BinOp, Builtin, ExprKind, InterpolatedTextContents, LitKind,
+};
 
 pub(crate) fn apply_any(f: Value, a: Value) -> ValueKind {
     match f.kind() {
@@ -98,40 +100,44 @@ fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option<Ret<'a>> {
         NaturalTimes, RecursiveRecordMerge, RecursiveRecordTypeMerge,
         RightBiasedRecordMerge, TextAppend,
     };
-    use ValueKind::{
-        BoolLit, EmptyListLit, NEListLit, NaturalLit, RecordLit, RecordType,
-    };
+    use LitKind::{Bool, Natural};
+    use ValueKind::{EmptyListLit, Lit, NEListLit, RecordLit, RecordType};
+
     Some(match (o, x.kind(), y.kind()) {
-        (BoolAnd, BoolLit(true), _) => Ret::ValueRef(y),
-        (BoolAnd, _, BoolLit(true)) => Ret::ValueRef(x),
-        (BoolAnd, BoolLit(false), _) => Ret::ValueKind(BoolLit(false)),
-        (BoolAnd, _, BoolLit(false)) => Ret::ValueKind(BoolLit(false)),
+        (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, BoolLit(true), _) => Ret::ValueKind(BoolLit(true)),
-        (BoolOr, _, BoolLit(true)) => Ret::ValueKind(BoolLit(true)),
-        (BoolOr, BoolLit(false), _) => Ret::ValueRef(y),
-        (BoolOr, _, BoolLit(false)) => 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, BoolLit(true), _) => Ret::ValueRef(y),
-        (BoolEQ, _, BoolLit(true)) => Ret::ValueRef(x),
-        (BoolEQ, BoolLit(x), BoolLit(y)) => Ret::ValueKind(BoolLit(x == y)),
-        (BoolEQ, _, _) if x == y => Ret::ValueKind(BoolLit(true)),
-        (BoolNE, BoolLit(false), _) => Ret::ValueRef(y),
-        (BoolNE, _, BoolLit(false)) => Ret::ValueRef(x),
-        (BoolNE, BoolLit(x), BoolLit(y)) => Ret::ValueKind(BoolLit(x != y)),
-        (BoolNE, _, _) if x == y => Ret::ValueKind(BoolLit(false)),
+        (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))),
 
-        (NaturalPlus, NaturalLit(0), _) => Ret::ValueRef(y),
-        (NaturalPlus, _, NaturalLit(0)) => Ret::ValueRef(x),
-        (NaturalPlus, NaturalLit(x), NaturalLit(y)) => {
-            Ret::ValueKind(NaturalLit(x + y))
-        }
-        (NaturalTimes, NaturalLit(0), _) => Ret::ValueKind(NaturalLit(0)),
-        (NaturalTimes, _, NaturalLit(0)) => Ret::ValueKind(NaturalLit(0)),
-        (NaturalTimes, NaturalLit(1), _) => Ret::ValueRef(y),
-        (NaturalTimes, _, NaturalLit(1)) => Ret::ValueRef(x),
-        (NaturalTimes, NaturalLit(x), NaturalLit(y)) => {
-            Ret::ValueKind(NaturalLit(x * y))
+        (NaturalPlus, Lit(Natural(0)), _) => Ret::ValueRef(y),
+        (NaturalPlus, _, Lit(Natural(0))) => Ret::ValueRef(x),
+        (NaturalPlus, Lit(Natural(x)), Lit(Natural(y))) => {
+            Ret::ValueKind(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(x)), Lit(Natural(y))) => {
+            Ret::ValueKind(Lit(Natural(x * y)))
         }
 
         (ListAppend, EmptyListLit(_), _) => Ret::ValueRef(y),
@@ -217,10 +223,11 @@ pub(crate) fn normalize_one_layer(
     expr: ExprKind<Value>,
     env: &NzEnv,
 ) -> ValueKind {
+    use LitKind::Bool;
     use ValueKind::{
-        BoolLit, DoubleLit, EmptyListLit, EmptyOptionalLit, IntegerLit,
-        NEListLit, NEOptionalLit, NaturalLit, PartialExpr, RecordLit,
-        RecordType, UnionConstructor, UnionLit, UnionType,
+        EmptyListLit, EmptyOptionalLit, Lit, NEListLit, NEOptionalLit,
+        PartialExpr, RecordLit, RecordType, UnionConstructor, UnionLit,
+        UnionType,
     };
 
     let ret = match expr {
@@ -240,10 +247,7 @@ pub(crate) fn normalize_one_layer(
         ExprKind::Builtin(b) => Ret::Value(Value::from_builtin_env(b, env)),
         ExprKind::Assert(_) => Ret::Expr(expr),
         ExprKind::App(v, a) => Ret::Value(v.app(a)),
-        ExprKind::BoolLit(b) => Ret::ValueKind(BoolLit(b)),
-        ExprKind::NaturalLit(n) => Ret::ValueKind(NaturalLit(n)),
-        ExprKind::IntegerLit(n) => Ret::ValueKind(IntegerLit(n)),
-        ExprKind::DoubleLit(n) => Ret::ValueKind(DoubleLit(n)),
+        ExprKind::Lit(l) => Ret::ValueKind(Lit(l.clone())),
         ExprKind::SomeLit(e) => Ret::ValueKind(NEOptionalLit(e)),
         ExprKind::EmptyListLit(t) => {
             let arg = match t.kind() {
@@ -279,12 +283,12 @@ pub(crate) fn normalize_one_layer(
         }
         ExprKind::BoolIf(ref b, ref e1, ref e2) => {
             match b.kind() {
-                BoolLit(true) => Ret::ValueRef(e1),
-                BoolLit(false) => Ret::ValueRef(e2),
+                Lit(Bool(true)) => Ret::ValueRef(e1),
+                Lit(Bool(false)) => Ret::ValueRef(e2),
                 _ => {
                     match (e1.kind(), e2.kind()) {
                         // Simplify `if b then True else False`
-                        (BoolLit(true), BoolLit(false)) => Ret::ValueRef(b),
+                        (Lit(Bool(true)), Lit(Bool(false))) => Ret::ValueRef(b),
                         _ if e1 == e2 => Ret::ValueRef(e1),
                         _ => Ret::Expr(expr),
                     }
diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs
index 0df3c74..2ae6852 100644
--- a/dhall/src/semantics/nze/value.rs
+++ b/dhall/src/semantics/nze/value.rs
@@ -9,8 +9,8 @@ use crate::semantics::{
     TyExpr, VarEnv,
 };
 use crate::syntax::{
-    BinOp, Builtin, Const, ExprKind, Integer, InterpolatedTextContents, Label,
-    NaiveDouble, Natural, Span,
+    BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, Label, LitKind,
+    Span,
 };
 use crate::{NormalizedExpr, ToExprOptions};
 
@@ -76,10 +76,7 @@ pub(crate) enum ValueKind {
 
     Var(NzVar),
     Const(Const),
-    BoolLit(bool),
-    NaturalLit(Natural),
-    IntegerLit(Integer),
-    DoubleLit(NaiveDouble),
+    Lit(LitKind),
     EmptyOptionalLit(Value),
     NEOptionalLit(Value),
     // EmptyListLit(t) means `[] : List t`, not `[] : t`
@@ -205,10 +202,7 @@ impl Value {
                     closure.to_hir(venv),
                 ),
                 ValueKind::Const(c) => ExprKind::Const(*c),
-                ValueKind::BoolLit(b) => ExprKind::BoolLit(*b),
-                ValueKind::NaturalLit(n) => ExprKind::NaturalLit(*n),
-                ValueKind::IntegerLit(n) => ExprKind::IntegerLit(*n),
-                ValueKind::DoubleLit(n) => ExprKind::DoubleLit(*n),
+                ValueKind::Lit(l) => ExprKind::Lit(l.clone()),
                 ValueKind::EmptyOptionalLit(n) => ExprKind::App(
                     Value::from_builtin(Builtin::OptionalNone).to_hir(venv),
                     n.to_hir(venv),
@@ -317,12 +311,7 @@ impl ValueKind {
 
     pub(crate) fn normalize(&self) {
         match self {
-            ValueKind::Var(..)
-            | ValueKind::Const(_)
-            | ValueKind::BoolLit(_)
-            | ValueKind::NaturalLit(_)
-            | ValueKind::IntegerLit(_)
-            | ValueKind::DoubleLit(_) => {}
+            ValueKind::Var(..) | ValueKind::Const(_) | ValueKind::Lit(_) => {}
 
             ValueKind::EmptyOptionalLit(tth) | ValueKind::EmptyListLit(tth) => {
                 tth.normalize();
-- 
cgit v1.2.3


From f29a40fb55b898b3a3cc51f198e8522eaecf0777 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Thu, 13 Feb 2020 20:17:41 +0000
Subject: Simplify conversions to/from TyExpr

---
 dhall/src/semantics/nze/value.rs | 20 +++-----------------
 1 file changed, 3 insertions(+), 17 deletions(-)

(limited to 'dhall/src/semantics/nze')

diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs
index 2ae6852..0603fb5 100644
--- a/dhall/src/semantics/nze/value.rs
+++ b/dhall/src/semantics/nze/value.rs
@@ -1,12 +1,10 @@
 use std::collections::HashMap;
 use std::rc::Rc;
 
-use crate::error::TypeError;
 use crate::semantics::nze::lazy;
 use crate::semantics::{
-    apply_any, normalize_hir_whnf, normalize_one_layer, squash_textlit,
-    type_with, Binder, BuiltinClosure, Hir, HirKind, NzEnv, NzVar, TyEnv,
-    TyExpr, VarEnv,
+    apply_any, normalize_hir_whnf, normalize_one_layer, squash_textlit, Binder,
+    BuiltinClosure, Hir, HirKind, NzEnv, NzVar, TyEnv, VarEnv,
 };
 use crate::syntax::{
     BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, Label, LitKind,
@@ -146,8 +144,7 @@ impl Value {
         if opts.normalize {
             self.normalize();
         }
-
-        self.to_tyexpr_noenv().to_expr(opts)
+        self.to_hir_noenv().to_expr(opts)
     }
     pub(crate) fn to_expr_tyenv(&self, tyenv: &TyEnv) -> NormalizedExpr {
         self.to_hir(tyenv.as_varenv()).to_expr_tyenv(tyenv)
@@ -161,10 +158,6 @@ impl Value {
         Value::from_kind(apply_any(self.clone(), v))
     }
 
-    pub(crate) fn get_type(&self, tyenv: &TyEnv) -> Result<Value, TypeError> {
-        self.to_tyexpr_tyenv(tyenv).get_type()
-    }
-
     pub fn to_hir(&self, venv: VarEnv) -> Hir {
         let map_uniontype = |kts: &HashMap<Label, Option<Value>>| {
             ExprKind::UnionType(
@@ -270,13 +263,6 @@ impl Value {
     pub fn to_hir_noenv(&self) -> Hir {
         self.to_hir(VarEnv::new())
     }
-    pub fn to_tyexpr_tyenv(&self, tyenv: &TyEnv) -> TyExpr {
-        let hir = self.to_hir(tyenv.as_varenv());
-        type_with(tyenv, &hir).unwrap()
-    }
-    pub fn to_tyexpr_noenv(&self) -> TyExpr {
-        self.to_tyexpr_tyenv(&TyEnv::new())
-    }
 }
 
 impl ValueInternal {
-- 
cgit v1.2.3


From d65d639ff93691adbf0a208edb99736003bc64bd Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sat, 15 Feb 2020 19:05:26 +0000
Subject: Factor some tck code to avoid needing get_type_tyexpr

---
 dhall/src/semantics/nze/normalize.rs | 2 +-
 dhall/src/semantics/nze/value.rs     | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'dhall/src/semantics/nze')

diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs
index 4111190..c8dd5ae 100644
--- a/dhall/src/semantics/nze/normalize.rs
+++ b/dhall/src/semantics/nze/normalize.rs
@@ -475,7 +475,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(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 0603fb5..3a5b5b5 100644
--- a/dhall/src/semantics/nze/value.rs
+++ b/dhall/src/semantics/nze/value.rs
@@ -87,7 +87,7 @@ pub(crate) enum ValueKind {
     UnionLit(Label, Value, HashMap<Label, Option<Value>>),
     TextLit(TextLit),
     Equivalence(Value, Value),
-    /// Invariant: evaluation must not be able to progress with `normalize_one_layer`?
+    /// Invariant: evaluation must not be able to progress with `normalize_one_layer`.
     PartialExpr(ExprKind<Value>),
 }
 
@@ -387,7 +387,7 @@ impl Closure {
     pub fn apply(&self, val: Value) -> Value {
         match self {
             Closure::Closure { env, body, .. } => {
-                body.eval(&env.insert_value(val, ()))
+                body.eval(env.insert_value(val, ()))
             }
             Closure::ConstantClosure { body, .. } => body.clone(),
         }
-- 
cgit v1.2.3


From 5057144ed99bc4e1a76a0840dd39fc1bd862665c Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sat, 15 Feb 2020 19:10:52 +0000
Subject: Desugar Completion during resolution

---
 dhall/src/semantics/nze/normalize.rs | 20 +++++++++-----------
 1 file changed, 9 insertions(+), 11 deletions(-)

(limited to 'dhall/src/semantics/nze')

diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs
index c8dd5ae..0e09511 100644
--- a/dhall/src/semantics/nze/normalize.rs
+++ b/dhall/src/semantics/nze/normalize.rs
@@ -231,17 +231,16 @@ pub(crate) fn normalize_one_layer(
     };
 
     let ret = match expr {
-        ExprKind::Import(_) => unreachable!(
-            "There should remain no imports in a resolved expression"
-        ),
-        // Those cases have already been completely handled in the typechecking phase (using
-        // `RetWhole`), so they won't appear here.
-        ExprKind::Lam(..)
-        | ExprKind::Pi(..)
-        | ExprKind::Let(..)
-        | ExprKind::Var(_) => {
-            unreachable!("This case should have been handled in typecheck")
+        ExprKind::Import(..) | ExprKind::Completion(..) => {
+            unreachable!("This case should have been handled in resolution")
         }
+        ExprKind::Var(..)
+        | ExprKind::Lam(..)
+        | ExprKind::Pi(..)
+        | ExprKind::Let(..) => unreachable!(
+            "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)),
@@ -391,7 +390,6 @@ pub(crate) fn normalize_one_layer(
         ExprKind::ProjectionByExpr(_, _) => {
             unimplemented!("selection by expression")
         }
-        ExprKind::Completion(_, _) => unimplemented!("record completion"),
 
         ExprKind::Merge(ref handlers, ref variant, _) => {
             match handlers.kind() {
-- 
cgit v1.2.3


From aa867b21f57f9bef2ec2b9d8450736f9111189ee Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sat, 15 Feb 2020 19:44:40 +0000
Subject: Introduce proper Type struct

---
 dhall/src/semantics/nze/value.rs | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'dhall/src/semantics/nze')

diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs
index 3a5b5b5..f31fd6c 100644
--- a/dhall/src/semantics/nze/value.rs
+++ b/dhall/src/semantics/nze/value.rs
@@ -4,7 +4,7 @@ use std::rc::Rc;
 use crate::semantics::nze::lazy;
 use crate::semantics::{
     apply_any, normalize_hir_whnf, normalize_one_layer, squash_textlit, Binder,
-    BuiltinClosure, Hir, HirKind, NzEnv, NzVar, TyEnv, VarEnv,
+    BuiltinClosure, Hir, HirKind, NzEnv, NzVar, TyEnv, Type, VarEnv,
 };
 use crate::syntax::{
     BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, Label, LitKind,
@@ -139,6 +139,9 @@ impl Value {
         self.0.kind()
     }
 
+    pub(crate) fn to_type(&self) -> Type {
+        self.clone().into()
+    }
     /// Converts a value back to the corresponding AST expression.
     pub(crate) fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr {
         if opts.normalize {
-- 
cgit v1.2.3


From 130de8cea49c848a06174c61c747d9414a5c71b7 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 16 Feb 2020 19:06:23 +0000
Subject: Start requiring Universe to build a Type

---
 dhall/src/semantics/nze/normalize.rs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dhall/src/semantics/nze')

diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs
index 0e09511..c2d2dc2 100644
--- a/dhall/src/semantics/nze/normalize.rs
+++ b/dhall/src/semantics/nze/normalize.rs
@@ -471,7 +471,7 @@ pub(crate) fn normalize_hir_whnf(env: &NzEnv, hir: &Hir) -> ValueKind {
                 closure: Closure::new(env, body.clone()),
             }
         }
-        HirKind::Expr(ExprKind::Let(_, None, val, body)) => {
+        HirKind::Expr(ExprKind::Let(_, _, val, body)) => {
             let val = val.eval(env);
             body.eval(env.insert_value(val, ())).kind().clone()
         }
-- 
cgit v1.2.3


From c451c18103b871e563b12c524bc3feec5451154c Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 16 Feb 2020 19:48:35 +0000
Subject: Avoid recomputing universes in tck

---
 dhall/src/semantics/nze/value.rs | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'dhall/src/semantics/nze')

diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs
index f31fd6c..7084af6 100644
--- a/dhall/src/semantics/nze/value.rs
+++ b/dhall/src/semantics/nze/value.rs
@@ -4,7 +4,7 @@ use std::rc::Rc;
 use crate::semantics::nze::lazy;
 use crate::semantics::{
     apply_any, normalize_hir_whnf, normalize_one_layer, squash_textlit, Binder,
-    BuiltinClosure, Hir, HirKind, NzEnv, NzVar, TyEnv, Type, VarEnv,
+    BuiltinClosure, Hir, HirKind, NzEnv, NzVar, TyEnv, Type, Universe, VarEnv,
 };
 use crate::syntax::{
     BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, Label, LitKind,
@@ -139,8 +139,8 @@ impl Value {
         self.0.kind()
     }
 
-    pub(crate) fn to_type(&self) -> Type {
-        self.clone().into()
+    pub(crate) fn to_type(&self, u: impl Into<Universe>) -> Type {
+        Type::new(self.clone(), u.into())
     }
     /// Converts a value back to the corresponding AST expression.
     pub(crate) fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr {
-- 
cgit v1.2.3


From cd5e172002ce724be7bdd52883e121efa8817f20 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Mon, 17 Feb 2020 18:22:06 +0000
Subject: Rename Value to Nir

---
 dhall/src/semantics/nze/env.rs       |  10 +-
 dhall/src/semantics/nze/mod.rs       |   4 +-
 dhall/src/semantics/nze/nir.rs       | 521 ++++++++++++++++++++++++++++++++++
 dhall/src/semantics/nze/normalize.rs | 243 ++++++++--------
 dhall/src/semantics/nze/value.rs     | 526 -----------------------------------
 dhall/src/semantics/nze/var.rs       |   2 +-
 6 files changed, 644 insertions(+), 662 deletions(-)
 create mode 100644 dhall/src/semantics/nze/nir.rs
 delete mode 100644 dhall/src/semantics/nze/value.rs

(limited to 'dhall/src/semantics/nze')

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/nir.rs b/dhall/src/semantics/nze/nir.rs
new file mode 100644
index 0000000..a6dafa2
--- /dev/null
+++ b/dhall/src/semantics/nze/nir.rs
@@ -0,0 +1,521 @@
+use std::collections::HashMap;
+use std::rc::Rc;
+
+use crate::semantics::nze::lazy;
+use crate::semantics::{
+    apply_any, normalize_hir_whnf, normalize_one_layer, squash_textlit, Binder,
+    BuiltinClosure, Hir, HirKind, NzEnv, NzVar, TyEnv, Type, Universe, VarEnv,
+};
+use crate::syntax::{
+    BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, Label, LitKind,
+    Span,
+};
+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 `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 Nir(Rc<NirInternal>);
+
+#[derive(Debug)]
+struct NirInternal {
+    kind: lazy::Lazy<Thunk, NirKind>,
+    span: Span,
+}
+
+/// An unevaluated subexpression
+#[derive(Debug, Clone)]
+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<Nir> },
+}
+
+/// An unevaluated subexpression that takes an argument.
+#[derive(Debug, Clone)]
+pub(crate) enum Closure {
+    /// Normal closure
+    Closure { env: NzEnv, body: Hir },
+    /// Closure that ignores the argument passed
+    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<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 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 `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 NirKind {
+    /// Closures
+    LamClosure {
+        binder: Binder,
+        annot: Nir,
+        closure: Closure,
+    },
+    PiClosure {
+        binder: Binder,
+        annot: Nir,
+        closure: Closure,
+    },
+    AppliedBuiltin(BuiltinClosure<Nir>),
+
+    Var(NzVar),
+    Const(Const),
+    Lit(LitKind),
+    EmptyOptionalLit(Nir),
+    NEOptionalLit(Nir),
+    // EmptyListLit(t) means `[] : List t`, not `[] : t`
+    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(Nir, Nir),
+    /// Invariant: evaluation must not be able to progress with `normalize_one_layer`.
+    PartialExpr(ExprKind<Nir>),
+}
+
+impl Nir {
+    /// Construct a Nir from a completely unnormalized expression.
+    pub(crate) fn new_thunk(env: NzEnv, hir: Hir) -> Nir {
+        let span = hir.span();
+        NirInternal::from_thunk(Thunk::new(env, hir), span).into_nir()
+    }
+    /// 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();
+        NirInternal::from_thunk(
+            Thunk::from_partial_expr(env, e),
+            Span::Artificial,
+        )
+        .into_nir()
+    }
+    /// 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 = 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 {
+        Nir::from_kind(NirKind::from_builtin_env(b, env.clone()))
+    }
+    pub(crate) fn from_text(txt: impl ToString) -> Self {
+        Nir::from_kind(NirKind::TextLit(TextLit::from_text(txt.to_string())))
+    }
+
+    pub(crate) fn as_const(&self) -> Option<Const> {
+        match &*self.kind() {
+            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) -> &NirKind {
+        self.0.kind()
+    }
+
+    pub(crate) fn to_type(&self, u: impl Into<Universe>) -> Type {
+        Type::new(self.clone(), u.into())
+    }
+    /// Converts a value back to the corresponding AST expression.
+    pub(crate) fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr {
+        if opts.normalize {
+            self.normalize();
+        }
+        self.to_hir_noenv().to_expr(opts)
+    }
+    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) {
+        self.0.normalize()
+    }
+
+    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<Nir>>| {
+            ExprKind::UnionType(
+                kts.iter()
+                    .map(|(k, v)| {
+                        (k.clone(), v.as_ref().map(|v| v.to_hir(venv)))
+                    })
+                    .collect(),
+            )
+        };
+
+        let hir = match &*self.kind() {
+            NirKind::Var(v) => HirKind::Var(venv.lookup(v)),
+            NirKind::AppliedBuiltin(closure) => closure.to_hirkind(venv),
+            self_kind => HirKind::Expr(match self_kind {
+                NirKind::Var(..) | NirKind::AppliedBuiltin(..) => {
+                    unreachable!()
+                }
+                NirKind::LamClosure {
+                    binder,
+                    annot,
+                    closure,
+                } => ExprKind::Lam(
+                    binder.to_label(),
+                    annot.to_hir(venv),
+                    closure.to_hir(venv),
+                ),
+                NirKind::PiClosure {
+                    binder,
+                    annot,
+                    closure,
+                } => ExprKind::Pi(
+                    binder.to_label(),
+                    annot.to_hir(venv),
+                    closure.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),
+                ),
+                NirKind::NEOptionalLit(n) => ExprKind::SomeLit(n.to_hir(venv)),
+                NirKind::EmptyListLit(n) => ExprKind::EmptyListLit(Hir::new(
+                    HirKind::Expr(ExprKind::App(
+                        Nir::from_builtin(Builtin::List).to_hir(venv),
+                        n.to_hir(venv),
+                    )),
+                    Span::Artificial,
+                )),
+                NirKind::NEListLit(elts) => ExprKind::NEListLit(
+                    elts.iter().map(|v| v.to_hir(venv)).collect(),
+                ),
+                NirKind::TextLit(elts) => ExprKind::TextLit(
+                    elts.iter()
+                        .map(|t| t.map_ref(|v| v.to_hir(venv)))
+                        .collect(),
+                ),
+                NirKind::RecordLit(kvs) => ExprKind::RecordLit(
+                    kvs.iter()
+                        .map(|(k, v)| (k.clone(), v.to_hir(venv)))
+                        .collect(),
+                ),
+                NirKind::RecordType(kts) => ExprKind::RecordType(
+                    kts.iter()
+                        .map(|(k, v)| (k.clone(), v.to_hir(venv)))
+                        .collect(),
+                ),
+                NirKind::UnionType(kts) => map_uniontype(kts),
+                NirKind::UnionConstructor(l, kts) => ExprKind::Field(
+                    Hir::new(
+                        HirKind::Expr(map_uniontype(kts)),
+                        Span::Artificial,
+                    ),
+                    l.clone(),
+                ),
+                NirKind::UnionLit(l, v, kts) => ExprKind::App(
+                    Hir::new(
+                        HirKind::Expr(ExprKind::Field(
+                            Hir::new(
+                                HirKind::Expr(map_uniontype(kts)),
+                                Span::Artificial,
+                            ),
+                            l.clone(),
+                        )),
+                        Span::Artificial,
+                    ),
+                    v.to_hir(venv),
+                ),
+                NirKind::Equivalence(x, y) => ExprKind::BinOp(
+                    BinOp::Equivalence,
+                    x.to_hir(venv),
+                    y.to_hir(venv),
+                ),
+                NirKind::PartialExpr(e) => e.map_ref(|v| v.to_hir(venv)),
+            }),
+        };
+
+        Hir::new(hir, self.0.span.clone())
+    }
+    pub fn to_hir_noenv(&self) -> Hir {
+        self.to_hir(VarEnv::new())
+    }
+}
+
+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 {
+        NirInternal {
+            kind: lazy::Lazy::new(th),
+            span,
+        }
+    }
+    fn into_nir(self) -> Nir {
+        Nir(Rc::new(self))
+    }
+
+    fn kind(&self) -> &NirKind {
+        &self.kind
+    }
+    fn normalize(&self) {
+        self.kind().normalize();
+    }
+}
+
+impl NirKind {
+    pub(crate) fn into_nir(self) -> Nir {
+        Nir::from_kind(self)
+    }
+
+    pub(crate) fn normalize(&self) {
+        match self {
+            NirKind::Var(..) | NirKind::Const(_) | NirKind::Lit(_) => {}
+
+            NirKind::EmptyOptionalLit(tth) | NirKind::EmptyListLit(tth) => {
+                tth.normalize();
+            }
+
+            NirKind::NEOptionalLit(th) => {
+                th.normalize();
+            }
+            NirKind::LamClosure { annot, closure, .. }
+            | NirKind::PiClosure { annot, closure, .. } => {
+                annot.normalize();
+                closure.normalize();
+            }
+            NirKind::AppliedBuiltin(closure) => closure.normalize(),
+            NirKind::NEListLit(elts) => {
+                for x in elts.iter() {
+                    x.normalize();
+                }
+            }
+            NirKind::RecordLit(kvs) => {
+                for x in kvs.values() {
+                    x.normalize();
+                }
+            }
+            NirKind::RecordType(kvs) => {
+                for x in kvs.values() {
+                    x.normalize();
+                }
+            }
+            NirKind::UnionType(kts) | NirKind::UnionConstructor(_, kts) => {
+                for x in kts.values().flat_map(|opt| opt) {
+                    x.normalize();
+                }
+            }
+            NirKind::UnionLit(_, v, kts) => {
+                v.normalize();
+                for x in kts.values().flat_map(|opt| opt) {
+                    x.normalize();
+                }
+            }
+            NirKind::TextLit(tlit) => tlit.normalize(),
+            NirKind::Equivalence(x, y) => {
+                x.normalize();
+                y.normalize();
+            }
+            NirKind::PartialExpr(e) => {
+                e.map_ref(Nir::normalize);
+            }
+        }
+    }
+
+    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) -> NirKind {
+        NirKind::AppliedBuiltin(BuiltinClosure::new(b, env))
+    }
+}
+
+impl Thunk {
+    fn new(env: NzEnv, body: Hir) -> Self {
+        Thunk::Thunk { env, body }
+    }
+    fn from_partial_expr(env: NzEnv, expr: ExprKind<Nir>) -> Self {
+        Thunk::PartialExpr { env, expr }
+    }
+    fn eval(self) -> NirKind {
+        match self {
+            Thunk::Thunk { env, body } => normalize_hir_whnf(&env, &body),
+            Thunk::PartialExpr { env, expr } => normalize_one_layer(expr, &env),
+        }
+    }
+}
+
+impl Closure {
+    pub fn new(env: &NzEnv, body: Hir) -> Self {
+        Closure::Closure {
+            env: env.clone(),
+            body,
+        }
+    }
+    /// New closure that ignores its argument
+    pub fn new_constant(body: Nir) -> Self {
+        Closure::ConstantClosure { body }
+    }
+
+    pub fn apply(&self, val: Nir) -> Nir {
+        match self {
+            Closure::Closure { env, body, .. } => {
+                body.eval(env.insert_value(val, ()))
+            }
+            Closure::ConstantClosure { body, .. } => body.clone(),
+        }
+    }
+    fn apply_var(&self, var: NzVar) -> Nir {
+        match self {
+            Closure::Closure { .. } => {
+                self.apply(Nir::from_kind(NirKind::Var(var)))
+            }
+            Closure::ConstantClosure { body, .. } => body.clone(),
+        }
+    }
+
+    // TODO: somehow normalize the body. Might require to pass an env.
+    pub fn normalize(&self) {}
+
+    /// Convert this closure to a Hir expression
+    pub fn to_hir(&self, venv: VarEnv) -> Hir {
+        self.apply_var(NzVar::new(venv.size()))
+            .to_hir(venv.insert())
+    }
+    /// 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<Nir, ()> {
+        match self {
+            Closure::Closure { .. } => {
+                let v = NzVar::fresh();
+                // TODO: handle case where variable is used in closure
+                // TODO: return information about where the variable is used
+                Ok(self.apply_var(v))
+            }
+            Closure::ConstantClosure { body, .. } => Ok(body.clone()),
+        }
+    }
+}
+
+impl TextLit {
+    pub fn new(
+        elts: impl Iterator<Item = InterpolatedTextContents<Nir>>,
+    ) -> Self {
+        TextLit(squash_textlit(elts))
+    }
+    pub fn interpolate(v: Nir) -> TextLit {
+        TextLit(vec![InterpolatedTextContents::Expr(v)])
+    }
+    pub fn from_text(s: String) -> TextLit {
+        TextLit(vec![InterpolatedTextContents::Text(s)])
+    }
+
+    pub fn concat(&self, other: &TextLit) -> TextLit {
+        TextLit::new(self.iter().chain(other.iter()).cloned())
+    }
+    pub fn is_empty(&self) -> bool {
+        self.0.is_empty()
+    }
+    /// If the literal consists of only one interpolation and not text, return the interpolated
+    /// value.
+    pub fn as_single_expr(&self) -> Option<&Nir> {
+        use InterpolatedTextContents::Expr;
+        if let [Expr(v)] = self.0.as_slice() {
+            Some(v)
+        } else {
+            None
+        }
+    }
+    /// If there are no interpolations, return the corresponding text value.
+    pub fn as_text(&self) -> Option<String> {
+        use InterpolatedTextContents::Text;
+        if self.is_empty() {
+            Some(String::new())
+        } else if let [Text(s)] = self.0.as_slice() {
+            Some(s.clone())
+        } else {
+            None
+        }
+    }
+    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(Nir::normalize);
+        }
+    }
+}
+
+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 Nir {
+    fn eq(&self, other: &Self) -> bool {
+        Rc::ptr_eq(&self.0, &other.0) || self.kind() == other.kind()
+    }
+}
+impl std::cmp::Eq for Nir {}
+
+impl std::cmp::PartialEq for Thunk {
+    fn eq(&self, _other: &Self) -> bool {
+        unreachable!(
+            "Trying to compare thunks but we should only compare WHNFs"
+        )
+    }
+}
+impl std::cmp::Eq for Thunk {}
+
+impl std::cmp::PartialEq for Closure {
+    fn eq(&self, other: &Self) -> bool {
+        let v = NzVar::fresh();
+        self.apply_var(v) == other.apply_var(v)
+    }
+}
+impl std::cmp::Eq for Closure {}
+
+impl std::fmt::Debug for Nir {
+    fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        let vint: &NirInternal = &self.0;
+        let kind = vint.kind();
+        if let NirKind::Const(c) = kind {
+            return write!(fmt, "{:?}", c);
+        }
+        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/value.rs b/dhall/src/semantics/nze/value.rs
deleted file mode 100644
index 7084af6..0000000
--- a/dhall/src/semantics/nze/value.rs
+++ /dev/null
@@ -1,526 +0,0 @@
-use std::collections::HashMap;
-use std::rc::Rc;
-
-use crate::semantics::nze::lazy;
-use crate::semantics::{
-    apply_any, normalize_hir_whnf, normalize_one_layer, squash_textlit, Binder,
-    BuiltinClosure, Hir, HirKind, NzEnv, NzVar, TyEnv, Type, Universe, VarEnv,
-};
-use crate::syntax::{
-    BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, Label, LitKind,
-    Span,
-};
-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
-/// (renaming of bound variables) and beta-equivalence (normalization). It will recursively
-/// normalize as needed.
-#[derive(Clone)]
-pub(crate) struct Value(Rc<ValueInternal>);
-
-#[derive(Debug)]
-struct ValueInternal {
-    kind: lazy::Lazy<Thunk, ValueKind>,
-    span: Span,
-}
-
-/// An unevaluated subexpression
-#[derive(Debug, Clone)]
-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> },
-}
-
-/// An unevaluated subexpression that takes an argument.
-#[derive(Debug, Clone)]
-pub(crate) enum Closure {
-    /// Normal closure
-    Closure { env: NzEnv, body: Hir },
-    /// Closure that ignores the argument passed
-    ConstantClosure { body: Value },
-}
-
-/// 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>>);
-
-/// 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
-/// 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.
-#[derive(Debug, Clone, PartialEq, Eq)]
-pub(crate) enum ValueKind {
-    /// Closures
-    LamClosure {
-        binder: Binder,
-        annot: Value,
-        closure: Closure,
-    },
-    PiClosure {
-        binder: Binder,
-        annot: Value,
-        closure: Closure,
-    },
-    AppliedBuiltin(BuiltinClosure<Value>),
-
-    Var(NzVar),
-    Const(Const),
-    Lit(LitKind),
-    EmptyOptionalLit(Value),
-    NEOptionalLit(Value),
-    // 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>>),
-    TextLit(TextLit),
-    Equivalence(Value, Value),
-    /// Invariant: evaluation must not be able to progress with `normalize_one_layer`.
-    PartialExpr(ExprKind<Value>),
-}
-
-impl Value {
-    /// Construct a Value from a completely unnormalized expression.
-    pub(crate) fn new_thunk(env: NzEnv, hir: Hir) -> Value {
-        let span = hir.span();
-        ValueInternal::from_thunk(Thunk::new(env, hir), span).into_value()
-    }
-    /// Construct a Value from a partially normalized expression that's not in WHNF.
-    pub(crate) fn from_partial_expr(e: ExprKind<Value>) -> Value {
-        // TODO: env
-        let env = NzEnv::new();
-        ValueInternal::from_thunk(
-            Thunk::from_partial_expr(env, e),
-            Span::Artificial,
-        )
-        .into_value()
-    }
-    /// Make a Value from a ValueKind
-    pub(crate) fn from_kind(v: ValueKind) -> Value {
-        ValueInternal::from_whnf(v, Span::Artificial).into_value()
-    }
-    pub(crate) fn from_const(c: Const) -> Self {
-        let v = ValueKind::Const(c);
-        ValueInternal::from_whnf(v, Span::Artificial).into_value()
-    }
-    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()))
-    }
-    pub(crate) fn from_text(txt: impl ToString) -> Self {
-        Value::from_kind(ValueKind::TextLit(TextLit::from_text(
-            txt.to_string(),
-        )))
-    }
-
-    pub(crate) fn as_const(&self) -> Option<Const> {
-        match &*self.kind() {
-            ValueKind::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 {
-        self.0.kind()
-    }
-
-    pub(crate) fn to_type(&self, u: impl Into<Universe>) -> Type {
-        Type::new(self.clone(), u.into())
-    }
-    /// Converts a value back to the corresponding AST expression.
-    pub(crate) fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr {
-        if opts.normalize {
-            self.normalize();
-        }
-        self.to_hir_noenv().to_expr(opts)
-    }
-    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) {
-        self.0.normalize()
-    }
-
-    pub(crate) fn app(&self, v: Value) -> Value {
-        Value::from_kind(apply_any(self.clone(), v))
-    }
-
-    pub fn to_hir(&self, venv: VarEnv) -> Hir {
-        let map_uniontype = |kts: &HashMap<Label, Option<Value>>| {
-            ExprKind::UnionType(
-                kts.iter()
-                    .map(|(k, v)| {
-                        (k.clone(), v.as_ref().map(|v| v.to_hir(venv)))
-                    })
-                    .collect(),
-            )
-        };
-
-        let hir = match &*self.kind() {
-            ValueKind::Var(v) => HirKind::Var(venv.lookup(v)),
-            ValueKind::AppliedBuiltin(closure) => closure.to_hirkind(venv),
-            self_kind => HirKind::Expr(match self_kind {
-                ValueKind::Var(..) | ValueKind::AppliedBuiltin(..) => {
-                    unreachable!()
-                }
-                ValueKind::LamClosure {
-                    binder,
-                    annot,
-                    closure,
-                } => ExprKind::Lam(
-                    binder.to_label(),
-                    annot.to_hir(venv),
-                    closure.to_hir(venv),
-                ),
-                ValueKind::PiClosure {
-                    binder,
-                    annot,
-                    closure,
-                } => ExprKind::Pi(
-                    binder.to_label(),
-                    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),
-                    n.to_hir(venv),
-                ),
-                ValueKind::NEOptionalLit(n) => {
-                    ExprKind::SomeLit(n.to_hir(venv))
-                }
-                ValueKind::EmptyListLit(n) => ExprKind::EmptyListLit(Hir::new(
-                    HirKind::Expr(ExprKind::App(
-                        Value::from_builtin(Builtin::List).to_hir(venv),
-                        n.to_hir(venv),
-                    )),
-                    Span::Artificial,
-                )),
-                ValueKind::NEListLit(elts) => ExprKind::NEListLit(
-                    elts.iter().map(|v| v.to_hir(venv)).collect(),
-                ),
-                ValueKind::TextLit(elts) => ExprKind::TextLit(
-                    elts.iter()
-                        .map(|t| t.map_ref(|v| v.to_hir(venv)))
-                        .collect(),
-                ),
-                ValueKind::RecordLit(kvs) => ExprKind::RecordLit(
-                    kvs.iter()
-                        .map(|(k, v)| (k.clone(), v.to_hir(venv)))
-                        .collect(),
-                ),
-                ValueKind::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(
-                    Hir::new(
-                        HirKind::Expr(map_uniontype(kts)),
-                        Span::Artificial,
-                    ),
-                    l.clone(),
-                ),
-                ValueKind::UnionLit(l, v, kts) => ExprKind::App(
-                    Hir::new(
-                        HirKind::Expr(ExprKind::Field(
-                            Hir::new(
-                                HirKind::Expr(map_uniontype(kts)),
-                                Span::Artificial,
-                            ),
-                            l.clone(),
-                        )),
-                        Span::Artificial,
-                    ),
-                    v.to_hir(venv),
-                ),
-                ValueKind::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)),
-            }),
-        };
-
-        Hir::new(hir, self.0.span.clone())
-    }
-    pub fn to_hir_noenv(&self) -> Hir {
-        self.to_hir(VarEnv::new())
-    }
-}
-
-impl ValueInternal {
-    fn from_whnf(k: ValueKind, span: Span) -> Self {
-        ValueInternal {
-            kind: lazy::Lazy::new_completed(k),
-            span,
-        }
-    }
-    fn from_thunk(th: Thunk, span: Span) -> Self {
-        ValueInternal {
-            kind: lazy::Lazy::new(th),
-            span,
-        }
-    }
-    fn into_value(self) -> Value {
-        Value(Rc::new(self))
-    }
-
-    fn kind(&self) -> &ValueKind {
-        &self.kind
-    }
-    fn normalize(&self) {
-        self.kind().normalize();
-    }
-}
-
-impl ValueKind {
-    pub(crate) fn into_value(self) -> Value {
-        Value::from_kind(self)
-    }
-
-    pub(crate) fn normalize(&self) {
-        match self {
-            ValueKind::Var(..) | ValueKind::Const(_) | ValueKind::Lit(_) => {}
-
-            ValueKind::EmptyOptionalLit(tth) | ValueKind::EmptyListLit(tth) => {
-                tth.normalize();
-            }
-
-            ValueKind::NEOptionalLit(th) => {
-                th.normalize();
-            }
-            ValueKind::LamClosure { annot, closure, .. }
-            | ValueKind::PiClosure { annot, closure, .. } => {
-                annot.normalize();
-                closure.normalize();
-            }
-            ValueKind::AppliedBuiltin(closure) => closure.normalize(),
-            ValueKind::NEListLit(elts) => {
-                for x in elts.iter() {
-                    x.normalize();
-                }
-            }
-            ValueKind::RecordLit(kvs) => {
-                for x in kvs.values() {
-                    x.normalize();
-                }
-            }
-            ValueKind::RecordType(kvs) => {
-                for x in kvs.values() {
-                    x.normalize();
-                }
-            }
-            ValueKind::UnionType(kts) | ValueKind::UnionConstructor(_, kts) => {
-                for x in kts.values().flat_map(|opt| opt) {
-                    x.normalize();
-                }
-            }
-            ValueKind::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) => {
-                x.normalize();
-                y.normalize();
-            }
-            ValueKind::PartialExpr(e) => {
-                e.map_ref(Value::normalize);
-            }
-        }
-    }
-
-    pub(crate) fn from_builtin(b: Builtin) -> ValueKind {
-        ValueKind::from_builtin_env(b, NzEnv::new())
-    }
-    pub(crate) fn from_builtin_env(b: Builtin, env: NzEnv) -> ValueKind {
-        ValueKind::AppliedBuiltin(BuiltinClosure::new(b, env))
-    }
-}
-
-impl Thunk {
-    fn new(env: NzEnv, body: Hir) -> Self {
-        Thunk::Thunk { env, body }
-    }
-    fn from_partial_expr(env: NzEnv, expr: ExprKind<Value>) -> Self {
-        Thunk::PartialExpr { env, expr }
-    }
-    fn eval(self) -> ValueKind {
-        match self {
-            Thunk::Thunk { env, body } => normalize_hir_whnf(&env, &body),
-            Thunk::PartialExpr { env, expr } => normalize_one_layer(expr, &env),
-        }
-    }
-}
-
-impl Closure {
-    pub fn new(env: &NzEnv, body: Hir) -> Self {
-        Closure::Closure {
-            env: env.clone(),
-            body,
-        }
-    }
-    /// New closure that ignores its argument
-    pub fn new_constant(body: Value) -> Self {
-        Closure::ConstantClosure { body }
-    }
-
-    pub fn apply(&self, val: Value) -> Value {
-        match self {
-            Closure::Closure { env, body, .. } => {
-                body.eval(env.insert_value(val, ()))
-            }
-            Closure::ConstantClosure { body, .. } => body.clone(),
-        }
-    }
-    fn apply_var(&self, var: NzVar) -> Value {
-        match self {
-            Closure::Closure { .. } => {
-                self.apply(Value::from_kind(ValueKind::Var(var)))
-            }
-            Closure::ConstantClosure { body, .. } => body.clone(),
-        }
-    }
-
-    // TODO: somehow normalize the body. Might require to pass an env.
-    pub fn normalize(&self) {}
-
-    /// Convert this closure to a Hir expression
-    pub fn to_hir(&self, venv: VarEnv) -> Hir {
-        self.apply_var(NzVar::new(venv.size()))
-            .to_hir(venv.insert())
-    }
-    /// 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, ()> {
-        match self {
-            Closure::Closure { .. } => {
-                let v = NzVar::fresh();
-                // TODO: handle case where variable is used in closure
-                // TODO: return information about where the variable is used
-                Ok(self.apply_var(v))
-            }
-            Closure::ConstantClosure { body, .. } => Ok(body.clone()),
-        }
-    }
-}
-
-impl TextLit {
-    pub fn new(
-        elts: impl Iterator<Item = InterpolatedTextContents<Value>>,
-    ) -> Self {
-        TextLit(squash_textlit(elts))
-    }
-    pub fn interpolate(v: Value) -> TextLit {
-        TextLit(vec![InterpolatedTextContents::Expr(v)])
-    }
-    pub fn from_text(s: String) -> TextLit {
-        TextLit(vec![InterpolatedTextContents::Text(s)])
-    }
-
-    pub fn concat(&self, other: &TextLit) -> TextLit {
-        TextLit::new(self.iter().chain(other.iter()).cloned())
-    }
-    pub fn is_empty(&self) -> bool {
-        self.0.is_empty()
-    }
-    /// If the literal consists of only one interpolation and not text, return the interpolated
-    /// value.
-    pub fn as_single_expr(&self) -> Option<&Value> {
-        use InterpolatedTextContents::Expr;
-        if let [Expr(v)] = self.0.as_slice() {
-            Some(v)
-        } else {
-            None
-        }
-    }
-    /// If there are no interpolations, return the corresponding text value.
-    pub fn as_text(&self) -> Option<String> {
-        use InterpolatedTextContents::Text;
-        if self.is_empty() {
-            Some(String::new())
-        } else if let [Text(s)] = self.0.as_slice() {
-            Some(s.clone())
-        } else {
-            None
-        }
-    }
-    pub fn iter(
-        &self,
-    ) -> impl Iterator<Item = &InterpolatedTextContents<Value>> {
-        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);
-        }
-    }
-}
-
-impl lazy::Eval<ValueKind> for Thunk {
-    fn eval(self) -> ValueKind {
-        self.eval()
-    }
-}
-
-/// Compare two values for equality modulo alpha/beta-equivalence.
-impl std::cmp::PartialEq for Value {
-    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::PartialEq for Thunk {
-    fn eq(&self, _other: &Self) -> bool {
-        unreachable!(
-            "Trying to compare thunks but we should only compare WHNFs"
-        )
-    }
-}
-impl std::cmp::Eq for Thunk {}
-
-impl std::cmp::PartialEq for Closure {
-    fn eq(&self, other: &Self) -> bool {
-        let v = NzVar::fresh();
-        self.apply_var(v) == other.apply_var(v)
-    }
-}
-impl std::cmp::Eq for Closure {}
-
-impl std::fmt::Debug for Value {
-    fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
-        let vint: &ValueInternal = &self.0;
-        let kind = vint.kind();
-        if let ValueKind::Const(c) = kind {
-            return write!(fmt, "{:?}", c);
-        }
-        let mut x = fmt.debug_struct(&format!("Value@WHNF"));
-        x.field("kind", kind);
-        x.finish()
-    }
-}
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,
-- 
cgit v1.2.3


From da69fe3eef7e001a1a0bdd2a2f3ebefccc3426e3 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Mon, 17 Feb 2020 18:24:06 +0000
Subject: Remove spans from Nir

That info was too unreliable: we need clean tracking mechanisms if we
want to improve error messages
---
 dhall/src/semantics/nze/nir.rs | 22 +++++++---------------
 1 file changed, 7 insertions(+), 15 deletions(-)

(limited to 'dhall/src/semantics/nze')

diff --git a/dhall/src/semantics/nze/nir.rs b/dhall/src/semantics/nze/nir.rs
index a6dafa2..44a23fe 100644
--- a/dhall/src/semantics/nze/nir.rs
+++ b/dhall/src/semantics/nze/nir.rs
@@ -24,7 +24,6 @@ pub(crate) struct Nir(Rc<NirInternal>);
 #[derive(Debug)]
 struct NirInternal {
     kind: lazy::Lazy<Thunk, NirKind>,
-    span: Span,
 }
 
 /// An unevaluated subexpression
@@ -95,26 +94,21 @@ pub(crate) enum NirKind {
 impl Nir {
     /// Construct a Nir from a completely unnormalized expression.
     pub(crate) fn new_thunk(env: NzEnv, hir: Hir) -> Nir {
-        let span = hir.span();
-        NirInternal::from_thunk(Thunk::new(env, hir), span).into_nir()
+        NirInternal::from_thunk(Thunk::new(env, hir)).into_nir()
     }
     /// 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();
-        NirInternal::from_thunk(
-            Thunk::from_partial_expr(env, e),
-            Span::Artificial,
-        )
-        .into_nir()
+        NirInternal::from_thunk(Thunk::from_partial_expr(env, e)).into_nir()
     }
     /// Make a Nir from a NirKind
     pub(crate) fn from_kind(v: NirKind) -> Nir {
-        NirInternal::from_whnf(v, Span::Artificial).into_nir()
+        NirInternal::from_whnf(v).into_nir()
     }
     pub(crate) fn from_const(c: Const) -> Self {
         let v = NirKind::Const(c);
-        NirInternal::from_whnf(v, Span::Artificial).into_nir()
+        NirInternal::from_whnf(v).into_nir()
     }
     pub(crate) fn from_builtin(b: Builtin) -> Self {
         Self::from_builtin_env(b, &NzEnv::new())
@@ -258,7 +252,7 @@ impl Nir {
             }),
         };
 
-        Hir::new(hir, self.0.span.clone())
+        Hir::new(hir, Span::Artificial)
     }
     pub fn to_hir_noenv(&self) -> Hir {
         self.to_hir(VarEnv::new())
@@ -266,16 +260,14 @@ impl Nir {
 }
 
 impl NirInternal {
-    fn from_whnf(k: NirKind, span: Span) -> Self {
+    fn from_whnf(k: NirKind) -> Self {
         NirInternal {
             kind: lazy::Lazy::new_completed(k),
-            span,
         }
     }
-    fn from_thunk(th: Thunk, span: Span) -> Self {
+    fn from_thunk(th: Thunk) -> Self {
         NirInternal {
             kind: lazy::Lazy::new(th),
-            span,
         }
     }
     fn into_nir(self) -> Nir {
-- 
cgit v1.2.3


From 50a9dc4b9af19a35a983fe17108453d1d82d80ed Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 18 Feb 2020 18:46:26 +0000
Subject: Remove useless `normalize` option from ToExprOptions

---
 dhall/src/semantics/nze/nir.rs | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'dhall/src/semantics/nze')

diff --git a/dhall/src/semantics/nze/nir.rs b/dhall/src/semantics/nze/nir.rs
index 44a23fe..4ed66b7 100644
--- a/dhall/src/semantics/nze/nir.rs
+++ b/dhall/src/semantics/nze/nir.rs
@@ -137,9 +137,6 @@ impl Nir {
     }
     /// Converts a value back to the corresponding AST expression.
     pub(crate) fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr {
-        if opts.normalize {
-            self.normalize();
-        }
         self.to_hir_noenv().to_expr(opts)
     }
     pub(crate) fn to_expr_tyenv(&self, tyenv: &TyEnv) -> NormalizedExpr {
-- 
cgit v1.2.3


From 7cbfc1a0d32766a383d1f48902502adaa2234d2f Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 18 Feb 2020 19:12:31 +0000
Subject: Avoid re-typechecking after import

---
 dhall/src/semantics/nze/normalize.rs | 1 +
 1 file changed, 1 insertion(+)

(limited to 'dhall/src/semantics/nze')

diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs
index 4c2aa33..604db8f 100644
--- a/dhall/src/semantics/nze/normalize.rs
+++ b/dhall/src/semantics/nze/normalize.rs
@@ -442,6 +442,7 @@ pub(crate) fn normalize_one_layer(expr: ExprKind<Nir>, env: &NzEnv) -> NirKind {
 pub(crate) fn normalize_hir_whnf(env: &NzEnv, hir: &Hir) -> NirKind {
     match hir.kind() {
         HirKind::Var(var) => env.lookup_val(var),
+        HirKind::Import(hir, _) => normalize_hir_whnf(env, hir),
         HirKind::Expr(ExprKind::Lam(binder, annot, body)) => {
             let annot = annot.eval(env);
             NirKind::LamClosure {
-- 
cgit v1.2.3