From ec28905d32c23109da17696faefab284fde3e103 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sat, 18 Jan 2020 18:46:09 +0000
Subject: Introduce intermediate representation that stores typed expr

---
 dhall/src/semantics/tck/mod.rs    |  2 +
 dhall/src/semantics/tck/tyexpr.rs | 83 +++++++++++++++++++++++++++++++++++++++
 2 files changed, 85 insertions(+)
 create mode 100644 dhall/src/semantics/tck/mod.rs
 create mode 100644 dhall/src/semantics/tck/tyexpr.rs

(limited to 'dhall/src/semantics/tck')

diff --git a/dhall/src/semantics/tck/mod.rs b/dhall/src/semantics/tck/mod.rs
new file mode 100644
index 0000000..407605d
--- /dev/null
+++ b/dhall/src/semantics/tck/mod.rs
@@ -0,0 +1,2 @@
+pub mod tyexpr;
+pub(crate) use tyexpr::*;
diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
new file mode 100644
index 0000000..a8b8e58
--- /dev/null
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -0,0 +1,83 @@
+#![allow(dead_code)]
+use crate::semantics::core::var::AlphaVar;
+use crate::semantics::phase::typecheck::rc;
+use crate::semantics::phase::Normalized;
+use crate::semantics::phase::{NormalizedExpr, ToExprOptions};
+use crate::semantics::Value;
+use crate::syntax::{ExprKind, Label, Span, V};
+
+pub(crate) type Type = Value;
+
+// An expression with inferred types at every node and resolved variables.
+pub(crate) struct TyExpr {
+    kind: Box<TyExprKind>,
+    ty: Option<Type>,
+    span: Span,
+}
+
+pub(crate) enum TyExprKind {
+    Var(AlphaVar),
+    // Forbidden ExprKind variants: Var
+    Expr(ExprKind<TyExpr, Normalized>),
+}
+
+impl TyExpr {
+    pub fn new(kind: TyExprKind, ty: Option<Type>, span: Span) -> Self {
+        TyExpr {
+            kind: Box::new(kind),
+            ty,
+            span,
+        }
+    }
+
+    pub fn kind(&self) -> &TyExprKind {
+        &*self.kind
+    }
+
+    /// Converts a value back to the corresponding AST expression.
+    pub fn to_expr<'a>(&'a self, opts: ToExprOptions) -> NormalizedExpr {
+        tyexpr_to_expr(self, opts, &Vec::new())
+    }
+}
+
+// TODO: mutate context once map_ref gets simplified
+fn tyexpr_to_expr<'a>(
+    tyexpr: &'a TyExpr,
+    opts: ToExprOptions,
+    ctx: &Vec<&'a Label>,
+) -> NormalizedExpr {
+    rc(match tyexpr.kind() {
+        TyExprKind::Var(v) if opts.alpha => {
+            ExprKind::Var(V("_".into(), v.idx()))
+        }
+        TyExprKind::Var(v) => {
+            let name = ctx[ctx.len() - 1 - v.idx()];
+            let mut idx = 0;
+            for l in ctx.iter().rev().take(v.idx()) {
+                if *l == name {
+                    idx += 1;
+                }
+            }
+            ExprKind::Var(V(name.clone(), idx))
+        }
+        TyExprKind::Expr(e) => {
+            let e = e.map_ref_with_special_handling_of_binders(
+                |tye| tyexpr_to_expr(tye, opts, ctx),
+                |l, tye| {
+                    let ctx = ctx.iter().copied().chain(Some(l)).collect();
+                    tyexpr_to_expr(tye, opts, &ctx)
+                },
+            );
+
+            match e {
+                ExprKind::Lam(_, t, e) if opts.alpha => {
+                    ExprKind::Lam("_".into(), t, e)
+                }
+                ExprKind::Pi(_, t, e) if opts.alpha => {
+                    ExprKind::Pi("_".into(), t, e)
+                }
+                e => e,
+            }
+        }
+    })
+}
-- 
cgit v1.2.3


From d6e5c56a5ef1d5f2b7cafd4a8fb44ce038932547 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sat, 18 Jan 2020 19:08:34 +0000
Subject: Add Expr visitor and improve tyexpr_to_expr

---
 dhall/src/semantics/tck/tyexpr.rs | 22 ++++++++++++----------
 1 file changed, 12 insertions(+), 10 deletions(-)

(limited to 'dhall/src/semantics/tck')

diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index a8b8e58..f0fcdd1 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -36,15 +36,14 @@ impl TyExpr {
 
     /// Converts a value back to the corresponding AST expression.
     pub fn to_expr<'a>(&'a self, opts: ToExprOptions) -> NormalizedExpr {
-        tyexpr_to_expr(self, opts, &Vec::new())
+        tyexpr_to_expr(self, opts, &mut Vec::new())
     }
 }
 
-// TODO: mutate context once map_ref gets simplified
 fn tyexpr_to_expr<'a>(
     tyexpr: &'a TyExpr,
     opts: ToExprOptions,
-    ctx: &Vec<&'a Label>,
+    ctx: &mut Vec<&'a Label>,
 ) -> NormalizedExpr {
     rc(match tyexpr.kind() {
         TyExprKind::Var(v) if opts.alpha => {
@@ -61,13 +60,16 @@ fn tyexpr_to_expr<'a>(
             ExprKind::Var(V(name.clone(), idx))
         }
         TyExprKind::Expr(e) => {
-            let e = e.map_ref_with_special_handling_of_binders(
-                |tye| tyexpr_to_expr(tye, opts, ctx),
-                |l, tye| {
-                    let ctx = ctx.iter().copied().chain(Some(l)).collect();
-                    tyexpr_to_expr(tye, opts, &ctx)
-                },
-            );
+            let e = e.map_ref_maybe_binder(|l, tye| {
+                if let Some(l) = l {
+                    ctx.push(l);
+                }
+                let e = tyexpr_to_expr(tye, opts, ctx);
+                if let Some(_) = l {
+                    ctx.pop();
+                }
+                e
+            });
 
             match e {
                 ExprKind::Lam(_, t, e) if opts.alpha => {
-- 
cgit v1.2.3


From aec80599f161096b68cac88ffb8852a61b62fcfa Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 19 Jan 2020 18:30:13 +0000
Subject: Restore more types in value_to_tyexpr

---
 dhall/src/semantics/tck/mod.rs    |  2 ++
 dhall/src/semantics/tck/tyexpr.rs | 14 +++++++++++++-
 2 files changed, 15 insertions(+), 1 deletion(-)

(limited to 'dhall/src/semantics/tck')

diff --git a/dhall/src/semantics/tck/mod.rs b/dhall/src/semantics/tck/mod.rs
index 407605d..ba95847 100644
--- a/dhall/src/semantics/tck/mod.rs
+++ b/dhall/src/semantics/tck/mod.rs
@@ -1,2 +1,4 @@
+pub mod context;
 pub mod tyexpr;
+pub mod typecheck;
 pub(crate) use tyexpr::*;
diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index f0fcdd1..36cae04 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -1,4 +1,6 @@
 #![allow(dead_code)]
+use crate::error::{TypeError, TypeMessage};
+use crate::semantics::core::context::TyCtx;
 use crate::semantics::core::var::AlphaVar;
 use crate::semantics::phase::typecheck::rc;
 use crate::semantics::phase::Normalized;
@@ -33,11 +35,21 @@ impl TyExpr {
     pub fn kind(&self) -> &TyExprKind {
         &*self.kind
     }
+    pub fn get_type(&self) -> Result<Type, TypeError> {
+        match &self.ty {
+            Some(t) => Ok(t.clone()),
+            None => Err(TypeError::new(&TyCtx::new(), TypeMessage::Sort)),
+        }
+    }
 
     /// Converts a value back to the corresponding AST expression.
-    pub fn to_expr<'a>(&'a self, opts: ToExprOptions) -> NormalizedExpr {
+    pub fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr {
         tyexpr_to_expr(self, opts, &mut Vec::new())
     }
+    // TODO: temporary hack
+    pub fn to_value(&self) -> Value {
+        todo!()
+    }
 }
 
 fn tyexpr_to_expr<'a>(
-- 
cgit v1.2.3


From c448698f797f2304dca0e0b8b833959de00ca079 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Mon, 20 Jan 2020 15:27:19 +0000
Subject: Reimplement basic tck/nze with proper environments

Inspired from dhall_haskell
---
 dhall/src/semantics/tck/tyexpr.rs | 16 +++++++++-------
 1 file changed, 9 insertions(+), 7 deletions(-)

(limited to 'dhall/src/semantics/tck')

diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index 36cae04..72f5b1d 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -11,15 +11,17 @@ use crate::syntax::{ExprKind, Label, Span, V};
 pub(crate) type Type = Value;
 
 // An expression with inferred types at every node and resolved variables.
+#[derive(Debug, Clone)]
 pub(crate) struct TyExpr {
     kind: Box<TyExprKind>,
     ty: Option<Type>,
     span: Span,
 }
 
+#[derive(Debug, Clone)]
 pub(crate) enum TyExprKind {
     Var(AlphaVar),
-    // Forbidden ExprKind variants: Var
+    // Forbidden ExprKind variants: Var, Import, Embed
     Expr(ExprKind<TyExpr, Normalized>),
 }
 
@@ -63,12 +65,12 @@ fn tyexpr_to_expr<'a>(
         }
         TyExprKind::Var(v) => {
             let name = ctx[ctx.len() - 1 - v.idx()];
-            let mut idx = 0;
-            for l in ctx.iter().rev().take(v.idx()) {
-                if *l == name {
-                    idx += 1;
-                }
-            }
+            let idx = ctx
+                .iter()
+                .rev()
+                .take(v.idx())
+                .filter(|l| **l == name)
+                .count();
             ExprKind::Var(V(name.clone(), idx))
         }
         TyExprKind::Expr(e) => {
-- 
cgit v1.2.3


From 015b24b04128cbf5a60fbc8ac3f526306ca27378 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 21 Jan 2020 17:43:44 +0000
Subject: Simplify type error type

---
 dhall/src/semantics/tck/tyexpr.rs | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'dhall/src/semantics/tck')

diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index 72f5b1d..983f3f8 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -1,6 +1,5 @@
 #![allow(dead_code)]
 use crate::error::{TypeError, TypeMessage};
-use crate::semantics::core::context::TyCtx;
 use crate::semantics::core::var::AlphaVar;
 use crate::semantics::phase::typecheck::rc;
 use crate::semantics::phase::Normalized;
@@ -40,7 +39,7 @@ impl TyExpr {
     pub fn get_type(&self) -> Result<Type, TypeError> {
         match &self.ty {
             Some(t) => Ok(t.clone()),
-            None => Err(TypeError::new(&TyCtx::new(), TypeMessage::Sort)),
+            None => Err(TypeError::new(TypeMessage::Sort)),
         }
     }
 
-- 
cgit v1.2.3


From 9e7cc77b6a25569b61340f39a2058e23cdc4a437 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Thu, 23 Jan 2020 22:22:01 +0000
Subject: Implement basic env-based normalization for Value-based TyExpr

---
 dhall/src/semantics/tck/tyexpr.rs | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'dhall/src/semantics/tck')

diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index 983f3f8..c8be3a3 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -1,6 +1,7 @@
 #![allow(dead_code)]
 use crate::error::{TypeError, TypeMessage};
 use crate::semantics::core::var::AlphaVar;
+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};
@@ -51,6 +52,13 @@ impl TyExpr {
     pub fn to_value(&self) -> Value {
         todo!()
     }
+
+    pub fn normalize_whnf(&self, env: &NzEnv) -> Value {
+        normalize_tyexpr_whnf(self, env)
+    }
+    pub fn normalize_whnf_noenv(&self) -> Value {
+        normalize_tyexpr_whnf(self, &NzEnv::new())
+    }
 }
 
 fn tyexpr_to_expr<'a>(
-- 
cgit v1.2.3


From b72f0968ac19058b9cc513ab0ed1785133232a3d Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Fri, 24 Jan 2020 21:33:21 +0000
Subject: Implement basic typecheck with new approach

---
 dhall/src/semantics/tck/typecheck.rs | 147 +++++++++++++++++++++++++++++++++++
 1 file changed, 147 insertions(+)
 create mode 100644 dhall/src/semantics/tck/typecheck.rs

(limited to 'dhall/src/semantics/tck')

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)
+}
-- 
cgit v1.2.3


From 70e6e3a06c05cfe7d8ca3d6f072e7182639c147f Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sat, 25 Jan 2020 10:15:17 +0000
Subject: Typecheck more cases

---
 dhall/src/semantics/tck/typecheck.rs | 187 +++++++++++++++++++++++++----------
 1 file changed, 134 insertions(+), 53 deletions(-)

(limited to 'dhall/src/semantics/tck')

diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index aab5f83..046c999 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -10,6 +10,9 @@ 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::typecheck::{
+    builtin_to_value, const_to_value, type_of_builtin,
+};
 use crate::semantics::phase::Normalized;
 use crate::semantics::{
     AlphaVar, Binder, Closure, TyExpr, TyExprKind, Type, Value, ValueKind,
@@ -55,93 +58,171 @@ impl TyEnv {
             items: self.items.insert_value(e),
         }
     }
-    pub fn lookup_var(&self, var: &V<Label>) -> Option<(TyExprKind, Value)> {
+    pub fn lookup(&self, var: &V<Label>) -> Option<(TyExprKind, Value)> {
         let var = self.names.unlabel_var(var)?;
-        let ty = self.lookup_val(&var).get_type().unwrap();
+        let ty = self.items.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()
     }
 }
 
+fn mkerr<T>(x: impl ToString) -> Result<T, TypeError> {
+    Err(TypeError::new(TypeMessage::Custom(x.to_string())))
+}
+
+fn type_last_layer(
+    env: &TyEnv,
+    kind: &ExprKind<TyExpr, Normalized>,
+) -> Result<Value, TypeError> {
+    Ok(match &kind {
+        ExprKind::Import(..) => unreachable!(
+            "There should remain no imports in a resolved expression"
+        ),
+        ExprKind::Var(..)
+        | ExprKind::Lam(..)
+        | ExprKind::Pi(..)
+        | ExprKind::Let(..)
+        | ExprKind::Const(Const::Sort)
+        | ExprKind::Embed(..) => unreachable!(),
+
+        ExprKind::Const(Const::Type) => const_to_value(Const::Kind),
+        ExprKind::Const(Const::Kind) => const_to_value(Const::Sort),
+        ExprKind::Builtin(b) => {
+            type_with(env, &type_of_builtin(*b))?.normalize_whnf(env.as_nzenv())
+        }
+        ExprKind::BoolLit(_) => builtin_to_value(Builtin::Bool),
+        ExprKind::NaturalLit(_) => builtin_to_value(Builtin::Natural),
+        ExprKind::IntegerLit(_) => builtin_to_value(Builtin::Integer),
+        ExprKind::DoubleLit(_) => builtin_to_value(Builtin::Double),
+
+        ExprKind::Annot(x, t) => {
+            if x.get_type()? != t.normalize_whnf(env.as_nzenv()) {
+                return mkerr("annot mismatch");
+            }
+            x.normalize_whnf(env.as_nzenv())
+        }
+        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 mkerr(format!("apply to not Pi: {:?}", tf_borrow)),
+            };
+            // if arg.get_type()? != *expected_arg_ty {
+            //     return mkerr(format!(
+            //         "function annot mismatch: {:?}, {:?}",
+            //         arg.get_type()?,
+            //         expected_arg_ty
+            //     ));
+            // }
+
+            let arg_nf = arg.normalize_whnf(env.as_nzenv());
+            ty_closure.apply(arg_nf)
+        }
+        ExprKind::BoolIf(x, y, z) => {
+            if *x.get_type()?.as_whnf()
+                != ValueKind::from_builtin(Builtin::Bool)
+            {
+                return mkerr("InvalidPredicate");
+            }
+            if y.get_type()?.get_type()?.as_const() != Some(Const::Type) {
+                return mkerr("IfBranchMustBeTerm");
+            }
+            if z.get_type()?.get_type()?.as_const() != Some(Const::Type) {
+                return mkerr("IfBranchMustBeTerm");
+            }
+            if y.get_type()? != z.get_type()? {
+                return mkerr("IfBranchMismatch");
+            }
+
+            y.get_type()?
+        }
+
+        _ => Value::from_const(Const::Type), // TODO
+    })
+}
+
 /// 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()),
+fn type_with(
+    env: &TyEnv,
+    expr: &Expr<Normalized>,
+) -> Result<TyExpr, TypeError> {
+    let (tyekind, ty) = match expr.as_ref() {
+        ExprKind::Var(var) => match env.lookup(&var) {
+            Some((k, ty)) => (k, Some(ty)),
+            None => return mkerr("unbound variable"),
         },
         ExprKind::Lam(binder, annot, body) => {
-            let annot = type_with(env, annot.clone())?;
+            let annot = type_with(env, annot)?;
             let annot_nf = annot.normalize_whnf(env.as_nzenv());
-            let body = type_with(
-                &env.insert_type(&binder, annot_nf.clone()),
-                body.clone(),
-            )?;
+            let body =
+                type_with(&env.insert_type(&binder, annot_nf.clone()), body)?;
             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()),
+                        body.get_type()?.to_tyexpr(env.as_quoteenv().insert()),
                     ),
                 },
                 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 = type_with(env, annot)?;
             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(
+            let body =
+                type_with(&env.insert_type(binder, annot_nf.clone()), body)?;
+            (
                 TyExprKind::Expr(ExprKind::Pi(binder.clone(), annot, body)),
-                None, // TODO: function_check
-                expr.span(),
-            ))
+                Some(Value::from_const(Const::Type)), // TODO: function_check
+            )
         }
