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/expr.rs      |   7 ---
 dhall/src/normalize.rs |  74 ++++++++++++--------------
 dhall/src/typecheck.rs | 137 ++++++++++++++++++++++---------------------------
 3 files changed, 94 insertions(+), 124 deletions(-)

(limited to 'dhall/src')

diff --git a/dhall/src/expr.rs b/dhall/src/expr.rs
index c794324..1ddc4ba 100644
--- a/dhall/src/expr.rs
+++ b/dhall/src/expr.rs
@@ -43,13 +43,6 @@ pub(crate) struct Typed<'a>(
     pub(crate) PhantomData<&'a ()>,
 );
 
-#[derive(Debug, Clone)]
-pub(crate) struct PartiallyNormalized<'a>(
-    pub(crate) crate::normalize::Value,
-    pub(crate) Option<Type<'static>>,
-    pub(crate) PhantomData<&'a ()>,
-);
-
 #[derive(Debug, Clone)]
 pub(crate) struct Normalized<'a>(
     pub(crate) SubExpr<X, X>,
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 5151790..f15eea4 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -9,7 +9,7 @@ use dhall_core::{
 };
 use dhall_generator as dhall;
 
-use crate::expr::{Normalized, PartiallyNormalized, Type, Typed};
+use crate::expr::{Normalized, Type, Typed};
 
 type InputSubExpr = SubExpr<X, Normalized<'static>>;
 type OutputSubExpr = SubExpr<X, X>;
@@ -25,37 +25,35 @@ impl<'a> Typed<'a> {
     /// leave ill-typed sub-expressions unevaluated.
     ///
     pub fn normalize(self) -> Normalized<'a> {
-        self.partially_normalize().normalize()
+        Normalized(self.0.as_whnf().normalize_to_expr(), self.1, self.2)
     }
-    pub(crate) fn partially_normalize(self) -> PartiallyNormalized<'a> {
-        PartiallyNormalized(self.0.as_whnf(), self.1, self.2)
-    }
-}
 
