From b694e567392256eb0a429586b2230253d4d80564 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Thu, 11 Apr 2019 15:25:04 +0200
Subject: Improve simple type handling in typecheck

---
 dhall/src/expr.rs      |  5 ++++
 dhall/src/typecheck.rs | 71 ++++++++++++++++++++++++--------------------------
 2 files changed, 39 insertions(+), 37 deletions(-)

(limited to 'dhall/src')

diff --git a/dhall/src/expr.rs b/dhall/src/expr.rs
index 6458be9..30ca6c6 100644
--- a/dhall/src/expr.rs
+++ b/dhall/src/expr.rs
@@ -88,3 +88,8 @@ impl Normalized {
     }
 }
 
+impl SimpleType {
+    pub(crate) fn into_type(self) -> Type {
+        Normalized(self.0, Some(Type::const_type())).into_type()
+    }
+}
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 3350964..cab734e 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -278,9 +278,10 @@ macro_rules! ensure_matches {
     };
 }
 
-macro_rules! ensure_is_type {
+// Ensure the provided type has type `Type`
+macro_rules! ensure_simple_type {
     ($x:expr, $err:expr $(,)*) => {
-        ensure_matches!($x, Const(Type) => {}, $err)
+        ensure_matches!($x.get_type()?, Const(Type) => {}, $err)
     };
 }
 
@@ -297,7 +298,6 @@ pub fn type_with(
     e: SubExpr<X, X>,
 ) -> Result<Typed, TypeError<X>> {
     use dhall_core::BinOp::*;
-    use dhall_core::Builtin::*;
     use dhall_core::Const::*;
     use dhall_core::ExprF::*;
     let mkerr = |msg: TypeMessage<_>| TypeError::new(ctx, e.clone(), msg);
@@ -305,6 +305,8 @@ pub fn type_with(
     let mktype =
         |ctx, x: SubExpr<X, X>| Ok(type_with(ctx, x)?.normalize().into_type());
 
+    let mksimpletype = |x: SubExpr<X, X>| SimpleType(x).into_type();
+
     enum Ret {
         RetType(crate::expr::Type),
         RetExpr(Expr<X, X>),
@@ -396,8 +398,8 @@ pub fn type_with(
             Lam(_, _, _) => unreachable!(),
             Pi(_, _, _) => unreachable!(),
             Let(_, _, _, _) => unreachable!(),
-            Const(Type) => Ok(RetExpr(dhall::expr!(Kind))),
-            Const(Kind) => Ok(RetExpr(dhall::expr!(Sort))),
+            Const(Type) => Ok(RetType(crate::expr::Type::const_kind())),
+            Const(Kind) => Ok(RetType(crate::expr::Type::const_sort())),
             Const(Sort) => {
                 Ok(RetType(crate::expr::Type(TypeInternal::SuperType)))
             }
@@ -446,16 +448,17 @@ pub fn type_with(
             BoolIf(x, y, z) => {
                 ensure_equal!(
                     x.get_type()?,
-                    &mktype(ctx, rc(Builtin(Bool)))?,
+                    &mksimpletype(dhall::subexpr!(Bool)),
                     mkerr(InvalidPredicate(x)),
                 );
-                ensure_is_type!(
-                    y.get_type()?.get_type()?,
+
+                ensure_simple_type!(
+                    y.get_type()?,
                     mkerr(IfBranchMustBeTerm(true, y)),
                 );
 
-                ensure_is_type!(
-                    z.get_type()?.get_type()?,
+                ensure_simple_type!(
+                    z.get_type()?,
                     mkerr(IfBranchMustBeTerm(false, z)),
                 );
 
@@ -469,8 +472,8 @@ pub fn type_with(
             }
             EmptyListLit(t) => {
                 let t = t.normalize().into_type();
-                ensure_is_type!(
-                    t.get_type()?,
+                ensure_simple_type!(
+                    t,
                     mkerr(InvalidListType(t.into_normalized()?)),
                 );
                 let t = t.into_normalized()?.into_expr();
@@ -479,8 +482,8 @@ pub fn type_with(
             NEListLit(xs) => {
                 let mut iter = xs.into_iter().enumerate();
                 let (_, x) = iter.next().unwrap();
-                ensure_is_type!(
-                    x.get_type()?.get_type()?,
+                ensure_simple_type!(
+                    x.get_type()?,
                     mkerr(InvalidListType(
                         x.get_type_move()?.into_normalized()?
                     )),
@@ -501,8 +504,8 @@ pub fn type_with(
             }
             EmptyOptionalLit(t) => {
                 let t = t.normalize().into_type();
-                ensure_is_type!(
-                    t.get_type()?,
+                ensure_simple_type!(
+                    t,
                     mkerr(InvalidOptionalType(t.into_normalized()?)),
                 );
                 let t = t.into_normalized()?.into_expr();
@@ -510,8 +513,8 @@ pub fn type_with(
             }
             NEOptionalLit(x) => {
                 let tx = x.get_type_move()?;
-                ensure_is_type!(
-                    tx.get_type()?,
+                ensure_simple_type!(
+                    tx,
                     mkerr(InvalidOptionalType(tx.into_normalized()?,)),
                 );
                 let t = tx.into_normalized()?.into_expr();
@@ -519,10 +522,7 @@ pub fn type_with(
             }
             RecordType(kts) => {
                 for (k, t) in kts {
-                    ensure_is_type!(
-                        t.get_type()?,
-                        mkerr(InvalidFieldType(k, t)),
-                    );
+                    ensure_simple_type!(t, mkerr(InvalidFieldType(k, t)),);
                 }
                 Ok(RetExpr(dhall::expr!(Type)))
             }
@@ -530,8 +530,8 @@ pub fn type_with(
                 let kts = kvs
                     .into_iter()
                     .map(|(k, v)| {
-                        ensure_is_type!(
-                            v.get_type()?.get_type()?,
+                        ensure_simple_type!(
+                            v.get_type()?,
                             mkerr(InvalidField(k, v)),
                         );
                         Ok((
@@ -557,19 +557,16 @@ pub fn type_with(
             // TODO: check type of interpolations
             TextLit(_) => Ok(RetExpr(dhall::expr!(Text))),
             BinOp(o, l, r) => {
-                let t = mktype(
-                    ctx,
-                    match o {
-                        BoolAnd => dhall::subexpr!(Bool),
-                        BoolOr => dhall::subexpr!(Bool),
-                        BoolEQ => dhall::subexpr!(Bool),
-                        BoolNE => dhall::subexpr!(Bool),
-                        NaturalPlus => dhall::subexpr!(Natural),
-                        NaturalTimes => dhall::subexpr!(Natural),
-                        TextAppend => dhall::subexpr!(Text),
-                        _ => panic!("Unimplemented typecheck case: {:?}", e),
-                    },
-                )?;
+                let t = mksimpletype(match o {
+                    BoolAnd => dhall::subexpr!(Bool),
+                    BoolOr => dhall::subexpr!(Bool),
+                    BoolEQ => dhall::subexpr!(Bool),
+                    BoolNE => dhall::subexpr!(Bool),
+                    NaturalPlus => dhall::subexpr!(Natural),
+                    NaturalTimes => dhall::subexpr!(Natural),
+                    TextAppend => dhall::subexpr!(Text),
+                    _ => panic!("Unimplemented typecheck case: {:?}", e),
+                });
 
                 ensure_equal!(
                     l.get_type()?,
-- 
cgit v1.2.3