summaryrefslogtreecommitdiff
path: root/dhall/src/core
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src/core')
-rw-r--r--dhall/src/core/thunk.rs8
-rw-r--r--dhall/src/core/value.rs21
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>),
}