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/src/core | |
parent | a506632b27b287d1bf898e2f77ae09a56902474c (diff) |
Introduce a new enum to store either a Value or a ValueF
Diffstat (limited to 'dhall/src/core')
-rw-r--r-- | dhall/src/core/value.rs | 54 | ||||
-rw-r--r-- | dhall/src/core/valuef.rs | 9 |
2 files changed, 57 insertions, 6 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 { |