From ec349d42703a8a31715cf97b44845ba3dd7a6805 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 20 Aug 2019 22:20:59 +0200
Subject: Propagate type information in Value::app()

---
 dhall/src/phase/normalize.rs | 35 ++++++++++++++++-------------------
 dhall/src/phase/typecheck.rs | 10 ++--------
 2 files changed, 18 insertions(+), 27 deletions(-)

(limited to 'dhall/src/phase')

diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs
index a146ec7..e4a0c5b 100644
--- a/dhall/src/phase/normalize.rs
+++ b/dhall/src/phase/normalize.rs
@@ -34,7 +34,6 @@ macro_rules! make_closure {
     (List $($rest:tt)*) => {
         Value::from_builtin(Builtin::List)
             .app(make_closure!($($rest)*))
-            .into_value_simple_type()
     };
     (Some($($rest:tt)*)) => {
         ValueF::NEOptionalLit(make_closure!($($rest)*))
@@ -251,9 +250,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> VoVF {
                 }
             }
             _ => {
-                let list_t = Value::from_builtin(List)
-                    .app(t.clone())
-                    .into_value_simple_type();
+                let list_t = Value::from_builtin(List).app(t.clone());
                 Ok((
                     r,
                     f.app(list_t.clone())
@@ -269,18 +266,19 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> VoVF {
                         .app(
                             EmptyListLit(t.clone())
                                 .into_value_with_type(list_t),
-                        ),
+                        )
+                        .into_vovf(),
                 ))
             }
         },
         (ListFold, [_, l, _, cons, nil, r..]) => match &*l.as_whnf() {
             EmptyListLit(_) => Ok((r, nil.clone().into_vovf())),
             NEListLit(xs) => {
-                let mut v = nil.clone().into_vovf();
+                let mut v = nil.clone();
                 for x in xs.iter().cloned().rev() {
-                    v = cons.app(x).app(v.into_value_untyped());
+                    v = cons.app(x).app(v);
                 }
-                Ok((r, v))
+                Ok((r, v.into_vovf()))
             }
             _ => Err(()),
         },
@@ -295,9 +293,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> VoVF {
                 }
             }
             _ => {
-                let optional_t = Value::from_builtin(Optional)
-                    .app(t.clone())
-                    .into_value_simple_type();
+                let optional_t = Value::from_builtin(Optional).app(t.clone());
                 Ok((
                     r,
                     f.app(optional_t.clone())
@@ -305,13 +301,14 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> VoVF {
                         .app(
                             EmptyOptionalLit(t.clone())
                                 .into_value_with_type(optional_t),
-                        ),
+                        )
+                        .into_vovf(),
                 ))
             }
         },
         (OptionalFold, [_, v, _, just, nothing, r..]) => match &*v.as_whnf() {
             EmptyOptionalLit(_) => Ok((r, nothing.clone().into_vovf())),
-            NEOptionalLit(x) => Ok((r, just.app(x.clone()))),
+            NEOptionalLit(x) => Ok((r, just.app(x.clone()).into_vovf())),
             _ => Err(()),
         },
         (NaturalBuild, [f, r..]) => match &*f.as_whnf() {
@@ -331,7 +328,8 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> VoVF {
                     .app(
                         NaturalLit(0)
                             .into_value_with_type(Value::from_builtin(Natural)),
-                    ),
+                    )
+                    .into_vovf(),
             )),
         },
         (NaturalFold, [n, t, succ, zero, r..]) => match &*n.as_whnf() {
@@ -344,9 +342,8 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> VoVF {
                     )
                     .app(t.clone())
                     .app(succ.clone())
-                    .app(zero.clone())
-                    .into_value_with_type(t.clone());
-                Ok((r, succ.app(fold)))
+                    .app(zero.clone());
+                Ok((r, succ.app(fold).into_vovf()))
             }
             _ => Err(()),
         },
@@ -643,7 +640,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> VoVF {
         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::VoVF(v.app(a)),
+        ExprF::App(v, a) => Ret::Value(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)),
@@ -765,7 +762,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> VoVF {
                     }
                 },
                 (RecordLit(kvs), UnionLit(l, v, _)) => match kvs.get(l) {
-                    Some(h) => Ret::VoVF(h.app(v.clone())),
+                    Some(h) => Ret::Value(h.app(v.clone())),
                     None => {
                         drop(handlers_borrow);
                         drop(variant_borrow);
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs
index 4abc314..abe05a3 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/phase/typecheck.rs
@@ -455,11 +455,7 @@ fn type_last_layer(
                 return mkerr(InvalidListType(t));
             }
 
-            RetTypeOnly(
-                ValueF::from_builtin(dhall_syntax::Builtin::List)
-                    .app(t)
-                    .into_value_simple_type(),
-            )
+            RetTypeOnly(Value::from_builtin(dhall_syntax::Builtin::List).app(t))
         }
         SomeLit(x) => {
             let t = x.get_type()?;
@@ -468,9 +464,7 @@ fn type_last_layer(
             }
 
             RetTypeOnly(
-                Value::from_builtin(dhall_syntax::Builtin::Optional)
-                    .app(t)
-                    .into_value_simple_type(),
+                Value::from_builtin(dhall_syntax::Builtin::Optional).app(t),
             )
         }
         RecordType(kts) => RetWhole(tck_record_type(
-- 
cgit v1.2.3