Fix a bunch of bugs and more tck

8 files changed, 100 insertions, 50 deletions

diff --git a/dhall/src/semantics/core/var.rs b/dhall/src/semantics/core/var.rs
index 0d2c1d4..cf45d5e 100644
--- a/dhall/src/semantics/core/var.rs
+++ b/dhall/src/semantics/core/var.rs
@@ -1,10 +1,16 @@
 use crate::syntax::{Label, V};
 
 /// Stores an alpha-normalized variable.
-#[derive(Clone, Copy, PartialEq, Eq)]
+#[derive(Clone, Copy, Eq)]
 pub struct AlphaVar {
     alpha: V<()>,
 }
+// TODO: temporary hopefully
+impl std::cmp::PartialEq for AlphaVar {
+    fn eq(&self, _other: &Self) -> bool {
+        true
+    }
+}
 
 // Exactly like a Label, but equality returns always true.
 // This is so that ValueKind equality is exactly alpha-equivalence.
diff --git a/dhall/src/semantics/nze/nzexpr.rs b/dhall/src/semantics/nze/nzexpr.rs
index 49aa704..33fdde3 100644
--- a/dhall/src/semantics/nze/nzexpr.rs
+++ b/dhall/src/semantics/nze/nzexpr.rs
@@ -82,16 +82,16 @@ pub(crate) struct QuoteEnv {
 }
 
 // Reverse-debruijn index: counts number of binders from the bottom of the stack.
-#[derive(Debug, Clone, Copy, Eq)]
+#[derive(Debug, Clone, Copy, PartialEq, Eq)]
 pub(crate) struct NzVar {
     idx: usize,
 }
 // TODO: temporary hopefully