-        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
+        ExprKind::Let(binder, annot, val, body) => {
+            let v = if let Some(t) = annot {
+                t.rewrap(ExprKind::Annot(val.clone(), t.clone()))
+            } else {
+                val.clone()
             };
 
-            Ok(TyExpr::new(TyExprKind::Expr(kind), Some(ty), expr.span()))
+            let val = type_with(env, val)?;
+            let val_nf = val.normalize_whnf(&env.as_nzenv());
+            let body = type_with(&env.insert_value(&binder, val_nf), body)?;
+            let body_ty = body.get_type().ok();
+            (
+                TyExprKind::Expr(ExprKind::Let(
+                    binder.clone(),
+                    None,
+                    val,
+                    body,
+                )),
+                body_ty,
+            )
         }
-    }
+        ExprKind::Const(Const::Sort) => {
+            (TyExprKind::Expr(ExprKind::Const(Const::Sort)), None)
+        }
+        ExprKind::Embed(p) => {
+            return Ok(p.clone().into_typed().into_value().to_tyexpr_noenv())
+        }
+        ekind => {
+            let ekind = ekind.traverse_ref(|e| type_with(env, e))?;
+            let ty = type_last_layer(env, &ekind)?;
+            (TyExprKind::Expr(ekind), Some(ty))
+        }
+    };
+
+    Ok(TyExpr::new(tyekind, ty, expr.span()))
 }
 
-pub(crate) fn typecheck(e: Expr<Normalized>) -> Result<TyExpr, TypeError> {
+pub(crate) fn typecheck(e: &Expr<Normalized>) -> Result<TyExpr, TypeError> {
     type_with(&TyEnv::new(), e)
 }
-- 
cgit v1.2.3


From f2e8c414993d5c9fcc63f5c035f755712c01dad0 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sat, 25 Jan 2020 10:20:53 +0000
Subject: Enable comparing Closures for equality

---
 dhall/src/semantics/tck/typecheck.rs | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'dhall/src/semantics/tck')

diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 046c999..52c7ac7 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -163,8 +163,9 @@ fn type_with(
             let ty = Value::from_kind_and_type(
                 ValueKind::PiClosure {
                     binder: Binder::new(binder.clone()),
-                    annot: annot_nf,
+                    annot: annot_nf.clone(),
                     closure: Closure::new(
+                        annot_nf,
                         env.as_nzenv(),
                         body.get_type()?.to_tyexpr(env.as_quoteenv().insert()),
                     ),
-- 
cgit v1.2.3


From 574fb56e87c1a71dc8d7efbff2789d3cfabdc529 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sat, 25 Jan 2020 13:51:24 +0000
Subject: More typecheck

---
 dhall/src/semantics/tck/typecheck.rs | 239 +++++++++++++++++++++++++++++++++--
 1 file changed, 231 insertions(+), 8 deletions(-)

(limited to 'dhall/src/semantics/tck')

diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 52c7ac7..1687185 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -19,8 +19,8 @@ use crate::semantics::{
 };
 use crate::syntax;
 use crate::syntax::{
-    Builtin, Const, Expr, ExprKind, InterpolatedTextContents, Label, Span,
-    UnspannedExpr, V,
+    BinOp, Builtin, Const, Expr, ExprKind, InterpolatedTextContents, Label,
+    Span, UnspannedExpr, V,
 };
 
 #[derive(Debug, Clone)]
@@ -46,7 +46,7 @@ impl TyEnv {
         &self.names
     }
 
-    pub fn insert_type(&self, x: &Label, t: Value) -> Self {
+    pub fn insert_type(&self, x: &Label, t: Type) -> Self {
         TyEnv {
             names: self.names.insert(x),
             items: self.items.insert_type(t),
@@ -58,7 +58,7 @@ impl TyEnv {
             items: self.items.insert_value(e),
         }
     }
-    pub fn lookup(&self, var: &V<Label>) -> Option<(TyExprKind, Value)> {
+    pub fn lookup(&self, var: &V<Label>) -> Option<(TyExprKind, Type)> {
         let var = self.names.unlabel_var(var)?;
         let ty = self.items.lookup_val(&var).get_type().unwrap();
         Some((TyExprKind::Var(var), ty))
@@ -72,10 +72,10 @@ fn mkerr<T>(x: impl ToString) -> Result<T, TypeError> {
     Err(TypeError::new(TypeMessage::Custom(x.to_string())))
 }
 
-fn type_last_layer(
+fn type_one_layer(
     env: &TyEnv,
     kind: &ExprKind<TyExpr, Normalized>,
-) -> Result<Value, TypeError> {
+) -> Result<Type, TypeError> {
     Ok(match &kind {
         ExprKind::Import(..) => unreachable!(
             "There should remain no imports in a resolved expression"
@@ -85,7 +85,7 @@ fn type_last_layer(
         | ExprKind::Pi(..)
         | ExprKind::Let(..)
         | ExprKind::Const(Const::Sort)
-        | ExprKind::Embed(..) => unreachable!(),
+        | ExprKind::Embed(..) => unreachable!(), // Handled in type_with
 
         ExprKind::Const(Const::Type) => const_to_value(Const::Kind),
         ExprKind::Const(Const::Kind) => const_to_value(Const::Sort),
@@ -96,7 +96,99 @@ fn type_last_layer(
         ExprKind::NaturalLit(_) => builtin_to_value(Builtin::Natural),
         ExprKind::IntegerLit(_) => builtin_to_value(Builtin::Integer),
         ExprKind::DoubleLit(_) => builtin_to_value(Builtin::Double),
+        ExprKind::TextLit(interpolated) => {
+            let text_type = builtin_to_value(Builtin::Text);
+            for contents in interpolated.iter() {
+                use InterpolatedTextContents::Expr;
+                if let Expr(x) = contents {
+                    if x.get_type()? != text_type {
+                        return mkerr("InvalidTextInterpolation");
+                    }
+                }
+            }
+            text_type
+        }
+
+        // ExprKind::EmptyListLit(t) => {
+        //     let arg = match &*t.as_whnf() {
+        //         ValueKind::AppliedBuiltin(Builtin::List, args, _)
+        //             if args.len() == 1 =>
+        //         {
+        //             args[0].clone()
+        //         }
+        //         _ => return mkerr("InvalidListType"),
+        //     };
+        //     RetWhole(Value::from_kind_and_type(
+        //         ValueKind::EmptyListLit(arg),
+        //         t.clone(),
+        //     ))
+        // }
+        ExprKind::NEListLit(xs) => {
+            let mut iter = xs.iter().enumerate();
+            let (_, x) = iter.next().unwrap();
+            for (i, y) in iter {
+                if x.get_type()? != y.get_type()? {
+                    return mkerr("InvalidListElement");
+                }
+            }
+            let t = x.get_type()?;
+            if t.get_type()?.as_const() != Some(Const::Type) {
+                return mkerr("InvalidListType");
+            }
+
+            Value::from_builtin(Builtin::List).app(t)
+        }
+        ExprKind::SomeLit(x) => {
+            let t = x.get_type()?;
+            if t.get_type()?.as_const() != Some(Const::Type) {
+                return mkerr("InvalidOptionalType");
+            }
 
+            Value::from_builtin(Builtin::Optional).app(t)
+        }
+        // ExprKind::RecordType(kts) => RetWhole(tck_record_type(
+        //     kts.iter().map(|(x, t)| Ok((x.clone(), t.clone()))),
+        // )?),
+        // ExprKind::UnionType(kts) => RetWhole(tck_union_type(
+        //     kts.iter().map(|(x, t)| Ok((x.clone(), t.clone()))),
+        // )?),
+        // ExprKind::RecordLit(kvs) => RetTypeOnly(tck_record_type(
+        //     kvs.iter().map(|(x, v)| Ok((x.clone(), v.get_type()?))),
+        // )?),
+        ExprKind::Field(r, x) => {
+            match &*r.get_type()?.as_whnf() {
+                ValueKind::RecordType(kts) => match kts.get(&x) {
+                    Some(tth) => tth.clone(),
+                    None => return mkerr("MissingRecordField"),
+                },
+                // TODO: branch here only when r.get_type() is a Const
+                _ => {
+                    let r_nf = r.normalize_whnf(env.as_nzenv());
+                    let r_nf_borrow = r_nf.as_whnf();
+                    match &*r_nf_borrow {
+                        ValueKind::UnionType(kts) => match kts.get(x) {
+                            // Constructor has type T -> < x: T, ... >
+                            // TODO: check pi type properly
+                            Some(Some(t)) => Value::from_kind_and_type(
+                                ValueKind::PiClosure {
+                                    binder: Binder::new(x.clone()),
+                                    annot: t.clone(),
+                                    closure: Closure::new(
+                                        t.clone(),
+                                        env.as_nzenv(),
+                                        r.clone(),
+                                    ),
+                                },
+                                Value::from_const(Const::Type),
+                            ),
+                            Some(None) => r_nf.clone(),
+                            None => return mkerr("MissingUnionField"),
+                        },
+                        _ => return mkerr("NotARecord"),
+                    }
+                } // _ => mkerr("NotARecord"),
+            }
+        }
         ExprKind::Annot(x, t) => {
             if x.get_type()? != t.normalize_whnf(env.as_nzenv()) {
                 return mkerr("annot mismatch");
@@ -139,7 +231,138 @@ fn type_last_layer(
 
             y.get_type()?
         }
+        // ExprKind::BinOp(BinOp::RightBiasedRecordMerge, l, r) => {
+        //     let l_type = l.get_type()?;
+        //     let r_type = r.get_type()?;
+
+        //     // Extract the LHS record type
+        //     let l_type_borrow = l_type.as_whnf();
+        //     let kts_x = match &*l_type_borrow {
+        //         ValueKind::RecordType(kts) => kts,
+        //         _ => return mkerr("MustCombineRecord"),
+        //     };
+
+        //     // Extract the RHS record type
+        //     let r_type_borrow = r_type.as_whnf();
+        //     let kts_y = match &*r_type_borrow {
+        //         ValueKind::RecordType(kts) => kts,
+        //         _ => return mkerr("MustCombineRecord"),
+        //     };
 
+        //     // Union the two records, prefering
+        //     // the values found in the RHS.
+        //     let kts = merge_maps::<_, _, _, !>(kts_x, kts_y, |_, _, r_t| {
+        //         Ok(r_t.clone())
+        //     })?;
+
+        //     // Construct the final record type from the union
+        //     RetTypeOnly(tck_record_type(
+        //         kts.into_iter().map(|(x, v)| Ok((x.clone(), v))),
+        //     )?)
+        // }
+        // ExprKind::BinOp(BinOp::RecursiveRecordMerge, l, r) => RetTypeOnly(type_last_layer(
+        //     ctx,
+        //     ExprKind::BinOp(
+        //         RecursiveRecordTypeMerge,
+        //         l.get_type()?,
+        //         r.get_type()?,
+        //     ),
+        //     Span::Artificial,
+        // )?),
+        // ExprKind::BinOp(BinOp::RecursiveRecordTypeMerge, l, r) => {
+        //     // Extract the LHS record type
+        //     let borrow_l = l.as_whnf();
+        //     let kts_x = match &*borrow_l {
+        //         ValueKind::RecordType(kts) => kts,
+        //         _ => {
+        //             return mkerr("RecordTypeMergeRequiresRecordType")
+        //         }
+        //     };
+
+        //     // Extract the RHS record type
+        //     let borrow_r = r.as_whnf();
+        //     let kts_y = match &*borrow_r {
+        //         ValueKind::RecordType(kts) => kts,
+        //         _ => {
+        //             return mkerr("RecordTypeMergeRequiresRecordType")
+        //         }
+        //     };
+
+        //     // Ensure that the records combine without a type error
+        //     let kts = merge_maps(
+        //         kts_x,
+        //         kts_y,
+        //         // If the Label exists for both records, then we hit the recursive case.
+        //         |_, l: &Value, r: &Value| {
+        //             type_last_layer(
+        //                 ctx,
+        //                 ExprKind::BinOp(
+        //                     RecursiveRecordTypeMerge,
+        //                     l.clone(),
+        //                     r.clone(),
+        //                 ),
+        //                 Span::Artificial,
+        //             )
+        //         },
+        //     )?;
+
+        //     RetWhole(tck_record_type(kts.into_iter().map(Ok))?)
+        // }
+        // 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");
+        //     }
+
+        //     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.get_type()? != r.get_type()? {
+        //         return mkerr("EquivalenceTypeMismatch");
+        //     }
+
+        //     RetWhole(Value::from_kind_and_type(
+        //         ValueKind::Equivalence(l.clone(), r.clone()),
+        //         Value::from_const(Type),
+        //     ))
+        // }
+        ExprKind::BinOp(o, l, r) => {
+            let t = builtin_to_value(match o {
+                BinOp::BoolAnd
+                | BinOp::BoolOr
+                | BinOp::BoolEQ
+                | BinOp::BoolNE => Builtin::Bool,
+                BinOp::NaturalPlus | BinOp::NaturalTimes => Builtin::Natural,
+                BinOp::TextAppend => Builtin::Text,
+                BinOp::ListAppend
+                | BinOp::RightBiasedRecordMerge
+                | BinOp::RecursiveRecordMerge
+                | BinOp::RecursiveRecordTypeMerge
+                | BinOp::Equivalence => unreachable!(),
+                BinOp::ImportAlt => unreachable!("ImportAlt leftover in tck"),
+            });
+
+            if l.get_type()? != t {
+                return mkerr("BinOpTypeMismatch");
+            }
+
+            if r.get_type()? != t {
+                return mkerr("BinOpTypeMismatch");
+            }
+
+            t
+        }
         _ => Value::from_const(Const::Type), // TODO
     })
 }
@@ -216,7 +439,7 @@ fn type_with(
         }
         ekind => {
             let ekind = ekind.traverse_ref(|e| type_with(env, e))?;
-            let ty = type_last_layer(env, &ekind)?;
+            let ty = type_one_layer(env, &ekind)?;
             (TyExprKind::Expr(ekind), Some(ty))
         }
     };
-- 
cgit v1.2.3


From 6c51ad1da8dc4df54618af80b445bf49f771ec43 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sat, 25 Jan 2020 15:49:16 +0000
Subject: Moar typecheck

---
 dhall/src/semantics/tck/typecheck.rs | 487 ++++++++++++++++++++++++-----------
 1 file changed, 342 insertions(+), 145 deletions(-)

(limited to 'dhall/src/semantics/tck')

diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 1687185..1b64d28 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -1,5 +1,4 @@
 #![allow(dead_code)]
-#![allow(unused_variables)]
 #![allow(unreachable_code)]
 #![allow(unused_imports)]
 use std::borrow::Cow;
@@ -68,6 +67,41 @@ impl TyEnv {
     }
 }
 
+fn type_of_recordtype<'a>(
+    tys: impl Iterator<Item = Cow<'a, TyExpr>>,
+) -> Result<Type, TypeError> {
+    // An empty record type has type Type
+    let mut k = Const::Type;
+    for t in tys {
+        match t.get_type()?.as_const() {
+            Some(c) => k = max(k, c),
+            None => return mkerr("InvalidFieldType"),
+        }
+    }
+    Ok(Value::from_const(k))
+}
+
+fn function_check(a: Const, b: Const) -> Const {
+    if b == Const::Type {
+        Const::Type
+    } else {
+        max(a, b)
+    }
+}
+
+fn type_of_function(src: Type, tgt: Type) -> Result<Type, TypeError> {
+    let ks = match src.as_const() {
+        Some(k) => k,
+        _ => return Err(TypeError::new(TypeMessage::InvalidInputType(src))),
+    };
+    let kt = match tgt.as_const() {
+        Some(k) => k,
+        _ => return Err(TypeError::new(TypeMessage::InvalidOutputType(tgt))),
+    };
+
+    Ok(Value::from_const(function_check(ks, kt)))
+}
+
 fn mkerr<T>(x: impl ToString) -> Result<T, TypeError> {
     Err(TypeError::new(TypeMessage::Custom(x.to_string())))
 }
@@ -76,7 +110,7 @@ fn type_one_layer(
     env: &TyEnv,
     kind: &ExprKind<TyExpr, Normalized>,
 ) -> Result<Type, TypeError> {
-    Ok(match &kind {
+    Ok(match kind {
         ExprKind::Import(..) => unreachable!(
             "There should remain no imports in a resolved expression"
         ),
@@ -90,7 +124,9 @@ fn type_one_layer(
         ExprKind::Const(Const::Type) => const_to_value(Const::Kind),
         ExprKind::Const(Const::Kind) => const_to_value(Const::Sort),
         ExprKind::Builtin(b) => {
-            type_with(env, &type_of_builtin(*b))?.normalize_whnf(env.as_nzenv())
+            let t_expr = type_of_builtin(*b);
+            let t_tyexpr = type_with(env, &t_expr)?;
+            t_tyexpr.normalize_whnf(env.as_nzenv())
         }
         ExprKind::BoolLit(_) => builtin_to_value(Builtin::Bool),
         ExprKind::NaturalLit(_) => builtin_to_value(Builtin::Natural),
@@ -108,25 +144,19 @@ fn type_one_layer(
             }
             text_type
         }
-
-        // ExprKind::EmptyListLit(t) => {
-        //     let arg = match &*t.as_whnf() {
-        //         ValueKind::AppliedBuiltin(Builtin::List, args, _)
-        //             if args.len() == 1 =>
-        //         {
-        //             args[0].clone()
-        //         }
-        //         _ => return mkerr("InvalidListType"),
-        //     };
-        //     RetWhole(Value::from_kind_and_type(
-        //         ValueKind::EmptyListLit(arg),
-        //         t.clone(),
-        //     ))
-        // }
+        ExprKind::EmptyListLit(t) => {
+            let t = t.normalize_whnf(env.as_nzenv());
+            match &*t.as_whnf() {
+                ValueKind::AppliedBuiltin(Builtin::List, args, _)
+                    if args.len() == 1 => {}
+                _ => return mkerr("InvalidListType"),
+            };
+            t
+        }
         ExprKind::NEListLit(xs) => {
-            let mut iter = xs.iter().enumerate();
-            let (_, x) = iter.next().unwrap();
-            for (i, y) in iter {
+            let mut iter = xs.iter();
+            let x = iter.next().unwrap();
+            for y in iter {
                 if x.get_type()? != y.get_type()? {
                     return mkerr("InvalidListElement");
                 }
@@ -146,42 +176,96 @@ fn type_one_layer(
 
             Value::from_builtin(Builtin::Optional).app(t)
         }
-        // ExprKind::RecordType(kts) => RetWhole(tck_record_type(
-        //     kts.iter().map(|(x, t)| Ok((x.clone(), t.clone()))),
-        // )?),
-        // ExprKind::UnionType(kts) => RetWhole(tck_union_type(
-        //     kts.iter().map(|(x, t)| Ok((x.clone(), t.clone()))),
-        // )?),
-        // ExprKind::RecordLit(kvs) => RetTypeOnly(tck_record_type(
-        //     kvs.iter().map(|(x, v)| Ok((x.clone(), v.get_type()?))),
-        // )?),
-        ExprKind::Field(r, x) => {
-            match &*r.get_type()?.as_whnf() {
+        ExprKind::RecordLit(kvs) => {
+            use std::collections::hash_map::Entry;
+            let mut kts = HashMap::new();
+            for (x, v) in kvs {
+                // Check for duplicated entries
+                match kts.entry(x.clone()) {
+                    Entry::Occupied(_) => {
+                        return mkerr("RecordTypeDuplicateField")
+                    }
+                    Entry::Vacant(e) => e.insert(v.get_type()?),
+                };
+            }
+
+            let ty = type_of_recordtype(
+                kts.iter()
+                    .map(|(_, t)| Cow::Owned(t.to_tyexpr(env.as_quoteenv()))),
+            )?;
+            Value::from_kind_and_type(ValueKind::RecordType(kts), ty)
+        }
+        ExprKind::RecordType(kts) => {
+            use std::collections::hash_map::Entry;
+            let mut seen_fields = HashMap::new();
+            for (x, _) in kts {
+                // Check for duplicated entries
+                match seen_fields.entry(x.clone()) {
+                    Entry::Occupied(_) => {
+                        return mkerr("RecordTypeDuplicateField")
+                    }
+                    Entry::Vacant(e) => e.insert(()),
+                };
+            }
+
+            type_of_recordtype(kts.iter().map(|(_, t)| Cow::Borrowed(t)))?
+        }
+        ExprKind::UnionType(kts) => {
+            use std::collections::hash_map::Entry;
+            let mut seen_fields = HashMap::new();
+            // Check that all types are the same const
+            let mut k = None;
+            for (x, t) in kts {
+                if let Some(t) = t {
+                    match (k, t.get_type()?.as_const()) {
+                        (None, Some(k2)) => k = Some(k2),
+                        (Some(k1), Some(k2)) if k1 == k2 => {}
+                        _ => return mkerr("InvalidFieldType"),
+                    }
+                }
+                match seen_fields.entry(x) {
+                    Entry::Occupied(_) => {
+                        return mkerr("UnionTypeDuplicateField")
+                    }
+                    Entry::Vacant(e) => e.insert(()),
+                };
+            }
+
+            // An empty union type has type Type;
+            // an union type with only unary variants also has type Type
+            let k = k.unwrap_or(Const::Type);
+
+            Value::from_const(k)
+        }
+        ExprKind::Field(scrut, x) => {
+            match &*scrut.get_type()?.as_whnf() {
                 ValueKind::RecordType(kts) => match kts.get(&x) {
                     Some(tth) => tth.clone(),
                     None => return mkerr("MissingRecordField"),
                 },
-                // TODO: branch here only when r.get_type() is a Const
+                // TODO: branch here only when scrut.get_type() is a Const
                 _ => {
-                    let r_nf = r.normalize_whnf(env.as_nzenv());
-                    let r_nf_borrow = r_nf.as_whnf();
-                    match &*r_nf_borrow {
+                    let scrut_nf = scrut.normalize_whnf(env.as_nzenv());
+                    let scrut_nf_borrow = scrut_nf.as_whnf();
+                    match &*scrut_nf_borrow {
                         ValueKind::UnionType(kts) => match kts.get(x) {
                             // Constructor has type T -> < x: T, ... >
-                            // TODO: check pi type properly
-                            Some(Some(t)) => Value::from_kind_and_type(
+                            Some(Some(ty)) => Value::from_kind_and_type(
                                 ValueKind::PiClosure {
                                     binder: Binder::new(x.clone()),
-                                    annot: t.clone(),
+                                    annot: ty.clone(),
                                     closure: Closure::new(
-                                        t.clone(),
+                                        ty.clone(),
                                         env.as_nzenv(),
-                                        r.clone(),
+                                        scrut.clone(),
                                     ),
                                 },
-                                Value::from_const(Const::Type),
+                                type_of_function(
+                                    ty.get_type()?,
+                                    scrut.get_type()?,
+                                )?,
                             ),
-                            Some(None) => r_nf.clone(),
+                            Some(None) => scrut_nf.clone(),
                             None => return mkerr("MissingUnionField"),
                         },
                         _ => return mkerr("NotARecord"),
@@ -190,28 +274,45 @@ fn type_one_layer(
             }
         }
         ExprKind::Annot(x, t) => {
-            if x.get_type()? != t.normalize_whnf(env.as_nzenv()) {
+            let t = t.normalize_whnf(env.as_nzenv());
+            if x.get_type()? != t {
                 return mkerr("annot mismatch");
             }
-            x.normalize_whnf(env.as_nzenv())
+            t
         }
         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),
+            match &*tf_borrow {
+                // ValueKind::PiClosure { annot, closure, .. } => (annot, closure),
+                ValueKind::PiClosure {
+                    annot: _expected_arg_ty,
+                    closure: ty_closure,
+                    ..
+                } => {
+                    // if arg.get_type()? != *expected_arg_ty {
+                    //     return mkerr(format!(
+                    //         "function annot mismatch: {:?}, {:?}",
+                    //         arg.get_type()?,
+                    //         expected_arg_ty
+                    //     ));
+                    // }
+
+                    let arg_nf = arg.normalize_whnf(env.as_nzenv());
+                    ty_closure.apply(arg_nf)
+                }
+                // ValueKind::Pi(_, _expected_arg_ty, body) => {
+                //     // if arg.get_type()? != *tx {
+                //     //     return mkerr("TypeMismatch");
+                //     // }
+
+                //     let arg_nf = arg.normalize_whnf(env.as_nzenv());
+                //     let ret = body.subst_shift(&AlphaVar::default(), &arg_nf);
+                //     ret.normalize_nf();
+                //     ret
+                // }
                 _ => return mkerr(format!("apply to not Pi: {:?}", tf_borrow)),
-            };
-            // if arg.get_type()? != *expected_arg_ty {
-            //     return mkerr(format!(
-            //         "function annot mismatch: {:?}, {:?}",
-            //         arg.get_type()?,
-            //         expected_arg_ty
-            //     ));
-            // }
-
-            let arg_nf = arg.normalize_whnf(env.as_nzenv());
-            ty_closure.apply(arg_nf)
+            }
         }
         ExprKind::BoolIf(x, y, z) => {
             if *x.get_type()?.as_whnf()
@@ -231,83 +332,63 @@ fn type_one_layer(
 
             y.get_type()?
         }
-        // ExprKind::BinOp(BinOp::RightBiasedRecordMerge, l, r) => {
-        //     let l_type = l.get_type()?;
-        //     let r_type = r.get_type()?;
-
-        //     // Extract the LHS record type
-        //     let l_type_borrow = l_type.as_whnf();
-        //     let kts_x = match &*l_type_borrow {
-        //         ValueKind::RecordType(kts) => kts,
-        //         _ => return mkerr("MustCombineRecord"),
-        //     };
-
-        //     // Extract the RHS record type
-        //     let r_type_borrow = r_type.as_whnf();
-        //     let kts_y = match &*r_type_borrow {
-        //         ValueKind::RecordType(kts) => kts,
-        //         _ => return mkerr("MustCombineRecord"),
-        //     };
+        ExprKind::BinOp(BinOp::RightBiasedRecordMerge, x, y) => {
+            let x_type = x.get_type()?;
+            let y_type = y.get_type()?;
 
-        //     // Union the two records, prefering
-        //     // the values found in the RHS.
-        //     let kts = merge_maps::<_, _, _, !>(kts_x, kts_y, |_, _, r_t| {
-        //         Ok(r_t.clone())
-        //     })?;
+            // Extract the LHS record type
+            let x_type_borrow = x_type.as_whnf();
+            let kts_x = match &*x_type_borrow {
+                ValueKind::RecordType(kts) => kts,
+                _ => return mkerr("MustCombineRecord"),
+            };
 
-        //     // Construct the final record type from the union
-        //     RetTypeOnly(tck_record_type(
-        //         kts.into_iter().map(|(x, v)| Ok((x.clone(), v))),
-        //     )?)
-        // }
-        // ExprKind::BinOp(BinOp::RecursiveRecordMerge, l, r) => RetTypeOnly(type_last_layer(
-        //     ctx,
-        //     ExprKind::BinOp(
-        //         RecursiveRecordTypeMerge,
-        //         l.get_type()?,
-        //         r.get_type()?,
-        //     ),
-        //     Span::Artificial,
-        // )?),
-        // ExprKind::BinOp(BinOp::RecursiveRecordTypeMerge, l, r) => {
-        //     // Extract the LHS record type
-        //     let borrow_l = l.as_whnf();
-        //     let kts_x = match &*borrow_l {
-        //         ValueKind::RecordType(kts) => kts,
-        //         _ => {
-        //             return mkerr("RecordTypeMergeRequiresRecordType")
-        //         }
-        //     };
+            // Extract the RHS record type
+            let y_type_borrow = y_type.as_whnf();
+            let kts_y = match &*y_type_borrow {
+                ValueKind::RecordType(kts) => kts,
+                _ => return mkerr("MustCombineRecord"),
+            };
 
-        //     // Extract the RHS record type
-        //     let borrow_r = r.as_whnf();
-        //     let kts_y = match &*borrow_r {
-        //         ValueKind::RecordType(kts) => kts,
-        //         _ => {
-        //             return mkerr("RecordTypeMergeRequiresRecordType")
-        //         }
-        //     };
+            // Union the two records, prefering
+            // the values found in the RHS.
+            let kts = merge_maps::<_, _, _, !>(kts_x, kts_y, |_, _, r_t| {
+                Ok(r_t.clone())
+            })?;
 
-        //     // Ensure that the records combine without a type error
-        //     let kts = merge_maps(
-        //         kts_x,
-        //         kts_y,
-        //         // If the Label exists for both records, then we hit the recursive case.
-        //         |_, l: &Value, r: &Value| {
-        //             type_last_layer(
-        //                 ctx,
-        //                 ExprKind::BinOp(
-        //                     RecursiveRecordTypeMerge,
-        //                     l.clone(),
-        //                     r.clone(),
-        //                 ),
-        //                 Span::Artificial,
-        //             )
-        //         },
-        //     )?;
-
-        //     RetWhole(tck_record_type(kts.into_iter().map(Ok))?)
-        // }
+            // Construct the final record type
+            let ty = type_of_recordtype(
+                kts.iter()
+                    .map(|(_, t)| Cow::Owned(t.to_tyexpr(env.as_quoteenv()))),
+            )?;
+            Value::from_kind_and_type(ValueKind::RecordType(kts), ty)
+        }
+        ExprKind::BinOp(BinOp::RecursiveRecordMerge, x, y) => {
+            let ekind = ExprKind::BinOp(
+                BinOp::RecursiveRecordTypeMerge,
+                x.get_type()?.to_tyexpr(env.as_quoteenv()),
+                y.get_type()?.to_tyexpr(env.as_quoteenv()),
+            );
+            let ty = type_one_layer(env, &ekind)?;
+            TyExpr::new(TyExprKind::Expr(ekind), Some(ty), Span::Artificial)
+                .normalize_whnf(env.as_nzenv())
+        }
+        ExprKind::BinOp(BinOp::RecursiveRecordTypeMerge, x, y) => {
+            let x_val = x.normalize_whnf(env.as_nzenv());
+            let y_val = y.normalize_whnf(env.as_nzenv());
+            match &*x_val.as_whnf() {
+                ValueKind::RecordType(_) => {}
+                _ => return mkerr("RecordTypeMergeRequiresRecordType"),
+            }
+            match &*y_val.as_whnf() {
+                ValueKind::RecordType(_) => {}
+                _ => return mkerr("RecordTypeMergeRequiresRecordType"),
+            }
+            // A RecordType's type is always a const
+            let xk = x.get_type()?.as_const().unwrap();
+            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, _, _) => {}
@@ -363,6 +444,122 @@ fn type_one_layer(
 
             t
         }
+        // ExprKind::Merge(record, union, type_annot) => {
+        //     let record_type = record.get_type()?;
+        //     let record_borrow = record_type.as_whnf();
+        //     let handlers = match &*record_borrow {
+        //         ValueKind::RecordType(kts) => kts,
+        //         _ => return mkerr("Merge1ArgMustBeRecord"),
+        //     };
+
+        //     let union_type = union.get_type()?;
+        //     let union_borrow = union_type.as_whnf();
+        //     let variants = match &*union_borrow {
+        //         ValueKind::UnionType(kts) => Cow::Borrowed(kts),
+        //         ValueKind::AppliedBuiltin(
+        //             syntax::Builtin::Optional,
+        //             args,
+        //             _,
+        //         ) if args.len() == 1 => {
+        //             let ty = &args[0];
+        //             let mut kts = HashMap::new();
+        //             kts.insert("None".into(), None);
+        //             kts.insert("Some".into(), Some(ty.clone()));
+        //             Cow::Owned(kts)
+        //         }
+        //         _ => return mkerr("Merge2ArgMustBeUnionOrOptional"),
+        //     };
+
+        //     let mut inferred_type = None;
+        //     for (x, handler_type) in handlers {
+        //         let handler_return_type =
+        //             match variants.get(x) {
+        //                 // Union alternative with type
+        //                 Some(Some(variant_type)) => {
+        //                     let handler_type_borrow = handler_type.as_whnf();
+        //                     let (tx, tb) = match &*handler_type_borrow {
+        //                         ValueKind::Pi(_, tx, tb) => (tx, tb),
+        //                         _ => return mkerr("NotAFunction"),
+        //                     };
+
+        //                     if variant_type != tx {
+        //                         return mkerr("TypeMismatch");
+        //                     }
+
+        //                     // Extract `tb` from under the binder. Fails if the variable was used
+        //                     // in `tb`.
+        //                     match tb.over_binder() {
+        //                         Some(x) => x,
+        //                         None => return mkerr(
+        //                             "MergeHandlerReturnTypeMustNotBeDependent",
+        //                         ),
+        //                     }
+        //                 }
+        //                 // Union alternative without type
+        //                 Some(None) => handler_type.clone(),
+        //                 None => return mkerr("MergeHandlerMissingVariant"),
+        //             };
+        //         match &inferred_type {
+        //             None => inferred_type = Some(handler_return_type),
+        //             Some(t) => {
+        //                 if t != &handler_return_type {
+        //                     return mkerr("MergeHandlerTypeMismatch");
+        //                 }
+        //             }
+        //         }
+        //     }
+        //     for x in variants.keys() {
+        //         if !handlers.contains_key(x) {
+        //             return mkerr("MergeVariantMissingHandler");
+        //         }
+        //     }
+
+        //     match (inferred_type, type_annot.as_ref()) {
+        //         (Some(t1), Some(t2)) => {
+        //             if &t1 != t2 {
+        //                 return mkerr("MergeAnnotMismatch");
+        //             }
+        //             RetTypeOnly(t1)
+        //         }
+        //         (Some(t), None) => RetTypeOnly(t),
+        //         (None, Some(t)) => RetTypeOnly(t.clone()),
+        //         (None, None) => return mkerr("MergeEmptyNeedsAnnotation"),
+        //     }
+        // }
+        ExprKind::ToMap(_, _) => unimplemented!("toMap"),
+        ExprKind::Projection(record, labels) => {
+            let record_type = record.get_type()?;
+            let record_type_borrow = record_type.as_whnf();
+            let kts = match &*record_type_borrow {
+                ValueKind::RecordType(kts) => kts,
+                _ => return mkerr("ProjectionMustBeRecord"),
+            };
+
+            let mut new_kts = HashMap::new();
+            for l in labels {
+                match kts.get(l) {
+                    None => return mkerr("ProjectionMissingEntry"),
+                    Some(t) => {
+                        use std::collections::hash_map::Entry;
+                        match new_kts.entry(l.clone()) {
+                            Entry::Occupied(_) => {
+                                return mkerr("ProjectionDuplicateField")
+                            }
+                            Entry::Vacant(e) => e.insert(t.clone()),
+                        }
+                    }
+                };
+            }
+
+            Value::from_kind_and_type(
+                ValueKind::RecordType(new_kts),
+                record_type.get_type()?,
+            )
+        }
+        ExprKind::ProjectionByExpr(_, _) => {
+            unimplemented!("selection by expression")
+        }
+        ExprKind::Completion(_, _) => unimplemented!("record completion"),
         _ => Value::from_const(Const::Type), // TODO
     })
 }
@@ -383,18 +580,17 @@ fn type_with(
             let annot_nf = annot.normalize_whnf(env.as_nzenv());
             let body =
                 type_with(&env.insert_type(&binder, annot_nf.clone()), body)?;
-            let ty = Value::from_kind_and_type(
-                ValueKind::PiClosure {
-                    binder: Binder::new(binder.clone()),
-                    annot: annot_nf.clone(),
-                    closure: Closure::new(
-                        annot_nf,
-                        env.as_nzenv(),
-                        body.get_type()?.to_tyexpr(env.as_quoteenv().insert()),
-                    ),
-                },
-                Value::from_const(Const::Type), // TODO: function_check
+            let body_ty = body.get_type()?;
+            let ty = TyExpr::new(
+                TyExprKind::Expr(ExprKind::Pi(
+                    binder.clone(),
+                    annot.clone(),
+                    body_ty.to_tyexpr(env.as_quoteenv().insert()),
+                )),
+                Some(type_of_function(annot.get_type()?, body_ty.get_type()?)?),
+                Span::Artificial,
             );
+            let ty = ty.normalize_whnf(env.as_nzenv());
             (
                 TyExprKind::Expr(ExprKind::Lam(binder.clone(), annot, body)),
                 Some(ty),
@@ -405,19 +601,20 @@ fn type_with(
             let annot_nf = annot.normalize_whnf(env.as_nzenv());
             let body =
                 type_with(&env.insert_type(binder, annot_nf.clone()), body)?;
+            let ty = type_of_function(annot.get_type()?, body.get_type()?)?;
             (
                 TyExprKind::Expr(ExprKind::Pi(binder.clone(), annot, body)),
-                Some(Value::from_const(Const::Type)), // TODO: function_check
+                Some(ty),
             )
         }
         ExprKind::Let(binder, annot, val, body) => {
-            let v = if let Some(t) = annot {
+            let val = if let Some(t) = annot {
                 t.rewrap(ExprKind::Annot(val.clone(), t.clone()))
             } else {
                 val.clone()
             };
 
-            let val = type_with(env, val)?;
+            let val = type_with(env, &val)?;
             let val_nf = val.normalize_whnf(&env.as_nzenv());
             let body = type_with(&env.insert_value(&binder, val_nf), body)?;
             let body_ty = body.get_type().ok();
-- 
cgit v1.2.3


From 5a835d9db35bf76858e178e1bd66e60128879629 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Mon, 27 Jan 2020 18:45:09 +0000
Subject: Fix a bunch of bugs and more tck

---
 dhall/src/semantics/tck/tyexpr.rs    | 10 ++++++
 dhall/src/semantics/tck/typecheck.rs | 64 ++++++++++++++++++++----------------
 2 files changed, 45 insertions(+), 29 deletions(-)

(limited to 'dhall/src/semantics/tck')

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
-- 
cgit v1.2.3


From 8ced62a2cdde95c4d67298289756c12f53656df0 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 28 Jan 2020 18:41:20 +0000
Subject: Fix all sorts of variable shenanigans

---
 dhall/src/semantics/tck/tyexpr.rs | 15 ++++++++++++++-
 1 file changed, 14 insertions(+), 1 deletion(-)

(limited to 'dhall/src/semantics/tck')

diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index a42265d..9e8dc47 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -12,7 +12,7 @@ use crate::syntax::{ExprKind, Label, Span, V};
 pub(crate) type Type = Value;
 
 // An expression with inferred types at every node and resolved variables.
-#[derive(Debug, Clone)]
+#[derive(Clone)]
 pub(crate) struct TyExpr {
     kind: Box<TyExprKind>,
     ty: Option<Type>,
@@ -114,3 +114,16 @@ fn tyexpr_to_expr<'a>(
         }
     })
 }
+
+impl std::fmt::Debug for TyExpr {
+    fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        let mut x = fmt.debug_struct("TyExpr");
+        x.field("kind", self.kind());
+        if let Some(ty) = self.ty.as_ref() {
+            x.field("type", &ty);
+        } else {
+            x.field("type", &None::<()>);
+        }
+        x.finish()
+    }
+}
-- 
cgit v1.2.3


From 084e81956e99bc759012be7c171f4095c2e59d22 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 28 Jan 2020 19:34:11 +0000
Subject: Thread env through nztion to fix Foo/build closures

---
 dhall/src/semantics/tck/typecheck.rs | 14 +++++++++++---
 1 file changed, 11 insertions(+), 3 deletions(-)

(limited to 'dhall/src/semantics/tck')

diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 4ca5d4d..e2619b5 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -35,6 +35,14 @@ impl TyEnv {
             items: NzEnv::new(),
         }
     }
+    pub fn from_nzenv_alpha(items: &NzEnv) -> Self {
+        TyEnv {
+            names: NameEnv::from_binders(
+                std::iter::repeat("_".into()).take(items.size()),
+            ),
+            items: items.clone(),
+        }
+    }
     pub fn as_quoteenv(&self) -> QuoteEnv {
         self.names.as_quoteenv()
     }
@@ -147,7 +155,7 @@ fn type_one_layer(
         ExprKind::EmptyListLit(t) => {
             let t = t.normalize_whnf(env.as_nzenv());
             match &*t.as_whnf() {
-                ValueKind::AppliedBuiltin(Builtin::List, args, _)
+                ValueKind::AppliedBuiltin(Builtin::List, args, _, _)
                     if args.len() == 1 => {}
                 _ => return mkerr("InvalidListType"),
             };
@@ -404,7 +412,7 @@ fn type_one_layer(
         ExprKind::BinOp(BinOp::ListAppend, l, r) => {
             let l_ty = l.get_type()?;
             match &*l_ty.as_whnf() {
-                ValueKind::AppliedBuiltin(Builtin::List, _, _) => {}
+                ValueKind::AppliedBuiltin(Builtin::List, _, _, _) => {}
                 _ => return mkerr("BinOpTypeMismatch"),
             }
 
@@ -572,7 +580,7 @@ fn type_one_layer(
 
 /// 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(
+pub(crate) fn type_with(
     env: &TyEnv,
     expr: &Expr<Normalized>,
 ) -> Result<TyExpr, TypeError> {
-- 
cgit v1.2.3


From 7683b0d762cf0df489ad4bc006e8db2358e81cf4 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 28 Jan 2020 21:50:04 +0000
Subject: Implement assert & merge and fix more bugs

---
 dhall/src/semantics/tck/typecheck.rs | 208 ++++++++++++++++++++---------------
 1 file changed, 118 insertions(+), 90 deletions(-)

(limited to 'dhall/src/semantics/tck')

diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index e2619b5..1b8f261 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -7,7 +7,7 @@ use std::collections::HashMap;
 
 use crate::error::{TypeError, TypeMessage};
 use crate::semantics::core::context::TyCtx;
-use crate::semantics::nze::{NameEnv, QuoteEnv};
+use crate::semantics::nze::{NameEnv, NzVar, QuoteEnv};
 use crate::semantics::phase::normalize::{merge_maps, NzEnv};
 use crate::semantics::phase::typecheck::{
     builtin_to_value, const_to_value, type_of_builtin,
@@ -44,7 +44,7 @@ impl TyEnv {
         }
     }
     pub fn as_quoteenv(&self) -> QuoteEnv {
-        self.names.as_quoteenv()
+        self.items.as_quoteenv()
     }
     pub fn as_nzenv(&self) -> &NzEnv {
         &self.items
@@ -262,8 +262,7 @@ fn type_one_layer(
                                 ValueKind::PiClosure {
                                     binder: Binder::new(x.clone()),
                                     annot: ty.clone(),
-                                    closure: Closure::new(
-                                        ty.clone(),
+                                    closure: Closure::new_constant(
                                         env.as_nzenv(),
                                         scrut.clone(),
                                     ),
@@ -300,6 +299,15 @@ fn type_one_layer(
             }
             x_ty
         }
+        ExprKind::Assert(t) => {
+            let t = t.normalize_whnf(env.as_nzenv());
+            match &*t.as_whnf() {
+                ValueKind::Equivalence(x, y) if x == y => {}
+                ValueKind::Equivalence(..) => return mkerr("AssertMismatch"),
+                _ => return mkerr("AssertMustTakeEquivalence"),
+            }
+            t
+        }
         ExprKind::App(f, arg) => {
             let tf = f.get_type()?;
             let tf_borrow = tf.as_whnf();
@@ -458,88 +466,109 @@ fn type_one_layer(
 
             t
         }
-        // ExprKind::Merge(record, union, type_annot) => {
-        //     let record_type = record.get_type()?;
-        //     let record_borrow = record_type.as_whnf();
-        //     let handlers = match &*record_borrow {
-        //         ValueKind::RecordType(kts) => kts,
-        //         _ => return mkerr("Merge1ArgMustBeRecord"),
-        //     };
-
-        //     let union_type = union.get_type()?;
-        //     let union_borrow = union_type.as_whnf();
-        //     let variants = match &*union_borrow {
-        //         ValueKind::UnionType(kts) => Cow::Borrowed(kts),
-        //         ValueKind::AppliedBuiltin(
-        //             syntax::Builtin::Optional,
-        //             args,
-        //             _,
-        //         ) if args.len() == 1 => {
-        //             let ty = &args[0];
-        //             let mut kts = HashMap::new();
-        //             kts.insert("None".into(), None);
-        //             kts.insert("Some".into(), Some(ty.clone()));
-        //             Cow::Owned(kts)
-        //         }
-        //         _ => return mkerr("Merge2ArgMustBeUnionOrOptional"),
-        //     };
-
-        //     let mut inferred_type = None;
-        //     for (x, handler_type) in handlers {
-        //         let handler_return_type =
-        //             match variants.get(x) {
-        //                 // Union alternative with type
-        //                 Some(Some(variant_type)) => {
-        //                     let handler_type_borrow = handler_type.as_whnf();
-        //                     let (tx, tb) = match &*handler_type_borrow {
-        //                         ValueKind::Pi(_, tx, tb) => (tx, tb),
-        //                         _ => return mkerr("NotAFunction"),
-        //                     };
-
-        //                     if variant_type != tx {
-        //                         return mkerr("TypeMismatch");
-        //                     }
-
-        //                     // Extract `tb` from under the binder. Fails if the variable was used
-        //                     // in `tb`.
-        //                     match tb.over_binder() {
-        //                         Some(x) => x,
-        //                         None => return mkerr(
-        //                             "MergeHandlerReturnTypeMustNotBeDependent",
-        //                         ),
-        //                     }
-        //                 }
-        //                 // Union alternative without type
-        //                 Some(None) => handler_type.clone(),
-        //                 None => return mkerr("MergeHandlerMissingVariant"),
-        //             };
-        //         match &inferred_type {
-        //             None => inferred_type = Some(handler_return_type),
-        //             Some(t) => {
-        //                 if t != &handler_return_type {
-        //                     return mkerr("MergeHandlerTypeMismatch");
-        //                 }
-        //             }
-        //         }
-        //     }
-        //     for x in variants.keys() {
-        //         if !handlers.contains_key(x) {
-        //             return mkerr("MergeVariantMissingHandler");
-        //         }
-        //     }
-
-        //     match (inferred_type, type_annot.as_ref()) {
-        //         (Some(t1), Some(t2)) => {
-        //             if &t1 != t2 {
-        //                 return mkerr("MergeAnnotMismatch");
-        //             }
-        //             RetTypeOnly(t1)
-        //         }
-        //         (Some(t), None) => RetTypeOnly(t),
-        //         (None, Some(t)) => RetTypeOnly(t.clone()),
-        //         (None, None) => return mkerr("MergeEmptyNeedsAnnotation"),
-        //     }
-        // }
+        ExprKind::Merge(record, union, type_annot) => {
+            let record_type = record.get_type()?;
+            let record_borrow = record_type.as_whnf();
+            let handlers = match &*record_borrow {
+                ValueKind::RecordType(kts) => kts,
+                _ => return mkerr("Merge1ArgMustBeRecord"),
+            };
+
+            let union_type = union.get_type()?;
+            let union_borrow = union_type.as_whnf();
+            let variants = match &*union_borrow {
+                ValueKind::UnionType(kts) => Cow::Borrowed(kts),
+                ValueKind::AppliedBuiltin(
+                    syntax::Builtin::Optional,
+                    args,
+                    _,
+                    _,
+                ) if args.len() == 1 => {
+                    let ty = &args[0];
+                    let mut kts = HashMap::new();
+                    kts.insert("None".into(), None);
+                    kts.insert("Some".into(), Some(ty.clone()));
+                    Cow::Owned(kts)
+                }
+                _ => return mkerr("Merge2ArgMustBeUnionOrOptional"),
+            };
+
+            let mut inferred_type = None;
+            for (x, handler_type) in handlers {
+                let handler_return_type = match variants.get(x) {
+                    // Union alternative with type
+                    Some(Some(variant_type)) => {
+                        let handler_type_borrow = handler_type.as_whnf();
+                        match &*handler_type_borrow {
+                            ValueKind::Pi(_, tx, tb) => {
+                                if variant_type != tx {
+                                    return mkerr("MergeHandlerTypeMismatch");
+                                }
+
+                                // Extract `tb` from under the binder. Fails if the variable was used
+                                // in `tb`.
+                                match tb.over_binder() {
+                                    Some(x) => x,
+                                    None => return mkerr(
+                                        "MergeHandlerReturnTypeMustNotBeDependent",
+                                    ),
+                                }
+                            }
+                            ValueKind::PiClosure { closure, annot, .. } => {
+                                if variant_type != annot {
+                                    // return mkerr("MergeHandlerTypeMismatch");
+                                    return mkerr(format!(
+                                        "MergeHandlerTypeMismatch: {:#?} != {:#?}",
+                                        variant_type,
+                                        annot
+                                    ));
+                                }
+
+                                let v = NzVar::fresh();
+                                // TODO: handle case where variable is used in closure
+                                closure.apply_var(v)
+                            }
+                            _ => return mkerr("NotAFunction"),
+                        }
+                    }
+                    // Union alternative without type
+                    Some(None) => handler_type.clone(),
+                    None => return mkerr("MergeHandlerMissingVariant"),
+                };
+                match &inferred_type {
+                    None => inferred_type = Some(handler_return_type),
+                    Some(t) => {
+                        if t != &handler_return_type {
+                            // return mkerr("MergeHandlerTypeMismatch");
+                            return mkerr(format!(
+                                "MergeHandlerTypeMismatch: {:#?} != {:#?}",
+                                t, handler_return_type,
+                            ));
+                        }
+                    }
+                }
+            }
+            for x in variants.keys() {
+                if !handlers.contains_key(x) {
+                    return mkerr("MergeVariantMissingHandler");
+                }
+            }
+
+            let type_annot = type_annot
+                .as_ref()
+                .map(|t| t.normalize_whnf(env.as_nzenv()));
+            match (inferred_type, type_annot) {
+                (Some(t1), Some(t2)) => {
+                    if t1 != t2 {
+                        return mkerr("MergeAnnotMismatch");
+                    }
+                    t1
+                }
+                (Some(t), None) => t,
+                (None, Some(t)) => t,
+                (None, None) => return mkerr("MergeEmptyNeedsAnnotation"),
+            }
+        }
         ExprKind::ToMap(_, _) => unimplemented!("toMap"),
         ExprKind::Projection(record, labels) => {
             let record_type = record.get_type()?;
@@ -574,7 +603,6 @@ fn type_one_layer(
             unimplemented!("selection by expression")
         }
         ExprKind::Completion(_, _) => unimplemented!("record completion"),
-        _ => Value::from_const(Const::Type), // TODO
     })
 }
 
@@ -592,14 +620,14 @@ pub(crate) fn type_with(
         ExprKind::Lam(binder, annot, body) => {
             let annot = type_with(env, annot)?;
             let annot_nf = annot.normalize_whnf(env.as_nzenv());
-            let body =
-                type_with(&env.insert_type(&binder, annot_nf.clone()), body)?;
+            let body_env = env.insert_type(&binder, annot_nf.clone());
+            let body = type_with(&body_env, body)?;
             let body_ty = body.get_type()?;
             let ty = TyExpr::new(
                 TyExprKind::Expr(ExprKind::Pi(
                     binder.clone(),
                     annot.clone(),
-                    body_ty.to_tyexpr(env.as_quoteenv().insert()),
+                    body_ty.to_tyexpr(body_env.as_quoteenv()),
                 )),
                 Some(type_of_function(annot.get_type()?, body_ty.get_type()?)?),
                 Span::Artificial,
-- 
cgit v1.2.3


From f31ccaa40df77b1ca8b37db46a819460c831006e Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Wed, 29 Jan 2020 18:17:12 +0000
Subject: Fix more bugs

---
 dhall/src/semantics/tck/typecheck.rs | 69 +++++++++++++++++++-----------------
 1 file changed, 36 insertions(+), 33 deletions(-)

(limited to 'dhall/src/semantics/tck')

diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 1b8f261..a83f175 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -44,7 +44,7 @@ impl TyEnv {
         }
     }
     pub fn as_quoteenv(&self) -> QuoteEnv {
-        self.items.as_quoteenv()
+        self.names.as_quoteenv()
     }
     pub fn as_nzenv(&self) -> &NzEnv {
         &self.items
@@ -70,9 +70,6 @@ impl TyEnv {
         let ty = self.items.lookup_val(&var).get_type().unwrap();
         Some((TyExprKind::Var(var), ty))
     }
-    pub fn size(&self) -> usize {
-        self.names.size()
-    }
 }
 
 fn type_of_recordtype<'a>(
@@ -312,33 +309,24 @@ fn type_one_layer(
             let tf = f.get_type()?;
             let tf_borrow = tf.as_whnf();
             match &*tf_borrow {
-                // ValueKind::PiClosure { annot, closure, .. } => (annot, closure),
-                ValueKind::PiClosure {
-                    annot: _expected_arg_ty,
-                    closure: ty_closure,
-                    ..
-                } => {
-                    // if arg.get_type()? != *expected_arg_ty {
-                    //     return mkerr(format!(
-                    //         "function annot mismatch: {:?}, {:?}",
-                    //         arg.get_type()?,
-                    //         expected_arg_ty
-                    //     ));
-                    // }
+                ValueKind::PiClosure { annot, closure, .. } => {
+                    if arg.get_type()? != *annot {
+                        // return mkerr(format!("function annot mismatch"));
+                        return mkerr(format!(
+                            "function annot mismatch: ({} : {}) : {}",
+                            arg.to_expr_tyenv(env),
+                            arg.get_type()?
+                                .to_tyexpr(env.as_quoteenv())
+                                .to_expr_tyenv(env),
+                            annot
+                                .to_tyexpr(env.as_quoteenv())
+                                .to_expr_tyenv(env),
+                        ));
+                    }
 
                     let arg_nf = arg.normalize_whnf(env.as_nzenv());
-                    ty_closure.apply(arg_nf)
+                    closure.apply(arg_nf)
                 }
-                // ValueKind::Pi(_, _expected_arg_ty, body) => {
-                //     // if arg.get_type()? != *tx {
-                //     //     return mkerr("TypeMismatch");
-                //     // }
-
-                //     let arg_nf = arg.normalize_whnf(env.as_nzenv());
-                //     let ret = body.subst_shift(&AlphaVar::default(), &arg_nf);
-                //     ret.normalize_nf();
-                //     ret
-                // }
                 _ => return mkerr(format!("apply to not Pi: {:?}", tf_borrow)),
             }
         }
@@ -404,14 +392,29 @@ fn type_one_layer(
         ExprKind::BinOp(BinOp::RecursiveRecordTypeMerge, x, y) => {
             let x_val = x.normalize_whnf(env.as_nzenv());
             let y_val = y.normalize_whnf(env.as_nzenv());
-            match &*x_val.as_whnf() {
-                ValueKind::RecordType(_) => {}
+            let x_val_borrow = x_val.as_whnf();
+            let y_val_borrow = y_val.as_whnf();
+            let kts_x = match &*x_val_borrow {
+                ValueKind::RecordType(kts) => kts,
                 _ => return mkerr("RecordTypeMergeRequiresRecordType"),
-            }
-            match &*y_val.as_whnf() {
-                ValueKind::RecordType(_) => {}
+            };
+            let kts_y = match &*y_val_borrow {
+                ValueKind::RecordType(kts) => kts,
                 _ => return mkerr("RecordTypeMergeRequiresRecordType"),
+            };
+            for (k, tx) in kts_x {
+                if let Some(ty) = kts_y.get(k) {
+                    type_one_layer(
+                        env,
+                        &ExprKind::BinOp(
+                            BinOp::RecursiveRecordTypeMerge,
+                            tx.to_tyexpr(env.as_quoteenv()),
+                            ty.to_tyexpr(env.as_quoteenv()),
+                        ),
+                    )?;
+                }
             }
+
             // A RecordType's type is always a const
             let xk = x.get_type()?.as_const().unwrap();
             let yk = y.get_type()?.as_const().unwrap();
-- 
cgit v1.2.3


From 1e466a20533d936f44430b1bc18508cd00e5ccd2 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Wed, 29 Jan 2020 18:48:19 +0000
Subject: Use TyExpr in Typed

---
 dhall/src/semantics/tck/typecheck.rs | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

(limited to 'dhall/src/semantics/tck')

diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index a83f175..5880d92 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -677,7 +677,7 @@ pub(crate) fn type_with(
             (TyExprKind::Expr(ExprKind::Const(Const::Sort)), None)
         }
         ExprKind::Embed(p) => {
-            return Ok(p.clone().into_typed().into_value().to_tyexpr_noenv())
+            return Ok(p.clone().into_value().to_tyexpr_noenv())
         }
         ekind => {
             let ekind = ekind.traverse_ref(|e| type_with(env, e))?;
@@ -692,3 +692,10 @@ pub(crate) fn type_with(
 pub(crate) fn typecheck(e: &Expr<Normalized>) -> Result<TyExpr, TypeError> {
     type_with(&TyEnv::new(), e)
 }
+
+pub(crate) fn typecheck_with(
+    expr: &Expr<Normalized>,
+    ty: Expr<Normalized>,
+) -> Result<TyExpr, TypeError> {
+    typecheck(&expr.rewrap(ExprKind::Annot(expr.clone(), ty)))
+}
-- 
cgit v1.2.3


From e410dbb428e621fe600be43ddecca1c7bff7cb2f Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Wed, 29 Jan 2020 19:11:52 +0000
Subject: Fix insufficient normalization

---
 dhall/src/semantics/tck/tyexpr.rs    | 10 +++++++++-
 dhall/src/semantics/tck/typecheck.rs | 12 ++++++------
 2 files changed, 15 insertions(+), 7 deletions(-)

(limited to 'dhall/src/semantics/tck')

diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index 9e8dc47..e4108ad 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -67,7 +67,15 @@ impl TyExpr {
         normalize_tyexpr_whnf(self, env)
     }
     pub fn normalize_whnf_noenv(&self) -> Value {
-        normalize_tyexpr_whnf(self, &NzEnv::new())
+        self.normalize_whnf(&NzEnv::new())
+    }
+    pub fn normalize_nf(&self, env: &NzEnv) -> Value {
+        let mut val = self.normalize_whnf(env);
+        val.normalize_mut();
+        val
+    }
+    pub fn normalize_nf_noenv(&self) -> Value {
+        self.normalize_nf(&NzEnv::new())
     }
 }
 
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 5880d92..abb36e1 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -150,7 +150,7 @@ fn type_one_layer(
             text_type
         }
         ExprKind::EmptyListLit(t) => {
-            let t = t.normalize_whnf(env.as_nzenv());
+            let t = t.normalize_nf(env.as_nzenv());
             match &*t.as_whnf() {
                 ValueKind::AppliedBuiltin(Builtin::List, args, _, _)
                     if args.len() == 1 => {}
@@ -250,7 +250,7 @@ fn type_one_layer(
                 },
                 // TODO: branch here only when scrut.get_type() is a Const
                 _ => {
-                    let scrut_nf = scrut.normalize_whnf(env.as_nzenv());
+                    let scrut_nf = scrut.normalize_nf(env.as_nzenv());
                     let scrut_nf_borrow = scrut_nf.as_whnf();
                     match &*scrut_nf_borrow {
                         ValueKind::UnionType(kts) => match kts.get(x) {
@@ -324,7 +324,7 @@ fn type_one_layer(
                         ));
                     }
 
-                    let arg_nf = arg.normalize_whnf(env.as_nzenv());
+                    let arg_nf = arg.normalize_nf(env.as_nzenv());
                     closure.apply(arg_nf)
                 }
                 _ => return mkerr(format!("apply to not Pi: {:?}", tf_borrow)),
@@ -387,7 +387,7 @@ fn type_one_layer(
             );
             let ty = type_one_layer(env, &ekind)?;
             TyExpr::new(TyExprKind::Expr(ekind), Some(ty), Span::Artificial)
-                .normalize_whnf(env.as_nzenv())
+                .normalize_nf(env.as_nzenv())
         }
         ExprKind::BinOp(BinOp::RecursiveRecordTypeMerge, x, y) => {
             let x_val = x.normalize_whnf(env.as_nzenv());
@@ -622,7 +622,7 @@ pub(crate) fn type_with(
         },
         ExprKind::Lam(binder, annot, body) => {
             let annot = type_with(env, annot)?;
-            let annot_nf = annot.normalize_whnf(env.as_nzenv());
+            let annot_nf = annot.normalize_nf(env.as_nzenv());
             let body_env = env.insert_type(&binder, annot_nf.clone());
             let body = type_with(&body_env, body)?;
             let body_ty = body.get_type()?;
@@ -660,7 +660,7 @@ pub(crate) fn type_with(
             };
 
             let val = type_with(env, &val)?;
-            let val_nf = val.normalize_whnf(&env.as_nzenv());
+            let val_nf = val.normalize_nf(&env.as_nzenv());
             let body = type_with(&env.insert_value(&binder, val_nf), body)?;
             let body_ty = body.get_type().ok();
             (
-- 
cgit v1.2.3


From db6c09f33c3c794e4b6ec8a7aa80978d945a9d7a Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Wed, 29 Jan 2020 21:26:42 +0000
Subject: Remove dead code

---
 dhall/src/semantics/tck/tyexpr.rs    |  5 -----
 dhall/src/semantics/tck/typecheck.rs | 30 ++++++++----------------------
 2 files changed, 8 insertions(+), 27 deletions(-)

(limited to 'dhall/src/semantics/tck')

diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index e4108ad..abb6fa8 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -1,4 +1,3 @@
-#![allow(dead_code)]
 use crate::error::{TypeError, TypeMessage};
 use crate::semantics::core::var::AlphaVar;
 use crate::semantics::phase::normalize::{normalize_tyexpr_whnf, NzEnv};
@@ -58,10 +57,6 @@ impl TyExpr {
         let mut env = env.iter().collect();
         tyexpr_to_expr(self, opts, &mut env)
     }
-    // TODO: temporary hack
-    pub fn to_value(&self) -> Value {
-        todo!()
-    }
 
     pub fn normalize_whnf(&self, env: &NzEnv) -> Value {
         normalize_tyexpr_whnf(self, env)
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index abb36e1..99eb31f 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -1,12 +1,8 @@
-#![allow(dead_code)]
-#![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, NzVar, QuoteEnv};
 use crate::semantics::phase::normalize::{merge_maps, NzEnv};
 use crate::semantics::phase::typecheck::{
@@ -14,12 +10,12 @@ use crate::semantics::phase::typecheck::{
 };
 use crate::semantics::phase::Normalized;
 use crate::semantics::{
-    AlphaVar, Binder, Closure, TyExpr, TyExprKind, Type, Value, ValueKind,
+    Binder, Closure, TyExpr, TyExprKind, Type, Value, ValueKind,
 };
 use crate::syntax;
 use crate::syntax::{
     BinOp, Builtin, Const, Expr, ExprKind, InterpolatedTextContents, Label,
-    Span, UnspannedExpr, V,
+    Span, V,
 };
 
 #[derive(Debug, Clone)]
@@ -111,6 +107,8 @@ fn mkerr<T>(x: impl ToString) -> Result<T, TypeError> {
     Err(TypeError::new(TypeMessage::Custom(x.to_string())))
 }
 
+/// When all sub-expressions have been typed, check the remaining toplevel
+/// layer.
 fn type_one_layer(
     env: &TyEnv,
     kind: &ExprKind<TyExpr, Normalized>,
@@ -503,20 +501,6 @@ fn type_one_layer(
                     Some(Some(variant_type)) => {
                         let handler_type_borrow = handler_type.as_whnf();
                         match &*handler_type_borrow {
-                            ValueKind::Pi(_, tx, tb) => {
-                                if variant_type != tx {
-                                    return mkerr("MergeHandlerTypeMismatch");
-                                }
-
-                                // Extract `tb` from under the binder. Fails if the variable was used
-                                // in `tb`.
-                                match tb.over_binder() {
-                                    Some(x) => x,
-                                    None => return mkerr(
-                                        "MergeHandlerReturnTypeMustNotBeDependent",
-                                    ),
-                                }
-                            }
                             ValueKind::PiClosure { closure, annot, .. } => {
                                 if variant_type != annot {
                                     // return mkerr("MergeHandlerTypeMismatch");
@@ -609,8 +593,7 @@ fn type_one_layer(
     })
 }
 
-/// Type-check an expression and return the expression alongside its type if type-checking
-/// succeeded, or an error if type-checking failed.
+/// `type_with` typechecks an expressio in the provided environment.
 pub(crate) fn type_with(
     env: &TyEnv,
     expr: &Expr<Normalized>,
@@ -689,10 +672,13 @@ pub(crate) fn type_with(
     Ok(TyExpr::new(tyekind, ty, expr.span()))
 }
 
+/// Typecheck an expression and return the expression annotated with types if type-checking
+/// succeeded, or an error if type-checking failed.
 pub(crate) fn typecheck(e: &Expr<Normalized>) -> Result<TyExpr, TypeError> {
     type_with(&TyEnv::new(), e)
 }
 
+/// Like `typecheck`, but additionally checks that the expression's type matches the provided type.
 pub(crate) fn typecheck_with(
     expr: &Expr<Normalized>,
     ty: Expr<Normalized>,
-- 
cgit v1.2.3


From 26d4975a4c94c2b9fd0c075ad94c2588e3cf24e8 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Wed, 29 Jan 2020 21:29:53 +0000
Subject: Use NameEnv in tyexpr_to_expr

---
 dhall/src/semantics/tck/tyexpr.rs | 27 +++++++++------------------
 1 file changed, 9 insertions(+), 18 deletions(-)

(limited to 'dhall/src/semantics/tck')

diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index abb6fa8..b64c519 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -1,12 +1,13 @@
 use crate::error::{TypeError, TypeMessage};
 use crate::semantics::core::var::AlphaVar;
+use crate::semantics::nze::nzexpr::NameEnv;
 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};
+use crate::syntax::{ExprKind, Span, V};
 
 pub(crate) type Type = Value;
 
@@ -46,15 +47,14 @@ impl TyExpr {
 
     /// Converts a value back to the corresponding AST expression.
     pub fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr {
-        tyexpr_to_expr(self, opts, &mut Vec::new())
+        tyexpr_to_expr(self, opts, &mut NameEnv::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();
+        let mut env = env.as_nameenv().clone();
         tyexpr_to_expr(self, opts, &mut env)
     }
 
@@ -77,30 +77,21 @@ impl TyExpr {
 fn tyexpr_to_expr<'a>(
     tyexpr: &'a TyExpr,
     opts: ToExprOptions,
-    ctx: &mut Vec<&'a Label>,
+    env: &mut NameEnv,
 ) -> NormalizedExpr {
     rc(match tyexpr.kind() {
         TyExprKind::Var(v) if opts.alpha => {
             ExprKind::Var(V("_".into(), v.idx()))
         }
-        TyExprKind::Var(v) => {
-            let name = ctx[ctx.len() - 1 - v.idx()];
-            let idx = ctx
-                .iter()
-                .rev()
-                .take(v.idx())
-                .filter(|l| **l == name)
-                .count();
-            ExprKind::Var(V(name.clone(), idx))
-        }
+        TyExprKind::Var(v) => ExprKind::Var(env.label_var(v)),
         TyExprKind::Expr(e) => {
             let e = e.map_ref_maybe_binder(|l, tye| {
                 if let Some(l) = l {
-                    ctx.push(l);
+                    env.insert_mut(l);
                 }
-                let e = tyexpr_to_expr(tye, opts, ctx);
+                let e = tyexpr_to_expr(tye, opts, env);
                 if let Some(_) = l {
-                    ctx.pop();
+                    env.remove_mut();
                 }
                 e
             });
-- 
cgit v1.2.3


From 22bec94618454f57773716870f5624579ab712ce Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Wed, 29 Jan 2020 21:31:53 +0000
Subject: s/QuoteEnv/VarEnv/

---
 dhall/src/semantics/tck/typecheck.rs | 34 ++++++++++++++++------------------
 1 file changed, 16 insertions(+), 18 deletions(-)

(limited to 'dhall/src/semantics/tck')

diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 99eb31f..7a225f7 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -3,7 +3,7 @@ use std::cmp::max;
 use std::collections::HashMap;
 
 use crate::error::{TypeError, TypeMessage};
-use crate::semantics::nze::{NameEnv, NzVar, QuoteEnv};
+use crate::semantics::nze::{NameEnv, NzVar, VarEnv};
 use crate::semantics::phase::normalize::{merge_maps, NzEnv};
 use crate::semantics::phase::typecheck::{
     builtin_to_value, const_to_value, type_of_builtin,
@@ -39,8 +39,8 @@ impl TyEnv {
             items: items.clone(),
         }
     }
-    pub fn as_quoteenv(&self) -> QuoteEnv {
-        self.names.as_quoteenv()
+    pub fn as_varenv(&self) -> VarEnv {
+        self.names.as_varenv()
     }
     pub fn as_nzenv(&self) -> &NzEnv {
         &self.items
@@ -194,7 +194,7 @@ fn type_one_layer(
 
             let ty = type_of_recordtype(
                 kts.iter()
-                    .map(|(_, t)| Cow::Owned(t.to_tyexpr(env.as_quoteenv()))),
+                    .map(|(_, t)| Cow::Owned(t.to_tyexpr(env.as_varenv()))),
             )?;
             Value::from_kind_and_type(ValueKind::RecordType(kts), ty)
         }
@@ -282,13 +282,13 @@ fn type_one_layer(
                 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)
+                    x_ty.to_tyexpr(env.as_varenv()).to_expr_tyenv(env),
+                    t.to_tyexpr(env.as_varenv()).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)
+                //     x_ty.to_tyexpr(env.as_varenv()).to_expr_tyenv(env),
+                //     t.to_tyexpr(env.as_varenv()).to_expr_tyenv(env)
                 // ));
                 // return mkerr(format!("annot mismatch: {:#?} : {:#?}", x, t,));
             }
@@ -314,11 +314,9 @@ fn type_one_layer(
                             "function annot mismatch: ({} : {}) : {}",
                             arg.to_expr_tyenv(env),
                             arg.get_type()?
-                                .to_tyexpr(env.as_quoteenv())
-                                .to_expr_tyenv(env),
-                            annot
-                                .to_tyexpr(env.as_quoteenv())
+                                .to_tyexpr(env.as_varenv())
                                 .to_expr_tyenv(env),
+                            annot.to_tyexpr(env.as_varenv()).to_expr_tyenv(env),
                         ));
                     }
 
@@ -373,15 +371,15 @@ fn type_one_layer(
             // Construct the final record type
             let ty = type_of_recordtype(
                 kts.iter()
-                    .map(|(_, t)| Cow::Owned(t.to_tyexpr(env.as_quoteenv()))),
+                    .map(|(_, t)| Cow::Owned(t.to_tyexpr(env.as_varenv()))),
             )?;
             Value::from_kind_and_type(ValueKind::RecordType(kts), ty)
         }
         ExprKind::BinOp(BinOp::RecursiveRecordMerge, x, y) => {
             let ekind = ExprKind::BinOp(
                 BinOp::RecursiveRecordTypeMerge,
-                x.get_type()?.to_tyexpr(env.as_quoteenv()),
-                y.get_type()?.to_tyexpr(env.as_quoteenv()),
+                x.get_type()?.to_tyexpr(env.as_varenv()),
+                y.get_type()?.to_tyexpr(env.as_varenv()),
             );
             let ty = type_one_layer(env, &ekind)?;
             TyExpr::new(TyExprKind::Expr(ekind), Some(ty), Span::Artificial)
@@ -406,8 +404,8 @@ fn type_one_layer(
                         env,
                         &ExprKind::BinOp(
                             BinOp::RecursiveRecordTypeMerge,
-                            tx.to_tyexpr(env.as_quoteenv()),
-                            ty.to_tyexpr(env.as_quoteenv()),
+                            tx.to_tyexpr(env.as_varenv()),
+                            ty.to_tyexpr(env.as_varenv()),
                         ),
                     )?;
                 }
@@ -613,7 +611,7 @@ pub(crate) fn type_with(
                 TyExprKind::Expr(ExprKind::Pi(
                     binder.clone(),
                     annot.clone(),
-                    body_ty.to_tyexpr(body_env.as_quoteenv()),
+                    body_ty.to_tyexpr(body_env.as_varenv()),
                 )),
                 Some(type_of_function(annot.get_type()?, body_ty.get_type()?)?),
                 Span::Artificial,
-- 
cgit v1.2.3


From 489174a426e6057a68b6edd2e9b4387d09912a25 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Wed, 29 Jan 2020 21:56:52 +0000
Subject: Move envs to their own files

---
 dhall/src/semantics/tck/env.rs       | 137 +++++++++++++++++++++++++++++++++++
 dhall/src/semantics/tck/mod.rs       |   2 +
 dhall/src/semantics/tck/tyexpr.rs    |   6 +-
 dhall/src/semantics/tck/typecheck.rs |  58 +--------------
 4 files changed, 144 insertions(+), 59 deletions(-)
 create mode 100644 dhall/src/semantics/tck/env.rs

(limited to 'dhall/src/semantics/tck')

diff --git a/dhall/src/semantics/tck/env.rs b/dhall/src/semantics/tck/env.rs
new file mode 100644
index 0000000..32c2f21
--- /dev/null
+++ b/dhall/src/semantics/tck/env.rs
@@ -0,0 +1,137 @@
+use crate::semantics::{AlphaVar, NzEnv, NzVar, TyExprKind, Type, Value};
+use crate::syntax::{Label, V};
+
+/// Environment for indexing variables.
+#[derive(Debug, Clone, Copy)]
+pub(crate) struct VarEnv {
+    size: usize,
+}
+
+/// Environment for resolving names.
+#[derive(Debug, Clone)]
+pub(crate) struct NameEnv {
+    names: Vec<Label>,
+}
+
+/// Environment for typing expressions.
+#[derive(Debug, Clone)]
+pub(crate) struct TyEnv {
+    names: NameEnv,
+    items: NzEnv,
+}
+
+impl VarEnv {
+    pub fn new() -> Self {
+        VarEnv { size: 0 }
+    }
+    pub fn size(&self) -> usize {
+        self.size
+    }
+    pub fn insert(&self) -> Self {
+        VarEnv {
+            size: self.size + 1,
+        }
+    }
+    pub fn lookup(&self, var: &NzVar) -> AlphaVar {
+        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)))
+    }
+}
+
+impl NameEnv {
+    pub fn new() -> Self {
+        NameEnv { names: Vec::new() }
+    }
+    pub fn from_binders(names: impl Iterator<Item = Label>) -> Self {
+        NameEnv {
+            names: names.collect(),
+        }
+    }
+    pub fn as_varenv(&self) -> VarEnv {
+        VarEnv {
+            size: self.names.len(),
+        }
+    }
+
+    pub fn insert(&self, x: &Label) -> Self {
+        let mut env = self.clone();
+        env.insert_mut(x);
+        env
+    }
+    pub fn insert_mut(&mut self, x: &Label) {
+        self.names.push(x.clone())
+    }
+    pub fn remove_mut(&mut self) {
+        self.names.pop();
+    }
+
+    pub fn unlabel_var(&self, var: &V<Label>) -> Option<AlphaVar> {
+        let V(name, idx) = var;
+        let (idx, _) = self
+            .names
+            .iter()
+            .rev()
+            .enumerate()
+            .filter(|(_, n)| *n == name)
+            .nth(*idx)?;
+        Some(AlphaVar::new(V((), idx)))
+    }
+    pub fn label_var(&self, var: &AlphaVar) -> V<Label> {
+        let name = &self.names[self.names.len() - 1 - var.idx()];
+        let idx = self
+            .names
+            .iter()
+            .rev()
+            .take(var.idx())
+            .filter(|n| *n == name)
+            .count();
+        V(name.clone(), idx)
+    }
+}
+
+impl TyEnv {
+    pub fn new() -> Self {
+        TyEnv {
+            names: NameEnv::new(),
+            items: NzEnv::new(),
+        }
+    }
+    pub fn from_nzenv_alpha(items: &NzEnv) -> Self {
+        TyEnv {
+            names: NameEnv::from_binders(
+                std::iter::repeat("_".into()).take(items.size()),
+            ),
+            items: items.clone(),
+        }
+    }
+    pub fn as_varenv(&self) -> VarEnv {
+        self.names.as_varenv()
+    }
+    pub fn as_nzenv(&self) -> &NzEnv {
+        &self.items
+    }
+    pub fn as_nameenv(&self) -> &NameEnv {
+        &self.names
+    }
+
+    pub fn insert_type(&self, x: &Label, t: Type) -> 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(&self, var: &V<Label>) -> Option<(TyExprKind, Type)> {
+        let var = self.names.unlabel_var(var)?;
+        let ty = self.items.lookup_val(&var).get_type().unwrap();
+        Some((TyExprKind::Var(var), ty))
+    }
+}
diff --git a/dhall/src/semantics/tck/mod.rs b/dhall/src/semantics/tck/mod.rs
index ba95847..28974af 100644
--- a/dhall/src/semantics/tck/mod.rs
+++ b/dhall/src/semantics/tck/mod.rs
@@ -1,4 +1,6 @@
 pub mod context;
+pub mod env;
 pub mod tyexpr;
 pub mod typecheck;
+pub(crate) use env::*;
 pub(crate) use tyexpr::*;
diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index b64c519..262cda6 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -1,12 +1,10 @@
 use crate::error::{TypeError, TypeMessage};
 use crate::semantics::core::var::AlphaVar;
-use crate::semantics::nze::nzexpr::NameEnv;
-use crate::semantics::phase::normalize::{normalize_tyexpr_whnf, NzEnv};
+use crate::semantics::phase::normalize::normalize_tyexpr_whnf;
 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::semantics::{NameEnv, NzEnv, TyEnv, Value};
 use crate::syntax::{ExprKind, Span, V};
 
 pub(crate) type Type = Value;
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 7a225f7..789105f 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -3,71 +3,19 @@ use std::cmp::max;
 use std::collections::HashMap;
 
 use crate::error::{TypeError, TypeMessage};
-use crate::semantics::nze::{NameEnv, NzVar, VarEnv};
-use crate::semantics::phase::normalize::{merge_maps, NzEnv};
+use crate::semantics::phase::normalize::merge_maps;
 use crate::semantics::phase::typecheck::{
     builtin_to_value, const_to_value, type_of_builtin,
 };
 use crate::semantics::phase::Normalized;
 use crate::semantics::{
-    Binder, Closure, TyExpr, TyExprKind, Type, Value, ValueKind,
+    Binder, Closure, NzVar, TyEnv, TyExpr, TyExprKind, Type, Value, ValueKind,
 };
 use crate::syntax;
 use crate::syntax::{
-    BinOp, Builtin, Const, Expr, ExprKind, InterpolatedTextContents, Label,
-    Span, V,
+    BinOp, Builtin, Const, Expr, ExprKind, InterpolatedTextContents, Span,
 };
 
-#[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 from_nzenv_alpha(items: &NzEnv) -> Self {
-        TyEnv {
-            names: NameEnv::from_binders(
-                std::iter::repeat("_".into()).take(items.size()),
-            ),
-            items: items.clone(),
-        }
-    }
-    pub fn as_varenv(&self) -> VarEnv {
-        self.names.as_varenv()
-    }
-    pub fn as_nzenv(&self) -> &NzEnv {
-        &self.items
-    }
-    pub fn as_nameenv(&self) -> &NameEnv {
-        &self.names
-    }
-
-    pub fn insert_type(&self, x: &Label, t: Type) -> 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(&self, var: &V<Label>) -> Option<(TyExprKind, Type)> {
-        let var = self.names.unlabel_var(var)?;
-        let ty = self.items.lookup_val(&var).get_type().unwrap();
-        Some((TyExprKind::Var(var), ty))
-    }
-}
-
 fn type_of_recordtype<'a>(
     tys: impl Iterator<Item = Cow<'a, TyExpr>>,
 ) -> Result<Type, TypeError> {
-- 
cgit v1.2.3


From a928c3c4f51d87fd942e8a81727962c00abf6808 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Wed, 29 Jan 2020 22:06:01 +0000
Subject: Cleanup variable handling

---
 dhall/src/semantics/tck/env.rs    | 10 +++++-----
 dhall/src/semantics/tck/tyexpr.rs | 26 ++++++++++++++++++++------
 2 files changed, 25 insertions(+), 11 deletions(-)

(limited to 'dhall/src/semantics/tck')

diff --git a/dhall/src/semantics/tck/env.rs b/dhall/src/semantics/tck/env.rs
index 32c2f21..1276a48 100644
--- a/dhall/src/semantics/tck/env.rs
+++ b/dhall/src/semantics/tck/env.rs
@@ -37,7 +37,7 @@ impl VarEnv {
     }
     pub fn lookup_fallible(&self, var: &NzVar) -> Option<AlphaVar> {
         let idx = self.size.checked_sub(var.idx() + 1)?;
-        Some(AlphaVar::new(V((), idx)))
+        Some(AlphaVar::new(idx))
     }
 }
 
@@ -68,7 +68,7 @@ impl NameEnv {
         self.names.pop();
     }
 
-    pub fn unlabel_var(&self, var: &V<Label>) -> Option<AlphaVar> {
+    pub fn unlabel_var(&self, var: &V) -> Option<AlphaVar> {
         let V(name, idx) = var;
         let (idx, _) = self
             .names
@@ -77,9 +77,9 @@ impl NameEnv {
             .enumerate()
             .filter(|(_, n)| *n == name)
             .nth(*idx)?;
-        Some(AlphaVar::new(V((), idx)))
+        Some(AlphaVar::new(idx))
     }
-    pub fn label_var(&self, var: &AlphaVar) -> V<Label> {
+    pub fn label_var(&self, var: &AlphaVar) -> V {
         let name = &self.names[self.names.len() - 1 - var.idx()];
         let idx = self
             .names
@@ -129,7 +129,7 @@ impl TyEnv {
             items: self.items.insert_value(e),
         }
     }
-    pub fn lookup(&self, var: &V<Label>) -> Option<(TyExprKind, Type)> {
+    pub fn lookup(&self, var: &V) -> Option<(TyExprKind, Type)> {
         let var = self.names.unlabel_var(var)?;
         let ty = self.items.lookup_val(&var).get_type().unwrap();
         Some((TyExprKind::Var(var), ty))
diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index 262cda6..114bb14 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -1,5 +1,4 @@
 use crate::error::{TypeError, TypeMessage};
-use crate::semantics::core::var::AlphaVar;
 use crate::semantics::phase::normalize::normalize_tyexpr_whnf;
 use crate::semantics::phase::typecheck::rc;
 use crate::semantics::phase::Normalized;
@@ -9,6 +8,19 @@ use crate::syntax::{ExprKind, Span, V};
 
 pub(crate) type Type = Value;
 
+/// Stores an alpha-normalized variable.
+#[derive(Debug, Clone, Copy)]
+pub struct AlphaVar {
+    idx: usize,
+}
+
+#[derive(Debug, Clone)]
+pub(crate) enum TyExprKind {
+    Var(AlphaVar),
+    // Forbidden ExprKind variants: Var, Import, Embed
+    Expr(ExprKind<TyExpr, Normalized>),
+}
+
 // An expression with inferred types at every node and resolved variables.
 #[derive(Clone)]
 pub(crate) struct TyExpr {
@@ -17,11 +29,13 @@ pub(crate) struct TyExpr {
     span: Span,
 }
 
-#[derive(Debug, Clone)]
-pub(crate) enum TyExprKind {
-    Var(AlphaVar),
-    // Forbidden ExprKind variants: Var, Import, Embed
-    Expr(ExprKind<TyExpr, Normalized>),
+impl AlphaVar {
+    pub(crate) fn new(idx: usize) -> Self {
+        AlphaVar { idx }
+    }
+    pub(crate) fn idx(&self) -> usize {
+        self.idx
+    }
 }
 
 impl TyExpr {
-- 
cgit v1.2.3


From 655f67fb29ca847f86c3e19338757e7b031d4f50 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Thu, 30 Jan 2020 11:09:39 +0000
Subject: Move builtins-related code to its own module

---
 dhall/src/semantics/tck/mod.rs       |  2 +-
 dhall/src/semantics/tck/tyexpr.rs    |  3 +--
 dhall/src/semantics/tck/typecheck.rs | 22 ++++++++++------------
 3 files changed, 12 insertions(+), 15 deletions(-)

(limited to 'dhall/src/semantics/tck')

diff --git a/dhall/src/semantics/tck/mod.rs b/dhall/src/semantics/tck/mod.rs
index 28974af..1df2a48 100644
--- a/dhall/src/semantics/tck/mod.rs
+++ b/dhall/src/semantics/tck/mod.rs
@@ -1,6 +1,6 @@
-pub mod context;
 pub mod env;
 pub mod tyexpr;
 pub mod typecheck;
 pub(crate) use env::*;
 pub(crate) use tyexpr::*;
+pub(crate) use typecheck::*;
diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index 114bb14..bf7c130 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -1,9 +1,8 @@
 use crate::error::{TypeError, TypeMessage};
 use crate::semantics::phase::normalize::normalize_tyexpr_whnf;
-use crate::semantics::phase::typecheck::rc;
 use crate::semantics::phase::Normalized;
 use crate::semantics::phase::{NormalizedExpr, ToExprOptions};
-use crate::semantics::{NameEnv, NzEnv, TyEnv, Value};
+use crate::semantics::{rc, NameEnv, NzEnv, TyEnv, Value};
 use crate::syntax::{ExprKind, Span, V};
 
 pub(crate) type Type = Value;
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 789105f..22ba72d 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -4,12 +4,10 @@ use std::collections::HashMap;
 
 use crate::error::{TypeError, TypeMessage};
 use crate::semantics::phase::normalize::merge_maps;
-use crate::semantics::phase::typecheck::{
-    builtin_to_value, const_to_value, type_of_builtin,
-};
 use crate::semantics::phase::Normalized;
 use crate::semantics::{
-    Binder, Closure, NzVar, TyEnv, TyExpr, TyExprKind, Type, Value, ValueKind,
+    type_of_builtin, Binder, Closure, NzVar, TyEnv, TyExpr, TyExprKind, Type,
+    Value, ValueKind,
 };
 use crate::syntax;
 use crate::syntax::{
@@ -72,19 +70,19 @@ fn type_one_layer(
         | ExprKind::Const(Const::Sort)
         | ExprKind::Embed(..) => unreachable!(), // Handled in type_with
 
-        ExprKind::Const(Const::Type) => const_to_value(Const::Kind),
-        ExprKind::Const(Const::Kind) => const_to_value(Const::Sort),
+        ExprKind::Const(Const::Type) => Value::from_const(Const::Kind),
+        ExprKind::Const(Const::Kind) => Value::from_const(Const::Sort),
         ExprKind::Builtin(b) => {
             let t_expr = type_of_builtin(*b);
             let t_tyexpr = type_with(env, &t_expr)?;
             t_tyexpr.normalize_whnf(env.as_nzenv())
         }
-        ExprKind::BoolLit(_) => builtin_to_value(Builtin::Bool),
-        ExprKind::NaturalLit(_) => builtin_to_value(Builtin::Natural),
-        ExprKind::IntegerLit(_) => builtin_to_value(Builtin::Integer),
-        ExprKind::DoubleLit(_) => builtin_to_value(Builtin::Double),
+        ExprKind::BoolLit(_) => Value::from_builtin(Builtin::Bool),
+        ExprKind::NaturalLit(_) => Value::from_builtin(Builtin::Natural),
+        ExprKind::IntegerLit(_) => Value::from_builtin(Builtin::Integer),
+        ExprKind::DoubleLit(_) => Value::from_builtin(Builtin::Double),
         ExprKind::TextLit(interpolated) => {
-            let text_type = builtin_to_value(Builtin::Text);
+            let text_type = Value::from_builtin(Builtin::Text);
             for contents in interpolated.iter() {
                 use InterpolatedTextContents::Expr;
                 if let Expr(x) = contents {
@@ -388,7 +386,7 @@ fn type_one_layer(
             Value::from_const(Const::Type)
         }
         ExprKind::BinOp(o, l, r) => {
-            let t = builtin_to_value(match o {
+            let t = Value::from_builtin(match o {
                 BinOp::BoolAnd
                 | BinOp::BoolOr
                 | BinOp::BoolEQ
-- 
cgit v1.2.3


From 7dd2d64073b662acccb39601591c754279385308 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Thu, 30 Jan 2020 11:24:48 +0000
Subject: No need for the current env to tck Foo/build closures

---
 dhall/src/semantics/tck/env.rs | 13 -------------
 1 file changed, 13 deletions(-)

(limited to 'dhall/src/semantics/tck')

diff --git a/dhall/src/semantics/tck/env.rs b/dhall/src/semantics/tck/env.rs
index 1276a48..d4cc37d 100644
--- a/dhall/src/semantics/tck/env.rs
+++ b/dhall/src/semantics/tck/env.rs
@@ -45,11 +45,6 @@ impl NameEnv {
     pub fn new() -> Self {
         NameEnv { names: Vec::new() }
     }
-    pub fn from_binders(names: impl Iterator<Item = Label>) -> Self {
-        NameEnv {
-            names: names.collect(),
-        }
-    }
     pub fn as_varenv(&self) -> VarEnv {
         VarEnv {
             size: self.names.len(),
@@ -99,14 +94,6 @@ impl TyEnv {
             items: NzEnv::new(),
         }
     }
-    pub fn from_nzenv_alpha(items: &NzEnv) -> Self {
-        TyEnv {
-            names: NameEnv::from_binders(
-                std::iter::repeat("_".into()).take(items.size()),
-            ),
-            items: items.clone(),
-        }
-    }
     pub fn as_varenv(&self) -> VarEnv {
         self.names.as_varenv()
     }
-- 
cgit v1.2.3


From ec5fb594adf10b18a4457c3089ce4b00e2c50a39 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Thu, 30 Jan 2020 11:53:18 +0000
Subject: Remove debug output in type errors

---
 dhall/src/semantics/tck/typecheck.rs | 15 +++------------
 1 file changed, 3 insertions(+), 12 deletions(-)

(limited to 'dhall/src/semantics/tck')

diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 22ba72d..5422e6d 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -269,7 +269,7 @@ fn type_one_layer(
                     let arg_nf = arg.normalize_nf(env.as_nzenv());
                     closure.apply(arg_nf)
                 }
-                _ => return mkerr(format!("apply to not Pi: {:?}", tf_borrow)),
+                _ => return mkerr(format!("apply to not Pi")),
             }
         }
         ExprKind::BoolIf(x, y, z) => {
@@ -447,12 +447,7 @@ fn type_one_layer(
                         match &*handler_type_borrow {
                             ValueKind::PiClosure { closure, annot, .. } => {
                                 if variant_type != annot {
-                                    // return mkerr("MergeHandlerTypeMismatch");
-                                    return mkerr(format!(
-                                        "MergeHandlerTypeMismatch: {:#?} != {:#?}",
-                                        variant_type,
-                                        annot
-                                    ));
+                                    return mkerr("MergeHandlerTypeMismatch");
                                 }
 
                                 let v = NzVar::fresh();
@@ -470,11 +465,7 @@ fn type_one_layer(
                     None => inferred_type = Some(handler_return_type),
                     Some(t) => {
                         if t != &handler_return_type {
-                            // return mkerr("MergeHandlerTypeMismatch");
-                            return mkerr(format!(
-                                "MergeHandlerTypeMismatch: {:#?} != {:#?}",
-                                t, handler_return_type,
-                            ));
+                            return mkerr("MergeHandlerTypeMismatch");
                         }
                     }
                 }
-- 
cgit v1.2.3


From 17732b041dbd44f39ce3d04a289146db9882e865 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Thu, 30 Jan 2020 11:53:37 +0000
Subject: Encapsulate partially applied builtin in a separate struct

---
 dhall/src/semantics/tck/typecheck.rs | 26 +++++++++++++++-----------
 1 file changed, 15 insertions(+), 11 deletions(-)

(limited to 'dhall/src/semantics/tck')

diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 5422e6d..e1a9c11 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -6,10 +6,9 @@ use crate::error::{TypeError, TypeMessage};
 use crate::semantics::phase::normalize::merge_maps;
 use crate::semantics::phase::Normalized;
 use crate::semantics::{
-    type_of_builtin, Binder, Closure, NzVar, TyEnv, TyExpr, TyExprKind, Type,
-    Value, ValueKind,
+    type_of_builtin, Binder, BuiltinClosure, Closure, NzVar, TyEnv, TyExpr,
+    TyExprKind, Type, Value, ValueKind,
 };
-use crate::syntax;
 use crate::syntax::{
     BinOp, Builtin, Const, Expr, ExprKind, InterpolatedTextContents, Span,
 };
@@ -96,8 +95,11 @@ fn type_one_layer(
         ExprKind::EmptyListLit(t) => {
             let t = t.normalize_nf(env.as_nzenv());
             match &*t.as_whnf() {
-                ValueKind::AppliedBuiltin(Builtin::List, args, _, _)
-                    if args.len() == 1 => {}
+                ValueKind::AppliedBuiltin(BuiltinClosure {
+                    b: Builtin::List,
+                    args,
+                    ..
+                }) if args.len() == 1 => {}
                 _ => return mkerr("InvalidListType"),
             };
             t
@@ -365,7 +367,10 @@ fn type_one_layer(
         ExprKind::BinOp(BinOp::ListAppend, l, r) => {
             let l_ty = l.get_type()?;
             match &*l_ty.as_whnf() {
-                ValueKind::AppliedBuiltin(Builtin::List, _, _, _) => {}
+                ValueKind::AppliedBuiltin(BuiltinClosure {
+                    b: Builtin::List,
+                    ..
+                }) => {}
                 _ => return mkerr("BinOpTypeMismatch"),
             }
 
@@ -423,12 +428,11 @@ fn type_one_layer(
             let union_borrow = union_type.as_whnf();
             let variants = match &*union_borrow {
                 ValueKind::UnionType(kts) => Cow::Borrowed(kts),
-                ValueKind::AppliedBuiltin(
-                    syntax::Builtin::Optional,
+                ValueKind::AppliedBuiltin(BuiltinClosure {
+                    b: Builtin::Optional,
                     args,
-                    _,
-                    _,
-                ) if args.len() == 1 => {
+                    ..
+                }) if args.len() == 1 => {
                     let ty = &args[0];
                     let mut kts = HashMap::new();
                     kts.insert("None".into(), None);
-- 
cgit v1.2.3


From cb86493012b268ec32ad85a42b54fb1a2adab7b0 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Thu, 30 Jan 2020 14:20:01 +0000
Subject: s/as_whnf/kind/

---
 dhall/src/semantics/tck/typecheck.rs | 32 +++++++++++++++-----------------
 1 file changed, 15 insertions(+), 17 deletions(-)

(limited to 'dhall/src/semantics/tck')

diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index e1a9c11..0c5e779 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -94,7 +94,7 @@ fn type_one_layer(
         }
         ExprKind::EmptyListLit(t) => {
             let t = t.normalize_nf(env.as_nzenv());
-            match &*t.as_whnf() {
+            match &*t.kind() {
                 ValueKind::AppliedBuiltin(BuiltinClosure {
                     b: Builtin::List,
                     args,
@@ -189,7 +189,7 @@ fn type_one_layer(
             Value::from_const(k)
         }
         ExprKind::Field(scrut, x) => {
-            match &*scrut.get_type()?.as_whnf() {
+            match &*scrut.get_type()?.kind() {
                 ValueKind::RecordType(kts) => match kts.get(&x) {
                     Some(tth) => tth.clone(),
                     None => return mkerr("MissingRecordField"),
@@ -197,7 +197,7 @@ fn type_one_layer(
                 // TODO: branch here only when scrut.get_type() is a Const
                 _ => {
                     let scrut_nf = scrut.normalize_nf(env.as_nzenv());
-                    let scrut_nf_borrow = scrut_nf.as_whnf();
+                    let scrut_nf_borrow = scrut_nf.kind();
                     match &*scrut_nf_borrow {
                         ValueKind::UnionType(kts) => match kts.get(x) {
                             // Constructor has type T -> < x: T, ... >
@@ -244,7 +244,7 @@ fn type_one_layer(
         }
         ExprKind::Assert(t) => {
             let t = t.normalize_whnf(env.as_nzenv());
-            match &*t.as_whnf() {
+            match &*t.kind() {
                 ValueKind::Equivalence(x, y) if x == y => {}
                 ValueKind::Equivalence(..) => return mkerr("AssertMismatch"),
                 _ => return mkerr("AssertMustTakeEquivalence"),
@@ -253,7 +253,7 @@ fn type_one_layer(
         }
         ExprKind::App(f, arg) => {
             let tf = f.get_type()?;
-            let tf_borrow = tf.as_whnf();
+            let tf_borrow = tf.kind();
             match &*tf_borrow {
                 ValueKind::PiClosure { annot, closure, .. } => {
                     if arg.get_type()? != *annot {
@@ -275,9 +275,7 @@ fn type_one_layer(
             }
         }
         ExprKind::BoolIf(x, y, z) => {
-            if *x.get_type()?.as_whnf()
-                != ValueKind::from_builtin(Builtin::Bool)
-            {
+            if *x.get_type()?.kind() != ValueKind::from_builtin(Builtin::Bool) {
                 return mkerr("InvalidPredicate");
             }
             if y.get_type()?.get_type()?.as_const() != Some(Const::Type) {
@@ -297,14 +295,14 @@ fn type_one_layer(
             let y_type = y.get_type()?;
 
             // Extract the LHS record type
-            let x_type_borrow = x_type.as_whnf();
+            let x_type_borrow = x_type.kind();
             let kts_x = match &*x_type_borrow {
                 ValueKind::RecordType(kts) => kts,
                 _ => return mkerr("MustCombineRecord"),
             };
 
             // Extract the RHS record type
-            let y_type_borrow = y_type.as_whnf();
+            let y_type_borrow = y_type.kind();
             let kts_y = match &*y_type_borrow {
                 ValueKind::RecordType(kts) => kts,
                 _ => return mkerr("MustCombineRecord"),
@@ -336,8 +334,8 @@ fn type_one_layer(
         ExprKind::BinOp(BinOp::RecursiveRecordTypeMerge, x, y) => {
             let x_val = x.normalize_whnf(env.as_nzenv());
             let y_val = y.normalize_whnf(env.as_nzenv());
-            let x_val_borrow = x_val.as_whnf();
-            let y_val_borrow = y_val.as_whnf();
+            let x_val_borrow = x_val.kind();
+            let y_val_borrow = y_val.kind();
             let kts_x = match &*x_val_borrow {
                 ValueKind::RecordType(kts) => kts,
                 _ => return mkerr("RecordTypeMergeRequiresRecordType"),
@@ -366,7 +364,7 @@ fn type_one_layer(
         }
         ExprKind::BinOp(BinOp::ListAppend, l, r) => {
             let l_ty = l.get_type()?;
-            match &*l_ty.as_whnf() {
+            match &*l_ty.kind() {
                 ValueKind::AppliedBuiltin(BuiltinClosure {
                     b: Builtin::List,
                     ..
@@ -418,14 +416,14 @@ fn type_one_layer(
         }
         ExprKind::Merge(record, union, type_annot) => {
             let record_type = record.get_type()?;
-            let record_borrow = record_type.as_whnf();
+            let record_borrow = record_type.kind();
             let handlers = match &*record_borrow {
                 ValueKind::RecordType(kts) => kts,
                 _ => return mkerr("Merge1ArgMustBeRecord"),
             };
 
             let union_type = union.get_type()?;
-            let union_borrow = union_type.as_whnf();
+            let union_borrow = union_type.kind();
             let variants = match &*union_borrow {
                 ValueKind::UnionType(kts) => Cow::Borrowed(kts),
                 ValueKind::AppliedBuiltin(BuiltinClosure {
@@ -447,7 +445,7 @@ fn type_one_layer(
                 let handler_return_type = match variants.get(x) {
                     // Union alternative with type
                     Some(Some(variant_type)) => {
-                        let handler_type_borrow = handler_type.as_whnf();
+                        let handler_type_borrow = handler_type.kind();
                         match &*handler_type_borrow {
                             ValueKind::PiClosure { closure, annot, .. } => {
                                 if variant_type != annot {
@@ -498,7 +496,7 @@ fn type_one_layer(
         ExprKind::ToMap(_, _) => unimplemented!("toMap"),
         ExprKind::Projection(record, labels) => {
             let record_type = record.get_type()?;
-            let record_type_borrow = record_type.as_whnf();
+            let record_type_borrow = record_type.kind();
             let kts = match &*record_type_borrow {
                 ValueKind::RecordType(kts) => kts,
                 _ => return mkerr("ProjectionMustBeRecord"),
-- 
cgit v1.2.3


From 25bd09136742403d7f3d6c6143f72e6687f39457 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Thu, 30 Jan 2020 14:48:38 +0000
Subject: Make unnormalized Values unobservable

---
 dhall/src/semantics/tck/tyexpr.rs | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'dhall/src/semantics/tck')

diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index bf7c130..5492b8b 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -76,9 +76,7 @@ impl TyExpr {
         self.normalize_whnf(&NzEnv::new())
     }
     pub fn normalize_nf(&self, env: &NzEnv) -> Value {
-        let mut val = self.normalize_whnf(env);
-        val.normalize_mut();
-        val
+        self.normalize_whnf(env)
     }
     pub fn normalize_nf_noenv(&self) -> Value {
         self.normalize_nf(&NzEnv::new())
-- 
cgit v1.2.3


From 837298f26e07bb264a6b6f0286cbb811553b0477 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Thu, 30 Jan 2020 14:49:17 +0000
Subject: Increase encapsulation for Closures

---
 dhall/src/semantics/tck/typecheck.rs | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'dhall/src/semantics/tck')

diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 0c5e779..bc1c87f 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -6,7 +6,7 @@ use crate::error::{TypeError, TypeMessage};
 use crate::semantics::phase::normalize::merge_maps;
 use crate::semantics::phase::Normalized;
 use crate::semantics::{
-    type_of_builtin, Binder, BuiltinClosure, Closure, NzVar, TyEnv, TyExpr,
+    type_of_builtin, Binder, BuiltinClosure, Closure, TyEnv, TyExpr,
     TyExprKind, Type, Value, ValueKind,
 };
 use crate::syntax::{
@@ -48,7 +48,7 @@ fn type_of_function(src: Type, tgt: Type) -> Result<Type, TypeError> {
     Ok(Value::from_const(function_check(ks, kt)))
 }
 
-fn mkerr<T>(x: impl ToString) -> Result<T, TypeError> {
+fn mkerr<T, S: ToString>(x: S) -> Result<T, TypeError> {
     Err(TypeError::new(TypeMessage::Custom(x.to_string())))
 }
 
@@ -452,9 +452,9 @@ fn type_one_layer(
                                     return mkerr("MergeHandlerTypeMismatch");
                                 }
 
-                                let v = NzVar::fresh();
-                                // TODO: handle case where variable is used in closure
-                                closure.apply_var(v)
+                                closure.remove_binder().or_else(|()| {
+                                    mkerr("MergeReturnTypeIsDependent")
+                                })?
                             }
                             _ => return mkerr("NotAFunction"),
                         }
-- 
cgit v1.2.3


From 67bbbafbc9730d74e20e5ac082ae9a87bdf2234e Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Thu, 30 Jan 2020 16:39:25 +0000
Subject: Introduce Thunks and normalize lazily

---
 dhall/src/semantics/tck/tyexpr.rs    | 22 +++++++++++++---------
 dhall/src/semantics/tck/typecheck.rs | 31 +++++++++++++++----------------
 2 files changed, 28 insertions(+), 25 deletions(-)

(limited to 'dhall/src/semantics/tck')

diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index 5492b8b..0a27f32 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -49,6 +49,9 @@ impl TyExpr {
     pub fn kind(&self) -> &TyExprKind {
         &*self.kind
     }
+    pub fn span(&self) -> &Span {
+        &self.span
+    }
     pub fn get_type(&self) -> Result<Type, TypeError> {
         match &self.ty {
             Some(t) => Ok(t.clone()),
@@ -69,17 +72,18 @@ impl TyExpr {
         tyexpr_to_expr(self, opts, &mut env)
     }
 
-    pub fn normalize_whnf(&self, env: &NzEnv) -> Value {
-        normalize_tyexpr_whnf(self, env)
-    }
-    pub fn normalize_whnf_noenv(&self) -> Value {
-        self.normalize_whnf(&NzEnv::new())
+    /// Eval the TyExpr. It will actually get evaluated only as needed on demand.
+    pub fn eval(&self, env: &NzEnv) -> Value {
+        Value::new_thunk(env, self.clone())
     }
-    pub fn normalize_nf(&self, env: &NzEnv) -> Value {
-        self.normalize_whnf(env)
+    /// Eval a closed TyExpr (i.e. without free variables). It will actually get evaluated only as
+    /// needed on demand.
+    pub fn eval_closed_expr(&self) -> Value {
+        self.eval(&NzEnv::new())
     }
-    pub fn normalize_nf_noenv(&self) -> Value {
-        self.normalize_nf(&NzEnv::new())
+    /// Eval a closed TyExpr fully and recursively;
+    pub fn rec_eval_closed_expr(&self) -> Value {
+        normalize_tyexpr_whnf(self, &NzEnv::new())
     }
 }
 
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index bc1c87f..d741b40 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -74,7 +74,7 @@ fn type_one_layer(
         ExprKind::Builtin(b) => {
             let t_expr = type_of_builtin(*b);
             let t_tyexpr = type_with(env, &t_expr)?;
-            t_tyexpr.normalize_whnf(env.as_nzenv())
+            t_tyexpr.eval(env.as_nzenv())
         }
         ExprKind::BoolLit(_) => Value::from_builtin(Builtin::Bool),
         ExprKind::NaturalLit(_) => Value::from_builtin(Builtin::Natural),
@@ -93,7 +93,7 @@ fn type_one_layer(
             text_type
         }
         ExprKind::EmptyListLit(t) => {
-            let t = t.normalize_nf(env.as_nzenv());
+            let t = t.eval(env.as_nzenv());
             match &*t.kind() {
                 ValueKind::AppliedBuiltin(BuiltinClosure {
                     b: Builtin::List,
@@ -196,7 +196,7 @@ fn type_one_layer(
                 },
                 // TODO: branch here only when scrut.get_type() is a Const
                 _ => {
-                    let scrut_nf = scrut.normalize_nf(env.as_nzenv());
+                    let scrut_nf = scrut.eval(env.as_nzenv());
                     let scrut_nf_borrow = scrut_nf.kind();
                     match &*scrut_nf_borrow {
                         ValueKind::UnionType(kts) => match kts.get(x) {
@@ -224,7 +224,7 @@ fn type_one_layer(
             }
         }
         ExprKind::Annot(x, t) => {
-            let t = t.normalize_whnf(env.as_nzenv());
+            let t = t.eval(env.as_nzenv());
             let x_ty = x.get_type()?;
             if x_ty != t {
                 return mkerr(format!(
@@ -243,7 +243,7 @@ fn type_one_layer(
             x_ty
         }
         ExprKind::Assert(t) => {
-            let t = t.normalize_whnf(env.as_nzenv());
+            let t = t.eval(env.as_nzenv());
             match &*t.kind() {
                 ValueKind::Equivalence(x, y) if x == y => {}
                 ValueKind::Equivalence(..) => return mkerr("AssertMismatch"),
@@ -268,7 +268,7 @@ fn type_one_layer(
                         ));
                     }
 
-                    let arg_nf = arg.normalize_nf(env.as_nzenv());
+                    let arg_nf = arg.eval(env.as_nzenv());
                     closure.apply(arg_nf)
                 }
                 _ => return mkerr(format!("apply to not Pi")),
@@ -329,11 +329,11 @@ fn type_one_layer(
             );
             let ty = type_one_layer(env, &ekind)?;
             TyExpr::new(TyExprKind::Expr(ekind), Some(ty), Span::Artificial)
-                .normalize_nf(env.as_nzenv())
+                .eval(env.as_nzenv())
         }
         ExprKind::BinOp(BinOp::RecursiveRecordTypeMerge, x, y) => {
-            let x_val = x.normalize_whnf(env.as_nzenv());
-            let y_val = y.normalize_whnf(env.as_nzenv());
+            let x_val = x.eval(env.as_nzenv());
+            let y_val = y.eval(env.as_nzenv());
             let x_val_borrow = x_val.kind();
             let y_val_borrow = y_val.kind();
             let kts_x = match &*x_val_borrow {
@@ -478,9 +478,8 @@ fn type_one_layer(
                 }
             }
 
-            let type_annot = type_annot
-                .as_ref()
-                .map(|t| t.normalize_whnf(env.as_nzenv()));
+            let type_annot =
+                type_annot.as_ref().map(|t| t.eval(env.as_nzenv()));
             match (inferred_type, type_annot) {
                 (Some(t1), Some(t2)) => {
                     if t1 != t2 {
@@ -542,7 +541,7 @@ pub(crate) fn type_with(
         },
         ExprKind::Lam(binder, annot, body) => {
             let annot = type_with(env, annot)?;
-            let annot_nf = annot.normalize_nf(env.as_nzenv());
+            let annot_nf = annot.eval(env.as_nzenv());
             let body_env = env.insert_type(&binder, annot_nf.clone());
             let body = type_with(&body_env, body)?;
             let body_ty = body.get_type()?;
@@ -555,7 +554,7 @@ pub(crate) fn type_with(
                 Some(type_of_function(annot.get_type()?, body_ty.get_type()?)?),
                 Span::Artificial,
             );
-            let ty = ty.normalize_whnf(env.as_nzenv());
+            let ty = ty.eval(env.as_nzenv());
             (
                 TyExprKind::Expr(ExprKind::Lam(binder.clone(), annot, body)),
                 Some(ty),
@@ -563,7 +562,7 @@ pub(crate) fn type_with(
         }
         ExprKind::Pi(binder, annot, body) => {
             let annot = type_with(env, annot)?;
-            let annot_nf = annot.normalize_whnf(env.as_nzenv());
+            let annot_nf = annot.eval(env.as_nzenv());
             let body =
                 type_with(&env.insert_type(binder, annot_nf.clone()), body)?;
             let ty = type_of_function(annot.get_type()?, body.get_type()?)?;
@@ -580,7 +579,7 @@ pub(crate) fn type_with(
             };
 
             let val = type_with(env, &val)?;
-            let val_nf = val.normalize_nf(&env.as_nzenv());
+            let val_nf = val.eval(&env.as_nzenv());
             let body = type_with(&env.insert_value(&binder, val_nf), body)?;
             let body_ty = body.get_type().ok();
             (
-- 
cgit v1.2.3


From 653cdb44cec4f54697d18f2c4ae9f67bbbc2fb3d Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Thu, 30 Jan 2020 17:04:28 +0000
Subject: Move normalize under nze

---
 dhall/src/semantics/tck/tyexpr.rs    | 2 +-
 dhall/src/semantics/tck/typecheck.rs | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'dhall/src/semantics/tck')

diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index 0a27f32..98dc3f9 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -1,5 +1,5 @@
 use crate::error::{TypeError, TypeMessage};
-use crate::semantics::phase::normalize::normalize_tyexpr_whnf;
+use crate::semantics::normalize_tyexpr_whnf;
 use crate::semantics::phase::Normalized;
 use crate::semantics::phase::{NormalizedExpr, ToExprOptions};
 use crate::semantics::{rc, NameEnv, NzEnv, TyEnv, Value};
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index d741b40..348471f 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -3,7 +3,7 @@ use std::cmp::max;
 use std::collections::HashMap;
 
 use crate::error::{TypeError, TypeMessage};
-use crate::semantics::phase::normalize::merge_maps;
+use crate::semantics::merge_maps;
 use crate::semantics::phase::Normalized;
 use crate::semantics::{
     type_of_builtin, Binder, BuiltinClosure, Closure, TyEnv, TyExpr,
-- 
cgit v1.2.3


From 5197c26c23edd6c499f8e0f8a239fe4393b2e3d2 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Thu, 30 Jan 2020 17:09:16 +0000
Subject: Move main API to lib.rs

---
 dhall/src/semantics/tck/tyexpr.rs    | 4 ++--
 dhall/src/semantics/tck/typecheck.rs | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'dhall/src/semantics/tck')

diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index 98dc3f9..4b88048 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -1,9 +1,9 @@
 use crate::error::{TypeError, TypeMessage};
 use crate::semantics::normalize_tyexpr_whnf;
-use crate::semantics::phase::Normalized;
-use crate::semantics::phase::{NormalizedExpr, ToExprOptions};
 use crate::semantics::{rc, NameEnv, NzEnv, TyEnv, Value};
 use crate::syntax::{ExprKind, Span, V};
+use crate::Normalized;
+use crate::{NormalizedExpr, ToExprOptions};
 
 pub(crate) type Type = Value;
 
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 348471f..212e6e7 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -4,7 +4,6 @@ use std::collections::HashMap;
 
 use crate::error::{TypeError, TypeMessage};
 use crate::semantics::merge_maps;
-use crate::semantics::phase::Normalized;
 use crate::semantics::{
     type_of_builtin, Binder, BuiltinClosure, Closure, TyEnv, TyExpr,
     TyExprKind, Type, Value, ValueKind,
@@ -12,6 +11,7 @@ use crate::semantics::{
 use crate::syntax::{
     BinOp, Builtin, Const, Expr, ExprKind, InterpolatedTextContents, Span,
 };
+use crate::Normalized;
 
 fn type_of_recordtype<'a>(
     tys: impl Iterator<Item = Cow<'a, TyExpr>>,
-- 
cgit v1.2.3


From d8de45763037937b5c2dedbe5f7bb95a4e7bc7cd Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Thu, 30 Jan 2020 19:56:31 +0000
Subject: Avoid unnecessary allocations of `Value`s

---
 dhall/src/semantics/tck/env.rs    | 2 +-
 dhall/src/semantics/tck/tyexpr.rs | 5 +++--
 2 files changed, 4 insertions(+), 3 deletions(-)

(limited to 'dhall/src/semantics/tck')

diff --git a/dhall/src/semantics/tck/env.rs b/dhall/src/semantics/tck/env.rs
index d4cc37d..812ca7a 100644
--- a/dhall/src/semantics/tck/env.rs
+++ b/dhall/src/semantics/tck/env.rs
@@ -118,7 +118,7 @@ impl TyEnv {
     }
     pub fn lookup(&self, var: &V) -> Option<(TyExprKind, Type)> {
         let var = self.names.unlabel_var(var)?;
-        let ty = self.items.lookup_val(&var).get_type().unwrap();
+        let ty = self.items.lookup_ty(&var);
         Some((TyExprKind::Var(var), ty))
     }
 }
diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index 4b88048..1a048f9 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -1,5 +1,4 @@
 use crate::error::{TypeError, TypeMessage};
-use crate::semantics::normalize_tyexpr_whnf;
 use crate::semantics::{rc, NameEnv, NzEnv, TyEnv, Value};
 use crate::syntax::{ExprKind, Span, V};
 use crate::Normalized;
@@ -83,7 +82,9 @@ impl TyExpr {
     }
     /// Eval a closed TyExpr fully and recursively;
     pub fn rec_eval_closed_expr(&self) -> Value {
-        normalize_tyexpr_whnf(self, &NzEnv::new())
+        let mut val = self.eval_closed_expr();
+        val.normalize_mut();
+        val
     }
 }
 
-- 
cgit v1.2.3


From ace2a1f2783f770dc801f74e9118d39c73eb158a Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Thu, 30 Jan 2020 22:00:32 +0000
Subject: Get rid of all the manual Ref borrows

---
 dhall/src/semantics/tck/typecheck.rs | 54 +++++++++++++-----------------------
 1 file changed, 20 insertions(+), 34 deletions(-)

(limited to 'dhall/src/semantics/tck')

diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 212e6e7..e3f57c2 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -197,8 +197,7 @@ fn type_one_layer(
                 // TODO: branch here only when scrut.get_type() is a Const
                 _ => {
                     let scrut_nf = scrut.eval(env.as_nzenv());
-                    let scrut_nf_borrow = scrut_nf.kind();
-                    match &*scrut_nf_borrow {
+                    match scrut_nf.kind() {
                         ValueKind::UnionType(kts) => match kts.get(x) {
                             // Constructor has type T -> < x: T, ... >
                             Some(Some(ty)) => Value::from_kind_and_type(
@@ -215,7 +214,7 @@ fn type_one_layer(
                                     scrut.get_type()?,
                                 )?,
                             ),
-                            Some(None) => scrut_nf.clone(),
+                            Some(None) => scrut_nf,
                             None => return mkerr("MissingUnionField"),
                         },
                         _ => return mkerr("NotARecord"),
@@ -252,9 +251,7 @@ fn type_one_layer(
             t
         }
         ExprKind::App(f, arg) => {
-            let tf = f.get_type()?;
-            let tf_borrow = tf.kind();
-            match &*tf_borrow {
+            match f.get_type()?.kind() {
                 ValueKind::PiClosure { annot, closure, .. } => {
                     if arg.get_type()? != *annot {
                         // return mkerr(format!("function annot mismatch"));
@@ -295,15 +292,12 @@ fn type_one_layer(
             let y_type = y.get_type()?;
 
             // Extract the LHS record type
-            let x_type_borrow = x_type.kind();
-            let kts_x = match &*x_type_borrow {
+            let kts_x = match x_type.kind() {
                 ValueKind::RecordType(kts) => kts,
                 _ => return mkerr("MustCombineRecord"),
             };
-
             // Extract the RHS record type
-            let y_type_borrow = y_type.kind();
-            let kts_y = match &*y_type_borrow {
+            let kts_y = match y_type.kind() {
                 ValueKind::RecordType(kts) => kts,
                 _ => return mkerr("MustCombineRecord"),
             };
@@ -334,13 +328,11 @@ fn type_one_layer(
         ExprKind::BinOp(BinOp::RecursiveRecordTypeMerge, x, y) => {
             let x_val = x.eval(env.as_nzenv());
             let y_val = y.eval(env.as_nzenv());
-            let x_val_borrow = x_val.kind();
-            let y_val_borrow = y_val.kind();
-            let kts_x = match &*x_val_borrow {
+            let kts_x = match x_val.kind() {
                 ValueKind::RecordType(kts) => kts,
                 _ => return mkerr("RecordTypeMergeRequiresRecordType"),
             };
-            let kts_y = match &*y_val_borrow {
+            let kts_y = match y_val.kind() {
                 ValueKind::RecordType(kts) => kts,
                 _ => return mkerr("RecordTypeMergeRequiresRecordType"),
             };
@@ -416,15 +408,13 @@ fn type_one_layer(
         }
         ExprKind::Merge(record, union, type_annot) => {
             let record_type = record.get_type()?;
-            let record_borrow = record_type.kind();
-            let handlers = match &*record_borrow {
+            let handlers = match record_type.kind() {
                 ValueKind::RecordType(kts) => kts,
                 _ => return mkerr("Merge1ArgMustBeRecord"),
             };
 
             let union_type = union.get_type()?;
-            let union_borrow = union_type.kind();
-            let variants = match &*union_borrow {
+            let variants = match union_type.kind() {
                 ValueKind::UnionType(kts) => Cow::Borrowed(kts),
                 ValueKind::AppliedBuiltin(BuiltinClosure {
                     b: Builtin::Optional,
@@ -444,21 +434,18 @@ fn type_one_layer(
             for (x, handler_type) in handlers {
                 let handler_return_type = match variants.get(x) {
                     // Union alternative with type
-                    Some(Some(variant_type)) => {
-                        let handler_type_borrow = handler_type.kind();
-                        match &*handler_type_borrow {
-                            ValueKind::PiClosure { closure, annot, .. } => {
-                                if variant_type != annot {
-                                    return mkerr("MergeHandlerTypeMismatch");
-                                }
-
-                                closure.remove_binder().or_else(|()| {
-                                    mkerr("MergeReturnTypeIsDependent")
-                                })?
+                    Some(Some(variant_type)) => match handler_type.kind() {
+                        ValueKind::PiClosure { closure, annot, .. } => {
+                            if variant_type != annot {
+                                return mkerr("MergeHandlerTypeMismatch");
                             }
-                            _ => return mkerr("NotAFunction"),
+
+                            closure.remove_binder().or_else(|()| {
+                                mkerr("MergeReturnTypeIsDependent")
+                            })?
                         }
-                    }
+                        _ => return mkerr("NotAFunction"),
+                    },
                     // Union alternative without type
                     Some(None) => handler_type.clone(),
                     None => return mkerr("MergeHandlerMissingVariant"),
@@ -495,8 +482,7 @@ fn type_one_layer(
         ExprKind::ToMap(_, _) => unimplemented!("toMap"),
         ExprKind::Projection(record, labels) => {
             let record_type = record.get_type()?;
-            let record_type_borrow = record_type.kind();
-            let kts = match &*record_type_borrow {
+            let kts = match record_type.kind() {
                 ValueKind::RecordType(kts) => kts,
                 _ => return mkerr("ProjectionMustBeRecord"),
             };
-- 
cgit v1.2.3


From 70af1a47bce9e6c8282d6e53cf82aeda9aab10de Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Thu, 30 Jan 2020 22:08:57 +0000
Subject: Tweak ConstantClosure

---
 dhall/src/semantics/tck/typecheck.rs | 26 ++++++++++++++------------
 1 file changed, 14 insertions(+), 12 deletions(-)

(limited to 'dhall/src/semantics/tck')

diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index e3f57c2..20076cd 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -200,20 +200,22 @@ fn type_one_layer(
                     match scrut_nf.kind() {
                         ValueKind::UnionType(kts) => match kts.get(x) {
                             // Constructor has type T -> < x: T, ... >
-                            Some(Some(ty)) => Value::from_kind_and_type(
-                                ValueKind::PiClosure {
-                                    binder: Binder::new(x.clone()),
-                                    annot: ty.clone(),
-                                    closure: Closure::new_constant(
-                                        env.as_nzenv(),
-                                        scrut.clone(),
-                                    ),
-                                },
-                                type_of_function(
+                            Some(Some(ty)) => {
+                                let pi_ty = type_of_function(
                                     ty.get_type()?,
                                     scrut.get_type()?,
-                                )?,
-                            ),
+                                )?;
+                                Value::from_kind_and_type(
+                                    ValueKind::PiClosure {
+                                        binder: Binder::new(x.clone()),
+                                        annot: ty.clone(),
+                                        closure: Closure::new_constant(
+                                            scrut_nf,
+                                        ),
+                                    },
+                                    pi_ty,
+                                )
+                            }
                             Some(None) => scrut_nf,
                             None => return mkerr("MissingUnionField"),
                         },
-- 
cgit v1.2.3