summaryrefslogtreecommitdiff
path: root/dhall/src/core
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src/core')
-rw-r--r--dhall/src/core/value.rs39
1 files changed, 28 insertions, 11 deletions
diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs
index 69d372a..6f9f78a 100644
--- a/dhall/src/core/value.rs
+++ b/dhall/src/core/value.rs
@@ -70,12 +70,25 @@ impl ValueInternal {
ty: None,
},
|vint| match &vint.form {
- Unevaled => ValueInternal {
- form: WHNF,
- // TODO: thunk chaining
- value: normalize_whnf(vint.value).into_whnf(),
- ty: vint.ty,
- },
+ Unevaled => {
+ let (value, ty) = (vint.value, vint.ty);
+ let vovf = normalize_whnf(value, ty.as_ref());
+ // let was_value = if let VoVF::Value(_) = &vovf {
+ // true
+ // } else {
+ // false
+ // };
+ let (new_val, _new_ty) =
+ vovf.into_whnf_and_type(ty.as_ref());
+ // if was_value {
+ // debug_assert_eq!(ty, new_ty);
+ // }
+ ValueInternal {
+ form: WHNF,
+ value: new_val,
+ ty: ty,
+ }
+ }
// Already in WHNF
WHNF | NF => vint,
},
@@ -221,7 +234,8 @@ impl Value {
}
pub(crate) fn app(&self, v: Value) -> Value {
- let vovf = apply_any(self.clone(), v.clone());
+ let ty = self.get_type().ok();
+ let vovf = apply_any(self.clone(), v.clone(), ty.as_ref());
match self.as_internal().get_type() {
Err(_) => vovf.into_value_untyped(),
Ok(t) => match &*t.as_whnf() {
@@ -240,15 +254,18 @@ impl Value {
}
impl VoVF {
- pub(crate) fn into_whnf(self) -> ValueF {
+ pub(crate) fn into_whnf_and_type(
+ self,
+ ty: Option<&Value>,
+ ) -> (ValueF, Option<Value>) {
match self {
- VoVF::Value(v) => v.to_whnf(),
VoVF::ValueF {
val,
form: Unevaled,
- } => normalize_whnf(val).into_whnf(),
+ } => normalize_whnf(val, ty).into_whnf_and_type(ty),
// Already at lest in WHNF
- VoVF::ValueF { val, .. } => val,
+ VoVF::ValueF { val, .. } => (val, None),
+ VoVF::Value(v) => (v.to_whnf(), v.get_type().ok()),
}
}
pub(crate) fn into_value_untyped(self) -> Value {