From db3ca819283f9bd99d197de464717f0b58b52fe4 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Thu, 2 May 2019 17:07:11 +0200
Subject: Instead of possibly nonexistent Type, treat Sort specially

---
 dhall/src/expr.rs | 158 ++++++++++++++++++++++++++++++++++++++++++++----------
 1 file changed, 129 insertions(+), 29 deletions(-)

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

diff --git a/dhall/src/expr.rs b/dhall/src/expr.rs
index a753ffd..4d55f4a 100644
--- a/dhall/src/expr.rs
+++ b/dhall/src/expr.rs
@@ -1,4 +1,5 @@
 use crate::imports::ImportRoot;
+use crate::normalize::{Thunk, Value};
 use dhall_core::*;
 use std::marker::PhantomData;
 
@@ -36,23 +37,23 @@ pub(crate) struct Resolved<'a>(
 );
 derive_other_traits!(Resolved);
 
+pub(crate) use self::typed::TypedInternal;
+
 #[derive(Debug, Clone)]
 pub(crate) struct Typed<'a>(
-    pub(crate) crate::normalize::Thunk,
-    pub(crate) Option<Type<'static>>,
+    pub(crate) TypedInternal,
     pub(crate) PhantomData<&'a ()>,
 );
 
 #[derive(Debug, Clone)]
 pub(crate) struct Normalized<'a>(
-    pub(crate) crate::normalize::Thunk,
-    pub(crate) Option<Type<'static>>,
+    pub(crate) TypedInternal,
     pub(crate) PhantomData<&'a ()>,
 );
 
 impl<'a> std::cmp::PartialEq for Normalized<'a> {
     fn eq(&self, other: &Self) -> bool {
-        self.0.normalize_to_expr() == other.0.normalize_to_expr()
+        self.to_expr() == other.to_expr()
     }
 }
 
@@ -60,7 +61,110 @@ impl<'a> std::cmp::Eq for Normalized<'a> {}
 
 impl<'a> std::fmt::Display for Normalized<'a> {
     fn fmt(&self, f: &mut std::fmt::Formatter) -> Result<(), std::fmt::Error> {
-        self.0.normalize_to_expr().fmt(f)
+        self.to_expr().fmt(f)
+    }
+}
+
+mod typed {
+    use super::{Type, Typed};
+    use crate::normalize::{Thunk, Value};
+    use crate::typecheck::{
+        TypeError, TypeInternal, TypeMessage, TypecheckContext,
+    };
+    use dhall_core::{Const, Label, SubExpr, V, X};
+    use std::borrow::Cow;
+    use std::marker::PhantomData;
+
+    #[derive(Debug, Clone)]
+    pub(crate) enum TypedInternal {
+        // The `Sort` higher-kinded type doesn't have a type
+        Sort,
+        // Any other value, along with its type
+        Value(Thunk, Option<Type<'static>>),
+    }
+
+    impl TypedInternal {
+        pub(crate) fn from_thunk_and_type(th: Thunk, t: Type<'static>) -> Self {
+            TypedInternal::Value(th, Some(t))
+        }
+
+        pub(crate) fn from_thunk_untyped(th: Thunk) -> Self {
+            TypedInternal::Value(th, None)
+        }
+
+        // TODO: Avoid cloning if possible
+        pub(crate) fn to_value(&self) -> Value {
+            match self {
+                TypedInternal::Value(th, _) => th.normalize_whnf().clone(),
+                TypedInternal::Sort => Value::Const(Const::Sort),
+            }
+        }
+
+        pub(crate) fn to_expr(&self) -> SubExpr<X, X> {
+            self.to_value().normalize_to_expr()
+        }
+
+        pub(crate) fn to_thunk(&self) -> Thunk {
+            match self {
+                TypedInternal::Value(th, _) => th.clone(),
+                TypedInternal::Sort => {
+                    Thunk::from_whnf(Value::Const(Const::Sort))
+                }
+            }
+        }
+
+        pub(crate) fn to_type(&self) -> Type<'static> {
+            match self {
+                TypedInternal::Sort => Type(TypeInternal::Const(Const::Sort)),
+                TypedInternal::Value(th, _) => match &*th.normalize_whnf() {
+                    Value::Const(c) => Type(TypeInternal::Const(*c)),
+                    _ => Type(TypeInternal::Typed(Box::new(Typed(
+                        self.clone(),
+                        PhantomData,
+                    )))),
+                },
+            }
+        }
+
+        pub(crate) fn get_type(
+            &self,
+        ) -> Result<Cow<'_, Type<'static>>, TypeError> {
+            match self {
+                TypedInternal::Value(_, Some(t)) => Ok(Cow::Borrowed(t)),
+                TypedInternal::Value(_, None) => Err(TypeError::new(
+                    &TypecheckContext::new(),
+                    TypeMessage::Untyped,
+                )),
+                TypedInternal::Sort => Err(TypeError::new(
+                    &TypecheckContext::new(),
+                    TypeMessage::Sort,
+                )),
+            }
+        }
+
+        pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+            match self {
+                TypedInternal::Value(th, t) => TypedInternal::Value(
+                    th.shift(delta, var),
+                    t.as_ref().map(|x| x.shift(delta, var)),
+                ),
+                TypedInternal::Sort => TypedInternal::Sort,
+            }
+        }
+
+        pub(crate) fn subst_shift(
+            &self,
+            var: &V<Label>,
+            val: &Typed<'static>,
+        ) -> Self {
+            match self {
+                TypedInternal::Value(th, t) => TypedInternal::Value(
+                    th.subst_shift(var, val),
+                    t.as_ref().map(|x| x.subst_shift(var, val)),
+                ),
+                TypedInternal::Sort => TypedInternal::Sort,
+            }
+        }
     }
 }
 
