More improvements to typecheck

1 files changed, 114 insertions, 133 deletions

diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index d0e1d44..0ebc67e 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -21,6 +21,9 @@ impl Resolved {
     }
 }
 impl Typed {
+    fn as_expr(&self) -> &SubExpr<X, X> {
+        &self.0
+    }
     pub fn get_type(&self) -> &Type {
         &self.1
     }
@@ -29,15 +32,18 @@ impl Normalized {
     pub fn get_type(&self) -> &Type {
         &self.1
     }
+    fn into_type(self) -> Type {
+        crate::expr::Type(TypeInternal::Expr(Box::new(self)))
+    }
 }
 impl Type {
     // pub fn as_expr(&self) -> &Normalized {
     //     &*self.0
     // }
-    pub fn as_expr(&self) -> &SubExpr<X, X> {
+    fn as_expr(&self) -> &SubExpr<X, X> {
         &self.as_normalized().0
     }
-    pub fn as_normalized(&self) -> &Normalized {
+    fn as_normalized(&self) -> &Normalized {
         use TypeInternal::*;
         match &self.0 {
             Expr(e) => &e,
@@ -49,6 +55,9 @@ impl Type {
     }
 }
 
+const TYPE_OF_SORT: crate::expr::Type =
+    crate::expr::Type(TypeInternal::Universe(4));
+
 fn rule(a: Const, b: Const) -> Result<Const, ()> {
     use dhall_core::Const::*;
     match (a, b) {
@@ -209,8 +218,8 @@ fn type_of_builtin<S>(b: Builtin) -> Expr<S, X> {
 }
 
 fn ensure_equal<'a, S, F1, F2>(
-    x: &'a Expr<S, X>,
-    y: &'a Expr<S, X>,
+    x: &'a Type,
+    y: &'a Type,
     mkerr: F1,
     mkmsg: F2,
 ) -> Result<(), TypeError<S>>
@@ -219,7 +228,7 @@ where
     F1: FnOnce(TypeMessage<S>) -> TypeError<S>,
     F2: FnOnce() -> TypeMessage<S>,
 {
-    if prop_equal(x, y) {
+    if prop_equal(x.as_expr().as_ref(), y.as_expr().as_ref()) {
         Ok(())
     } else {
         Err(mkerr(mkmsg()))
@@ -253,33 +262,40 @@ pub fn type_with(
             _ => Err(mkerr(msg)),
         };
 
+    let mktype =
+        |ctx, x: SubExpr<X, X>| Ok(type_with(ctx, x)?.normalize().into_type());
+
     enum Ret {
-        ErrRet(TypeError<X>),
-        OkNormalized(Normalized),
-        OkType(crate::expr::Type),
-        OkRet(Expr<X, X>),
+        RetType(crate::expr::Type),
+        RetExpr(Expr<X, X>),
     }
     use Ret::*;
     let ret = match e.as_ref() {
         Lam(x, t, b) => {
-            let t2 = type_with(ctx, t.clone())?.normalize();
+            let t2 = mktype(ctx, t.clone())?;
             let ctx2 = ctx
-                .insert(x.clone(), t2.0.clone())
+                .insert(x.clone(), t2.as_expr().clone())
                 .map(|e| shift(1, &V(x.clone(), 0), e));
             let b = type_with(&ctx2, b.clone())?;
             let _ = type_with(
                 ctx,
                 rc(Pi(x.clone(), t.clone(), b.get_type().as_expr().clone())),
             )?;
-            OkRet(Pi(x.clone(), t2.0, b.get_type().as_expr().clone()))
+            Ok(RetExpr(Pi(
+                x.clone(),
+                t2.as_expr().clone(),
+                b.get_type().as_expr().clone(),
+            )))
         }
         Pi(x, tA, tB) => {
-            let tA = type_with(ctx, tA.clone())?.normalize();
-            let kA =
-                ensure_const(tA.get_type(), InvalidInputType(tA.0.clone()))?;
+            let tA = mktype(ctx, tA.clone())?;
+            let kA = ensure_const(
+                tA.get_type(),
+                InvalidInputType(tA.as_expr().clone()),
+            )?;
 
             let ctx2 = ctx
-                .insert(x.clone(), tA.0.clone())
+                .insert(x.clone(), tA.as_expr().clone())
                 .map(|e| shift(1, &V(x.clone(), 0), e));
             let tB = type_with(&ctx2, tB.clone())?;
             let kB = match tB.get_type().as_expr().as_ref() {
@@ -294,11 +310,11 @@ pub fn type_with(
             };
 
             match rule(kA, kB) {
-                Err(()) => ErrRet(mkerr(NoDependentTypes(
-                    tA.0.clone(),
+                Err(()) => Err(mkerr(NoDependentTypes(
+                    tA.as_expr().clone(),
                     tB.get_type().clone(),
                 ))),
-                Ok(_) => OkRet(Const(kB)),
+                Ok(k) => Ok(RetExpr(Const(k))),
             }
         }
         Let(f, mt, r, b) => {
@@ -332,7 +348,7 @@ pub fn type_with(
                 )));
             }
 
-            OkType(b.get_type().clone())
+            Ok(RetType(b.get_type().clone()))
         }
         _ => match e
             .as_ref()
@@ -341,20 +357,20 @@ pub fn type_with(
             Lam(_, _, _) => unreachable!(),
             Pi(_, _, _) => unreachable!(),
             Let(_, _, _, _) => unreachable!(),
-            Const(Type) => OkRet(Const(Kind)),
-            Const(Kind) => OkRet(Const(Sort)),
-            Const(Sort) => ErrRet(mkerr(Untyped)),
+            Const(Type) => Ok(RetExpr(Const(Kind))),
+            Const(Kind) => Ok(RetExpr(Const(Sort))),
+            Const(Sort) => Ok(RetType(TYPE_OF_SORT)),
             Var(V(x, n)) => match ctx.lookup(&x, n) {
-                Some(e) => OkRet(e.unroll()),
-                None => ErrRet(mkerr(UnboundVariable)),
+                Some(e) => Ok(RetExpr(e.unroll())),
+                None => Err(mkerr(UnboundVariable)),
             },
             App(f, args) => {
                 let mut iter = args.into_iter();
                 let mut seen_args: Vec<SubExpr<_, _>> = vec![];
-                let mut tf = f.get_type().as_normalized().clone();
+                let mut tf = f.get_type().clone();
                 while let Some(a) = iter.next() {
                     seen_args.push(a.0.clone());
-                    let (x, tx, tb) = match tf.0.as_ref() {
+                    let (x, tx, tb) = match tf.as_expr().as_ref() {
                         Pi(x, tx, tb) => (x, tx, tb),
                         _ => {
                             return Err(mkerr(NotAFunction(
@@ -363,40 +379,29 @@ pub fn type_with(
                             )));
                         }
                     };
-                    ensure_equal(
-                        tx.as_ref(),
-                        a.get_type().as_expr().as_ref(),
-                        mkerr,
-                        || {
-                            TypeMismatch(
-                                rc(App(f.0.clone(), seen_args.clone())),
-                                tx.clone(),
-                                a.clone(),
-                            )
-                        },
-                    )?;
-                    tf = type_with(
-                        ctx,
-                        subst_shift(&V(x.clone(), 0), &a.0, &tb),
-                    )?
-                    .normalize();
+                    let tx = mktype(ctx, tx.clone())?;
+                    ensure_equal(&tx, a.get_type(), mkerr, || {
+                        TypeMismatch(
+                            rc(App(f.0.clone(), seen_args.clone())),
+                            tx.clone(),
+                            a.clone(),
+                        )
+                    })?;
+                    tf = mktype(ctx, subst_shift(&V(x.clone(), 0), &a.0, &tb))?;
                 }
-                OkNormalized(tf)
+                Ok(RetType(tf))
             }
             Annot(x, t) => {
-                let t = t.normalize();
-                ensure_equal(
-                    t.0.as_ref(),
-                    x.get_type().as_expr().as_ref(),
-                    mkerr,
-                    || AnnotMismatch(x.clone(), t.clone()),
-                )?;
-                OkType(x.get_type().clone())
+                let t = t.normalize().into_type();
+                ensure_equal(&t, x.get_type(), mkerr, || {
+                    AnnotMismatch(x.clone(), t.clone())
+                })?;
+                Ok(RetType(x.get_type().clone()))
             }
             BoolIf(x, y, z) => {
                 ensure_equal(
-                    x.get_type().as_expr().as_ref(),
-                    &Builtin(Bool),
+                    x.get_type(),
+                    &mktype(ctx, rc(Builtin(Bool)))?,
                     mkerr,
                     || InvalidPredicate(x.clone()),
                 )?;
@@ -410,19 +415,16 @@ pub fn type_with(
                     IfBranchMustBeTerm(false, z.clone()),
                 )?;
 
-                ensure_equal(
-                    y.get_type().as_expr().as_ref(),
-                    z.get_type().as_expr().as_ref(),
-                    mkerr,
-                    || IfBranchMismatch(y.clone(), z.clone()),
-                )?;
+                ensure_equal(y.get_type(), z.get_type(), mkerr, || {
+                    IfBranchMismatch(y.clone(), z.clone())
+                })?;
 
-                OkType(y.get_type().clone())
+                Ok(RetType(y.get_type().clone()))
             }
             EmptyListLit(t) => {
                 ensure_is_type(t.get_type(), InvalidListType(t.0.clone()))?;
                 let t = t.normalize().0;
-                OkRet(dhall::expr!(List t))
+                Ok(RetExpr(dhall::expr!(List t)))
             }
             NEListLit(xs) => {
                 let mut iter = xs.into_iter().enumerate();
@@ -432,26 +434,21 @@ pub fn type_with(
                     InvalidListType(x.get_type().as_expr().clone()),
                 )?;
                 for (i, y) in iter {
-                    ensure_equal(
-                        x.get_type().as_expr().as_ref(),
-                        y.get_type().as_expr().as_ref(),
-                        mkerr,
-                        || {
-                            InvalidListElement(
-                                i,
-                                x.get_type().as_expr().clone(),
-                                y.clone(),
-                            )
-                        },
-                    )?;
+                    ensure_equal(x.get_type(), y.get_type(), mkerr, || {
+                        InvalidListElement(
+                            i,
+                            x.get_type().as_expr().clone(),
+                            y.clone(),
+                        )
+                    })?;
                 }
                 let t = x.get_type().as_expr().clone();
-                OkRet(dhall::expr!(List t))
+                Ok(RetExpr(dhall::expr!(List t)))
             }
             EmptyOptionalLit(t) => {
                 ensure_is_type(t.get_type(), InvalidOptionalType(t.0.clone()))?;
                 let t = t.normalize().0;
-                OkRet(dhall::expr!(Optional t))
+                Ok(RetExpr(dhall::expr!(Optional t)))
             }
             NEOptionalLit(x) => {
                 ensure_is_type(
@@ -459,7 +456,7 @@ pub fn type_with(
                     InvalidOptionalType(x.get_type().as_expr().clone()),
                 )?;
                 let t = x.get_type().as_expr().clone();
-                OkRet(dhall::expr!(Optional t))
+                Ok(RetExpr(dhall::expr!(Optional t)))
             }
             RecordType(kts) => {
                 for (k, t) in kts {
@@ -468,7 +465,7 @@ pub fn type_with(
                         InvalidFieldType(k.clone(), t.clone()),
                     )?;
                 }
-                OkRet(Const(Type))
+                Ok(RetExpr(Const(Type)))
             }
             RecordLit(kvs) => {
                 let kts = kvs
@@ -481,70 +478,54 @@ pub fn type_with(
                         Ok((k.clone(), v.get_type().as_expr().clone()))
                     })
                     .collect::<Result<_, _>>()?;
-                OkRet(RecordType(kts))
+                Ok(RetExpr(RecordType(kts)))
             }
             Field(r, x) => match r.get_type().as_expr().as_ref() {
                 RecordType(kts) => match kts.get(&x) {
-                    Some(e) => OkRet(e.unroll()),
-                    None => ErrRet(mkerr(MissingField(x.clone(), r.clone()))),
+                    Some(e) => Ok(RetExpr(e.unroll())),
+                    None => Err(mkerr(MissingField(x.clone(), r.clone()))),
                 },
-                _ => ErrRet(mkerr(NotARecord(x.clone(), r.clone()))),
+                _ => Err(mkerr(NotARecord(x.clone(), r.clone()))),
             },
-            Builtin(b) => OkRet(type_of_builtin(b)),
-            BoolLit(_) => OkRet(Builtin(Bool)),
-            NaturalLit(_) => OkRet(Builtin(Natural)),
-            IntegerLit(_) => OkRet(Builtin(Integer)),
-            DoubleLit(_) => OkRet(Builtin(Double)),
+            Builtin(b) => Ok(RetExpr(type_of_builtin(b))),
+            BoolLit(_) => Ok(RetExpr(Builtin(Bool))),
+            NaturalLit(_) => Ok(RetExpr(Builtin(Natural))),
+            IntegerLit(_) => Ok(RetExpr(Builtin(Integer))),
+            DoubleLit(_) => Ok(RetExpr(Builtin(Double))),
             // TODO: check type of interpolations
-            TextLit(_) => OkRet(Builtin(Text)),
+            TextLit(_) => Ok(RetExpr(Builtin(Text))),
             BinOp(o, l, r) => {
-                let t = Builtin(match o {
-                    BoolAnd => Bool,
-                    BoolOr => Bool,
-                    BoolEQ => Bool,
-                    BoolNE => Bool,
-                    NaturalPlus => Natural,
-                    NaturalTimes => Natural,
-                    TextAppend => Text,
-                    _ => panic!("Unimplemented typecheck case: {:?}", e),
-                });
-
-                ensure_equal(
-                    l.get_type().as_expr().as_ref(),
-                    &t,
-                    mkerr,
-                    || BinOpTypeMismatch(o, l.clone()),
+                let t = mktype(
+                    ctx,
+                    rc(Builtin(match o {
+                        BoolAnd => Bool,
+                        BoolOr => Bool,
+                        BoolEQ => Bool,
+                        BoolNE => Bool,
+                        NaturalPlus => Natural,
+                        NaturalTimes => Natural,
+                        TextAppend => Text,
+                        _ => panic!("Unimplemented typecheck case: {:?}", e),
+                    })),
                 )?;
 
-                ensure_equal(
-                    r.get_type().as_expr().as_ref(),
-                    &t,
-                    mkerr,
-                    || BinOpTypeMismatch(o, r.clone()),
-                )?;
+                ensure_equal(l.get_type(), &t, mkerr, || {
+                    BinOpTypeMismatch(o, l.clone())
+                })?;
 
-                OkRet(t)
+                ensure_equal(r.get_type(), &t, mkerr, || {
+                    BinOpTypeMismatch(o, r.clone())
+                })?;
+
+                Ok(RetType(t))
             }
             Embed(p) => match p {},
             _ => panic!("Unimplemented typecheck case: {:?}", e),
         },
-    };
+    }?;
     match ret {
-        OkRet(Const(Sort)) => {
-            Ok(Typed(e, crate::expr::Type(TypeInternal::Universe(3))))
-        }
-        OkRet(ret) => Ok(Typed(
-            e,
-            crate::expr::Type(TypeInternal::Expr(Box::new(
-                type_with(ctx, rc(ret))?.normalize(),
-            ))),
-        )),
-        OkNormalized(ret) => Ok(Typed(
-            e,
-            crate::expr::Type(TypeInternal::Expr(Box::new(ret))),
-        )),
-        OkType(ret) => Ok(Typed(e, ret)),
-        ErrRet(e) => Err(e),
+        RetExpr(ret) => Ok(Typed(e, mktype(ctx, rc(ret))?)),
+        RetType(typ) => Ok(Typed(e, typ)),
     }
 }
 
@@ -567,9 +548,9 @@ pub enum TypeMessage<S> {
     UnboundVariable,
     InvalidInputType(SubExpr<S, X>),
     InvalidOutputType(crate::expr::Type),
-    NotAFunction(SubExpr<S, X>, Normalized),
-    TypeMismatch(SubExpr<S, X>, SubExpr<S, X>, Typed),
-    AnnotMismatch(Typed, Normalized),
+    NotAFunction(SubExpr<S, X>, crate::expr::Type),
+    TypeMismatch(SubExpr<S, X>, crate::expr::Type, Typed),
+    AnnotMismatch(Typed, crate::expr::Type),
     Untyped,
     InvalidListElement(usize, SubExpr<S, X>, Typed),
     InvalidListType(SubExpr<S, X>),
@@ -645,8 +626,8 @@ impl<S> fmt::Display for TypeMessage<S> {
                 let template = include_str!("errors/TypeMismatch.txt");
                 let s = template
                     .replace("$txt0", &format!("{}", e0))
-                    .replace("$txt1", &format!("{}", e1))
-                    .replace("$txt2", &format!("{}", e2.0))
+                    .replace("$txt1", &format!("{}", e1.as_expr()))
+                    .replace("$txt2", &format!("{}", e2.as_expr()))
                     .replace("$txt3", &format!("{}", e2.get_type().as_expr()));
                 f.write_str(&s)
             }