summaryrefslogtreecommitdiff
path: root/dhall/src
diff options
context:
space:
mode:
authorNadrieril2020-01-29 21:29:53 +0000
committerNadrieril2020-01-29 21:29:53 +0000
commit26d4975a4c94c2b9fd0c075ad94c2588e3cf24e8 (patch)
treebca94cbb8f2b9ca8f92f0d2dd97aae5a05c5019f /dhall/src
parentdb6c09f33c3c794e4b6ec8a7aa80978d945a9d7a (diff)
Use NameEnv in tyexpr_to_expr
Diffstat (limited to 'dhall/src')
-rw-r--r--dhall/src/semantics/nze/nzexpr.rs31
-rw-r--r--dhall/src/semantics/tck/tyexpr.rs27
2 files changed, 23 insertions, 35 deletions
diff --git a/dhall/src/semantics/nze/nzexpr.rs b/dhall/src/semantics/nze/nzexpr.rs
index 043840e..7263cac 100644
--- a/dhall/src/semantics/nze/nzexpr.rs
+++ b/dhall/src/semantics/nze/nzexpr.rs
@@ -35,9 +35,6 @@ impl NameEnv {
size: self.names.len(),
}
}
- pub fn names(&self) -> &[Binder] {
- &self.names
- }
pub fn insert(&self, x: &Binder) -> Self {
let mut env = self.clone();
@@ -47,9 +44,9 @@ impl NameEnv {
pub fn insert_mut(&mut self, x: &Binder) {
self.names.push(x.clone())
}
- // pub fn remove_mut(&mut self) {
- // self.names.pop();
- // }
+ pub fn remove_mut(&mut self) {
+ self.names.pop();
+ }
pub fn unlabel_var(&self, var: &V<Binder>) -> Option<AlphaVar> {
let V(name, idx) = var;
@@ -62,17 +59,17 @@ impl NameEnv {
.nth(*idx)?;
Some(AlphaVar::new(V((), idx)))
}
- // pub fn label_var(&self, var: &AlphaVar) -> V<Binder> {
- // 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)
- // }
+ pub fn label_var(&self, var: &AlphaVar) -> V<Binder> {
+ 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)
+ }
}
// TODO: rename to VarEnv
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
});