-impl<'a> PartiallyNormalized<'a> {
-    pub(crate) fn normalize(self) -> Normalized<'a> {
-        Normalized(self.0.normalize_to_expr(), self.1, self.2)
-    }
     pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self {
-        PartiallyNormalized(
+        Typed(
             self.0.shift(delta, var),
             self.1.as_ref().map(|x| x.shift(delta, var)),
             self.2,
         )
     }
+
     pub(crate) fn subst_shift(
         &self,
         var: &V<Label>,
-        val: &PartiallyNormalized<'static>,
+        val: &Typed<'static>,
     ) -> Self {
-        PartiallyNormalized(
+        Typed(
             self.0.subst_shift(var, val),
             self.1.as_ref().map(|x| x.subst_shift(var, val)),
             self.2,
         )
     }
-    pub(crate) fn into_whnf(self) -> Value {
-        self.0
+
+    pub(crate) fn normalize_whnf(&self) -> Value {
+        self.0.as_whnf()
+    }
+
+    pub(crate) fn as_thunk(&self) -> Thunk {
+        self.0.clone()
     }
 }
 
@@ -268,13 +266,11 @@ impl EnvItem {
     pub(crate) fn subst_shift(
         &self,
         var: &V<Label>,
-        val: &PartiallyNormalized<'static>,
+        val: &Typed<'static>,
     ) -> Self {
         match self {
             EnvItem::Thunk(e) => EnvItem::Thunk(e.subst_shift(var, val)),
-            EnvItem::Skip(v) if v == var => {
-                EnvItem::Thunk(Thunk::from_whnf(val.clone().into_whnf()))
-            }
+            EnvItem::Skip(v) if v == var => EnvItem::Thunk(val.as_thunk()),
             EnvItem::Skip(v) => EnvItem::Skip(v.shift(-1, var)),
         }
     }
@@ -331,11 +327,7 @@ impl NormalizationContext {
         NormalizationContext(Rc::new(self.0.map(|_, e| e.shift(delta, var))))
     }
 
-    fn subst_shift(
-        &self,
-        var: &V<Label>,
-        val: &PartiallyNormalized<'static>,
-    ) -> Self {
+    fn subst_shift(&self, var: &V<Label>, val: &Typed<'static>) -> Self {
         NormalizationContext(Rc::new(
             self.0.map(|_, e| e.subst_shift(var, val)),
         ))
@@ -377,6 +369,10 @@ pub(crate) enum Value {
 }
 
 impl Value {
+    pub(crate) fn into_thunk(self) -> Thunk {
+        Thunk::from_whnf(self)
+    }
+
     /// Convert the value back to a (normalized) syntactic expression
     pub(crate) fn normalize_to_expr(self) -> OutputSubExpr {
         match self {
@@ -585,8 +581,11 @@ impl Value {
     pub(crate) fn app(self, val: Value) -> Value {
         match (self, val) {
             (Value::Lam(x, _, e), val) => {
-                let val =
-                    PartiallyNormalized(val, None, std::marker::PhantomData);
+                let val = Typed(
+                    Thunk::from_whnf(val),
+                    None,
+                    std::marker::PhantomData,
+                );
                 e.subst_shift(&V(x, 0), &val).as_whnf()
             }
             (Value::AppliedBuiltin(b, mut args), val) => {
@@ -717,7 +716,7 @@ impl Value {
     pub(crate) fn subst_shift(
         &self,
         var: &V<Label>,
-        val: &PartiallyNormalized<'static>,
+        val: &Typed<'static>,
     ) -> Self {
         match self {
             Value::Lam(x, t, e) => Value::Lam(
@@ -742,7 +741,7 @@ impl Value {
                 t.subst_shift(var, val),
                 e.subst_shift(&var.shift0(1, x), val),
             ),
-            Value::Var(v) if v == var => val.clone().into_whnf(),
+            Value::Var(v) if v == var => val.normalize_whnf(),
             Value::Var(v) => Value::Var(v.shift(-1, var)),
             Value::Const(c) => Value::Const(*c),
             Value::BoolLit(b) => Value::BoolLit(*b),
@@ -814,7 +813,7 @@ impl Value {
 
 mod thunk {
     use super::{normalize_whnf, InputSubExpr, NormalizationContext, Value};
-    use crate::expr::PartiallyNormalized;
+    use crate::expr::Typed;
     use dhall_core::{Label, V};
     use std::cell::RefCell;
     use std::rc::Rc;
@@ -900,11 +899,7 @@ mod thunk {
             }
         }
 
-        fn subst_shift(
-            &self,
-            var: &V<Label>,
-            val: &PartiallyNormalized<'static>,
-        ) -> Self {
+        fn subst_shift(&self, var: &V<Label>, val: &Typed<'static>) -> Self {
             match self {
                 ThunkInternal::Unnormalized(ctx, e) => {
                     ThunkInternal::Unnormalized(
@@ -953,7 +948,7 @@ mod thunk {
         pub(crate) fn subst_shift(
             &self,
             var: &V<Label>,
-            val: &PartiallyNormalized<'static>,
+            val: &Typed<'static>,
         ) -> Self {
             self.0.borrow().subst_shift(var, val).into_thunk()
         }
@@ -1003,7 +998,7 @@ impl TypeThunk {
     pub(crate) fn subst_shift(
         &self,
         var: &V<Label>,
-        val: &PartiallyNormalized<'static>,
+        val: &Typed<'static>,
     ) -> Self {
         match self {
             TypeThunk::Thunk(th) => TypeThunk::Thunk(th.subst_shift(var, val)),
@@ -1015,12 +1010,7 @@ impl TypeThunk {
         match self {
             TypeThunk::Thunk(th) => th.as_nf(),
             // TODO: let's hope for the best with the unwrap
-            TypeThunk::Type(t) => t
-                .clone()
-                .partially_normalize()
-                .unwrap()
-                .into_whnf()
-                .normalize(),
+            TypeThunk::Type(t) => t.normalize_whnf().unwrap().normalize(),
         }
     }
 }
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