1 files changed, 10 insertions, 32 deletions

diff --git a/dhall/src/core/valuef.rs b/dhall/src/core/valuef.rs
index 0c3058d..9ea2467 100644
--- a/dhall/src/core/valuef.rs
+++ b/dhall/src/core/valuef.rs
@@ -7,8 +7,7 @@ use dhall_syntax::{
 
 use crate::core::value::Value;
 use crate::core::var::{AlphaLabel, AlphaVar, Shift, Subst};
-use crate::phase::normalize::OutputSubExpr;
-use crate::phase::Normalized;
+use crate::phase::{Normalized, NormalizedSubExpr};
 
 /// A semantic value. Subexpressions are Values, which are partially evaluated expressions that are
 /// normalized on-demand.
@@ -16,11 +15,11 @@ use crate::phase::Normalized;
 /// alpha-equivalence (renaming of bound variables) and beta-equivalence (normalization). It will
 /// recursively normalize as needed.
 #[derive(Debug, Clone, PartialEq, Eq)]
-pub enum ValueF {
+pub(crate) enum ValueF {
     /// Closures
     Lam(AlphaLabel, Value, Value),
     Pi(AlphaLabel, Value, Value),
-    // Invariant: the evaluation must not be able to progress further.
+    // Invariant: in whnf, the evaluation must not be able to progress further.
     AppliedBuiltin(Builtin, Vec<Value>),
 
     Var(AlphaVar),
@@ -34,32 +33,26 @@ pub enum ValueF {
     // EmptyListLit(t) means `[] : List t`, not `[] : t`
     EmptyListLit(Value),
     NEListLit(Vec<Value>),
-    RecordLit(HashMap<Label, 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: this must not contain interpolations that are themselves TextLits, and
+    // 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: this must not contain a value captured by one of the variants above.
+    // 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_untyped(self) -> Value {
-        Value::from_valuef_untyped(self)
-    }
     pub(crate) fn into_value_with_type(self, t: Value) -> Value {
         Value::from_valuef_and_type(self, t)
     }
-    pub(crate) fn into_value_simple_type(self) -> Value {
-        Value::from_valuef_simple_type(self)
-    }
 
     /// Convert the value to a fully normalized syntactic expression
-    pub(crate) fn normalize_to_expr(&self) -> OutputSubExpr {
+    pub(crate) fn normalize_to_expr(&self) -> NormalizedSubExpr {
         self.normalize_to_expr_maybe_alpha(false)
     }
     /// Convert the value to a fully normalized syntactic expression. Also alpha-normalize
@@ -67,7 +60,7 @@ impl ValueF {
     pub(crate) fn normalize_to_expr_maybe_alpha(
         &self,
         alpha: bool,
-    ) -> OutputSubExpr {
+    ) -> NormalizedSubExpr {
         match self {
             ValueF::Lam(x, t, e) => rc(ExprF::Lam(
                 x.to_label_maybe_alpha(alpha),
@@ -257,22 +250,7 @@ impl ValueF {
         }
     }
 
-    /// Apply to a valuef
-    pub(crate) fn app(self, val: ValueF) -> ValueF {
-        self.app_valuef(val)
-    }
-
-    /// Apply to a valuef
-    pub(crate) fn app_valuef(self, val: ValueF) -> ValueF {
-        self.app_value(val.into_value_untyped())
-    }
-
-    /// Apply to a value
-    pub fn app_value(self, th: Value) -> ValueF {
-        Value::from_valuef_untyped(self).app_value(th)
-    }
-
-    pub fn from_builtin(b: Builtin) -> ValueF {
+    pub(crate) fn from_builtin(b: Builtin) -> ValueF {
         ValueF::AppliedBuiltin(b, vec![])
     }
 }
@@ -355,7 +333,7 @@ impl Subst<Value> for ValueF {
                 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(),
+            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),