Fix a bunch of bugs and more tck

4 files changed, 31 insertions, 13 deletions

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 {