Reimplement basic tck/nze with proper environments

Inspired from dhall_haskell

1 files changed, 9 insertions, 7 deletions

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) => {