diff options
author | Nadrieril | 2019-08-20 18:03:59 +0200 |
---|---|---|
committer | Nadrieril | 2019-08-20 18:03:59 +0200 |
commit | 4f1f37cfc115510500e83d2dfbfa8ed7ddeae74a (patch) | |
tree | 77c743b9c55afbbb5966a3c90614c6d3d257813d /dhall | |
parent | a506632b27b287d1bf898e2f77ae09a56902474c (diff) |
Introduce a new enum to store either a Value or a ValueF
Diffstat (limited to 'dhall')
-rw-r--r-- | dhall/src/core/value.rs | 54 | ||||
-rw-r--r-- | dhall/src/core/valuef.rs | 9 | ||||
-rw-r--r-- | dhall/src/phase/normalize.rs | 141 | ||||
-rw-r--r-- | dhall/src/phase/typecheck.rs | 17 |
4 files changed, 147 insertions, 74 deletions
diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index 5055ac2..25fcaae 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -44,6 +44,14 @@ struct ValueInternal { #[derive(Clone)] pub struct Value(Rc<RefCell<ValueInternal>>); +/// 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. +pub enum VoVF { + Value(Value), + ValueF(ValueF), +} + impl ValueInternal { fn into_value(self) -> Value { Value(Rc::new(RefCell::new(self))) @@ -56,7 +64,8 @@ impl ValueInternal { take_mut::take(self, |vint| match &vint.form { Unevaled => ValueInternal { form: WHNF, - value: normalize_whnf(vint.value), + // TODO: thunk chaining + value: normalize_whnf(vint.value).into_whnf(), ty: vint.ty, }, // Already in WHNF @@ -166,6 +175,9 @@ impl Value { pub(crate) fn into_typed(self) -> Typed { Typed::from_value(self) } + pub(crate) fn into_vovf(self) -> VoVF { + VoVF::Value(self) + } /// Mutates the contents. If no one else shares this, this avoids a RefCell lock. fn mutate_internal(&mut self, f: impl FnOnce(&mut ValueInternal)) { @@ -212,8 +224,8 @@ impl Value { self.as_nf().normalize_to_expr_maybe_alpha(alpha) } - pub(crate) fn app(&self, th: Value) -> ValueF { - apply_any(self.clone(), th) + pub(crate) fn app(&self, v: Value) -> VoVF { + apply_any(self.clone(), v) } pub(crate) fn get_type(&self) -> Result<Cow<'_, Value>, TypeError> { @@ -221,6 +233,42 @@ impl Value { } } +impl VoVF { + pub fn into_whnf(self) -> ValueF { + match self { + VoVF::Value(v) => v.to_whnf(), + VoVF::ValueF(v) => v, + } + } + pub(crate) fn into_value_untyped(self) -> Value { + match self { + VoVF::Value(v) => v, + VoVF::ValueF(v) => v.into_value_untyped(), + } + } + 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), + } + } + 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(), + } + } + + 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), + } + } +} + impl Shift for Value { fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { Some(Value(self.0.shift(delta, var)?)) diff --git a/dhall/src/core/valuef.rs b/dhall/src/core/valuef.rs index e9049c7..80978a7 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; +use crate::core::value::{Value, VoVF}; use crate::core::var::{AlphaLabel, AlphaVar, Shift, Subst}; use crate::phase::{Normalized, NormalizedSubExpr}; @@ -56,6 +56,9 @@ impl ValueF { pub(crate) fn into_value_simple_type(self) -> Value { Value::from_valuef_simple_type(self) } + pub(crate) fn into_vovf(self) -> VoVF { + VoVF::ValueF(self) + } /// Convert the value to a fully normalized syntactic expression pub(crate) fn normalize_to_expr(&self) -> NormalizedSubExpr { @@ -257,8 +260,8 @@ impl ValueF { } /// Apply to a value - pub fn app(self, th: Value) -> ValueF { - Value::from_valuef_untyped(self).app(th) + pub fn app(self, v: Value) -> VoVF { + self.into_vovf().app(v) } pub fn from_builtin(b: Builtin) -> ValueF { diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs index afc2e7f..e044018 100644 --- a/dhall/src/phase/normalize.rs +++ b/dhall/src/phase/normalize.rs @@ -5,7 +5,7 @@ use dhall_syntax::{ NaiveDouble, }; -use crate::core::value::Value; +use crate::core::value::{Value, VoVF}; use crate::core::valuef::ValueF; use crate::core::var::{Shift, Subst}; use crate::phase::Normalized; @@ -63,44 +63,48 @@ macro_rules! make_closure { } #[allow(clippy::cognitive_complexity)] -pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF { +pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> VoVF { use dhall_syntax::Builtin::*; use ValueF::*; // 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()))), + (OptionalNone, [t, r..]) => { + Ok((r, EmptyOptionalLit(t.clone()).into_vovf())) + } (NaturalIsZero, [n, r..]) => match &*n.as_whnf() { - NaturalLit(n) => Ok((r, BoolLit(*n == 0))), + NaturalLit(n) => Ok((r, BoolLit(*n == 0).into_vovf())), _ => Err(()), }, (NaturalEven, [n, r..]) => match &*n.as_whnf() { - NaturalLit(n) => Ok((r, BoolLit(*n % 2 == 0))), + NaturalLit(n) => Ok((r, BoolLit(*n % 2 == 0).into_vovf())), _ => Err(()), }, (NaturalOdd, [n, r..]) => match &*n.as_whnf() { - NaturalLit(n) => Ok((r, BoolLit(*n % 2 != 0))), + NaturalLit(n) => Ok((r, BoolLit(*n % 2 != 0).into_vovf())), _ => Err(()), }, (NaturalToInteger, [n, r..]) => match &*n.as_whnf() { - NaturalLit(n) => Ok((r, IntegerLit(*n as isize))), + NaturalLit(n) => Ok((r, IntegerLit(*n as isize).into_vovf())), _ => Err(()), }, (NaturalShow, [n, r..]) => match &*n.as_whnf() { NaturalLit(n) => Ok(( r, - TextLit(vec![InterpolatedTextContents::Text(n.to_string())]), + TextLit(vec![InterpolatedTextContents::Text(n.to_string())]) + .into_vovf(), )), _ => Err(()), }, (NaturalSubtract, [a, b, r..]) => { match (&*a.as_whnf(), &*b.as_whnf()) { - (NaturalLit(a), NaturalLit(b)) => { - Ok((r, NaturalLit(if b > a { b - a } else { 0 }))) - } - (NaturalLit(0), b) => Ok((r, b.clone())), - (_, NaturalLit(0)) => Ok((r, NaturalLit(0))), - _ if a == b => Ok((r, NaturalLit(0))), + (NaturalLit(a), NaturalLit(b)) => Ok(( + r, + NaturalLit(if b > a { b - a } else { 0 }).into_vovf(), + )), + (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())), _ => Err(()), } } @@ -111,18 +115,25 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF { } else { format!("+{}", n) }; - Ok((r, TextLit(vec![InterpolatedTextContents::Text(s)]))) + Ok(( + r, + TextLit(vec![InterpolatedTextContents::Text(s)]) + .into_vovf(), + )) } _ => Err(()), }, (IntegerToDouble, [n, r..]) => match &*n.as_whnf() { - IntegerLit(n) => Ok((r, DoubleLit(NaiveDouble::from(*n as f64)))), + IntegerLit(n) => { + Ok((r, DoubleLit(NaiveDouble::from(*n as f64)).into_vovf())) + } _ => Err(()), }, (DoubleShow, [n, r..]) => match &*n.as_whnf() { DoubleLit(n) => Ok(( r, - TextLit(vec![InterpolatedTextContents::Text(n.to_string())]), + TextLit(vec![InterpolatedTextContents::Text(n.to_string())]) + .into_vovf(), )), _ => Err(()), }, @@ -137,7 +148,8 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF { let s = txt.to_string(); Ok(( r, - TextLit(vec![InterpolatedTextContents::Text(s)]), + TextLit(vec![InterpolatedTextContents::Text(s)]) + .into_vovf(), )) } // If there are no interpolations (invariants ensure that when there are no @@ -152,7 +164,8 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF { let s = txt.to_string(); Ok(( r, - TextLit(vec![InterpolatedTextContents::Text(s)]), + TextLit(vec![InterpolatedTextContents::Text(s)]) + .into_vovf(), )) } _ => Err(()), @@ -161,29 +174,33 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF { _ => Err(()), }, (ListLength, [_, l, r..]) => match &*l.as_whnf() { - EmptyListLit(_) => Ok((r, NaturalLit(0))), - NEListLit(xs) => Ok((r, NaturalLit(xs.len()))), + EmptyListLit(_) => Ok((r, NaturalLit(0).into_vovf())), + NEListLit(xs) => Ok((r, NaturalLit(xs.len()).into_vovf())), _ => Err(()), }, (ListHead, [_, l, r..]) => match &*l.as_whnf() { - EmptyListLit(n) => Ok((r, EmptyOptionalLit(n.clone()))), - NEListLit(xs) => { - Ok((r, NEOptionalLit(xs.iter().next().unwrap().clone()))) - } + EmptyListLit(n) => Ok((r, EmptyOptionalLit(n.clone()).into_vovf())), + NEListLit(xs) => Ok(( + r, + NEOptionalLit(xs.iter().next().unwrap().clone()).into_vovf(), + )), _ => Err(()), }, (ListLast, [_, l, r..]) => match &*l.as_whnf() { - EmptyListLit(n) => Ok((r, EmptyOptionalLit(n.clone()))), - NEListLit(xs) => { - Ok((r, NEOptionalLit(xs.iter().rev().next().unwrap().clone()))) - } + EmptyListLit(n) => Ok((r, EmptyOptionalLit(n.clone()).into_vovf())), + NEListLit(xs) => Ok(( + r, + NEOptionalLit(xs.iter().rev().next().unwrap().clone()) + .into_vovf(), + )), _ => Err(()), }, (ListReverse, [_, l, r..]) => match &*l.as_whnf() { - EmptyListLit(n) => Ok((r, EmptyListLit(n.clone()))), - NEListLit(xs) => { - Ok((r, NEListLit(xs.iter().rev().cloned().collect()))) - } + EmptyListLit(n) => Ok((r, EmptyListLit(n.clone()).into_vovf())), + NEListLit(xs) => Ok(( + r, + NEListLit(xs.iter().rev().cloned().collect()).into_vovf(), + )), _ => Err(()), }, (ListIndexed, [_, l, r..]) => match &*l.as_whnf() { @@ -193,7 +210,8 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF { kts.insert("value".into(), t.clone()); Ok(( r, - EmptyListLit(Value::from_valuef_untyped(RecordType(kts))), + EmptyListLit(Value::from_valuef_untyped(RecordType(kts))) + .into_vovf(), )) } NEListLit(xs) => { @@ -211,7 +229,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF { Value::from_valuef_untyped(RecordLit(kvs)) }) .collect(); - Ok((r, NEListLit(xs))) + Ok((r, NEListLit(xs).into_vovf())) } _ => Err(()), }, @@ -219,7 +237,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF { // fold/build fusion ValueF::AppliedBuiltin(ListFold, args) => { if args.len() >= 2 { - Ok((r, args[1].to_whnf())) + Ok((r, args[1].clone().into_vovf())) } else { // Do we really need to handle this case ? unimplemented!() @@ -249,13 +267,13 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF { } }, (ListFold, [_, l, _, cons, nil, r..]) => match &*l.as_whnf() { - EmptyListLit(_) => Ok((r, nil.to_whnf())), + EmptyListLit(_) => Ok((r, nil.clone().into_vovf())), NEListLit(xs) => { - let mut v = nil.clone(); - for x in xs.iter().rev() { - v = cons.clone().app(x.clone()).app(v).into_value_untyped(); + let mut v = nil.clone().into_vovf(); + for x in xs.iter().cloned().rev() { + v = cons.app(x).app(v.into_value_untyped()); } - Ok((r, v.to_whnf())) + Ok((r, v)) } _ => Err(()), }, @@ -263,7 +281,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF { // fold/build fusion ValueF::AppliedBuiltin(OptionalFold, args) => { if args.len() >= 2 { - Ok((r, args[1].to_whnf())) + Ok((r, args[1].clone().into_vovf())) } else { // Do we really need to handle this case ? unimplemented!() @@ -285,7 +303,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF { } }, (OptionalFold, [_, v, _, just, nothing, r..]) => match &*v.as_whnf() { - EmptyOptionalLit(_) => Ok((r, nothing.to_whnf())), + EmptyOptionalLit(_) => Ok((r, nothing.clone().into_vovf())), NEOptionalLit(x) => Ok((r, just.app(x.clone()))), _ => Err(()), }, @@ -293,7 +311,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF { // fold/build fusion ValueF::AppliedBuiltin(NaturalFold, args) => { if !args.is_empty() { - Ok((r, args[0].to_whnf())) + Ok((r, args[0].clone().into_vovf())) } else { // Do we really need to handle this case ? unimplemented!() @@ -310,7 +328,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF { )), }, (NaturalFold, [n, t, succ, zero, r..]) => match &*n.as_whnf() { - NaturalLit(0) => Ok((r, zero.to_whnf())), + NaturalLit(0) => Ok((r, zero.clone().into_vovf())), NaturalLit(n) => { let fold = Value::from_builtin(NaturalFold) .app( @@ -335,23 +353,24 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF { } v } - Err(()) => AppliedBuiltin(b, args), + Err(()) => AppliedBuiltin(b, args).into_vovf(), } } -pub(crate) fn apply_any(f: Value, a: Value) -> ValueF { - let fallback = |f: Value, a: Value| ValueF::PartialExpr(ExprF::App(f, a)); +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 f_borrow = f.as_whnf(); match &*f_borrow { - ValueF::Lam(x, _, e) => e.subst_shift(&x.into(), &a).to_whnf(), + ValueF::Lam(x, _, e) => e.subst_shift(&x.into(), &a).into_vovf(), ValueF::AppliedBuiltin(b, args) => { use std::iter::once; let args = args.iter().cloned().chain(once(a.clone())).collect(); apply_builtin(*b, args) } ValueF::UnionConstructor(l, kts) => { - ValueF::UnionLit(l.clone(), a, kts.clone()) + ValueF::UnionLit(l.clone(), a, kts.clone()).into_vovf() } _ => { drop(f_borrow); @@ -465,6 +484,7 @@ where enum Ret<'a> { ValueF(ValueF), Value(Value), + VoVF(VoVF), ValueRef(&'a Value), Expr(ExprF<Value, Normalized>), } @@ -597,7 +617,7 @@ fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option<Ret<'a>> { }) } -pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> ValueF { +pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> VoVF { use ValueF::{ AppliedBuiltin, BoolLit, DoubleLit, EmptyListLit, IntegerLit, Lam, NEListLit, NEOptionalLit, NaturalLit, Pi, RecordLit, RecordType, @@ -615,7 +635,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> ValueF { ExprF::Lam(x, t, e) => Ret::ValueF(Lam(x.into(), t, e)), ExprF::Pi(x, t, e) => Ret::ValueF(Pi(x.into(), t, e)), ExprF::Let(x, _, v, b) => Ret::Value(b.subst_shift(&x.into(), &v)), - ExprF::App(v, a) => Ret::ValueF(v.app(a)), + ExprF::App(v, a) => Ret::VoVF(v.app(a)), ExprF::Builtin(b) => Ret::ValueF(ValueF::from_builtin(b)), ExprF::Const(c) => Ret::ValueF(ValueF::Const(c)), ExprF::BoolLit(b) => Ret::ValueF(BoolLit(b)), @@ -737,7 +757,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> ValueF { } }, (RecordLit(kvs), UnionLit(l, v, _)) => match kvs.get(l) { - Some(h) => Ret::ValueF(h.app(v.clone())), + Some(h) => Ret::VoVF(h.app(v.clone())), None => { drop(handlers_borrow); drop(variant_borrow); @@ -754,22 +774,23 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> ValueF { }; match ret { - Ret::ValueF(v) => v, - Ret::Value(th) => th.as_whnf().clone(), - Ret::ValueRef(th) => th.as_whnf().clone(), - Ret::Expr(expr) => ValueF::PartialExpr(expr), + Ret::ValueF(v) => v.into_vovf(), + 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(), } } /// Normalize a ValueF into WHNF -pub(crate) fn normalize_whnf(v: ValueF) -> ValueF { +pub(crate) fn normalize_whnf(v: ValueF) -> VoVF { match v { 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())) + ValueF::TextLit(squash_textlit(elts.into_iter())).into_vovf() } // All other cases are already in WHNF - v => v, + v => v.into_vovf(), } } diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs index 440d694..996c26c 100644 --- a/dhall/src/phase/typecheck.rs +++ b/dhall/src/phase/typecheck.rs @@ -455,11 +455,11 @@ fn type_last_layer( return mkerr(InvalidListType(t.into_owned())); } - RetTypeOnly(Value::from_valuef_and_type( + RetTypeOnly( ValueF::from_builtin(dhall_syntax::Builtin::List) - .app(t.into_owned()), - Value::from_const(Type), - )) + .app(t.into_owned()) + .into_value_simple_type(), + ) } SomeLit(x) => { let t = x.get_type()?.into_owned(); @@ -467,10 +467,11 @@ fn type_last_layer( return mkerr(InvalidOptionalType(t)); } - RetTypeOnly(Value::from_valuef_and_type( - ValueF::from_builtin(dhall_syntax::Builtin::Optional).app(t), - Value::from_const(Type), - )) + RetTypeOnly( + Value::from_builtin(dhall_syntax::Builtin::Optional) + .app(t) + .into_value_simple_type(), + ) } RecordType(kts) => RetWhole(tck_record_type( ctx, |