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 ++++++++++++++------ dhall/src/phase/normalize.rs | 72 ++++++++++++++++++++++++-------------------- 3 files changed, 80 insertions(+), 68 deletions(-) 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 { diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs index e044018..a146ec7 100644 --- a/dhall/src/phase/normalize.rs +++ b/dhall/src/phase/normalize.rs @@ -70,29 +70,29 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> VoVF { // Return Ok((unconsumed args, returned value)), or Err(()) if value could not be produced. let ret = match (b, args.as_slice()) { (OptionalNone, [t, r..]) => { - Ok((r, EmptyOptionalLit(t.clone()).into_vovf())) + Ok((r, EmptyOptionalLit(t.clone()).into_vovf_whnf())) } (NaturalIsZero, [n, r..]) => match &*n.as_whnf() { - NaturalLit(n) => Ok((r, BoolLit(*n == 0).into_vovf())), + NaturalLit(n) => Ok((r, BoolLit(*n == 0).into_vovf_nf())), _ => Err(()), }, (NaturalEven, [n, r..]) => match &*n.as_whnf() { - NaturalLit(n) => Ok((r, BoolLit(*n % 2 == 0).into_vovf())), + NaturalLit(n) => Ok((r, BoolLit(*n % 2 == 0).into_vovf_nf())), _ => Err(()), }, (NaturalOdd, [n, r..]) => match &*n.as_whnf() { - NaturalLit(n) => Ok((r, BoolLit(*n % 2 != 0).into_vovf())), + NaturalLit(n) => Ok((r, BoolLit(*n % 2 != 0).into_vovf_nf())), _ => Err(()), }, (NaturalToInteger, [n, r..]) => match &*n.as_whnf() { - NaturalLit(n) => Ok((r, IntegerLit(*n as isize).into_vovf())), + NaturalLit(n) => Ok((r, IntegerLit(*n as isize).into_vovf_nf())), _ => Err(()), }, (NaturalShow, [n, r..]) => match &*n.as_whnf() { NaturalLit(n) => Ok(( r, TextLit(vec![InterpolatedTextContents::Text(n.to_string())]) - .into_vovf(), + .into_vovf_nf(), )), _ => Err(()), }, @@ -100,11 +100,11 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> VoVF { match (&*a.as_whnf(), &*b.as_whnf()) { (NaturalLit(a), NaturalLit(b)) => Ok(( r, - NaturalLit(if b > a { b - a } else { 0 }).into_vovf(), + NaturalLit(if b > a { b - a } else { 0 }).into_vovf_nf(), )), (NaturalLit(0), _) => Ok((r, b.clone().into_vovf())), - (_, NaturalLit(0)) => Ok((r, NaturalLit(0).into_vovf())), - _ if a == b => Ok((r, NaturalLit(0).into_vovf())), + (_, NaturalLit(0)) => Ok((r, NaturalLit(0).into_vovf_nf())), + _ if a == b => Ok((r, NaturalLit(0).into_vovf_nf())), _ => Err(()), } } @@ -118,14 +118,14 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> VoVF { Ok(( r, TextLit(vec![InterpolatedTextContents::Text(s)]) - .into_vovf(), + .into_vovf_nf(), )) } _ => Err(()), }, (IntegerToDouble, [n, r..]) => match &*n.as_whnf() { IntegerLit(n) => { - Ok((r, DoubleLit(NaiveDouble::from(*n as f64)).into_vovf())) + Ok((r, DoubleLit(NaiveDouble::from(*n as f64)).into_vovf_nf())) } _ => Err(()), }, @@ -133,7 +133,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> VoVF { DoubleLit(n) => Ok(( r, TextLit(vec![InterpolatedTextContents::Text(n.to_string())]) - .into_vovf(), + .into_vovf_nf(), )), _ => Err(()), }, @@ -149,7 +149,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> VoVF { Ok(( r, TextLit(vec![InterpolatedTextContents::Text(s)]) - .into_vovf(), + .into_vovf_nf(), )) } // If there are no interpolations (invariants ensure that when there are no @@ -165,7 +165,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> VoVF { Ok(( r, TextLit(vec![InterpolatedTextContents::Text(s)]) - .into_vovf(), + .into_vovf_nf(), )) } _ => Err(()), @@ -174,32 +174,39 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> VoVF { _ => Err(()), }, (ListLength, [_, l, r..]) => match &*l.as_whnf() { - EmptyListLit(_) => Ok((r, NaturalLit(0).into_vovf())), - NEListLit(xs) => Ok((r, NaturalLit(xs.len()).into_vovf())), + EmptyListLit(_) => Ok((r, NaturalLit(0).into_vovf_nf())), + NEListLit(xs) => Ok((r, NaturalLit(xs.len()).into_vovf_nf())), _ => Err(()), }, (ListHead, [_, l, r..]) => match &*l.as_whnf() { - EmptyListLit(n) => Ok((r, EmptyOptionalLit(n.clone()).into_vovf())), + EmptyListLit(n) => { + Ok((r, EmptyOptionalLit(n.clone()).into_vovf_whnf())) + } NEListLit(xs) => Ok(( r, - NEOptionalLit(xs.iter().next().unwrap().clone()).into_vovf(), + NEOptionalLit(xs.iter().next().unwrap().clone()) + .into_vovf_whnf(), )), _ => Err(()), }, (ListLast, [_, l, r..]) => match &*l.as_whnf() { - EmptyListLit(n) => Ok((r, EmptyOptionalLit(n.clone()).into_vovf())), + EmptyListLit(n) => { + Ok((r, EmptyOptionalLit(n.clone()).into_vovf_whnf())) + } NEListLit(xs) => Ok(( r, NEOptionalLit(xs.iter().rev().next().unwrap().clone()) - .into_vovf(), + .into_vovf_whnf(), )), _ => Err(()), }, (ListReverse, [_, l, r..]) => match &*l.as_whnf() { - EmptyListLit(n) => Ok((r, EmptyListLit(n.clone()).into_vovf())), + EmptyListLit(n) => { + Ok((r, EmptyListLit(n.clone()).into_vovf_whnf())) + } NEListLit(xs) => Ok(( r, - NEListLit(xs.iter().rev().cloned().collect()).into_vovf(), + NEListLit(xs.iter().rev().cloned().collect()).into_vovf_whnf(), )), _ => Err(()), }, @@ -211,7 +218,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> VoVF { Ok(( r, EmptyListLit(Value::from_valuef_untyped(RecordType(kts))) - .into_vovf(), + .into_vovf_whnf(), )) } NEListLit(xs) => { @@ -229,7 +236,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> VoVF { Value::from_valuef_untyped(RecordLit(kvs)) }) .collect(); - Ok((r, NEListLit(xs).into_vovf())) + Ok((r, NEListLit(xs).into_vovf_whnf())) } _ => Err(()), }, @@ -353,13 +360,14 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> VoVF { } v } - Err(()) => AppliedBuiltin(b, args).into_vovf(), + Err(()) => AppliedBuiltin(b, args).into_vovf_whnf(), } } pub(crate) fn apply_any(f: Value, a: Value) -> VoVF { - let fallback = - |f: Value, a: Value| ValueF::PartialExpr(ExprF::App(f, a)).into_vovf(); + let fallback = |f: Value, a: Value| { + ValueF::PartialExpr(ExprF::App(f, a)).into_vovf_whnf() + }; let f_borrow = f.as_whnf(); match &*f_borrow { @@ -370,7 +378,7 @@ pub(crate) fn apply_any(f: Value, a: Value) -> VoVF { apply_builtin(*b, args) } ValueF::UnionConstructor(l, kts) => { - ValueF::UnionLit(l.clone(), a, kts.clone()).into_vovf() + ValueF::UnionLit(l.clone(), a, kts.clone()).into_vovf_whnf() } _ => { drop(f_borrow); @@ -774,11 +782,11 @@ pub(crate) fn normalize_one_layer(expr: ExprF) -> VoVF { }; match ret { - Ret::ValueF(v) => v.into_vovf(), + Ret::ValueF(v) => v.into_vovf_whnf(), Ret::Value(v) => v.into_vovf(), Ret::VoVF(v) => v, Ret::ValueRef(v) => v.clone().into_vovf(), - Ret::Expr(expr) => ValueF::PartialExpr(expr).into_vovf(), + Ret::Expr(expr) => ValueF::PartialExpr(expr).into_vovf_whnf(), } } @@ -788,9 +796,9 @@ pub(crate) fn normalize_whnf(v: ValueF) -> VoVF { ValueF::AppliedBuiltin(b, args) => apply_builtin(b, args), ValueF::PartialExpr(e) => normalize_one_layer(e), ValueF::TextLit(elts) => { - ValueF::TextLit(squash_textlit(elts.into_iter())).into_vovf() + ValueF::TextLit(squash_textlit(elts.into_iter())).into_vovf_whnf() } // All other cases are already in WHNF - v => v.into_vovf(), + v => v.into_vovf_whnf(), } } -- cgit v1.2.3