summaryrefslogtreecommitdiff
path: root/dhall/src/core/value.rs
diff options
context:
space:
mode:
authorNadrieril2019-08-20 21:50:47 +0200
committerNadrieril2019-08-20 21:50:47 +0200
commitf70e45daef2570259eccd227a0126493c015d7b0 (patch)
tree560f32faa871f4a1df5ae6a3d9c06581d8c6f48a /dhall/src/core/value.rs
parentc157df5e66fb80ff6184cb3934e5b0883f0fdbf0 (diff)
Track evaluation status alongside ValueF in VoVF
Diffstat (limited to 'dhall/src/core/value.rs')
-rw-r--r--dhall/src/core/value.rs44
1 files changed, 18 insertions, 26 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<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.
+#[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>) -> 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),
}
}
}