@@ -88,10 +192,7 @@ pub struct Type<'a>(pub(crate) TypeInternal<'a>);
 
 impl<'a> std::fmt::Display for Type<'a> {
     fn fmt(&self, f: &mut std::fmt::Formatter) -> Result<(), std::fmt::Error> {
-        match self.0.clone().into_normalized() {
-            Ok(e) => e.fmt(f),
-            Err(_) => write!(f, "SuperType"),
-        }
+        self.to_normalized().fmt(f)
     }
 }
 
@@ -115,39 +216,38 @@ impl<'a> From<SubExpr<X, X>> for SimpleType<'a> {
 #[doc(hidden)]
 impl<'a> From<Normalized<'a>> for Typed<'a> {
     fn from(x: Normalized<'a>) -> Typed<'a> {
-        Typed(x.0, x.1, x.2)
+        Typed(x.0, x.1)
     }
 }
 
 impl<'a> Normalized<'a> {
+    pub(crate) fn from_thunk_and_type(th: Thunk, t: Type<'static>) -> Self {
+        Normalized(TypedInternal::from_thunk_and_type(th, t), PhantomData)
+    }
     // Deprecated
     pub(crate) fn as_expr(&self) -> SubExpr<X, X> {
-        self.0.normalize_to_expr()
+        self.0.to_expr()
     }
     pub(crate) fn to_expr(&self) -> SubExpr<X, X> {
-        self.0.normalize_to_expr()
+        self.0.to_expr()
     }
-    pub(crate) fn to_value(&self) -> crate::normalize::Value {
-        self.0.normalize_nf().clone()
+    pub(crate) fn to_value(&self) -> Value {
+        self.0.to_value()
     }
     #[allow(dead_code)]
     pub(crate) fn unnote<'b>(self) -> Normalized<'b> {
-        Normalized(self.0, self.1, PhantomData)
+        Normalized(self.0, PhantomData)
     }
 }
 
-#[doc(hidden)]
-impl<'a> Type<'a> {
-    pub(crate) fn unnote<'b>(self) -> Type<'b> {
-        // use TypeInternal::*;
-        // Type(match self.0 {
-        //     Expr(e) => Expr(Box::new(e.unnote())),
-        //     Pi(ctx, c, x, t, e) => Pi(ctx, c, x, t, e),
-        //     Const(c) => Const(c),
-        //     SuperType => SuperType,
-        // })
-
-        // Yes, this is positively horrible. Please forgive me.
-        unsafe { std::mem::transmute::<Type<'a>, Type<'b>>(self) }
+impl<'a> Typed<'a> {
+    pub(crate) fn from_thunk_and_type(th: Thunk, t: Type<'static>) -> Self {
+        Typed(TypedInternal::from_thunk_and_type(th, t), PhantomData)
+    }
+    pub(crate) fn from_thunk_untyped(th: Thunk) -> Self {
+        Typed(TypedInternal::from_thunk_untyped(th), PhantomData)
+    }
+    pub(crate) fn const_sort() -> Self {
+        Typed(TypedInternal::Sort, PhantomData)
     }
 }
-- 
cgit v1.2.3