diff options
author | Nadrieril | 2020-01-20 15:27:19 +0000 |
---|---|---|
committer | Nadrieril | 2020-01-20 15:27:19 +0000 |
commit | c448698f797f2304dca0e0b8b833959de00ca079 (patch) | |
tree | f5a292aa4aa53f95b1b058a65df48b201ee969d3 /dhall/src/semantics/tck | |
parent | aec80599f161096b68cac88ffb8852a61b62fcfa (diff) |
Reimplement basic tck/nze with proper environments
Inspired from dhall_haskell
Diffstat (limited to 'dhall/src/semantics/tck')
-rw-r--r-- | dhall/src/semantics/tck/tyexpr.rs | 16 |
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) => { |