Document Value and Thunk

2 files changed, 21 insertions, 8 deletions

diff --git a/dhall/src/core/thunk.rs b/dhall/src/core/thunk.rs
index 69c4347..2b013bb 100644
--- a/dhall/src/core/thunk.rs
+++ b/dhall/src/core/thunk.rs
@@ -29,12 +29,14 @@ enum ThunkInternal {
     Value(Marker, Value),
 }
 
-/// Stores a possibly unevaluated value. Uses RefCell to ensure that
-/// the value gets normalized at most once.
+/// Stores a possibly unevaluated value. Gets (partially) normalized on-demand,
+/// sharing computation automatically.
+/// Uses a RefCell to share computation.
 #[derive(Debug, Clone)]
 pub struct Thunk(Rc<RefCell<ThunkInternal>>);
 
-/// A thunk in type position.
+/// A thunk in type position. Can optionally store a Type from the typechecking phase to preserve
+/// type information through the normalization phase.
 #[derive(Debug, Clone)]
 pub(crate) enum TypeThunk {
     Thunk(Thunk),
diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs
index 31193d2..354c360 100644
--- a/dhall/src/core/value.rs
+++ b/dhall/src/core/value.rs
@@ -26,13 +26,23 @@ pub(crate) struct AlphaVar {
 #[derive(Debug, Clone, Eq)]
 pub(crate) struct AlphaLabel(Label);
 
-/// A semantic value.
-/// Equality is up to alpha-equivalence (renaming of bound variables)
-/// and beta-equivalence (normalization).
+/// A semantic value. The invariants ensure this value represents a Weak-Head
+/// Normal Form (WHNF). This means that this first constructor is the first constructor of the
+/// final Normal Form (NF).
+/// This WHNF must be preserved by operations on `Value`s. In particular, `subst_shift` could break
+/// the invariants so need to be careful to reevaluate as needed.
+/// Subexpressions are Thunks, which are partially evaluated expressions that are normalized
+/// on-demand. When all the Thunks in a Value are at least in WHNF, and recursively so, then the
+/// Value 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.
+/// Equality is up to alpha-equivalence (renaming of bound variables) and beta-equivalence
+/// (normalization). Equality will normalize only as needed.
 #[derive(Debug, Clone, PartialEq, Eq)]
 pub(crate) enum Value {
     /// Closures
     Lam(AlphaLabel, Thunk, Thunk),
+    Pi(AlphaLabel, TypeThunk, TypeThunk),
+    // Invariant: the evaluation must not be able to progress further.
     AppliedBuiltin(Builtin, Vec<Thunk>),
     /// `λ(x: a) -> Some x`
     OptionalSomeClosure(TypeThunk),
@@ -41,7 +51,6 @@ pub(crate) enum Value {
     ListConsClosure(TypeThunk, Option<Thunk>),
     /// `λ(x : Natural) -> x + 1`
     NaturalSuccClosure,
-    Pi(AlphaLabel, TypeThunk, TypeThunk),
 
     Var(AlphaVar),
     Const(Const),
@@ -57,8 +66,10 @@ pub(crate) enum Value {
     UnionType(BTreeMap<Label, Option<TypeThunk>>),
     UnionConstructor(Label, BTreeMap<Label, Option<TypeThunk>>),
     UnionLit(Label, Thunk, BTreeMap<Label, Option<TypeThunk>>),
+    // Invariant: this must not contain interpolations that are themselves TextLits, and
+    // contiguous text values must be merged.
     TextLit(Vec<InterpolatedTextContents<Thunk>>),
-    /// Invariant: This must not contain a value captured by one of the variants above.
+    // Invariant: this must not contain a value captured by one of the variants above.
     PartialExpr(ExprF<Thunk, Label, X>),
 }