From f70e45daef2570259eccd227a0126493c015d7b0 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 20 Aug 2019 21:50:47 +0200 Subject: Track evaluation status alongside ValueF in VoVF --- dhall/src/core/value.rs | 44 ++++++++++++++++++-------------------------- dhall/src/core/valuef.rs | 32 ++++++++++++++++++++++---------- 2 files changed, 40 insertions(+), 36 deletions(-) (limited to 'dhall/src/core') diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index 64a4842..b44dad6 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -12,7 +12,7 @@ use crate::phase::typecheck::{builtin_to_value, const_to_value}; use crate::phase::{NormalizedSubExpr, Typed}; #[derive(Debug, Clone, Copy)] -enum Form { +pub enum Form { /// No constraints; expression may not be normalized at all. Unevaled, /// Weak Head Normal Form, i.e. normalized up to the first constructor, but subexpressions may @@ -46,9 +46,10 @@ pub struct Value(Rc>); /// When a function needs to return either a freshly created ValueF or an existing Value, but /// doesn't want to convert both to the same thing, either to avoid unnecessary allocations or to /// avoid loss of typ information. +#[derive(Debug, Clone)] pub enum VoVF { Value(Value), - ValueF(ValueF), + ValueF { val: ValueF, form: Form }, } impl ValueInternal { @@ -98,24 +99,14 @@ impl ValueInternal { } impl Value { + pub(crate) fn new(value: ValueF, form: Form, ty: Option) -> Value { + ValueInternal { form, value, ty }.into_value() + } pub(crate) fn from_valuef_untyped(v: ValueF) -> Value { - ValueInternal { - form: Unevaled, - value: v, - ty: None, - } - .into_value() + Value::new(v, Unevaled, None) } pub(crate) fn from_valuef_and_type(v: ValueF, t: Value) -> Value { - ValueInternal { - form: Unevaled, - value: v, - ty: Some(t), - } - .into_value() - } - pub(crate) fn from_valuef_simple_type(v: ValueF) -> Value { - Value::from_valuef_and_type(v, Value::from_const(Const::Type)) + Value::new(v, Unevaled, Some(t)) } pub(crate) fn from_const(c: Const) -> Self { const_to_value(c) @@ -236,34 +227,35 @@ impl VoVF { pub fn into_whnf(self) -> ValueF { match self { VoVF::Value(v) => v.to_whnf(), - VoVF::ValueF(v) => v, + VoVF::ValueF { + val, + form: Unevaled, + } => normalize_whnf(val).into_whnf(), + // Already at lest in WHNF + VoVF::ValueF { val, .. } => val, } } pub(crate) fn into_value_untyped(self) -> Value { match self { VoVF::Value(v) => v, - VoVF::ValueF(v) => v.into_value_untyped(), + VoVF::ValueF { val, form } => Value::new(val, form, None), } } pub(crate) fn into_value_with_type(self, t: Value) -> Value { match self { // TODO: check type with debug_assert ? VoVF::Value(v) => v, - VoVF::ValueF(v) => v.into_value_with_type(t), + VoVF::ValueF { val, form } => Value::new(val, form, Some(t)), } } pub(crate) fn into_value_simple_type(self) -> Value { - match self { - // TODO: check type with debug_assert ? - VoVF::Value(v) => v, - VoVF::ValueF(v) => v.into_value_simple_type(), - } + self.into_value_with_type(Value::from_const(Const::Type)) } pub(crate) fn app(self, x: Value) -> Self { match self { VoVF::Value(v) => v.app(x), - VoVF::ValueF(v) => v.into_value_untyped().app(x), + VoVF::ValueF { val, .. } => val.into_value_untyped().app(x), } } } 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), Var(AlphaVar), @@ -33,16 +33,16 @@ pub enum ValueF { // EmptyListLit(t) means `[] : List t`, not `[] : t` EmptyListLit(Value), NEListLit(Vec), - RecordLit(HashMap), RecordType(HashMap), + RecordLit(HashMap), UnionType(HashMap>), UnionConstructor(Label, HashMap>), UnionLit(Label, Value, HashMap>), - // 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>), 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), } @@ -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 { -- cgit v1.2.3