diff options
author | Nadrieril | 2019-05-07 16:15:22 +0200 |
---|---|---|
committer | Nadrieril | 2019-05-07 16:18:13 +0200 |
commit | 5b4887f7ea3262bd0e280be4bb889fd67f708edf (patch) | |
tree | bdf267a7283f34c77626244c33b2be1a77446f5b | |
parent | 726c281cdd3824fcfdde34fe8d01f95416f7808c (diff) |
Document Value and Thunk
Diffstat (limited to '')
-rw-r--r-- | dhall/src/core/thunk.rs | 8 | ||||
-rw-r--r-- | dhall/src/core/value.rs | 21 |
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>), } |