From 98399997cf289d802fbed674558665547cf73d59 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 25 Aug 2019 16:09:55 +0200
Subject: Keep type information through normalization

---
 dhall/src/core/value.rs | 39 ++++++++++++++++++++++++++++-----------
 1 file changed, 28 insertions(+), 11 deletions(-)

(limited to 'dhall/src/core')

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 {
-- 
cgit v1.2.3