From 77198a2833297289770867acdaf31db0e2011ea9 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 30 Apr 2019 15:35:13 +0200
Subject: Merge Typed and PartiallyNormalized

---
 dhall/src/typecheck.rs | 137 ++++++++++++++++++++++---------------------------
 1 file changed, 62 insertions(+), 75 deletions(-)

(limited to 'dhall/src/typecheck.rs')

diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 85de42a..f22925a 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -68,8 +68,8 @@ impl<'a> Normalized<'a> {
                 // TODO: wasteful
                 type_with(ctx, self.0.embed_absurd())?.normalize_to_type()
             }
-            _ => Type(TypeInternal::PNzed(Box::new(PartiallyNormalized(
-                Value::Expr(self.0),
+            _ => Type(TypeInternal::Typed(Box::new(Typed(
+                Value::Expr(self.0).into_thunk(),
                 self.1,
                 self.2,
             )))),
@@ -86,11 +86,12 @@ impl Normalized<'static> {
         rc(ExprF::Embed(self))
     }
 }
-impl<'a> PartiallyNormalized<'a> {
+impl<'a> Typed<'a> {
     fn normalize_to_type(self) -> Type<'a> {
-        match &self.0 {
+        // TODO: avoid cloning Value
+        match &self.normalize_whnf() {
             Value::Const(c) => Type(TypeInternal::Const(*c)),
-            _ => Type(TypeInternal::PNzed(Box::new(self))),
+            _ => Type(TypeInternal::Typed(Box::new(self))),
         }
     }
 }
@@ -103,18 +104,16 @@ impl<'a> Type<'a> {
     pub(crate) fn into_normalized(self) -> Result<Normalized<'a>, TypeError> {
         self.0.into_normalized()
     }
-    fn normalize_whnf(self) -> Result<Value, TypeError> {
+    pub(crate) fn normalize_whnf(&self) -> Result<Value, TypeError> {
         self.0.normalize_whnf()
     }
-    pub(crate) fn partially_normalize(
-        self,
-    ) -> Result<PartiallyNormalized<'a>, TypeError> {
-        self.0.partially_normalize()
+    pub(crate) fn as_typed(&self) -> Result<Typed<'a>, TypeError> {
+        self.0.as_typed()
     }
     fn internal(&self) -> &TypeInternal<'a> {
         &self.0
     }
-    fn internal_whnf(&self) -> Option<&Value> {
+    fn internal_whnf(&self) -> Option<Value> {
         self.0.whnf()
     }
     pub(crate) fn shift0(&self, delta: isize, label: &Label) -> Self {
@@ -126,7 +125,7 @@ impl<'a> Type<'a> {
     pub(crate) fn subst_shift(
         &self,
         var: &V<Label>,
-        val: &PartiallyNormalized<'static>,
+        val: &Typed<'static>,
     ) -> Self {
         Type(self.0.subst_shift(var, val))
     }
@@ -172,20 +171,20 @@ pub(crate) enum TypeInternal<'a> {
     /// The type of `Sort`
     SuperType,
     /// This must not contain Const value.
-    PNzed(Box<PartiallyNormalized<'a>>),
+    Typed(Box<Typed<'a>>),
 }
 
 impl<'a> TypeInternal<'a> {
-    pub(crate) fn into_normalized(self) -> Result<Normalized<'a>, TypeError> {
-        Ok(self.partially_normalize()?.normalize())
+    pub(crate) fn into_normalized(&self) -> Result<Normalized<'a>, TypeError> {
+        Ok(self.as_typed()?.normalize())
     }
-    fn normalize_whnf(self) -> Result<Value, TypeError> {
-        Ok(self.partially_normalize()?.into_whnf())
+    fn normalize_whnf(&self) -> Result<Value, TypeError> {
+        Ok(self.as_typed()?.normalize_whnf())
     }
-    fn partially_normalize(self) -> Result<PartiallyNormalized<'a>, TypeError> {
+    fn as_typed(&self) -> Result<Typed<'a>, TypeError> {
         Ok(match self {
-            TypeInternal::PNzed(e) => *e,
-            TypeInternal::Const(c) => const_to_pnormalized(c),
+            TypeInternal::Typed(e) => e.as_ref().clone(),
+            TypeInternal::Const(c) => const_to_typed(*c),
             TypeInternal::SuperType => {
                 return Err(TypeError::new(
                     &TypecheckContext::new(),
@@ -194,9 +193,10 @@ impl<'a> TypeInternal<'a> {
             }
         })
     }
-    fn whnf(&self) -> Option<&Value> {
+    fn whnf(&self) -> Option<Value> {
+        // TODO: return reference
         match self {
-            TypeInternal::PNzed(e) => Some(&e.0),
+            TypeInternal::Typed(e) => Some(e.normalize_whnf()),
             _ => None,
         }
     }
@@ -206,19 +206,15 @@ impl<'a> TypeInternal<'a> {
     fn shift(&self, delta: isize, var: &V<Label>) -> Self {
         use TypeInternal::*;
         match self {
-            PNzed(e) => PNzed(Box::new(e.shift(delta, var))),
+            Typed(e) => Typed(Box::new(e.shift(delta, var))),
             Const(c) => Const(*c),
             SuperType => SuperType,
         }
     }
-    fn subst_shift(
-        &self,
-        var: &V<Label>,
-        val: &PartiallyNormalized<'static>,
-    ) -> Self {
+    fn subst_shift(&self, var: &V<Label>, val: &Typed<'static>) -> Self {
         use TypeInternal::*;
         match self {
-            PNzed(e) => PNzed(Box::new(e.subst_shift(var, val))),
+            Typed(e) => Typed(Box::new(e.subst_shift(var, val))),
             Const(c) => Const(*c),
             SuperType => SuperType,
         }
@@ -252,9 +248,7 @@ impl TypedOrType {
     }
     fn normalize_to_type(self) -> Type<'static> {
         match self {
-            TypedOrType::Typed(e) => {
-                e.partially_normalize().normalize_to_type()
-            }
+            TypedOrType::Typed(e) => e.normalize_to_type(),
             TypedOrType::Type(t) => t,
         }
     }
@@ -270,12 +264,10 @@ impl TypedOrType {
             TypedOrType::Type(t) => Ok(t.get_type()?.into_owned()),
         }
     }
-    fn partially_normalize(
-        self,
-    ) -> Result<PartiallyNormalized<'static>, TypeError> {
+    fn as_typed(&self) -> Result<Typed<'static>, TypeError> {
         match self {
-            TypedOrType::Typed(e) => Ok(e.partially_normalize()),
-            TypedOrType::Type(t) => Ok(t.partially_normalize()?),
+            TypedOrType::Typed(e) => Ok(e.clone()),
+            TypedOrType::Type(t) => Ok(t.as_typed()?),
         }
     }
 }
@@ -442,8 +434,12 @@ where
     }
 }
 
-fn const_to_pnormalized<'a>(c: Const) -> PartiallyNormalized<'a> {
-    PartiallyNormalized(Value::Const(c), Some(type_of_const(c)), PhantomData)
+fn const_to_typed<'a>(c: Const) -> Typed<'a> {
+    Typed(
+        Value::Const(c).into_thunk(),
+        Some(type_of_const(c)),
+        PhantomData,
+    )
 }
 
 fn const_to_type<'a>(c: Const) -> Type<'a> {
@@ -555,7 +551,7 @@ pub(crate) enum TypeIntermediate {
 impl TypeIntermediate {
     fn typecheck(self) -> Result<TypedOrType, TypeError> {
         let mkerr = |ctx, msg| TypeError::new(ctx, msg);
-        match &self {
+        let typed = match &self {
             TypeIntermediate::Pi(ctx, x, ta, tb) => {
                 let ctx2 = ctx.insert_type(x, ta.clone());
 
@@ -600,18 +596,16 @@ impl TypeIntermediate {
                     }
                 };
 
-                let pnormalized = PartiallyNormalized(
+                Typed(
                     Value::Pi(
                         x.clone(),
                         TypeThunk::from_type(ta.clone()),
                         TypeThunk::from_type(tb.clone()),
-                    ),
+                    )
+                    .into_thunk(),
                     Some(const_to_type(k)),
                     PhantomData,
-                );
-                Ok(TypedOrType::Type(Type(TypeInternal::PNzed(Box::new(
-                    pnormalized,
-                )))))
+                )
             }
             TypeIntermediate::RecordType(ctx, kts) => {
                 // Check that all types are the same const
@@ -634,20 +628,18 @@ impl TypeIntermediate {
                 // An empty record type has type Type
                 let k = k.unwrap_or(dhall_core::Const::Type);
 
-                let pnormalized = PartiallyNormalized(
+                Typed(
                     Value::RecordType(
                         kts.iter()
                             .map(|(k, t)| {
                                 (k.clone(), TypeThunk::from_type(t.clone()))
                             })
                             .collect(),
-                    ),
+                    )
+                    .into_thunk(),
                     Some(const_to_type(k)),
                     PhantomData,
-                );
-                Ok(TypedOrType::Type(Type(TypeInternal::PNzed(Box::new(
-                    pnormalized,
-                )))))
+                )
             }
             TypeIntermediate::UnionType(ctx, kts) => {
                 // Check that all types are the same const
@@ -675,7 +667,7 @@ impl TypeIntermediate {
                 // an union type with only unary variants also has type Type
                 let k = k.unwrap_or(dhall_core::Const::Type);
 
-                let pnormalized = PartiallyNormalized(
+                Typed(
                     Value::UnionType(
                         kts.iter()
                             .map(|(k, t)| {
@@ -687,28 +679,24 @@ impl TypeIntermediate {
                                 )
                             })
                             .collect(),
-                    ),
+                    )
+                    .into_thunk(),
                     Some(const_to_type(k)),
                     PhantomData,
-                );
-                Ok(TypedOrType::Type(Type(TypeInternal::PNzed(Box::new(
-                    pnormalized,
-                )))))
+                )
             }
             TypeIntermediate::ListType(ctx, t) => {
                 ensure_simple_type!(
                     t,
                     mkerr(ctx, InvalidListType(t.clone().into_normalized()?)),
                 );
-                let pnormalized = PartiallyNormalized(
+                Typed(
                     Value::from_builtin(Builtin::List)
-                        .app(t.clone().normalize_whnf()?),
+                        .app(t.clone().normalize_whnf()?)
+                        .into_thunk(),
                     Some(const_to_type(Const::Type)),
                     PhantomData,
-                );
-                Ok(TypedOrType::Type(Type(TypeInternal::PNzed(Box::new(
-                    pnormalized,
-                )))))
+                )
             }
             TypeIntermediate::OptionalType(ctx, t) => {
                 ensure_simple_type!(
@@ -718,17 +706,18 @@ impl TypeIntermediate {
                         InvalidOptionalType(t.clone().into_normalized()?)
                     ),
                 );
-                let pnormalized = PartiallyNormalized(
+                Typed(
                     Value::from_builtin(Builtin::Optional)
-                        .app(t.clone().normalize_whnf()?),
+                        .app(t.clone().normalize_whnf()?)
+                        .into_thunk(),
                     Some(const_to_type(Const::Type)),
                     PhantomData,
-                );
-                Ok(TypedOrType::Type(Type(TypeInternal::PNzed(Box::new(
-                    pnormalized,
-                )))))
+                )
             }
-        }
+        };
+        Ok(TypedOrType::Type(Type(TypeInternal::Typed(Box::new(
+            typed,
+        )))))
     }
 }
 
@@ -867,13 +856,11 @@ fn type_last_layer(
                 }
                 _ => return Err(mkerr(NotAFunction(f))),
             };
-            ensure_equal!(a.get_type()?, tx, {
+            ensure_equal!(a.get_type()?, &tx, {
                 mkerr(TypeMismatch(f.clone(), tx.clone().into_normalized()?, a))
             });
 
-            Ok(RetType(
-                tb.subst_shift(&V(x.clone(), 0), &a.partially_normalize()?),
-            ))
+            Ok(RetType(tb.subst_shift(&V(x.clone(), 0), &a.as_typed()?)))
         }
         Annot(x, t) => {
             let t = t.normalize_to_type();
-- 
cgit v1.2.3