Rename ValueF to ValueKind

6 files changed, 372 insertions, 362 deletions

diff --git a/dhall/src/semantics/core/context.rs b/dhall/src/semantics/core/context.rs
index d150e56..8861378 100644
--- a/dhall/src/semantics/core/context.rs
+++ b/dhall/src/semantics/core/context.rs
@@ -2,7 +2,7 @@ use std::collections::HashMap;
 use std::rc::Rc;
 
 use crate::semantics::core::value::Value;
-use crate::semantics::core::valuef::ValueF;
+use crate::semantics::core::value_kind::ValueKind;
 use crate::semantics::core::var::{AlphaVar, Shift, Subst};
 use crate::semantics::error::TypeError;
 use crate::syntax::{Label, V};
@@ -39,7 +39,7 @@ impl TypecheckContext {
                     let i = i.under_multiple_binders(&shift_map);
                     return Some(match i {
                         CtxItem::Kept(newvar, t) => {
-                            Value::from_valuef_and_type(ValueF::Var(newvar), t)
+                            Value::from_kind_and_type(ValueKind::Var(newvar), t)
                         }
                         CtxItem::Replaced(v) => v,
                     });
diff --git a/dhall/src/semantics/core/mod.rs b/dhall/src/semantics/core/mod.rs
index 08213f7..bf3d390 100644
--- a/dhall/src/semantics/core/mod.rs
+++ b/dhall/src/semantics/core/mod.rs
@@ -1,4 +1,4 @@
 pub mod context;
 pub mod value;
-pub mod valuef;
+pub mod value_kind;
 pub mod var;
diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs
index 6e6739f..7403742 100644
--- a/dhall/src/semantics/core/value.rs
+++ b/dhall/src/semantics/core/value.rs
@@ -2,7 +2,7 @@ use std::cell::{Ref, RefCell, RefMut};
 use std::rc::Rc;
 
 use crate::semantics::core::context::TypecheckContext;
-use crate::semantics::core::valuef::ValueF;
+use crate::semantics::core::value_kind::ValueKind;
 use crate::semantics::core::var::{AlphaVar, Shift, Subst};
 use crate::semantics::error::{TypeError, TypeMessage};
 use crate::semantics::phase::normalize::{apply_any, normalize_whnf};
@@ -15,12 +15,12 @@ pub(crate) enum Form {
     /// No constraints; expression may not be normalized at all.
     Unevaled,
     /// Weak Head Normal Form, i.e. normalized up to the first constructor, but subexpressions may
-    /// not be normalized. This means that the first constructor of the contained ValueF is the first
+    /// not be normalized. This means that the first constructor of the contained ValueKind is the first
     /// constructor of the final Normal Form (NF).
     WHNF,
     /// Normal Form, i.e. completely normalized.
-    /// When all the Values in a ValueF are at least in WHNF, and recursively so, then the
-    /// ValueF is in NF. This is because WHNF ensures that we have the first constructor of the NF; so
+    /// When all the Values in a ValueKind are at least in WHNF, and recursively so, then the
+    /// ValueKind is in 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.
     NF,
 }
@@ -32,7 +32,7 @@ use Form::{Unevaled, NF, WHNF};
 #[derive(Debug)]
 struct ValueInternal {
     form: Form,
-    value: ValueF,
+    kind: ValueKind,
     /// This is None if and only if `value` is `Sort` (which doesn't have a type)
     ty: Option<Value>,
     span: Span,
@@ -57,8 +57,8 @@ impl ValueInternal {
     fn into_value(self) -> Value {
         Value(Rc::new(RefCell::new(self)))
     }
-    fn as_valuef(&self) -> &ValueF {
-        &self.value
+    fn as_kind(&self) -> &ValueKind {
+        &self.kind
     }
 
     fn normalize_whnf(&mut self) {
@@ -67,21 +67,21 @@ impl ValueInternal {
             // Dummy value in case the other closure panics
             || ValueInternal {
                 form: Unevaled,
-                value: ValueF::Const(Const::Type),
+                kind: ValueKind::Const(Const::Type),
                 ty: None,
                 span: Span::Artificial,
             },
             |vint| match (&vint.form, &vint.ty) {
                 (Unevaled, Some(ty)) => ValueInternal {
                     form: WHNF,
-                    value: normalize_whnf(vint.value, &ty),
+                    kind: normalize_whnf(vint.kind, &ty),
                     ty: vint.ty,
                     span: vint.span,
                 },
                 // `value` is `Sort`
                 (Unevaled, None) => ValueInternal {
                     form: NF,
-                    value: ValueF::Const(Const::Sort),
+                    kind: ValueKind::Const(Const::Sort),
                     ty: None,
                     span: vint.span,
                 },
@@ -97,7 +97,7 @@ impl ValueInternal {
                 self.normalize_nf();
             }
             WHNF => {
-                self.value.normalize_mut();
+                self.kind.normalize_mut();
                 self.form = NF;
             }
             // Already in NF
@@ -116,10 +116,10 @@ impl ValueInternal {
 }
 
 impl Value {
-    fn new(value: ValueF, form: Form, ty: Value, span: Span) -> Value {
+    fn new(kind: ValueKind, form: Form, ty: Value, span: Span) -> Value {
         ValueInternal {
             form,
-            value,
+            kind,
             ty: Some(ty),
             span,
         }
@@ -128,23 +128,23 @@ impl Value {
     pub(crate) fn const_sort() -> Value {
         ValueInternal {
             form: NF,
-            value: ValueF::Const(Const::Sort),
+            kind: ValueKind::Const(Const::Sort),
             ty: None,
             span: Span::Artificial,
         }
         .into_value()
     }
-    pub(crate) fn from_valuef_and_type(v: ValueF, t: Value) -> Value {
+    pub(crate) fn from_kind_and_type(v: ValueKind, t: Value) -> Value {
         Value::new(v, Unevaled, t, Span::Artificial)
     }
-    pub(crate) fn from_valuef_and_type_and_span(
-        v: ValueF,
+    pub(crate) fn from_kind_and_type_and_span(
+        v: ValueKind,
         t: Value,
         span: Span,
     ) -> Value {
         Value::new(v, Unevaled, t, span)
     }
-    pub(crate) fn from_valuef_and_type_whnf(v: ValueF, t: Value) -> Value {
+    pub(crate) fn from_kind_and_type_whnf(v: ValueKind, t: Value) -> Value {
         Value::new(v, WHNF, t, Span::Artificial)
     }
     pub(crate) fn from_const(c: Const) -> Self {
@@ -160,7 +160,7 @@ impl Value {
 
     pub(crate) fn as_const(&self) -> Option<Const> {
         match &*self.as_whnf() {
-            ValueF::Const(c) => Some(*c),
+            ValueKind::Const(c) => Some(*c),
             _ => None,
         }
     }
@@ -174,30 +174,30 @@ impl Value {
     fn as_internal_mut(&self) -> RefMut<ValueInternal> {
         self.0.borrow_mut()
     }
-    /// WARNING: The returned ValueF may be entirely unnormalized, in aprticular it may just be an
+    /// WARNING: The returned ValueKind may be entirely unnormalized, in aprticular it may just be an
     /// unevaled PartialExpr. You probably want to use `as_whnf`.
-    fn as_valuef(&self) -> Ref<ValueF> {
-        Ref::map(self.as_internal(), ValueInternal::as_valuef)
+    fn as_kind(&self) -> Ref<ValueKind> {
+        Ref::map(self.as_internal(), ValueInternal::as_kind)
     }
     /// 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 as_whnf(&self) -> Ref<ValueF> {
+    pub(crate) fn as_whnf(&self) -> Ref<ValueKind> {
         self.normalize_whnf();
-        self.as_valuef()
+        self.as_kind()
     }
 
     pub(crate) fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr {
         if opts.normalize {
             self.normalize_whnf();
         }
-        self.as_valuef().to_expr(opts)
+        self.as_kind().to_expr(opts)
     }
-    pub(crate) fn to_whnf_ignore_type(&self) -> ValueF {
+    pub(crate) fn to_whnf_ignore_type(&self) -> ValueKind {
         self.as_whnf().clone()
     }
     /// Before discarding type information, check that it matches the expected return type.
-    pub(crate) fn to_whnf_check_type(&self, ty: &Value) -> ValueF {
+    pub(crate) fn to_whnf_check_type(&self, ty: &Value) -> ValueKind {
         self.check_type(ty);
         self.to_whnf_ignore_type()
     }
@@ -234,13 +234,13 @@ impl Value {
 
     pub(crate) fn app(&self, v: Value) -> Value {
         let body_t = match &*self.get_type_not_sort().as_whnf() {
-            ValueF::Pi(x, t, e) => {
+            ValueKind::Pi(x, t, e) => {
                 v.check_type(t);
                 e.subst_shift(&x.into(), &v)
             }
             _ => unreachable!("Internal type error"),
         };
-        Value::from_valuef_and_type_whnf(
+        Value::from_kind_and_type_whnf(
             apply_any(self.clone(), v, &body_t),
             body_t,
         )
@@ -275,7 +275,7 @@ impl Shift for ValueInternal {
     fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
         Some(ValueInternal {
             form: self.form,
-            value: self.value.shift(delta, var)?,
+            kind: self.kind.shift(delta, var)?,
             ty: self.ty.shift(delta, var)?,
             span: self.span.clone(),
         })
@@ -284,10 +284,10 @@ impl Shift for ValueInternal {
 
 impl Subst<Value> for Value {
     fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self {
-        match &*self.as_valuef() {
+        match &*self.as_kind() {
             // If the var matches, we can just reuse the provided value instead of copying it.
             // We also check that the types match, if in debug mode.
-            ValueF::Var(v) if v == var => {
+            ValueKind::Var(v) if v == var => {
                 if let Ok(self_ty) = self.get_type() {
                     val.check_type(&self_ty.subst_shift(var, val));
                 }
@@ -303,7 +303,7 @@ impl Subst<Value> for ValueInternal {
         ValueInternal {
             // The resulting value may not stay in wnhf after substitution
             form: Unevaled,
-            value: self.value.subst_shift(var, val),
+            kind: self.kind.subst_shift(var, val),
             ty: self.ty.subst_shift(var, val),
             span: self.span.clone(),
         }
@@ -321,11 +321,11 @@ impl std::cmp::Eq for Value {}
 impl std::fmt::Debug for Value {
     fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
         let vint: &ValueInternal = &self.as_internal();
-        if let ValueF::Const(c) = &vint.value {
+        if let ValueKind::Const(c) = &vint.kind {
             write!(fmt, "{:?}", c)
         } else {
             let mut x = fmt.debug_struct(&format!("Value@{:?}", &vint.form));
-            x.field("value", &vint.value);
+            x.field("value", &vint.kind);
             if let Some(ty) = vint.ty.as_ref() {
                 x.field("type", &ty);
             } else {
diff --git a/dhall/src/semantics/core/value_kind.rs b/dhall/src/semantics/core/value_kind.rs
new file mode 100644
index 0000000..36ba068
--- /dev/null
+++ b/dhall/src/semantics/core/value_kind.rs
@@ -0,0 +1,333 @@
+use std::collections::HashMap;
+
+use crate::semantics::core::value::{ToExprOptions, Value};
+use crate::semantics::core::var::{AlphaLabel, AlphaVar, Shift, Subst};
+use crate::semantics::phase::typecheck::rc;
+use crate::semantics::phase::{Normalized, NormalizedExpr};
+use crate::syntax;
+use crate::syntax::{
+    Builtin, Const, ExprF, Integer, InterpolatedTextContents, Label,
+    NaiveDouble, Natural,
+};
+
+/// A semantic value. Subexpressions are Values, which are partially evaluated expressions that are
+/// normalized on-demand.
+/// If you compare for equality two `ValueKind`s in WHNF, then equality will be up to
+/// alpha-equivalence (renaming of bound variables) and beta-equivalence (normalization). It will
+/// recursively normalize as needed.
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub(crate) enum ValueKind {
+    /// Closures
+    Lam(AlphaLabel, Value, Value),
+    Pi(AlphaLabel, Value, Value),
+    // Invariant: in whnf, the evaluation must not be able to progress further.
+    AppliedBuiltin(Builtin, Vec<Value>),
+
+    Var(AlphaVar),
+    Const(Const),
+    BoolLit(bool),
+    NaturalLit(Natural),
+    IntegerLit(Integer),
+    DoubleLit(NaiveDouble),
+    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>>),
+    // Invariant: in whnf, this must not contain interpolations that are themselves TextLits, and
+    // contiguous text values must be merged.
+    TextLit(Vec<InterpolatedTextContents<Value>>),
+    Equivalence(Value, Value),
+    // Invariant: in whnf, this must not contain a value captured by one of the variants above.
+    PartialExpr(ExprF<Value, Normalized>),
+}
+
+impl ValueKind {
+    pub(crate) fn into_value_with_type(self, t: Value) -> Value {
+        Value::from_kind_and_type(self, t)
+    }
+
+    pub(crate) fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr {
+        match self {
+            ValueKind::Lam(x, t, e) => rc(ExprF::Lam(
+                x.to_label_maybe_alpha(opts.alpha),
+                t.to_expr(opts),
+                e.to_expr(opts),
+            )),
+            ValueKind::AppliedBuiltin(b, args) => args
+                .iter()
+                .map(|v| v.to_expr(opts))
+                .fold(rc(ExprF::Builtin(*b)), |acc, v| rc(ExprF::App(acc, v))),
+            ValueKind::Pi(x, t, e) => rc(ExprF::Pi(
+                x.to_label_maybe_alpha(opts.alpha),
+                t.to_expr(opts),
+                e.to_expr(opts),
+            )),
+            ValueKind::Var(v) => rc(ExprF::Var(v.to_var(opts.alpha))),
+            ValueKind::Const(c) => rc(ExprF::Const(*c)),
+            ValueKind::BoolLit(b) => rc(ExprF::BoolLit(*b)),
+            ValueKind::NaturalLit(n) => rc(ExprF::NaturalLit(*n)),
+            ValueKind::IntegerLit(n) => rc(ExprF::IntegerLit(*n)),
+            ValueKind::DoubleLit(n) => rc(ExprF::DoubleLit(*n)),
+            ValueKind::EmptyOptionalLit(n) => rc(ExprF::App(
+                rc(ExprF::Builtin(Builtin::OptionalNone)),
+                n.to_expr(opts),
+            )),
+            ValueKind::NEOptionalLit(n) => rc(ExprF::SomeLit(n.to_expr(opts))),
+            ValueKind::EmptyListLit(n) => rc(ExprF::EmptyListLit(rc(
+                ExprF::App(rc(ExprF::Builtin(Builtin::List)), n.to_expr(opts)),
+            ))),
+            ValueKind::NEListLit(elts) => rc(ExprF::NEListLit(
+                elts.iter().map(|n| n.to_expr(opts)).collect(),
+            )),
+            ValueKind::RecordLit(kvs) => rc(ExprF::RecordLit(
+                kvs.iter()
+                    .map(|(k, v)| (k.clone(), v.to_expr(opts)))
+                    .collect(),
+            )),
+            ValueKind::RecordType(kts) => rc(ExprF::RecordType(
+                kts.iter()
+                    .map(|(k, v)| (k.clone(), v.to_expr(opts)))
+                    .collect(),
+            )),
+            ValueKind::UnionType(kts) => rc(ExprF::UnionType(
+                kts.iter()
+                    .map(|(k, v)| {
+                        (k.clone(), v.as_ref().map(|v| v.to_expr(opts)))
+                    })
+                    .collect(),
+            )),
+            ValueKind::UnionConstructor(l, kts) => rc(ExprF::Field(
+                ValueKind::UnionType(kts.clone()).to_expr(opts),
+                l.clone(),
+            )),
+            ValueKind::UnionLit(l, v, kts) => rc(ExprF::App(
+                ValueKind::UnionConstructor(l.clone(), kts.clone())
+                    .to_expr(opts),
+                v.to_expr(opts),
+            )),
+            ValueKind::TextLit(elts) => rc(ExprF::TextLit(
+                elts.iter()
+                    .map(|contents| contents.map_ref(|e| e.to_expr(opts)))
+                    .collect(),
+            )),
+            ValueKind::Equivalence(x, y) => rc(ExprF::BinOp(
+                syntax::BinOp::Equivalence,
+                x.to_expr(opts),
+                y.to_expr(opts),
+            )),
+            ValueKind::PartialExpr(e) => rc(e.map_ref(|v| v.to_expr(opts))),
+        }
+    }
+
+    pub(crate) fn normalize_mut(&mut self) {
+        match self {
+            ValueKind::Var(_)
+            | ValueKind::Const(_)
+            | ValueKind::BoolLit(_)
+            | ValueKind::NaturalLit(_)
+            | ValueKind::IntegerLit(_)
+            | ValueKind::DoubleLit(_) => {}
+
+            ValueKind::EmptyOptionalLit(tth) | ValueKind::EmptyListLit(tth) => {
+                tth.normalize_mut();
+            }
+
+            ValueKind::NEOptionalLit(th) => {
+                th.normalize_mut();
+            }
+            ValueKind::Lam(_, t, e) => {
+                t.normalize_mut();
+                e.normalize_mut();
+            }
+            ValueKind::Pi(_, t, e) => {
+                t.normalize_mut();
+                e.normalize_mut();
+            }
+            ValueKind::AppliedBuiltin(_, args) => {
+                for x in args.iter_mut() {
+                    x.normalize_mut();
+                }
+            }
+            ValueKind::NEListLit(elts) => {
+                for x in elts.iter_mut() {
+                    x.normalize_mut();
+                }
+            }
+            ValueKind::RecordLit(kvs) => {
+                for x in kvs.values_mut() {
+                    x.normalize_mut();
+                }
+            }
+            ValueKind::RecordType(kvs) => {
+                for x in kvs.values_mut() {
+                    x.normalize_mut();
+                }
+            }
+            ValueKind::UnionType(kts) | ValueKind::UnionConstructor(_, kts) => {
+                for x in kts.values_mut().flat_map(|opt| opt) {
+                    x.normalize_mut();
+                }
+            }
+            ValueKind::UnionLit(_, v, kts) => {
+                v.normalize_mut();
+                for x in kts.values_mut().flat_map(|opt| opt) {
+                    x.normalize_mut();
+                }
+            }
+            ValueKind::TextLit(elts) => {
+                for x in elts.iter_mut() {
+                    x.map_mut(Value::normalize_mut);
+                }
+            }
+            ValueKind::Equivalence(x, y) => {
+                x.normalize_mut();
+                y.normalize_mut();
+            }
+            ValueKind::PartialExpr(e) => {
+                e.map_mut(Value::normalize_mut);
+            }
+        }
+    }
+
+    pub(crate) fn from_builtin(b: Builtin) -> ValueKind {
+        ValueKind::AppliedBuiltin(b, vec![])
+    }
+}
+
+impl Shift for ValueKind {
+    fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
+        Some(match self {
+            ValueKind::Lam(x, t, e) => ValueKind::Lam(
+                x.clone(),
+                t.shift(delta, var)?,
+                e.shift(delta, &var.under_binder(x))?,
+            ),
+            ValueKind::AppliedBuiltin(b, args) => {
+                ValueKind::AppliedBuiltin(*b, args.shift(delta, var)?)
+            }
+            ValueKind::Pi(x, t, e) => ValueKind::Pi(
+                x.clone(),
+                t.shift(delta, var)?,
+                e.shift(delta, &var.under_binder(x))?,
+            ),
+            ValueKind::Var(v) => ValueKind::Var(v.shift(delta, var)?),
+            ValueKind::Const(c) => ValueKind::Const(*c),
+            ValueKind::BoolLit(b) => ValueKind::BoolLit(*b),
+            ValueKind::NaturalLit(n) => ValueKind::NaturalLit(*n),
+            ValueKind::IntegerLit(n) => ValueKind::IntegerLit(*n),
+            ValueKind::DoubleLit(n) => ValueKind::DoubleLit(*n),
+            ValueKind::EmptyOptionalLit(tth) => {
+                ValueKind::EmptyOptionalLit(tth.shift(delta, var)?)
+            }
+            ValueKind::NEOptionalLit(th) => {
+                ValueKind::NEOptionalLit(th.shift(delta, var)?)
+            }
+            ValueKind::EmptyListLit(tth) => {
+                ValueKind::EmptyListLit(tth.shift(delta, var)?)
+            }
+            ValueKind::NEListLit(elts) => {
+                ValueKind::NEListLit(elts.shift(delta, var)?)
+            }
+            ValueKind::RecordLit(kvs) => {
+                ValueKind::RecordLit(kvs.shift(delta, var)?)
+            }
+            ValueKind::RecordType(kvs) => {
+                ValueKind::RecordType(kvs.shift(delta, var)?)
+            }
+            ValueKind::UnionType(kts) => {
+                ValueKind::UnionType(kts.shift(delta, var)?)
+            }
+            ValueKind::UnionConstructor(x, kts) => {
+                ValueKind::UnionConstructor(x.clone(), kts.shift(delta, var)?)
+            }
+            ValueKind::UnionLit(x, v, kts) => ValueKind::UnionLit(
+                x.clone(),
+                v.shift(delta, var)?,
+                kts.shift(delta, var)?,
+            ),
+            ValueKind::TextLit(elts) => {
+                ValueKind::TextLit(elts.shift(delta, var)?)
+            }
+            ValueKind::Equivalence(x, y) => ValueKind::Equivalence(
+                x.shift(delta, var)?,
+                y.shift(delta, var)?,
+            ),
+            ValueKind::PartialExpr(e) => {
+                ValueKind::PartialExpr(e.shift(delta, var)?)
+            }
+        })
+    }
+}
+
+impl Subst<Value> for ValueKind {
+    fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self {
+        match self {
+            ValueKind::AppliedBuiltin(b, args) => {
+                ValueKind::AppliedBuiltin(*b, args.subst_shift(var, val))
+            }
+            ValueKind::PartialExpr(e) => {
+                ValueKind::PartialExpr(e.subst_shift(var, val))
+            }
+            ValueKind::TextLit(elts) => {
+                ValueKind::TextLit(elts.subst_shift(var, val))
+            }
+            ValueKind::Lam(x, t, e) => ValueKind::Lam(
+                x.clone(),
+                t.subst_shift(var, val),
+                e.subst_shift(&var.under_binder(x), &val.under_binder(x)),
+            ),
+            ValueKind::Pi(x, t, e) => ValueKind::Pi(
+                x.clone(),
+                t.subst_shift(var, val),
+                e.subst_shift(&var.under_binder(x), &val.under_binder(x)),
+            ),
+            ValueKind::Var(v) if v == var => val.to_whnf_ignore_type(),
+            ValueKind::Var(v) => ValueKind::Var(v.shift(-1, var).unwrap()),
+            ValueKind::Const(c) => ValueKind::Const(*c),
+            ValueKind::BoolLit(b) => ValueKind::BoolLit(*b),
+            ValueKind::NaturalLit(n) => ValueKind::NaturalLit(*n),
+            ValueKind::IntegerLit(n) => ValueKind::IntegerLit(*n),
+            ValueKind::DoubleLit(n) => ValueKind::DoubleLit(*n),
+            ValueKind::EmptyOptionalLit(tth) => {
+                ValueKind::EmptyOptionalLit(tth.subst_shift(var, val))
+            }
+            ValueKind::NEOptionalLit(th) => {
+                ValueKind::NEOptionalLit(th.subst_shift(var, val))
+            }
+            ValueKind::EmptyListLit(tth) => {
+                ValueKind::EmptyListLit(tth.subst_shift(var, val))
+            }
+            ValueKind::NEListLit(elts) => {
+                ValueKind::NEListLit(elts.subst_shift(var, val))
+            }
+            ValueKind::RecordLit(kvs) => {
+                ValueKind::RecordLit(kvs.subst_shift(var, val))
+            }
+            ValueKind::RecordType(kvs) => {
+                ValueKind::RecordType(kvs.subst_shift(var, val))
+            }
+            ValueKind::UnionType(kts) => {
+                ValueKind::UnionType(kts.subst_shift(var, val))
+            }
+            ValueKind::UnionConstructor(x, kts) => ValueKind::UnionConstructor(
+                x.clone(),
+                kts.subst_shift(var, val),
+            ),
+            ValueKind::UnionLit(x, v, kts) => ValueKind::UnionLit(
+                x.clone(),
+                v.subst_shift(var, val),
+                kts.subst_shift(var, val),
+            ),
+            ValueKind::Equivalence(x, y) => ValueKind::Equivalence(
+                x.subst_shift(var, val),
+                y.subst_shift(var, val),
+            ),
+        }
+    }
+}
diff --git a/dhall/src/semantics/core/valuef.rs b/dhall/src/semantics/core/valuef.rs
deleted file mode 100644
index 73c715a..0000000
--- a/dhall/src/semantics/core/valuef.rs
+++ /dev/null
@@ -1,323 +0,0 @@
-use std::collections::HashMap;
-
-use crate::semantics::core::value::{ToExprOptions, Value};
-use crate::semantics::core::var::{AlphaLabel, AlphaVar, Shift, Subst};
-use crate::semantics::phase::typecheck::rc;
-use crate::semantics::phase::{Normalized, NormalizedExpr};
-use crate::syntax;
-use crate::syntax::{
-    Builtin, Const, ExprF, Integer, InterpolatedTextContents, Label,
-    NaiveDouble, Natural,
-};
-
-/// A semantic value. Subexpressions are Values, which are partially evaluated expressions that are
-/// normalized on-demand.
-/// If you compare for equality two `ValueF`s in WHNF, then equality will be up to
-/// alpha-equivalence (renaming of bound variables) and beta-equivalence (normalization). It will
-/// recursively normalize as needed.
-#[derive(Debug, Clone, PartialEq, Eq)]
-pub(crate) enum ValueF {
-    /// Closures
-    Lam(AlphaLabel, Value, Value),
-    Pi(AlphaLabel, Value, Value),
-    // Invariant: in whnf, the evaluation must not be able to progress further.
-    AppliedBuiltin(Builtin, Vec<Value>),
-
-    Var(AlphaVar),
-    Const(Const),
-    BoolLit(bool),
-    NaturalLit(Natural),
-    IntegerLit(Integer),
-    DoubleLit(NaiveDouble),
-    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>>),
-    // Invariant: in whnf, this must not contain interpolations that are themselves TextLits, and
-    // contiguous text values must be merged.
-    TextLit(Vec<InterpolatedTextContents<Value>>),
-    Equivalence(Value, Value),
-    // Invariant: in whnf, this must not contain a value captured by one of the variants above.
-    PartialExpr(ExprF<Value, Normalized>),
-}
-
-impl ValueF {
-    pub(crate) fn into_value_with_type(self, t: Value) -> Value {
-        Value::from_valuef_and_type(self, t)
-    }
-
-    pub(crate) fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr {
-        match self {
-            ValueF::Lam(x, t, e) => rc(ExprF::Lam(
-                x.to_label_maybe_alpha(opts.alpha),
-                t.to_expr(opts),
-                e.to_expr(opts),
-            )),
-            ValueF::AppliedBuiltin(b, args) => args
-                .iter()
-                .map(|v| v.to_expr(opts))
-                .fold(rc(ExprF::Builtin(*b)), |acc, v| rc(ExprF::App(acc, v))),
-            ValueF::Pi(x, t, e) => rc(ExprF::Pi(
-                x.to_label_maybe_alpha(opts.alpha),
-                t.to_expr(opts),
-                e.to_expr(opts),
-            )),
-            ValueF::Var(v) => rc(ExprF::Var(v.to_var(opts.alpha))),
-            ValueF::Const(c) => rc(ExprF::Const(*c)),
-            ValueF::BoolLit(b) => rc(ExprF::BoolLit(*b)),
-            ValueF::NaturalLit(n) => rc(ExprF::NaturalLit(*n)),
-            ValueF::IntegerLit(n) => rc(ExprF::IntegerLit(*n)),
-            ValueF::DoubleLit(n) => rc(ExprF::DoubleLit(*n)),
-            ValueF::EmptyOptionalLit(n) => rc(ExprF::App(
-                rc(ExprF::Builtin(Builtin::OptionalNone)),
-                n.to_expr(opts),
-            )),
-            ValueF::NEOptionalLit(n) => rc(ExprF::SomeLit(n.to_expr(opts))),
-            ValueF::EmptyListLit(n) => rc(ExprF::EmptyListLit(rc(ExprF::App(
-                rc(ExprF::Builtin(Builtin::List)),
-                n.to_expr(opts),
-            )))),
-            ValueF::NEListLit(elts) => rc(ExprF::NEListLit(
-                elts.iter().map(|n| n.to_expr(opts)).collect(),
-            )),
-            ValueF::RecordLit(kvs) => rc(ExprF::RecordLit(
-                kvs.iter()
-                    .map(|(k, v)| (k.clone(), v.to_expr(opts)))
-                    .collect(),
-            )),
-            ValueF::RecordType(kts) => rc(ExprF::RecordType(
-                kts.iter()
-                    .map(|(k, v)| (k.clone(), v.to_expr(opts)))
-                    .collect(),
-            )),
-            ValueF::UnionType(kts) => rc(ExprF::UnionType(
-                kts.iter()
-                    .map(|(k, v)| {
-                        (k.clone(), v.as_ref().map(|v| v.to_expr(opts)))
-                    })
-                    .collect(),
-            )),
-            ValueF::UnionConstructor(l, kts) => rc(ExprF::Field(
-                ValueF::UnionType(kts.clone()).to_expr(opts),
-                l.clone(),
-            )),
-            ValueF::UnionLit(l, v, kts) => rc(ExprF::App(
-                ValueF::UnionConstructor(l.clone(), kts.clone()).to_expr(opts),
-                v.to_expr(opts),
-            )),
-            ValueF::TextLit(elts) => rc(ExprF::TextLit(
-                elts.iter()
-                    .map(|contents| contents.map_ref(|e| e.to_expr(opts)))
-                    .collect(),
-            )),
-            ValueF::Equivalence(x, y) => rc(ExprF::BinOp(
-                syntax::BinOp::Equivalence,
-                x.to_expr(opts),
-                y.to_expr(opts),
-            )),
-            ValueF::PartialExpr(e) => rc(e.map_ref(|v| v.to_expr(opts))),
-        }
-    }
-
-    pub(crate) fn normalize_mut(&mut self) {
-        match self {
-            ValueF::Var(_)
-            | ValueF::Const(_)
-            | ValueF::BoolLit(_)
-            | ValueF::NaturalLit(_)
-            | ValueF::IntegerLit(_)
-            | ValueF::DoubleLit(_) => {}
-
-            ValueF::EmptyOptionalLit(tth) | ValueF::EmptyListLit(tth) => {
-                tth.normalize_mut();
-            }
-
-            ValueF::NEOptionalLit(th) => {
-                th.normalize_mut();
-            }
-            ValueF::Lam(_, t, e) => {
-                t.normalize_mut();
-                e.normalize_mut();
-            }
-            ValueF::Pi(_, t, e) => {
-                t.normalize_mut();
-                e.normalize_mut();
-            }
-            ValueF::AppliedBuiltin(_, args) => {
-                for x in args.iter_mut() {
-                    x.normalize_mut();
-                }
-            }
-            ValueF::NEListLit(elts) => {
-                for x in elts.iter_mut() {
-                    x.normalize_mut();
-                }
-            }
-            ValueF::RecordLit(kvs) => {
-                for x in kvs.values_mut() {
-                    x.normalize_mut();
-                }
-            }
-            ValueF::RecordType(kvs) => {
-                for x in kvs.values_mut() {
-                    x.normalize_mut();
-                }
-            }
-            ValueF::UnionType(kts) | ValueF::UnionConstructor(_, kts) => {
-                for x in kts.values_mut().flat_map(|opt| opt) {
-                    x.normalize_mut();
-                }
-            }
-            ValueF::UnionLit(_, v, kts) => {
-                v.normalize_mut();
-                for x in kts.values_mut().flat_map(|opt| opt) {
-                    x.normalize_mut();
-                }
-            }
-            ValueF::TextLit(elts) => {
-                for x in elts.iter_mut() {
-                    x.map_mut(Value::normalize_mut);
-                }
-            }
-            ValueF::Equivalence(x, y) => {
-                x.normalize_mut();
-                y.normalize_mut();
-            }
-            ValueF::PartialExpr(e) => {
-                e.map_mut(Value::normalize_mut);
-            }
-        }
-    }
-
-    pub(crate) fn from_builtin(b: Builtin) -> ValueF {
-        ValueF::AppliedBuiltin(b, vec![])
-    }
-}
-
-impl Shift for ValueF {
-    fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
-        Some(match self {
-            ValueF::Lam(x, t, e) => ValueF::Lam(
-                x.clone(),
-                t.shift(delta, var)?,
-                e.shift(delta, &var.under_binder(x))?,
-            ),
-            ValueF::AppliedBuiltin(b, args) => {
-                ValueF::AppliedBuiltin(*b, args.shift(delta, var)?)
-            }
-            ValueF::Pi(x, t, e) => ValueF::Pi(
-                x.clone(),
-                t.shift(delta, var)?,
-                e.shift(delta, &var.under_binder(x))?,
-            ),
-            ValueF::Var(v) => ValueF::Var(v.shift(delta, var)?),
-            ValueF::Const(c) => ValueF::Const(*c),
-            ValueF::BoolLit(b) => ValueF::BoolLit(*b),
-            ValueF::NaturalLit(n) => ValueF::NaturalLit(*n),
-            ValueF::IntegerLit(n) => ValueF::IntegerLit(*n),
-            ValueF::DoubleLit(n) => ValueF::DoubleLit(*n),
-            ValueF::EmptyOptionalLit(tth) => {
-                ValueF::EmptyOptionalLit(tth.shift(delta, var)?)
-            }
-            ValueF::NEOptionalLit(th) => {
-                ValueF::NEOptionalLit(th.shift(delta, var)?)
-            }
-            ValueF::EmptyListLit(tth) => {
-                ValueF::EmptyListLit(tth.shift(delta, var)?)
-            }
-            ValueF::NEListLit(elts) => {
-                ValueF::NEListLit(elts.shift(delta, var)?)
-            }
-            ValueF::RecordLit(kvs) => ValueF::RecordLit(kvs.shift(delta, var)?),
-            ValueF::RecordType(kvs) => {
-                ValueF::RecordType(kvs.shift(delta, var)?)
-            }
-            ValueF::UnionType(kts) => ValueF::UnionType(kts.shift(delta, var)?),
-            ValueF::UnionConstructor(x, kts) => {
-                ValueF::UnionConstructor(x.clone(), kts.shift(delta, var)?)
-            }
-            ValueF::UnionLit(x, v, kts) => ValueF::UnionLit(
-                x.clone(),
-                v.shift(delta, var)?,
-                kts.shift(delta, var)?,
-            ),
-            ValueF::TextLit(elts) => ValueF::TextLit(elts.shift(delta, var)?),
-            ValueF::Equivalence(x, y) => {
-                ValueF::Equivalence(x.shift(delta, var)?, y.shift(delta, var)?)
-            }
-            ValueF::PartialExpr(e) => ValueF::PartialExpr(e.shift(delta, var)?),
-        })
-    }
-}
-
-impl Subst<Value> for ValueF {
-    fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self {
-        match self {
-            ValueF::AppliedBuiltin(b, args) => {
-                ValueF::AppliedBuiltin(*b, args.subst_shift(var, val))
-            }
-            ValueF::PartialExpr(e) => {
-                ValueF::PartialExpr(e.subst_shift(var, val))
-            }
-            ValueF::TextLit(elts) => {
-                ValueF::TextLit(elts.subst_shift(var, val))
-            }
-            ValueF::Lam(x, t, e) => ValueF::Lam(
-                x.clone(),
-                t.subst_shift(var, val),
-                e.subst_shift(&var.under_binder(x), &val.under_binder(x)),
-            ),
-            ValueF::Pi(x, t, e) => ValueF::Pi(
-                x.clone(),
-                t.subst_shift(var, val),
-                e.subst_shift(&var.under_binder(x), &val.under_binder(x)),
-            ),
-            ValueF::Var(v) if v == var => val.to_whnf_ignore_type(),
-            ValueF::Var(v) => ValueF::Var(v.shift(-1, var).unwrap()),
-            ValueF::Const(c) => ValueF::Const(*c),
-            ValueF::BoolLit(b) => ValueF::BoolLit(*b),
-            ValueF::NaturalLit(n) => ValueF::NaturalLit(*n),
-            ValueF::IntegerLit(n) => ValueF::IntegerLit(*n),
-            ValueF::DoubleLit(n) => ValueF::DoubleLit(*n),
-            ValueF::EmptyOptionalLit(tth) => {
-                ValueF::EmptyOptionalLit(tth.subst_shift(var, val))
-            }
-            ValueF::NEOptionalLit(th) => {
-                ValueF::NEOptionalLit(th.subst_shift(var, val))
-            }
-            ValueF::EmptyListLit(tth) => {
-                ValueF::EmptyListLit(tth.subst_shift(var, val))
-            }
-            ValueF::NEListLit(elts) => {
-                ValueF::NEListLit(elts.subst_shift(var, val))
-            }
-            ValueF::RecordLit(kvs) => {
-                ValueF::RecordLit(kvs.subst_shift(var, val))
-            }
-            ValueF::RecordType(kvs) => {
-                ValueF::RecordType(kvs.subst_shift(var, val))
-            }
-            ValueF::UnionType(kts) => {
-                ValueF::UnionType(kts.subst_shift(var, val))
-            }
-            ValueF::UnionConstructor(x, kts) => {
-                ValueF::UnionConstructor(x.clone(), kts.subst_shift(var, val))
-            }
-            ValueF::UnionLit(x, v, kts) => ValueF::UnionLit(
-                x.clone(),
-                v.subst_shift(var, val),
-                kts.subst_shift(var, val),
-            ),
-            ValueF::Equivalence(x, y) => ValueF::Equivalence(
-                x.subst_shift(var, val),
-                y.subst_shift(var, val),
-            ),
-        }
-    }
-}
diff --git a/dhall/src/semantics/core/var.rs b/dhall/src/semantics/core/var.rs
index 184a372..77473f6 100644
--- a/dhall/src/semantics/core/var.rs
+++ b/dhall/src/semantics/core/var.rs
@@ -12,7 +12,7 @@ pub struct AlphaVar {
 }
 
 // Exactly like a Label, but equality returns always true.
-// This is so that ValueF equality is exactly alpha-equivalence.
+// This is so that ValueKind equality is exactly alpha-equivalence.
 #[derive(Clone, Eq)]
 pub struct AlphaLabel(Label);