diff options
Diffstat (limited to '')
-rw-r--r-- | dhall/src/core/valuef.rs | 32 |
1 files changed, 22 insertions, 10 deletions
diff --git a/dhall/src/core/valuef.rs b/dhall/src/core/valuef.rs index 80978a7..db8a284 100644 --- a/dhall/src/core/valuef.rs +++ b/dhall/src/core/valuef.rs @@ -5,7 +5,7 @@ use dhall_syntax::{ NaiveDouble, Natural, }; -use crate::core::value::{Value, VoVF}; +use crate::core::value::{Form, Value, VoVF}; use crate::core::var::{AlphaLabel, AlphaVar, Shift, Subst}; use crate::phase::{Normalized, NormalizedSubExpr}; @@ -19,7 +19,7 @@ pub enum ValueF { /// Closures Lam(AlphaLabel, Value, Value), Pi(AlphaLabel, Value, Value), - // Invariant: the evaluation must not be able to progress further. + // Invariant: in whnf, the evaluation must not be able to progress further. AppliedBuiltin(Builtin, Vec<Value>), Var(AlphaVar), @@ -33,16 +33,16 @@ pub enum ValueF { // EmptyListLit(t) means `[] : List t`, not `[] : t` EmptyListLit(Value), NEListLit(Vec<Value>), - RecordLit(HashMap<Label, Value>), RecordType(HashMap<Label, Value>), + RecordLit(HashMap<Label, Value>), UnionType(HashMap<Label, Option<Value>>), UnionConstructor(Label, HashMap<Label, Option<Value>>), UnionLit(Label, Value, HashMap<Label, Option<Value>>), - // Invariant: this must not contain interpolations that are themselves TextLits, and + // Invariant: in whnf, this must not contain interpolations that are themselves TextLits, and // contiguous text values must be merged. TextLit(Vec<InterpolatedTextContents<Value>>), Equivalence(Value, Value), - // Invariant: this must not contain a value captured by one of the variants above. + // Invariant: in whnf, this must not contain a value captured by one of the variants above. PartialExpr(ExprF<Value, Normalized>), } @@ -53,11 +53,23 @@ impl ValueF { pub(crate) fn into_value_with_type(self, t: Value) -> Value { Value::from_valuef_and_type(self, t) } - pub(crate) fn into_value_simple_type(self) -> Value { - Value::from_valuef_simple_type(self) + pub(crate) fn into_vovf_unevaled(self) -> VoVF { + VoVF::ValueF { + val: self, + form: Form::Unevaled, + } + } + pub(crate) fn into_vovf_whnf(self) -> VoVF { + VoVF::ValueF { + val: self, + form: Form::WHNF, + } } - pub(crate) fn into_vovf(self) -> VoVF { - VoVF::ValueF(self) + pub(crate) fn into_vovf_nf(self) -> VoVF { + VoVF::ValueF { + val: self, + form: Form::NF, + } } /// Convert the value to a fully normalized syntactic expression @@ -261,7 +273,7 @@ impl ValueF { /// Apply to a value pub fn app(self, v: Value) -> VoVF { - self.into_vovf().app(v) + self.into_vovf_unevaled().app(v) } pub fn from_builtin(b: Builtin) -> ValueF { |