Move ValueKind into value.rs

8 files changed, 269 insertions, 279 deletions

diff --git a/dhall/src/semantics/core/context.rs b/dhall/src/semantics/core/context.rs
index 9dfd22b..f755f72 100644
--- a/dhall/src/semantics/core/context.rs
+++ b/dhall/src/semantics/core/context.rs
@@ -3,7 +3,7 @@ use std::rc::Rc;
 
 use crate::error::TypeError;
 use crate::semantics::core::value::Value;
-use crate::semantics::core::value_kind::ValueKind;
+use crate::semantics::core::value::ValueKind;
 use crate::semantics::core::var::{AlphaVar, Shift, Subst};
 use crate::syntax::{Label, V};
 
diff --git a/dhall/src/semantics/core/mod.rs b/dhall/src/semantics/core/mod.rs
index bf3d390..90d74ea 100644
--- a/dhall/src/semantics/core/mod.rs
+++ b/dhall/src/semantics/core/mod.rs
@@ -1,4 +1,3 @@
 pub mod context;
 pub mod value;
-pub mod value_kind;
 pub mod var;
diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs
index 1e3b965..ca7c4bc 100644
--- a/dhall/src/semantics/core/value.rs
+++ b/dhall/src/semantics/core/value.rs
@@ -1,21 +1,27 @@
 use std::cell::{Ref, RefCell, RefMut};
+use std::collections::HashMap;
 use std::rc::Rc;
 
 use crate::error::{TypeError, TypeMessage};
 use crate::semantics::core::context::TypecheckContext;
-use crate::semantics::core::value_kind::ValueKind;
-use crate::semantics::core::var::{AlphaVar, Shift, Subst};
+use crate::semantics::core::var::{AlphaLabel, AlphaVar, Shift, Subst};
 use crate::semantics::phase::normalize::{apply_any, normalize_whnf};
 use crate::semantics::phase::typecheck::{builtin_to_value, const_to_value};
-use crate::semantics::phase::{NormalizedExpr, Typed};
+use crate::semantics::phase::{Normalized, NormalizedExpr, Typed};
 use crate::semantics::to_expr;
-use crate::syntax::{Builtin, Const, Span};
+use crate::syntax::{
+    Builtin, Const, ExprKind, Integer, InterpolatedTextContents, Label,
+    NaiveDouble, Natural, Span,
+};
 
 use self::Form::{Unevaled, NF, WHNF};
 
-/// Stores a possibly unevaluated value. Gets (partially) normalized on-demand,
-/// sharing computation automatically. Uses a RefCell to share computation.
+/// Stores a possibly unevaluated value. Gets (partially) normalized on-demand, sharing computation
+/// automatically. Uses a RefCell to share computation.
 /// Can optionally store a type from typechecking to preserve type information.
+/// If you compare for equality two `Value`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(Clone)]
 pub(crate) struct Value(Rc<RefCell<ValueInternal>>);
 
@@ -45,6 +51,38 @@ pub(crate) enum Form {
     NF,
 }
 
