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