Clarify normalization to ensure we only nze once

4 files changed, 55 insertions, 58 deletions

diff --git a/dhall/src/semantics/builtins.rs b/dhall/src/semantics/builtins.rs
index 1357adf..85ef294 100644
--- a/dhall/src/semantics/builtins.rs
+++ b/dhall/src/semantics/builtins.rs
@@ -12,7 +12,7 @@ use std::collections::HashMap;
 use std::convert::TryInto;
 
 /// A partially applied builtin.
-/// Invariant: TODO
+/// Invariant: the evaluation of the given args must not be able to progress further
 #[derive(Debug, Clone)]
 pub(crate) struct BuiltinClosure<Value> {
     pub env: NzEnv,
@@ -41,9 +41,8 @@ impl BuiltinClosure<Value> {
         let types = self.types.iter().cloned().chain(once(f_ty)).collect();
         apply_builtin(self.b, args, ret_ty, types, self.env.clone())
     }
-    pub fn ensure_whnf(self, ret_ty: &Value) -> ValueKind {
-        apply_builtin(self.b, self.args, ret_ty, self.types, self.env)
-    }
+    /// This doesn't break the invariant because we already checked that the appropriate arguments
+    /// did not normalize to something that allows evaluation to proceed.
     pub fn normalize_mut(&mut self) {
         for x in self.args.iter_mut() {
             x.normalize_mut();
diff --git a/dhall/src/semantics/nze/env.rs b/dhall/src/semantics/nze/env.rs
index a083076..073886e 100644
--- a/dhall/src/semantics/nze/env.rs
+++ b/dhall/src/semantics/nze/env.rs
@@ -62,7 +62,7 @@ impl NzEnv {
     pub fn lookup_val(&self, var: &AlphaVar) -> Value {
         let idx = self.items.len() - 1 - var.idx();
         match &self.items[idx] {
-            NzEnvItem::Kept(ty) => Value::from_kind_and_type_whnf(
+            NzEnvItem::Kept(ty) => Value::from_kind_and_type(
                 ValueKind::Var(NzVar::new(idx)),
                 ty.clone(),
             ),
diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs
index 16c886e..7632d12 100644
--- a/dhall/src/semantics/nze/normalize.rs
+++ b/dhall/src/semantics/nze/normalize.rs
@@ -208,12 +208,12 @@ fn apply_binop<'a>(
                 _ => unreachable!("Internal type error"),
             };
             let kvs = merge_maps::<_, _, _, !>(kvs1, kvs2, |k, v1, v2| {
-                Ok(Value::from_kind_and_type(
-                    ValueKind::PartialExpr(ExprKind::BinOp(
+                Ok(Value::from_partial_expr(
+                    ExprKind::BinOp(
                         RecursiveRecordMerge,
                         v1.clone(),
                         v2.clone(),
-                    )),
+                    ),
                     kts.get(k).expect("Internal type error").clone(),
                 ))
             })?;
@@ -226,12 +226,12 @@ fn apply_binop<'a>(
                 kts_y,
                 // If the Label exists for both records, then we hit the recursive case.
                 |_, l: &Value, r: &Value| {
-                    Ok(Value::from_kind_and_type(
-                        ValueKind::PartialExpr(ExprKind::BinOp(
+                    Ok(Value::from_partial_expr(
+                        ExprKind::BinOp(
                             RecursiveRecordTypeMerge,
                             l.clone(),
                             r.clone(),
-                        )),
+                        ),
                         ty.clone(),
                     ))
                 },
@@ -444,16 +444,6 @@ pub(crate) fn normalize_one_layer(
     }
 }
 
-/// Normalize a ValueKind into WHNF
-pub(crate) fn normalize_whnf(v: ValueKind, ty: &Value) -> ValueKind {
-    match v {
-        ValueKind::AppliedBuiltin(closure) => closure.ensure_whnf(ty),
-        ValueKind::PartialExpr(e) => normalize_one_layer(e, ty, &NzEnv::new()),
-        // All other cases are already in WHNF
-        v => v,
-    }
-}
-
 /// Normalize a TyExpr into WHNF
 pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> Value {
     let ty = match tye.get_type() {
@@ -490,6 +480,5 @@ pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> Value {
         }
     };
 
-    // dbg!(tye.kind(), env, &kind);
-    Value::from_kind_and_type_whnf(kind, ty)
+    Value::from_kind_and_type(kind, ty)
 }
diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs
index 8ae0939..108dc9c 100644
--- a/dhall/src/semantics/nze/value.rs
+++ b/dhall/src/semantics/nze/value.rs
@@ -5,7 +5,7 @@ use std::rc::Rc;
 use crate::error::{TypeError, TypeMessage};
 use crate::semantics::Binder;
 use crate::semantics::{
-    apply_any, normalize_tyexpr_whnf, normalize_whnf, squash_textlit,
+    apply_any, normalize_one_layer, normalize_tyexpr_whnf, squash_textlit,
 };
 use crate::semantics::{type_of_builtin, typecheck, TyExpr, TyExprKind};
 use crate::semantics::{BuiltinClosure, NzEnv, NzVar, VarEnv};
@@ -16,34 +16,30 @@ use crate::syntax::{
 use crate::{Normalized, NormalizedExpr, ToExprOptions};
 
 /// 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
+/// automatically. Uses a Rc<RefCell> to share computation.
+/// If you compare for equality two `Value`s, 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>>);
 
-/// Invariant: if `form` is `WHNF`, `value` must be in Weak Head Normal Form
 #[derive(Debug)]
 struct ValueInternal {
     form: Form,
-    /// This is None if and only if `value` is `Sort` (which doesn't have a type)
+    /// This is None if and only if `form` is `Sort` (which doesn't have a type)
     ty: Option<Value>,
     span: Span,
 }
 
+/// A potentially un-evaluated expression. Once we get to WHNF we won't modify the form again, as
+/// explained in the doc for `ValueKind`.
 #[derive(Debug, Clone)]
 pub(crate) enum Form {
+    /// A totally unnormalized value.
     Thunk(Thunk),
-    /// No constraints; expression may not be normalized at all.
-    Unevaled(ValueKind),
-    /// 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 ValueKind is the first
-    /// constructor of the final Normal Form (NF).
-    /// When all the Values in a ValueKind are 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.
+    /// A partially normalized value that may need to go through `normalize_one_layer`.
+    PartialExpr(ExprKind<Value, Normalized>),
+    /// A value in WHNF.
     WHNF(ValueKind),
 }
 
@@ -73,6 +69,13 @@ pub(crate) enum Closure {
 #[derive(Debug, Clone, PartialEq, Eq)]
 pub(crate) struct TextLit(Vec<InterpolatedTextContents<Value>>);
 
+/// This represents a value in Weak Head Normal Form (WHNF). This means that the value is
+/// normalized up to the first constructor, but subexpressions may not be fully normalized.
+/// When all the Values in a ValueKind are in WHNF, and recursively so, then the ValueKind is in
+/// Normal Form (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.
+/// In particular, this means that once we get a `ValueKind`, it can be considered immutable, and
+/// we only need to recursively normalize its sub-`Value`s to get to the NF.
 #[derive(Debug, Clone, PartialEq, Eq)]
 pub(crate) enum ValueKind {
     /// Closures
@@ -86,7 +89,6 @@ pub(crate) enum ValueKind {
         annot: Value,
         closure: Closure,
     },
-    // Invariant: in whnf, the evaluation must not be able to progress further.
     AppliedBuiltin(BuiltinClosure<Value>),
 
     Var(NzVar),
@@ -109,7 +111,7 @@ pub(crate) enum ValueKind {
     UnionLit(Label, Value, HashMap<Label, Option<Value>>, Value, Value),
     TextLit(TextLit),
     Equivalence(Value, Value),
-    // Invariant: in whnf, this must not contain a value captured by one of the variants above.
+    /// Invariant: evaluation must not be able to progress with `normalize_one_layer`?
     PartialExpr(ExprKind<Value, Normalized>),
 }
 
@@ -130,6 +132,7 @@ impl Value {
         }
         .into_value()
     }
+    /// Construct a Value from a completely unnormalized expression.
     pub(crate) fn new_thunk(env: &NzEnv, tye: TyExpr) -> Value {
         ValueInternal {
             form: Form::Thunk(Thunk::new(env, tye.clone())),
@@ -138,10 +141,15 @@ impl Value {
         }
         .into_value()
     }
-    pub(crate) fn from_kind_and_type(v: ValueKind, t: Value) -> Value {
-        Value::new(Form::Unevaled(v), t, Span::Artificial)
+    /// Construct a Value from a partially normalized expression that's not in WHNF.
+    pub(crate) fn from_partial_expr(
+        e: ExprKind<Value, Normalized>,
+        t: Value,
+    ) -> Value {
+        Value::new(Form::PartialExpr(e), t, Span::Artificial)
     }
-    pub(crate) fn from_kind_and_type_whnf(v: ValueKind, t: Value) -> Value {
+    /// Make a Value from a ValueKind
+    pub(crate) fn from_kind_and_type(v: ValueKind, t: Value) -> Value {
         Value::new(Form::WHNF(v), t, Span::Artificial)
     }
     pub(crate) fn from_const(c: Const) -> Self {
@@ -188,7 +196,7 @@ impl Value {
     pub(crate) fn kind(&self) -> Ref<ValueKind> {
         self.normalize_whnf();
         Ref::map(self.as_internal(), |vint| match &vint.form {
-            Form::Thunk(..) | Form::Unevaled(..) => unreachable!(),
+            Form::Thunk(..) | Form::PartialExpr(..) => unreachable!(),
             Form::WHNF(k) => k,
         })
     }
@@ -228,7 +236,7 @@ impl Value {
     pub(crate) fn normalize_whnf(&self) {
         let borrow = self.as_internal();
         match borrow.form {
-            Form::Thunk(..) | Form::Unevaled(_) => {
+            Form::Thunk(..) | Form::PartialExpr(_) => {
                 drop(borrow);
                 self.as_internal_mut().normalize_whnf();
             }
@@ -248,10 +256,7 @@ impl Value {
             }
             _ => unreachable!("Internal type error"),
         };
-        Value::from_kind_and_type_whnf(
-            apply_any(self.clone(), v, &body_t),
-            body_t,
-        )
+        Value::from_kind_and_type(apply_any(self.clone(), v, &body_t), body_t)
     }
 
     /// In debug mode, panic if the provided type doesn't match the value's type.
@@ -398,12 +403,13 @@ impl ValueInternal {
 
     fn normalize_whnf(&mut self) {
         use std::mem::replace;
-        let dummy = Form::Unevaled(ValueKind::Const(Const::Type));
+        let dummy = Form::PartialExpr(ExprKind::Const(Const::Type));
         self.form = match replace(&mut self.form, dummy) {
             Form::Thunk(th) => Form::WHNF(th.eval().kind().clone()),
-            Form::Unevaled(kind) => {
+            Form::PartialExpr(e) => {
                 Form::WHNF(match &self.ty {
-                    Some(ty) => normalize_whnf(kind, &ty),
+                    // TODO: env
+                    Some(ty) => normalize_one_layer(e, &ty, &NzEnv::new()),
                     // `value` is `Sort`
                     None => ValueKind::Const(Const::Sort),
                 })
@@ -413,11 +419,11 @@ impl ValueInternal {
         };
     }
     fn normalize_nf(&mut self) {
-        if let Form::Thunk(..) | Form::Unevaled(_) = self.form {
+        if let Form::Thunk(..) | Form::PartialExpr(_) = self.form {
             self.normalize_whnf();
         }
         match &mut self.form {
-            Form::Thunk(..) | Form::Unevaled(_) => unreachable!(),
+            Form::Thunk(..) | Form::PartialExpr(_) => unreachable!(),
             Form::WHNF(k) => k.normalize_mut(),
         }
     }
@@ -451,9 +457,10 @@ impl ValueKind {
             ValueKind::NEOptionalLit(th) => {
                 th.normalize_mut();
             }
-            ValueKind::LamClosure { annot, .. }
-            | ValueKind::PiClosure { annot, .. } => {
+            ValueKind::LamClosure { annot, closure, .. }
+            | ValueKind::PiClosure { annot, closure, .. } => {
                 annot.normalize_mut();
+                closure.normalize_mut();
             }
             ValueKind::AppliedBuiltin(closure) => closure.normalize_mut(),
             ValueKind::NEListLit(elts) => {
@@ -553,6 +560,8 @@ impl Closure {
         }
     }
 
+    // TODO: somehow normalize the body. Might require to pass an env.
+    pub fn normalize_mut(&mut self) {}
     /// Convert this closure to a TyExpr
     pub fn to_tyexpr(&self, venv: VarEnv) -> TyExpr {
         self.apply_var(NzVar::new(venv.size()))
@@ -665,9 +674,9 @@ impl std::fmt::Debug for Value {
                 x.field("thunk", th);
                 x
             }
-            Form::Unevaled(kind) => {
-                let mut x = fmt.debug_struct(&format!("Value@Unevaled"));
-                x.field("kind", kind);
+            Form::PartialExpr(e) => {
+                let mut x = fmt.debug_struct(&format!("Value@PartialExpr"));
+                x.field("expr", e);
                 x
             }
             Form::WHNF(kind) => {