Implement basic typecheck with new approach

3 files changed, 150 insertions, 3 deletions

diff --git a/dhall/src/semantics/core/context.rs b/dhall/src/semantics/core/context.rs
index 0e62fef..9749c50 100644
--- a/dhall/src/semantics/core/context.rs
+++ b/dhall/src/semantics/core/context.rs
@@ -2,8 +2,8 @@ use crate::error::TypeError;
 use crate::semantics::core::value::Value;
 use crate::semantics::core::value::ValueKind;
 use crate::semantics::core::var::{AlphaVar, Binder};
-use crate::semantics::nze::{NzVar, QuoteEnv};
-use crate::semantics::phase::normalize::{NzEnv, NzEnvItem};
+use crate::semantics::nze::NzVar;
+// use crate::semantics::phase::normalize::{NzEnv, NzEnvItem};
 use crate::syntax::{Label, V};
 
 #[derive(Debug, Clone)]
@@ -71,7 +71,6 @@ impl TyCtx {
                 t.clone(),
             ),
             CtxItem::Replaced(v) => v.clone()
-                // .to_tyexpr(QuoteEnv::construct(var_idx))
                 // .normalize_whnf(&NzEnv::construct(
                 //     self.ctx
                 //         .iter()
diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs
index 3ddfb84..e848601 100644
--- a/dhall/src/semantics/phase/normalize.rs
+++ b/dhall/src/semantics/phase/normalize.rs
@@ -1,3 +1,4 @@
+#![allow(dead_code)]
 use std::collections::HashMap;
 use std::convert::TryInto;
 
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
new file mode 100644
index 0000000..aab5f83
--- /dev/null
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -0,0 +1,147 @@
+#![allow(dead_code)]
+#![allow(unused_variables)]
+#![allow(unreachable_code)]
+#![allow(unused_imports)]
+use std::borrow::Cow;
+use std::cmp::max;
+use std::collections::HashMap;
+
+use crate::error::{TypeError, TypeMessage};
+use crate::semantics::core::context::TyCtx;
+use crate::semantics::nze::{NameEnv, QuoteEnv};
+use crate::semantics::phase::normalize::{merge_maps, NzEnv};
+use crate::semantics::phase::Normalized;
+use crate::semantics::{
+    AlphaVar, Binder, Closure, TyExpr, TyExprKind, Type, Value, ValueKind,
+};
+use crate::syntax;
+use crate::syntax::{
+    Builtin, Const, Expr, ExprKind, InterpolatedTextContents, Label, Span,
+    UnspannedExpr, V,
+};
+
+#[derive(Debug, Clone)]
+pub(crate) struct TyEnv {
+    names: NameEnv,
+    items: NzEnv,
+}
+
+impl TyEnv {
+    pub fn new() -> Self {
+        TyEnv {
+            names: NameEnv::new(),
+            items: NzEnv::new(),
+        }
+    }
+    pub fn as_quoteenv(&self) -> QuoteEnv {
+        self.names.as_quoteenv()
+    }
+    pub fn as_nzenv(&self) -> &NzEnv {
+        &self.items
+    }
+    pub fn as_nameenv(&self) -> &NameEnv {
+        &self.names
+    }
+
+    pub fn insert_type(&self, x: &Label, t: Value) -> Self {
+        TyEnv {
+            names: self.names.insert(x),
+            items: self.items.insert_type(t),
+        }
+    }
+    pub fn insert_value(&self, x: &Label, e: Value) -> Self {
+        TyEnv {
+            names: self.names.insert(x),
+            items: self.items.insert_value(e),
+        }
+    }
+    pub fn lookup_var(&self, var: &V<Label>) -> Option<(TyExprKind, Value)> {
+        let var = self.names.unlabel_var(var)?;
+        let ty = self.lookup_val(&var).get_type().unwrap();
+        Some((TyExprKind::Var(var), ty))
+    }
+    pub fn lookup_val(&self, var: &AlphaVar) -> Value {
+        self.items.lookup_val(var)
+    }
+    pub fn size(&self) -> usize {
+        self.names.size()
+    }
+}
+
+/// Type-check an expression and return the expression alongside its type if type-checking
+/// succeeded, or an error if type-checking failed.
+fn type_with(env: &TyEnv, expr: Expr<Normalized>) -> Result<TyExpr, TypeError> {
+    let mkerr = || TypeError::new(TypeMessage::Sort);
+
+    match expr.as_ref() {
+        ExprKind::Var(var) => match env.lookup_var(&var) {
+            Some((e, ty)) => Ok(TyExpr::new(e, Some(ty), expr.span())),
+            None => Err(mkerr()),
+        },
+        ExprKind::Lam(binder, annot, body) => {
+            let annot = type_with(env, annot.clone())?;
+            let annot_nf = annot.normalize_whnf(env.as_nzenv());
+            let body = type_with(
+                &env.insert_type(&binder, annot_nf.clone()),
+                body.clone(),
+            )?;
+            let ty = Value::from_kind_and_type(
+                ValueKind::PiClosure {
+                    binder: Binder::new(binder.clone()),
+                    annot: annot_nf,
+                    closure: Closure::new(
+                        env.as_nzenv(),
+                        body.get_type()?.to_tyexpr(env.as_quoteenv()),
+                    ),
+                },
+                Value::from_const(Const::Type), // TODO: function_check
+            );
+            Ok(TyExpr::new(
+                TyExprKind::Expr(ExprKind::Lam(binder.clone(), annot, body)),
+                Some(ty),
+                expr.span(),
+            ))
+        }
+        ExprKind::Pi(binder, annot, body) => {
+            let annot = type_with(env, annot.clone())?;
+            let annot_nf = annot.normalize_whnf(env.as_nzenv());
+            let body = type_with(
+                &env.insert_type(binder, annot_nf.clone()),
+                body.clone(),
+            )?;
+            Ok(TyExpr::new(
+                TyExprKind::Expr(ExprKind::Pi(binder.clone(), annot, body)),
+                None, // TODO: function_check
+                expr.span(),
+            ))
+        }
+        kind => {
+            let kind = kind.traverse_ref(|e| type_with(env, e.clone()))?;
+            let ty = match &kind {
+                ExprKind::App(f, arg) => {
+                    let tf = f.get_type()?;
+                    let tf_borrow = tf.as_whnf();
+                    let (_expected_arg_ty, ty_closure) = match &*tf_borrow {
+                        ValueKind::PiClosure { annot, closure, .. } => {
+                            (annot, closure)
+                        }
+                        _ => return Err(mkerr()),
+                    };
+                    // if arg.get_type()? != *expected_arg_ty {
+                    //     return Err(mkerr());
+                    // }
+
+                    let arg_nf = arg.normalize_whnf(env.as_nzenv());
+                    ty_closure.apply(arg_nf)
+                }
+                _ => Value::from_const(Const::Type), // TODO
+            };
+
+            Ok(TyExpr::new(TyExprKind::Expr(kind), Some(ty), expr.span()))
+        }
+    }
+}
+
+pub(crate) fn typecheck(e: Expr<Normalized>) -> Result<TyExpr, TypeError> {
+    type_with(&TyEnv::new(), e)
+}