+#[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(ExprKind<Value, Normalized>),
+}
+
 impl Value {
     fn new(kind: ValueKind, form: Form, ty: Value, span: Span) -> Value {
         ValueInternal {
@@ -258,6 +296,94 @@ impl ValueInternal {
     }
 }
 
+impl ValueKind {
+    pub(crate) fn into_value_with_type(self, t: Value) -> Value {
+        Value::from_kind_and_type(self, t)
+    }
+
+    /// Converts a value back to the corresponding AST expression.
+    pub(crate) fn to_expr(
+        &self,
+        opts: to_expr::ToExprOptions,
+    ) -> NormalizedExpr {
+        to_expr::kind_to_expr(self, 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 Value {
     fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
         Some(Value(self.0.shift(delta, var)?))
@@ -275,6 +401,71 @@ impl Shift for ValueInternal {
     }
 }
 
+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 Value {
     fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self {
         match &*self.as_kind() {
@@ -303,6 +494,73 @@ impl Subst<Value> for ValueInternal {
     }
 }
 
+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),
+            ),
+        }
+    }
+}
+
 // TODO: use Rc comparison to shortcut on identical pointers
 impl std::cmp::PartialEq for Value {
     fn eq(&self, other: &Self) -> bool {
diff --git a/dhall/src/semantics/core/value_kind.rs b/dhall/src/semantics/core/value_kind.rs
deleted file mode 100644
index 35b2b23..0000000
--- a/dhall/src/semantics/core/value_kind.rs
+++ /dev/null
@@ -1,267 +0,0 @@
-use std::collections::HashMap;
-
-use crate::semantics::core::value::Value;
-use crate::semantics::core::var::{AlphaLabel, AlphaVar, Shift, Subst};
-use crate::semantics::phase::{Normalized, NormalizedExpr};
-use crate::semantics::to_expr;
-use crate::syntax::{
-    Builtin, Const, ExprKind, 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(ExprKind<Value, Normalized>),
-}
-
-impl ValueKind {
-    pub(crate) fn into_value_with_type(self, t: Value) -> Value {
-        Value::from_kind_and_type(self, t)
-    }
-
-    /// Converts a value back to the corresponding AST expression.
-    pub(crate) fn to_expr(
-        &self,
-        opts: to_expr::ToExprOptions,
-    ) -> NormalizedExpr {
-        to_expr::kind_to_expr(self, 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/phase/mod.rs b/dhall/src/semantics/phase/mod.rs
index 7c57c3f..b22120d 100644
--- a/dhall/src/semantics/phase/mod.rs
+++ b/dhall/src/semantics/phase/mod.rs
@@ -3,7 +3,7 @@ use std::path::Path;
 
 use crate::error::{EncodeError, Error, ImportError, TypeError};
 use crate::semantics::core::value::Value;
-use crate::semantics::core::value_kind::ValueKind;
+use crate::semantics::core::value::ValueKind;
 use crate::semantics::core::var::{AlphaVar, Shift, Subst};
 use crate::semantics::to_expr::ToExprOptions;
 use crate::syntax::binary;
diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs
index 3e612aa..d81a910 100644
--- a/dhall/src/semantics/phase/normalize.rs
+++ b/dhall/src/semantics/phase/normalize.rs
@@ -1,7 +1,7 @@
 use std::collections::HashMap;
 
 use crate::semantics::core::value::Value;
-use crate::semantics::core::value_kind::ValueKind;
+use crate::semantics::core::value::ValueKind;
 use crate::semantics::core::var::{AlphaLabel, AlphaVar, Shift, Subst};
 use crate::semantics::phase::Normalized;
 use crate::syntax;
diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs
index cf928d8..c439f74 100644
--- a/dhall/src/semantics/phase/typecheck.rs
+++ b/dhall/src/semantics/phase/typecheck.rs
@@ -4,7 +4,7 @@ use std::collections::HashMap;
 use crate::error::{TypeError, TypeMessage};
 use crate::semantics::core::context::TypecheckContext;
 use crate::semantics::core::value::Value;
-use crate::semantics::core::value_kind::ValueKind;
+use crate::semantics::core::value::ValueKind;
 use crate::semantics::core::var::{Shift, Subst};
 use crate::semantics::phase::normalize::merge_maps;
 use crate::semantics::phase::Normalized;
diff --git a/dhall/src/semantics/to_expr.rs b/dhall/src/semantics/to_expr.rs
index 6099976..b21fb29 100644
--- a/dhall/src/semantics/to_expr.rs
+++ b/dhall/src/semantics/to_expr.rs
@@ -1,5 +1,5 @@
 use crate::semantics::core::value::Value;
-use crate::semantics::core::value_kind::ValueKind;
+use crate::semantics::core::value::ValueKind;
 use crate::semantics::phase::typecheck::rc;
 use crate::semantics::phase::NormalizedExpr;
 use crate::syntax;