Move Thunk value into ValueInternal

2 files changed, 32 insertions, 35 deletions

diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs
index 89424e9..16c886e 100644
--- a/dhall/src/semantics/nze/normalize.rs
+++ b/dhall/src/semantics/nze/normalize.rs
@@ -449,7 +449,6 @@ 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()),
-        ValueKind::Thunk(th) => th.eval().kind().clone(),
         // All other cases are already in WHNF
         v => v,
     }
diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs
index 31acb11..8ae0939 100644
--- a/dhall/src/semantics/nze/value.rs
+++ b/dhall/src/semantics/nze/value.rs
@@ -15,8 +15,6 @@ use crate::syntax::{
 };
 use crate::{Normalized, NormalizedExpr, ToExprOptions};
 
-use self::Form::{Unevaled, WHNF};
-
 /// 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.
@@ -37,6 +35,7 @@ struct ValueInternal {
 
 #[derive(Debug, Clone)]
 pub(crate) enum Form {
+    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
@@ -112,8 +111,6 @@ pub(crate) enum ValueKind {
     Equivalence(Value, Value),
     // Invariant: in whnf, this must not contain a value captured by one of the variants above.
     PartialExpr(ExprKind<Value, Normalized>),
-    // Invariant: absent in whnf
-    Thunk(Thunk),
 }
 
 impl Value {
@@ -127,7 +124,7 @@ impl Value {
     }
     pub(crate) fn const_sort() -> Value {
         ValueInternal {
-            form: WHNF(ValueKind::Const(Const::Sort)),
+            form: Form::WHNF(ValueKind::Const(Const::Sort)),
             ty: None,
             span: Span::Artificial,
         }
@@ -135,17 +132,17 @@ impl Value {
     }
     pub(crate) fn new_thunk(env: &NzEnv, tye: TyExpr) -> Value {
         ValueInternal {
-            form: Unevaled(ValueKind::Thunk(Thunk::new(env, tye.clone()))),
+            form: Form::Thunk(Thunk::new(env, tye.clone())),
             ty: tye.get_type().ok(),
             span: tye.span().clone(),
         }
         .into_value()
     }
     pub(crate) fn from_kind_and_type(v: ValueKind, t: Value) -> Value {
-        Value::new(Unevaled(v), t, Span::Artificial)
+        Value::new(Form::Unevaled(v), t, Span::Artificial)
     }
     pub(crate) fn from_kind_and_type_whnf(v: ValueKind, t: Value) -> Value {
-        Value::new(WHNF(v), t, Span::Artificial)
+        Value::new(Form::WHNF(v), t, Span::Artificial)
     }
     pub(crate) fn from_const(c: Const) -> Self {
         let v = ValueKind::Const(c);
@@ -191,8 +188,8 @@ impl Value {
     pub(crate) fn kind(&self) -> Ref<ValueKind> {
         self.normalize_whnf();
         Ref::map(self.as_internal(), |vint| match &vint.form {
-            Unevaled(..) => unreachable!(),
-            WHNF(k) => k,
+            Form::Thunk(..) | Form::Unevaled(..) => unreachable!(),
+            Form::WHNF(k) => k,
         })
     }
 
@@ -231,12 +228,12 @@ impl Value {
     pub(crate) fn normalize_whnf(&self) {
         let borrow = self.as_internal();
         match borrow.form {
-            Unevaled(_) => {
+            Form::Thunk(..) | Form::Unevaled(_) => {
                 drop(borrow);
                 self.as_internal_mut().normalize_whnf();
             }
             // Already in WHNF
-            WHNF(_) => {}
+            Form::WHNF(_) => {}
         }
     }
     pub(crate) fn normalize_nf(&self) {
@@ -290,11 +287,10 @@ impl Value {
         let tye = match &*self.kind() {
             ValueKind::Var(v) => TyExprKind::Var(venv.lookup(v)),
             ValueKind::AppliedBuiltin(closure) => closure.to_tyexprkind(venv),
-            ValueKind::Thunk(th) => return th.to_tyexpr(venv),
             self_kind => TyExprKind::Expr(match self_kind {
-                ValueKind::Var(..)
-                | ValueKind::AppliedBuiltin(..)
-                | ValueKind::Thunk(..) => unreachable!(),
+                ValueKind::Var(..) | ValueKind::AppliedBuiltin(..) => {
+                    unreachable!()
+                }
                 ValueKind::LamClosure {
                     binder,
                     annot,
@@ -402,25 +398,27 @@ impl ValueInternal {
 
     fn normalize_whnf(&mut self) {
         use std::mem::replace;
-        let dummy = Unevaled(ValueKind::Const(Const::Type));
+        let dummy = Form::Unevaled(ValueKind::Const(Const::Type));
         self.form = match replace(&mut self.form, dummy) {
-            Unevaled(kind) => {
-                WHNF(match &self.ty {
+            Form::Thunk(th) => Form::WHNF(th.eval().kind().clone()),
+            Form::Unevaled(kind) => {
+                Form::WHNF(match &self.ty {
                     Some(ty) => normalize_whnf(kind, &ty),
                     // `value` is `Sort`
                     None => ValueKind::Const(Const::Sort),
                 })
             }
             // Already in WHNF
-            form @ WHNF(_) => form,
+            form @ Form::WHNF(_) => form,
         };
     }
     fn normalize_nf(&mut self) {
-        if let Unevaled(_) = self.form {
+        if let Form::Thunk(..) | Form::Unevaled(_) = self.form {
             self.normalize_whnf();
         }
         match &mut self.form {
-            Unevaled(k) | WHNF(k) => k.normalize_mut(),
+            Form::Thunk(..) | Form::Unevaled(_) => unreachable!(),
+            Form::WHNF(k) => k.normalize_mut(),
         }
     }
 
@@ -493,9 +491,6 @@ impl ValueKind {
             ValueKind::PartialExpr(e) => {
                 e.map_mut(Value::normalize_mut);
             }
-            ValueKind::Thunk(..) => {
-                unreachable!("Should only normalize_mut values in WHNF")
-            }
         }
     }
 
@@ -515,12 +510,10 @@ impl Thunk {
         }
     }
 
+    // TODO: maybe return a ValueKind ?
     pub fn eval(&self) -> Value {
         normalize_tyexpr_whnf(&self.body, &self.env)
     }
-    pub fn to_tyexpr(&self, venv: VarEnv) -> TyExpr {
-        self.eval().to_tyexpr(venv)
-    }
 }
 
 impl Closure {
@@ -667,7 +660,17 @@ impl std::fmt::Debug for Value {
     fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
         let vint: &ValueInternal = &self.as_internal();
         let mut x = match &vint.form {
-            WHNF(kind) => {
+            Form::Thunk(th) => {
+                let mut x = fmt.debug_struct(&format!("Value@Thunk"));
+                x.field("thunk", th);
+                x
+            }
+            Form::Unevaled(kind) => {
+                let mut x = fmt.debug_struct(&format!("Value@Unevaled"));
+                x.field("kind", kind);
+                x
+            }
+            Form::WHNF(kind) => {
                 if let ValueKind::Const(c) = kind {
                     return write!(fmt, "{:?}", c);
                 } else {
@@ -676,11 +679,6 @@ impl std::fmt::Debug for Value {
                     x
                 }
             }
-            Unevaled(kind) => {
-                let mut x = fmt.debug_struct(&format!("Value@Unevaled"));
-                x.field("kind", kind);
-                x
-            }
         };
         if let Some(ty) = vint.ty.as_ref() {
             x.field("type", &ty);