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, ty: Option, span: Span, } +#[derive(Debug, Clone)] pub(crate) enum TyExprKind { Var(AlphaVar), - // Forbidden ExprKind variants: Var + // Forbidden ExprKind variants: Var, Import, Embed Expr(ExprKind), } @@ -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