From 0ce048e4d95b08e50dec0f2e0f6736f3c5b646f2 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 7 Apr 2019 00:24:34 +0200
Subject: More typecheck

---
 dhall/src/typecheck.rs | 164 ++++++++++++++++++++++++++-----------------------
 1 file changed, 86 insertions(+), 78 deletions(-)

(limited to 'dhall/src')

diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 0ebc67e..29ad6d4 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -1,5 +1,4 @@
 #![allow(non_snake_case)]
-use std::collections::HashSet;
 use std::fmt;
 
 use crate::expr::*;
@@ -12,10 +11,6 @@ use self::TypeMessage::*;
 
 impl Resolved {
     pub fn typecheck(self) -> Result<Typed, TypeError<X>> {
-        // let typ = Type(Box::new(Normalized(crate::typecheck::type_of(
-        //     self.0.clone(),
-        // )?)));
-        // Ok(Typed(self.0, typ))
         let typ = crate::typecheck::type_of_(self.0.clone())?;
         Ok(typ)
     }
@@ -24,11 +19,23 @@ impl Typed {
     fn as_expr(&self) -> &SubExpr<X, X> {
         &self.0
     }
+    fn into_expr(self) -> SubExpr<X, X> {
+        self.0
+    }
+    pub fn into_type(self) -> Type {
+        self.1
+    }
     pub fn get_type(&self) -> &Type {
         &self.1
     }
 }
 impl Normalized {
+    fn as_expr(&self) -> &SubExpr<X, X> {
+        &self.0
+    }
+    fn into_expr(self) -> SubExpr<X, X> {
+        self.0
+    }
     pub fn get_type(&self) -> &Type {
         &self.1
     }
@@ -37,11 +44,8 @@ impl Normalized {
     }
 }
 impl Type {
-    // pub fn as_expr(&self) -> &Normalized {
-    //     &*self.0
-    // }
     fn as_expr(&self) -> &SubExpr<X, X> {
-        &self.as_normalized().0
+        &self.as_normalized().as_expr()
     }
     fn as_normalized(&self) -> &Normalized {
         use TypeInternal::*;
@@ -50,13 +54,24 @@ impl Type {
             Universe(_) => unimplemented!(),
         }
     }
+    fn into_expr(self) -> SubExpr<X, X> {
+        use TypeInternal::*;
+        match self.0 {
+            Expr(e) => e.into_expr(),
+            Universe(_) => unimplemented!(),
+        }
+    }
     pub fn get_type(&self) -> &Type {
-        self.as_normalized().get_type()
+        use TypeInternal::*;
+        match &self.0 {
+            Expr(e) => e.get_type(),
+            Universe(_) => unimplemented!(),
+            // Universe(n) => &Type(Universe(n+1)),
+        }
     }
 }
 
-const TYPE_OF_SORT: crate::expr::Type =
-    crate::expr::Type(TypeInternal::Universe(4));
+const TYPE_OF_SORT: Type = Type(TypeInternal::Universe(4));
 
 fn rule(a: Const, b: Const) -> Result<Const, ()> {
     use dhall_core::Const::*;
@@ -89,11 +104,7 @@ fn match_vars(vl: &V<Label>, vr: &V<Label>, ctx: &[(Label, Label)]) -> bool {
 }
 
 // Takes normalized expressions as input
-fn prop_equal<S, T>(eL0: &Expr<S, X>, eR0: &Expr<T, X>) -> bool
-where
-    S: ::std::fmt::Debug,
-    T: ::std::fmt::Debug,
-{
+fn prop_equal(eL0: &Type, eR0: &Type) -> bool {
     use dhall_core::ExprF::*;
     fn go<S, T>(
         ctx: &mut Vec<(Label, Label)>,
@@ -149,8 +160,16 @@ where
             (_, _) => false,
         }
     }
-    let mut ctx = vec![];
-    go::<S, T>(&mut ctx, eL0, eR0)
+    match (&eL0.0, &eR0.0) {
+        (TypeInternal::Universe(l), TypeInternal::Universe(r)) if r == l => {
+            true
+        }
+        (TypeInternal::Expr(l), TypeInternal::Expr(r)) => {
+            let mut ctx = vec![];
+            go(&mut ctx, l.as_expr().as_ref(), r.as_expr().as_ref())
+        }
+        _ => false,
+    }
 }
 
 fn type_of_builtin<S>(b: Builtin) -> Expr<S, X> {
@@ -228,18 +247,17 @@ where
     F1: FnOnce(TypeMessage<S>) -> TypeError<S>,
     F2: FnOnce() -> TypeMessage<S>,
 {
-    if prop_equal(x.as_expr().as_ref(), y.as_expr().as_ref()) {
+    if prop_equal(x, y) {
         Ok(())
     } else {
         Err(mkerr(mkmsg()))
     }
 }
 
-/// Type-check an expression and return the expression's type if type-checking
-/// succeeds or an error if type-checking fails
+/// Type-check an expression and return the expression alongside its type
+/// if type-checking succeeded, or an error if type-checking failed
 ///
-/// `type_with` normalizes the type since while type-checking. It expects the
-/// context to contain only normalized expressions.
+/// `type_with` expects the context to contain only normalized expressions.
 pub fn type_with(
     ctx: &Context<Label, SubExpr<X, X>>,
     e: SubExpr<X, X>,
@@ -284,15 +302,12 @@ pub fn type_with(
             Ok(RetExpr(Pi(
                 x.clone(),
                 t2.as_expr().clone(),
-                b.get_type().as_expr().clone(),
+                b.into_type().into_expr(),
             )))
         }
         Pi(x, tA, tB) => {
             let tA = mktype(ctx, tA.clone())?;
-            let kA = ensure_const(
-                tA.get_type(),
-                InvalidInputType(tA.as_expr().clone()),
-            )?;
+            let kA = ensure_const(tA.get_type(), InvalidInputType(tA.clone()))?;
 
             let ctx2 = ctx
                 .insert(x.clone(), tA.as_expr().clone())
@@ -311,7 +326,7 @@ pub fn type_with(
 
             match rule(kA, kB) {
                 Err(()) => Err(mkerr(NoDependentTypes(
-                    tA.as_expr().clone(),
+                    tA.clone(),
                     tB.get_type().clone(),
                 ))),
                 Ok(k) => Ok(RetExpr(Const(k))),
@@ -329,7 +344,7 @@ pub fn type_with(
             // message because this should never happen anyway
             let kR = ensure_const(
                 r.get_type().get_type(),
-                InvalidInputType(r.get_type().as_expr().clone()),
+                InvalidInputType(r.get_type().clone()),
             )?;
 
             let ctx2 = ctx.insert(f.clone(), r.get_type().as_expr().clone());
@@ -343,8 +358,8 @@ pub fn type_with(
 
             if let Err(()) = rule(kR, kB) {
                 return Err(mkerr(NoDependentLet(
-                    r.get_type().as_expr().clone(),
-                    b.get_type().as_expr().clone(),
+                    r.into_type(),
+                    b.into_type(),
                 )));
             }
 
@@ -369,25 +384,31 @@ pub fn type_with(
                 let mut seen_args: Vec<SubExpr<_, _>> = vec![];
                 let mut tf = f.get_type().clone();
                 while let Some(a) = iter.next() {
-                    seen_args.push(a.0.clone());
+                    seen_args.push(a.as_expr().clone());
                     let (x, tx, tb) = match tf.as_expr().as_ref() {
                         Pi(x, tx, tb) => (x, tx, tb),
                         _ => {
-                            return Err(mkerr(NotAFunction(
-                                rc(App(f.0.clone(), seen_args)),
+                            return Err(mkerr(NotAFunction(Typed(
+                                rc(App(f.into_expr(), seen_args)),
                                 tf,
-                            )));
+                            ))));
                         }
                     };
                     let tx = mktype(ctx, tx.clone())?;
                     ensure_equal(&tx, a.get_type(), mkerr, || {
                         TypeMismatch(
-                            rc(App(f.0.clone(), seen_args.clone())),
+                            Typed(
+                                rc(App(f.as_expr().clone(), seen_args.clone())),
+                                tf.clone(),
+                            ),
                             tx.clone(),
                             a.clone(),
                         )
                     })?;
-                    tf = mktype(ctx, subst_shift(&V(x.clone(), 0), &a.0, &tb))?;
+                    tf = mktype(
+                        ctx,
+                        subst_shift(&V(x.clone(), 0), &a.as_expr(), &tb),
+                    )?;
                 }
                 Ok(RetType(tf))
             }
@@ -422,8 +443,9 @@ pub fn type_with(
                 Ok(RetType(y.get_type().clone()))
             }
             EmptyListLit(t) => {
-                ensure_is_type(t.get_type(), InvalidListType(t.0.clone()))?;
-                let t = t.normalize().0;
+                let t = t.normalize().into_type();
+                ensure_is_type(t.get_type(), InvalidListType(t.clone()))?;
+                let t = t.into_expr();
                 Ok(RetExpr(dhall::expr!(List t)))
             }
             NEListLit(xs) => {
@@ -431,31 +453,28 @@ pub fn type_with(
                 let (_, x) = iter.next().unwrap();
                 ensure_is_type(
                     x.get_type().get_type(),
-                    InvalidListType(x.get_type().as_expr().clone()),
+                    InvalidListType(x.get_type().clone()),
                 )?;
                 for (i, y) in iter {
                     ensure_equal(x.get_type(), y.get_type(), mkerr, || {
-                        InvalidListElement(
-                            i,
-                            x.get_type().as_expr().clone(),
-                            y.clone(),
-                        )
+                        InvalidListElement(i, x.get_type().clone(), y.clone())
                     })?;
                 }
-                let t = x.get_type().as_expr().clone();
+                let t = x.into_type().into_expr();
                 Ok(RetExpr(dhall::expr!(List t)))
             }
             EmptyOptionalLit(t) => {
-                ensure_is_type(t.get_type(), InvalidOptionalType(t.0.clone()))?;
-                let t = t.normalize().0;
+                let t = t.normalize().into_type();
+                ensure_is_type(t.get_type(), InvalidOptionalType(t.clone()))?;
+                let t = t.into_expr();
                 Ok(RetExpr(dhall::expr!(Optional t)))
             }
             NEOptionalLit(x) => {
                 ensure_is_type(
                     x.get_type().get_type(),
-                    InvalidOptionalType(x.get_type().as_expr().clone()),
+                    InvalidOptionalType(x.get_type().clone()),
                 )?;
-                let t = x.get_type().as_expr().clone();
+                let t = x.into_type().into_expr();
                 Ok(RetExpr(dhall::expr!(Optional t)))
             }
             RecordType(kts) => {
@@ -475,7 +494,7 @@ pub fn type_with(
                             v.get_type().get_type(),
                             InvalidField(k.clone(), v.clone()),
                         )?;
-                        Ok((k.clone(), v.get_type().as_expr().clone()))
+                        Ok((k.clone(), v.into_type().into_expr()))
                     })
                     .collect::<Result<_, _>>()?;
                 Ok(RetExpr(RecordType(kts)))
@@ -534,7 +553,7 @@ pub fn type_with(
 /// will fail.
 pub fn type_of(e: SubExpr<X, X>) -> Result<SubExpr<X, X>, TypeError<X>> {
     let ctx = Context::new();
-    type_with(&ctx, e).map(|e| e.get_type().as_expr().clone())
+    type_with(&ctx, e).map(|e| e.into_type().into_expr())
 }
 
 pub fn type_of_(e: SubExpr<X, X>) -> Result<Typed, TypeError<X>> {
@@ -546,39 +565,28 @@ pub fn type_of_(e: SubExpr<X, X>) -> Result<Typed, TypeError<X>> {
 #[derive(Debug)]
 pub enum TypeMessage<S> {
     UnboundVariable,
-    InvalidInputType(SubExpr<S, X>),
-    InvalidOutputType(crate::expr::Type),
-    NotAFunction(SubExpr<S, X>, crate::expr::Type),
-    TypeMismatch(SubExpr<S, X>, crate::expr::Type, Typed),
-    AnnotMismatch(Typed, crate::expr::Type),
+    InvalidInputType(Type),
+    InvalidOutputType(Type),
+    NotAFunction(Typed),
+    TypeMismatch(Typed, Type, Typed),
+    AnnotMismatch(Typed, Type),
     Untyped,
-    InvalidListElement(usize, SubExpr<S, X>, Typed),
-    InvalidListType(SubExpr<S, X>),
-    InvalidOptionalElement(SubExpr<S, X>, SubExpr<S, X>, SubExpr<S, X>),
-    InvalidOptionalLiteral(usize),
-    InvalidOptionalType(SubExpr<S, X>),
+    InvalidListElement(usize, Type, Typed),
+    InvalidListType(Type),
+    InvalidOptionalType(Type),
     InvalidPredicate(Typed),
     IfBranchMismatch(Typed, Typed),
     IfBranchMustBeTerm(bool, Typed),
     InvalidField(Label, Typed),
     InvalidFieldType(Label, Typed),
-    InvalidAlternative(Label, SubExpr<S, X>),
-    InvalidAlternativeType(Label, SubExpr<S, X>),
     DuplicateAlternative(Label),
-    MustCombineARecord(SubExpr<S, X>, SubExpr<S, X>),
     FieldCollision(Label),
-    MustMergeARecord(SubExpr<S, X>, SubExpr<S, X>),
-    MustMergeUnion(SubExpr<S, X>, SubExpr<S, X>),
-    UnusedHandler(HashSet<Label>),
-    MissingHandler(HashSet<Label>),
-    HandlerInputTypeMismatch(Label, SubExpr<S, X>, SubExpr<S, X>),
-    HandlerOutputTypeMismatch(Label, SubExpr<S, X>, SubExpr<S, X>),
-    HandlerNotAFunction(Label, SubExpr<S, X>),
     NotARecord(Label, Typed),
     MissingField(Label, Typed),
     BinOpTypeMismatch(BinOp, Typed),
-    NoDependentLet(SubExpr<S, X>, SubExpr<S, X>),
-    NoDependentTypes(SubExpr<S, X>, crate::expr::Type),
+    NoDependentLet(Type, Type),
+    NoDependentTypes(Type, Type),
+    MustCombineARecord(SubExpr<S, X>, SubExpr<S, X>),
 }
 
 /// A structured type error that includes context
@@ -609,7 +617,7 @@ impl<S: fmt::Debug> ::std::error::Error for TypeMessage<S> {
             UnboundVariable => "Unbound variable",
             InvalidInputType(_) => "Invalid function input",
             InvalidOutputType(_) => "Invalid function output",
-            NotAFunction(_, _) => "Not a function",
+            NotAFunction(_) => "Not a function",
             TypeMismatch(_, _, _) => "Wrong type of function argument",
             _ => "Unhandled error",
         }
@@ -625,7 +633,7 @@ impl<S> fmt::Display for TypeMessage<S> {
             TypeMismatch(e0, e1, e2) => {
                 let template = include_str!("errors/TypeMismatch.txt");
                 let s = template
-                    .replace("$txt0", &format!("{}", e0))
+                    .replace("$txt0", &format!("{}", e0.as_expr()))
                     .replace("$txt1", &format!("{}", e1.as_expr()))
                     .replace("$txt2", &format!("{}", e2.as_expr()))
                     .replace("$txt3", &format!("{}", e2.get_type().as_expr()));
-- 
cgit v1.2.3