Remove now unnecessary VoVF enum

3 files changed, 53 insertions, 98 deletions

diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs
index 2554da1..13f8e59 100644
--- a/dhall/src/core/value.rs
+++ b/dhall/src/core/value.rs
@@ -44,15 +44,6 @@ struct ValueInternal {
 #[derive(Clone)]
 pub(crate) struct Value(Rc<RefCell<ValueInternal>>);
 
-/// When a function needs to return either a freshly created ValueF or an existing Value, but
-/// doesn't want to convert both to the same thing, either to avoid unnecessary allocations or to
-/// avoid loss of typ information.
-#[derive(Debug, Clone)]
-pub(crate) enum VoVF {
-    Value(Value),
-    ValueF { val: ValueF, form: Form },
-}
-
 impl ValueInternal {
     fn into_value(self) -> Value {
         Value(Rc::new(RefCell::new(self)))
@@ -76,15 +67,11 @@ impl ValueInternal {
                     value: ValueF::Const(Const::Sort),
                     ty: None,
                 },
-                (Unevaled, Some(ty)) => {
-                    let new_value =
-                        normalize_whnf(vint.value, &ty).into_whnf(&ty);
-                    ValueInternal {
-                        form: WHNF,
-                        value: new_value,
-                        ty: vint.ty,
-                    }
-                }
+                (Unevaled, Some(ty)) => ValueInternal {
+                    form: WHNF,
+                    value: normalize_whnf(vint.value, &ty),
+                    ty: vint.ty,
+                },
                 // Already in WHNF
                 (WHNF, _) | (NF, _) => vint,
             },
@@ -135,6 +122,9 @@ impl Value {
     pub(crate) fn from_valuef_and_type(v: ValueF, t: Value) -> Value {
         Value::new(v, Unevaled, t)
     }
+    pub(crate) fn from_valuef_and_type_whnf(v: ValueF, t: Value) -> Value {
+        Value::new(v, WHNF, t)
+    }
     pub(crate) fn from_const(c: Const) -> Self {
         const_to_value(c)
     }
@@ -182,16 +172,22 @@ impl Value {
     pub(crate) fn to_expr_alpha(&self) -> NormalizedSubExpr {
         self.as_whnf().normalize_to_expr_maybe_alpha(true)
     }
-    /// TODO: cloning a valuef can often be avoided
-    pub(crate) fn to_whnf(&self) -> ValueF {
+    pub(crate) fn to_whnf_ignore_type(&self) -> ValueF {
         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 {
+        let self_ty = self.get_type().ok();
+        debug_assert_eq!(
+            Some(ty),
+            self_ty.as_ref(),
+            "The value returned from normalization doesn't have the expected type."
+        );
+        self.to_whnf_ignore_type()
+    }
     pub(crate) fn into_typed(self) -> Typed {
         Typed::from_value(self)
     }
-    pub(crate) fn into_vovf(self) -> VoVF {
-        VoVF::Value(self)
-    }
 
     /// Mutates the contents. If no one else shares this, this avoids a RefCell lock.
     fn mutate_internal(&mut self, f: impl FnOnce(&mut ValueInternal)) {
@@ -239,16 +235,14 @@ impl Value {
     }
 
     pub(crate) fn app(&self, v: Value) -> Value {
-        let t = self.get_type_not_sort();
-        let vovf = apply_any(self.clone(), v.clone(), &t);
-        let t_borrow = t.as_whnf();
-        match &*t_borrow {
-            ValueF::Pi(x, _, e) => {
-                let t = e.subst_shift(&x.into(), &v);
-                vovf.into_value_with_type(t)
-            }
+        let body_t = match &*self.get_type_not_sort().as_whnf() {
+            ValueF::Pi(x, _, e) => e.subst_shift(&x.into(), &v),
             _ => unreachable!("Internal type error"),
-        }
+        };
+        Value::from_valuef_and_type_whnf(
+            apply_any(self.clone(), v, &body_t),
+            body_t,
+        )
     }
 
     pub(crate) fn get_type(&self) -> Result<Value, TypeError> {
@@ -261,42 +255,6 @@ impl Value {
     }
 }
 
-impl VoVF {
-    pub(crate) fn into_whnf(self, ty: &Value) -> ValueF {
-        match self {
-            VoVF::ValueF {
-                val,
-                form: Unevaled,
-            } => normalize_whnf(val, ty).into_whnf(ty),
-            // Already at lest in WHNF
-            VoVF::ValueF { val, .. } => val,
-            VoVF::Value(v) => {
-                let v_ty = v.get_type().ok();
-                debug_assert_eq!(
-                    Some(ty),
-                    v_ty.as_ref(),
-                    "The type recovered from normalization doesn't match the stored type."
-                );
-                v.to_whnf()
-            }
-        }
-    }
-    pub(crate) fn into_value_with_type(self, ty: Value) -> Value {
-        match self {
-            VoVF::Value(v) => {
-                let v_ty = v.get_type().ok();
-                debug_assert_eq!(
-                    Some(&ty),
-                    v_ty.as_ref(),
-                    "The type recovered from normalization doesn't match the stored type."
-                );
-                v
-            }
-            VoVF::ValueF { val, form } => Value::new(val, form, ty),
-        }
-    }
-}
-
 impl Shift for Value {
     fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
         Some(Value(self.0.shift(delta, var)?))
@@ -324,6 +282,7 @@ impl Subst<Value> for ValueInternal {
         ValueInternal {
             // The resulting value may not stay in wnhf after substitution
             form: Unevaled,
+            // TODO: check type info if self.value if Var(v) and v == var
             value: self.value.subst_shift(var, val),
             ty: self.ty.subst_shift(var, val),
         }
diff --git a/dhall/src/core/valuef.rs b/dhall/src/core/valuef.rs
index 5638078..9ea2467 100644
--- a/dhall/src/core/valuef.rs
+++ b/dhall/src/core/valuef.rs
@@ -5,7 +5,7 @@ use dhall_syntax::{
     NaiveDouble, Natural,
 };
 
-use crate::core::value::{Form, Value, VoVF};
+use crate::core::value::Value;
 use crate::core::var::{AlphaLabel, AlphaVar, Shift, Subst};
 use crate::phase::{Normalized, NormalizedSubExpr};
 
@@ -50,12 +50,6 @@ impl ValueF {
     pub(crate) fn into_value_with_type(self, t: Value) -> Value {
         Value::from_valuef_and_type(self, t)
     }
-    pub(crate) fn into_vovf_whnf(self) -> VoVF {
-        VoVF::ValueF {
-            val: self,
-            form: Form::WHNF,
-        }
-    }
 
     /// Convert the value to a fully normalized syntactic expression
     pub(crate) fn normalize_to_expr(&self) -> NormalizedSubExpr {
@@ -339,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),
diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs
index 77f5023..82a378c 100644
--- a/dhall/src/phase/normalize.rs
+++ b/dhall/src/phase/normalize.rs
@@ -6,7 +6,7 @@ use dhall_syntax::{
     NaiveDouble,
 };
 
-use crate::core::value::{Value, VoVF};
+use crate::core::value::Value;
 use crate::core::valuef::ValueF;
 use crate::core::var::{AlphaLabel, Shift, Subst};
 use crate::phase::Normalized;
@@ -71,7 +71,11 @@ macro_rules! make_closure {
 }
 
 #[allow(clippy::cognitive_complexity)]
-pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>, _ty: &Value) -> VoVF {
+pub(crate) fn apply_builtin(
+    b: Builtin,
+    args: Vec<Value>,
+    ty: &Value,
+) -> ValueF {
     use dhall_syntax::Builtin::*;
     use ValueF::*;
 
@@ -370,38 +374,36 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>, _ty: &Value) -> VoVF {
         _ => Ret::DoneAsIs,
     };
     match ret {
-        Ret::ValueF(v) => v.into_vovf_whnf(),
-        Ret::Value(v) => v.into_vovf(),
+        Ret::ValueF(v) => v,
+        Ret::Value(v) => v.to_whnf_check_type(ty),
         Ret::ValueWithRemainingArgs(unconsumed_args, mut v) => {
             let n_consumed_args = args.len() - unconsumed_args.len();
             for x in args.into_iter().skip(n_consumed_args) {
                 v = v.app(x);
             }
-            v.into_vovf()
+            v.to_whnf_check_type(ty)
         }
-        Ret::DoneAsIs => AppliedBuiltin(b, args).into_vovf_whnf(),
+        Ret::DoneAsIs => AppliedBuiltin(b, args),
     }
 }
 
-pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> VoVF {
-    let fallback = |f: Value, a: Value| {
-        ValueF::PartialExpr(ExprF::App(f, a)).into_vovf_whnf()
-    };
-
+pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueF {
     let f_borrow = f.as_whnf();
     match &*f_borrow {
-        ValueF::Lam(x, _, e) => e.subst_shift(&x.into(), &a).into_vovf(),
+        ValueF::Lam(x, _, e) => {
+            e.subst_shift(&x.into(), &a).to_whnf_check_type(ty)
+        }
         ValueF::AppliedBuiltin(b, args) => {
             use std::iter::once;
             let args = args.iter().cloned().chain(once(a.clone())).collect();
             apply_builtin(*b, args, ty)
         }
         ValueF::UnionConstructor(l, kts) => {
-            ValueF::UnionLit(l.clone(), a, kts.clone()).into_vovf_whnf()
+            ValueF::UnionLit(l.clone(), a, kts.clone())
         }
         _ => {
             drop(f_borrow);
-            fallback(f, a)
+            ValueF::PartialExpr(ExprF::App(f, a))
         }
     }
 }
@@ -609,7 +611,7 @@ fn apply_binop<'a>(
 pub(crate) fn normalize_one_layer(
     expr: ExprF<Value, Normalized>,
     ty: &Value,
-) -> VoVF {
+) -> ValueF {
     use ValueF::{
         AppliedBuiltin, BoolLit, DoubleLit, EmptyListLit, IntegerLit,
         NEListLit, NEOptionalLit, NaturalLit, RecordLit, TextLit,
@@ -766,22 +768,22 @@ pub(crate) fn normalize_one_layer(
     };
 
     match ret {
-        Ret::ValueF(v) => v.into_vovf_whnf(),
-        Ret::Value(v) => v.into_vovf(),
-        Ret::ValueRef(v) => v.clone().into_vovf(),
-        Ret::Expr(expr) => ValueF::PartialExpr(expr).into_vovf_whnf(),
+        Ret::ValueF(v) => v,
+        Ret::Value(v) => v.to_whnf_check_type(ty),
+        Ret::ValueRef(v) => v.to_whnf_check_type(ty),
+        Ret::Expr(expr) => ValueF::PartialExpr(expr),
     }
 }
 
 /// Normalize a ValueF into WHNF
-pub(crate) fn normalize_whnf(v: ValueF, ty: &Value) -> VoVF {
+pub(crate) fn normalize_whnf(v: ValueF, ty: &Value) -> ValueF {
     match v {
         ValueF::AppliedBuiltin(b, args) => apply_builtin(b, args, ty),
         ValueF::PartialExpr(e) => normalize_one_layer(e, ty),
         ValueF::TextLit(elts) => {
-            ValueF::TextLit(squash_textlit(elts.into_iter())).into_vovf_whnf()
+            ValueF::TextLit(squash_textlit(elts.into_iter()))
         }
         // All other cases are already in WHNF
-        v => v.into_vovf_whnf(),
+        v => v,
     }
 }