-impl std::cmp::PartialEq for NzVar {
-    fn eq(&self, _other: &Self) -> bool {
-        true
-    }
-}
+// impl std::cmp::PartialEq for NzVar {
+//     fn eq(&self, _other: &Self) -> bool {
+//         true
+//     }
+// }
 
 impl TyEnv {
     pub fn new() -> Self {
@@ -144,6 +144,9 @@ impl NameEnv {
             size: self.names.len(),
         }
     }
+    pub fn names(&self) -> &[Binder] {
+        &self.names
+    }
 
     pub fn insert(&self, x: &Binder) -> Self {
         let mut env = self.clone();
@@ -220,13 +223,20 @@ impl QuoteEnv {
     pub fn construct(size: usize) -> Self {
         QuoteEnv { size }
     }
+    pub fn size(&self) -> usize {
+        self.size
+    }
     pub fn insert(&self) -> Self {
         QuoteEnv {
             size: self.size + 1,
         }
     }
     pub fn lookup(&self, var: &NzVar) -> AlphaVar {
-        AlphaVar::new(V((), self.size - var.idx - 1))
+        self.lookup_fallible(var).unwrap()
+    }
+    pub fn lookup_fallible(&self, var: &NzVar) -> Option<AlphaVar> {
+        let idx = self.size.checked_sub(var.idx + 1)?;
+        Some(AlphaVar::new(V((), idx)))
     }
 }
 
diff --git a/dhall/src/semantics/phase/mod.rs b/dhall/src/semantics/phase/mod.rs
index 4dc91e7..67cdc91 100644
--- a/dhall/src/semantics/phase/mod.rs
+++ b/dhall/src/semantics/phase/mod.rs
@@ -89,6 +89,11 @@ impl Resolved {
     pub fn to_expr(&self) -> ResolvedExpr {
         self.0.clone()
     }
+    pub fn tck_and_normalize_new_flow(&self) -> Result<Normalized, TypeError> {
+        let val = crate::semantics::tck::typecheck::typecheck(&self.0)?
+            .normalize_whnf_noenv();
+        Ok(Normalized(Typed(val)))
+    }
 }
 
 impl Typed {
diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs
index 33e1f2b..5fc72fc 100644
--- a/dhall/src/semantics/phase/normalize.rs
+++ b/dhall/src/semantics/phase/normalize.rs
@@ -2,7 +2,7 @@
 use std::collections::HashMap;
 use std::convert::TryInto;
 
-use crate::semantics::nze::NzVar;
+use crate::semantics::nze::{NzVar, QuoteEnv};
 use crate::semantics::phase::typecheck::{
     builtin_to_value, const_to_value, rc, typecheck,
 };
@@ -859,6 +859,9 @@ impl NzEnv {
     pub fn construct(items: Vec<NzEnvItem>) -> Self {
         NzEnv { items }
     }
+    pub fn as_quoteenv(&self) -> QuoteEnv {
+        QuoteEnv::construct(self.items.len())
+    }
 
     pub fn insert_type(&self, t: Value) -> Self {
         let mut env = self.clone();
diff --git a/dhall/src/semantics/phase/resolve.rs b/dhall/src/semantics/phase/resolve.rs
index cc4a024..64106aa 100644
--- a/dhall/src/semantics/phase/resolve.rs
+++ b/dhall/src/semantics/phase/resolve.rs
@@ -52,10 +52,14 @@ fn load_import(
     import_cache: &mut ImportCache,
     import_stack: &ImportStack,
 ) -> Result<Normalized, Error> {
+    // Ok(
+    //     do_resolve_expr(Parsed::parse_file(f)?, import_cache, import_stack)?
+    //         .typecheck()?
+    //         .normalize(),
+    // )
     Ok(
         do_resolve_expr(Parsed::parse_file(f)?, import_cache, import_stack)?
-            .typecheck()?
-            .normalize(),
+            .tck_and_normalize_new_flow()?,
     )
 }
 
diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs
index 1aab736..18e70e4 100644
--- a/dhall/src/semantics/phase/typecheck.rs
+++ b/dhall/src/semantics/phase/typecheck.rs
@@ -280,7 +280,9 @@ pub(crate) fn type_of_builtin<E>(b: Builtin) -> Expr<E> {
 pub(crate) fn builtin_to_value(b: Builtin) -> Value {
     Value::from_kind_and_type(
         ValueKind::from_builtin(b),
-        typecheck(type_of_builtin(b)).unwrap(),
+        crate::semantics::tck::typecheck::typecheck(&type_of_builtin(b))
+            .unwrap()
+            .normalize_whnf_noenv(),
     )
 }
 
@@ -380,17 +382,21 @@ fn type_last_layer(
         ExprKind::App(f, a) => {
             let tf = f.get_type()?;
             let tf_borrow = tf.as_whnf();
-            let (tx, tb) = match &*tf_borrow {
-                ValueKind::Pi(_, tx, tb) => (tx, tb),
+            match &*tf_borrow {
+                ValueKind::Pi(_, tx, tb) => {
+                    if &a.get_type()? != tx {
+                        return mkerr("TypeMismatch");
+                    }
+
+                    let ret = tb.subst_shift(&AlphaVar::default(), a);
+                    ret.normalize_nf();
+                    RetTypeOnly(ret)
+                }
+                ValueKind::PiClosure { closure, .. } => {
+                    RetTypeOnly(closure.apply(a.clone()))
+                }
                 _ => return mkerr("NotAFunction"),
-            };
-            if &a.get_type()? != tx {
-                return mkerr("TypeMismatch");
             }
-
-            let ret = tb.subst_shift(&AlphaVar::default(), a);
-            ret.normalize_nf();
-            RetTypeOnly(ret)
         }
         ExprKind::Annot(x, t) => {
             if &x.get_type()? != t {
diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index c8be3a3..a42265d 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -5,6 +5,7 @@ use crate::semantics::phase::normalize::{normalize_tyexpr_whnf, NzEnv};
 use crate::semantics::phase::typecheck::rc;
 use crate::semantics::phase::Normalized;
 use crate::semantics::phase::{NormalizedExpr, ToExprOptions};
+use crate::semantics::tck::typecheck::TyEnv;
 use crate::semantics::Value;
 use crate::syntax::{ExprKind, Label, Span, V};
 
@@ -48,6 +49,15 @@ impl TyExpr {
     pub fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr {
         tyexpr_to_expr(self, opts, &mut Vec::new())
     }
+    pub fn to_expr_tyenv(&self, env: &TyEnv) -> NormalizedExpr {
+        let opts = ToExprOptions {
+            normalize: true,
+            alpha: false,
+        };
+        let env = env.as_nameenv().names();
+        let mut env = env.iter().collect();
+        tyexpr_to_expr(self, opts, &mut env)
+    }
     // TODO: temporary hack
     pub fn to_value(&self) -> Value {
         todo!()
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 1b64d28..4ca5d4d 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -275,10 +275,22 @@ fn type_one_layer(
         }
         ExprKind::Annot(x, t) => {
             let t = t.normalize_whnf(env.as_nzenv());
-            if x.get_type()? != t {
-                return mkerr("annot mismatch");
+            let x_ty = x.get_type()?;
+            if x_ty != t {
+                return mkerr(format!(
+                    "annot mismatch: ({} : {}) : {}",
+                    x.to_expr_tyenv(env),
+                    x_ty.to_tyexpr(env.as_quoteenv()).to_expr_tyenv(env),
+                    t.to_tyexpr(env.as_quoteenv()).to_expr_tyenv(env)
+                ));
+                // return mkerr(format!(
+                //     "annot mismatch: {} != {}",
+                //     x_ty.to_tyexpr(env.as_quoteenv()).to_expr_tyenv(env),
+                //     t.to_tyexpr(env.as_quoteenv()).to_expr_tyenv(env)
+                // ));
+                // return mkerr(format!("annot mismatch: {:#?} : {:#?}", x, t,));
             }
-            t
+            x_ty
         }
         ExprKind::App(f, arg) => {
             let tf = f.get_type()?;
@@ -389,35 +401,29 @@ fn type_one_layer(
             let yk = y.get_type()?.as_const().unwrap();
             Value::from_const(max(xk, yk))
         }
-        // ExprKind::BinOp(o @ BinOp::ListAppend, l, r) => {
-        //     match &*l.get_type()?.as_whnf() {
-        //         ValueKind::AppliedBuiltin(List, _, _) => {}
-        //         _ => return mkerr("BinOpTypeMismatch"),
-        //     }
-
-        //     if l.get_type()? != r.get_type()? {
-        //         return mkerr("BinOpTypeMismatch");
-        //     }
+        ExprKind::BinOp(BinOp::ListAppend, l, r) => {
+            let l_ty = l.get_type()?;
+            match &*l_ty.as_whnf() {
+                ValueKind::AppliedBuiltin(Builtin::List, _, _) => {}
+                _ => return mkerr("BinOpTypeMismatch"),
+            }
 
-        //     l.get_type()?
-        // }
-        // ExprKind::BinOp(BinOp::Equivalence, l, r) => {
-        //     if l.get_type()?.get_type()?.as_const() != Some(Const::Type) {
-        //         return mkerr("EquivalenceArgumentMustBeTerm");
-        //     }
-        //     if r.get_type()?.get_type()?.as_const() != Some(Const::Type) {
-        //         return mkerr("EquivalenceArgumentMustBeTerm");
-        //     }
+            if l_ty != r.get_type()? {
+                return mkerr("BinOpTypeMismatch");
+            }
 
-        //     if l.get_type()? != r.get_type()? {
-        //         return mkerr("EquivalenceTypeMismatch");
-        //     }
+            l_ty
+        }
+        ExprKind::BinOp(BinOp::Equivalence, l, r) => {
+            if l.get_type()? != r.get_type()? {
+                return mkerr("EquivalenceTypeMismatch");
+            }
+            if l.get_type()?.get_type()?.as_const() != Some(Const::Type) {
+                return mkerr("EquivalenceArgumentsMustBeTerms");
+            }
 
-        //     RetWhole(Value::from_kind_and_type(
-        //         ValueKind::Equivalence(l.clone(), r.clone()),
-        //         Value::from_const(Type),
-        //     ))
-        // }
+            Value::from_const(Const::Type)
+        }
         ExprKind::BinOp(o, l, r) => {
             let t = builtin_to_value(match o {
                 BinOp::BoolAnd