Track evaluation status alongside ValueF in VoVF

3 files changed, 80 insertions, 68 deletions

diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs
index 64a4842..b44dad6 100644
--- a/dhall/src/core/value.rs
+++ b/dhall/src/core/value.rs
@@ -12,7 +12,7 @@ use crate::phase::typecheck::{builtin_to_value, const_to_value};
 use crate::phase::{NormalizedSubExpr, Typed};
 
 #[derive(Debug, Clone, Copy)]
-enum Form {
+pub 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
@@ -46,9 +46,10 @@ pub 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 enum VoVF {
     Value(Value),
-    ValueF(ValueF),
+    ValueF { val: ValueF, form: Form },
 }
 
 impl ValueInternal {
@@ -98,24 +99,14 @@ impl ValueInternal {
 }
 
 impl Value {
+    pub(crate) fn new(value: ValueF, form: Form, ty: Option<Value>) -> Value {
+        ValueInternal { form, value, ty }.into_value()
+    }
     pub(crate) fn from_valuef_untyped(v: ValueF) -> Value {
-        ValueInternal {
-            form: Unevaled,
-            value: v,
-            ty: None,
-        }
-        .into_value()
+        Value::new(v, Unevaled, None)
     }
     pub(crate) fn from_valuef_and_type(v: ValueF, t: Value) -> Value {
-        ValueInternal {
-            form: Unevaled,
-            value: v,
-            ty: Some(t),
-        }
-        .into_value()
-    }
-    pub(crate) fn from_valuef_simple_type(v: ValueF) -> Value {
-        Value::from_valuef_and_type(v, Value::from_const(Const::Type))
+        Value::new(v, Unevaled, Some(t))
     }
     pub(crate) fn from_const(c: Const) -> Self {
         const_to_value(c)
@@ -236,34 +227,35 @@ impl VoVF {
     pub fn into_whnf(self) -> ValueF {
         match self {
             VoVF::Value(v) => v.to_whnf(),
-            VoVF::ValueF(v) => v,
+            VoVF::ValueF {
+                val,
+                form: Unevaled,
+            } => normalize_whnf(val).into_whnf(),
+            // Already at lest in WHNF
+            VoVF::ValueF { val, .. } => val,
         }
     }
     pub(crate) fn into_value_untyped(self) -> Value {
         match self {
             VoVF::Value(v) => v,
-            VoVF::ValueF(v) => v.into_value_untyped(),
+            VoVF::ValueF { val, form } => Value::new(val, form, None),
         }
     }
     pub(crate) fn into_value_with_type(self, t: Value) -> Value {
         match self {
             // TODO: check type with debug_assert ?
             VoVF::Value(v) => v,
-            VoVF::ValueF(v) => v.into_value_with_type(t),
+            VoVF::ValueF { val, form } => Value::new(val, form, Some(t)),
         }
     }
     pub(crate) fn into_value_simple_type(self) -> Value {
-        match self {
-            // TODO: check type with debug_assert ?
-            VoVF::Value(v) => v,
-            VoVF::ValueF(v) => v.into_value_simple_type(),
-        }
+        self.into_value_with_type(Value::from_const(Const::Type))
     }
 
     pub(crate) fn app(self, x: Value) -> Self {
         match self {
             VoVF::Value(v) => v.app(x),
-            VoVF::ValueF(v) => v.into_value_untyped().app(x),
+            VoVF::ValueF { val, .. } => val.into_value_untyped().app(x),
         }
     }
 }
diff --git a/dhall/src/core/valuef.rs b/dhall/src/core/valuef.rs
index 80978a7..db8a284 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::{Value, VoVF};
+use crate::core::value::{Form, Value, VoVF};
 use crate::core::var::{AlphaLabel, AlphaVar, Shift, Subst};
 use crate::phase::{Normalized, NormalizedSubExpr};
 
@@ -19,7 +19,7 @@ pub 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),
@@ -33,16 +33,16 @@ 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>),
 }
 
@@ -53,11 +53,23 @@ impl ValueF {
     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)
+    pub(crate) fn into_vovf_unevaled(self) -> VoVF {
+        VoVF::ValueF {
+            val: self,
+            form: Form::Unevaled,
+        }
+    }
+    pub(crate) fn into_vovf_whnf(self) -> VoVF {
+        VoVF::ValueF {
+            val: self,
+            form: Form::WHNF,
+        }
     }
-    pub(crate) fn into_vovf(self) -> VoVF {
-        VoVF::ValueF(self)
+    pub(crate) fn into_vovf_nf(self) -> VoVF {
+        VoVF::ValueF {
+            val: self,
+            form: Form::NF,
+        }
     }
 
     /// Convert the value to a fully normalized syntactic expression
@@ -261,7 +273,7 @@ impl ValueF {
 
     /// Apply to a value
     pub fn app(self, v: Value) -> VoVF {
-        self.into_vovf().app(v)
+        self.into_vovf_unevaled().app(v)
     }
 
     pub fn from_builtin(b: Builtin) -> ValueF {
diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs
index e044018..a146ec7 100644
--- a/dhall/src/phase/normalize.rs
+++ b/dhall/src/phase/normalize.rs
@@ -70,29 +70,29 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> VoVF {
     // Return Ok((unconsumed args, returned value)), or Err(()) if value could not be produced.
     let ret = match (b, args.as_slice()) {
         (OptionalNone, [t, r..]) => {
-            Ok((r, EmptyOptionalLit(t.clone()).into_vovf()))
+            Ok((r, EmptyOptionalLit(t.clone()).into_vovf_whnf()))
         }
         (NaturalIsZero, [n, r..]) => match &*n.as_whnf() {
-            NaturalLit(n) => Ok((r, BoolLit(*n == 0).into_vovf())),
+            NaturalLit(n) => Ok((r, BoolLit(*n == 0).into_vovf_nf())),
             _ => Err(()),
         },
         (NaturalEven, [n, r..]) => match &*n.as_whnf() {
-            NaturalLit(n) => Ok((r, BoolLit(*n % 2 == 0).into_vovf())),
+            NaturalLit(n) => Ok((r, BoolLit(*n % 2 == 0).into_vovf_nf())),
             _ => Err(()),
         },
         (NaturalOdd, [n, r..]) => match &*n.as_whnf() {
-            NaturalLit(n) => Ok((r, BoolLit(*n % 2 != 0).into_vovf())),
+            NaturalLit(n) => Ok((r, BoolLit(*n % 2 != 0).into_vovf_nf())),
             _ => Err(()),
         },
         (NaturalToInteger, [n, r..]) => match &*n.as_whnf() {
-            NaturalLit(n) => Ok((r, IntegerLit(*n as isize).into_vovf())),
+            NaturalLit(n) => Ok((r, IntegerLit(*n as isize).into_vovf_nf())),
             _ => Err(()),
         },
         (NaturalShow, [n, r..]) => match &*n.as_whnf() {
             NaturalLit(n) => Ok((
                 r,
                 TextLit(vec![InterpolatedTextContents::Text(n.to_string())])
-                    .into_vovf(),
+                    .into_vovf_nf(),
             )),
             _ => Err(()),
         },
@@ -100,11 +100,11 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> VoVF {
             match (&*a.as_whnf(), &*b.as_whnf()) {
                 (NaturalLit(a), NaturalLit(b)) => Ok((
                     r,
-                    NaturalLit(if b > a { b - a } else { 0 }).into_vovf(),
+                    NaturalLit(if b > a { b - a } else { 0 }).into_vovf_nf(),
                 )),
                 (NaturalLit(0), _) => Ok((r, b.clone().into_vovf())),
-                (_, NaturalLit(0)) => Ok((r, NaturalLit(0).into_vovf())),
-                _ if a == b => Ok((r, NaturalLit(0).into_vovf())),
+                (_, NaturalLit(0)) => Ok((r, NaturalLit(0).into_vovf_nf())),
+                _ if a == b => Ok((r, NaturalLit(0).into_vovf_nf())),
                 _ => Err(()),
             }
         }
@@ -118,14 +118,14 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> VoVF {
                 Ok((
                     r,
                     TextLit(vec![InterpolatedTextContents::Text(s)])
-                        .into_vovf(),
+                        .into_vovf_nf(),
                 ))
             }
             _ => Err(()),
         },
         (IntegerToDouble, [n, r..]) => match &*n.as_whnf() {
             IntegerLit(n) => {
-                Ok((r, DoubleLit(NaiveDouble::from(*n as f64)).into_vovf()))
+                Ok((r, DoubleLit(NaiveDouble::from(*n as f64)).into_vovf_nf()))
             }
             _ => Err(()),
         },
@@ -133,7 +133,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> VoVF {
             DoubleLit(n) => Ok((
                 r,
                 TextLit(vec![InterpolatedTextContents::Text(n.to_string())])
-                    .into_vovf(),
+                    .into_vovf_nf(),
             )),
             _ => Err(()),
         },
@@ -149,7 +149,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> VoVF {
                         Ok((
                             r,
                             TextLit(vec![InterpolatedTextContents::Text(s)])
-                                .into_vovf(),
+                                .into_vovf_nf(),
                         ))
                     }
                     // If there are no interpolations (invariants ensure that when there are no
@@ -165,7 +165,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> VoVF {
                         Ok((
                             r,
                             TextLit(vec![InterpolatedTextContents::Text(s)])
-                                .into_vovf(),
+                                .into_vovf_nf(),
                         ))
                     }
                     _ => Err(()),
@@ -174,32 +174,39 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> VoVF {
             _ => Err(()),
         },
         (ListLength, [_, l, r..]) => match &*l.as_whnf() {
-            EmptyListLit(_) => Ok((r, NaturalLit(0).into_vovf())),
-            NEListLit(xs) => Ok((r, NaturalLit(xs.len()).into_vovf())),
+            EmptyListLit(_) => Ok((r, NaturalLit(0).into_vovf_nf())),
+            NEListLit(xs) => Ok((r, NaturalLit(xs.len()).into_vovf_nf())),
             _ => Err(()),
         },
         (ListHead, [_, l, r..]) => match &*l.as_whnf() {
-            EmptyListLit(n) => Ok((r, EmptyOptionalLit(n.clone()).into_vovf())),
+            EmptyListLit(n) => {
+                Ok((r, EmptyOptionalLit(n.clone()).into_vovf_whnf()))
+            }
             NEListLit(xs) => Ok((
                 r,
-                NEOptionalLit(xs.iter().next().unwrap().clone()).into_vovf(),
+                NEOptionalLit(xs.iter().next().unwrap().clone())
+                    .into_vovf_whnf(),
             )),
             _ => Err(()),
         },
         (ListLast, [_, l, r..]) => match &*l.as_whnf() {
-            EmptyListLit(n) => Ok((r, EmptyOptionalLit(n.clone()).into_vovf())),
+            EmptyListLit(n) => {
+                Ok((r, EmptyOptionalLit(n.clone()).into_vovf_whnf()))
+            }
             NEListLit(xs) => Ok((
                 r,
                 NEOptionalLit(xs.iter().rev().next().unwrap().clone())
-                    .into_vovf(),
+                    .into_vovf_whnf(),
             )),
             _ => Err(()),
         },
         (ListReverse, [_, l, r..]) => match &*l.as_whnf() {
-            EmptyListLit(n) => Ok((r, EmptyListLit(n.clone()).into_vovf())),
+            EmptyListLit(n) => {
+                Ok((r, EmptyListLit(n.clone()).into_vovf_whnf()))
+            }
             NEListLit(xs) => Ok((
                 r,
-                NEListLit(xs.iter().rev().cloned().collect()).into_vovf(),
+                NEListLit(xs.iter().rev().cloned().collect()).into_vovf_whnf(),
             )),
             _ => Err(()),
         },
@@ -211,7 +218,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> VoVF {
                 Ok((
                     r,
                     EmptyListLit(Value::from_valuef_untyped(RecordType(kts)))
-                        .into_vovf(),
+                        .into_vovf_whnf(),
                 ))
             }
             NEListLit(xs) => {
@@ -229,7 +236,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> VoVF {
                         Value::from_valuef_untyped(RecordLit(kvs))
                     })
                     .collect();
-                Ok((r, NEListLit(xs).into_vovf()))
+                Ok((r, NEListLit(xs).into_vovf_whnf()))
             }
             _ => Err(()),
         },
@@ -353,13 +360,14 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> VoVF {
             }
             v
         }
-        Err(()) => AppliedBuiltin(b, args).into_vovf(),
+        Err(()) => AppliedBuiltin(b, args).into_vovf_whnf(),
     }
 }
 
 pub(crate) fn apply_any(f: Value, a: Value) -> VoVF {
-    let fallback =
-        |f: Value, a: Value| ValueF::PartialExpr(ExprF::App(f, a)).into_vovf();
+    let fallback = |f: Value, a: Value| {
+        ValueF::PartialExpr(ExprF::App(f, a)).into_vovf_whnf()
+    };
 
     let f_borrow = f.as_whnf();
     match &*f_borrow {
@@ -370,7 +378,7 @@ pub(crate) fn apply_any(f: Value, a: Value) -> VoVF {
             apply_builtin(*b, args)
         }
         ValueF::UnionConstructor(l, kts) => {
-            ValueF::UnionLit(l.clone(), a, kts.clone()).into_vovf()
+            ValueF::UnionLit(l.clone(), a, kts.clone()).into_vovf_whnf()
         }
         _ => {
             drop(f_borrow);
@@ -774,11 +782,11 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> VoVF {
     };
 
     match ret {
-        Ret::ValueF(v) => v.into_vovf(),
+        Ret::ValueF(v) => v.into_vovf_whnf(),
         Ret::Value(v) => v.into_vovf(),
         Ret::VoVF(v) => v,
         Ret::ValueRef(v) => v.clone().into_vovf(),
-        Ret::Expr(expr) => ValueF::PartialExpr(expr).into_vovf(),
+        Ret::Expr(expr) => ValueF::PartialExpr(expr).into_vovf_whnf(),
     }
 }
 
@@ -788,9 +796,9 @@ pub(crate) fn normalize_whnf(v: ValueF) -> VoVF {
         ValueF::AppliedBuiltin(b, args) => apply_builtin(b, args),
         ValueF::PartialExpr(e) => normalize_one_layer(e),
         ValueF::TextLit(elts) => {
-            ValueF::TextLit(squash_textlit(elts.into_iter())).into_vovf()
+            ValueF::TextLit(squash_textlit(elts.into_iter())).into_vovf_whnf()
         }
         // All other cases are already in WHNF
-        v => v.into_vovf(),
+        v => v.into_vovf_whnf(),
     }
 }