summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
authorNadrieril2020-01-17 18:31:45 +0000
committerNadrieril2020-01-17 18:31:45 +0000
commitab672506fd45e33f60b1b962c4757f912b6e27be (patch)
tree808846987354d14fa7f4b37317c9d7a930bd5777 /dhall
parent3881d36335fca6d72b0dd447130d6c1ce7ccbfee (diff)
Use alpha variables everywhere
Don't bother keeping name around, it complicates matters
Diffstat (limited to 'dhall')
-rw-r--r--dhall/src/semantics/core/value.rs2
-rw-r--r--dhall/src/semantics/core/var.rs30
-rw-r--r--dhall/src/semantics/to_expr.rs29
3 files changed, 34 insertions, 27 deletions
diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs
index 5aa337d..d843a1b 100644
--- a/dhall/src/semantics/core/value.rs
+++ b/dhall/src/semantics/core/value.rs
@@ -163,7 +163,7 @@ impl Value {
&self,
opts: to_expr::ToExprOptions,
) -> NormalizedExpr {
- to_expr::value_to_expr(self, opts)
+ to_expr::value_to_expr(self, opts, &vec![])
}
pub(crate) fn to_whnf_ignore_type(&self) -> ValueKind<Value> {
self.as_whnf().clone()
diff --git a/dhall/src/semantics/core/var.rs b/dhall/src/semantics/core/var.rs
index d7666e3..f3475e7 100644
--- a/dhall/src/semantics/core/var.rs
+++ b/dhall/src/semantics/core/var.rs
@@ -2,12 +2,9 @@ use std::collections::HashMap;
use crate::syntax::{Label, V};
-/// Stores a pair of variables: a normal one and one
-/// that corresponds to the alpha-normalized version of the first one.
-/// Equality is up to alpha-equivalence (compares on the second one only).
+/// Stores an alpha-normalized variable.
#[derive(Clone, Eq)]
pub struct AlphaVar {
- normal: V<Label>,
alpha: V<()>,
}
@@ -19,17 +16,12 @@ pub struct Binder {
}
impl AlphaVar {
- pub(crate) fn to_var_maybe_alpha(&self, alpha: bool) -> V<Label> {
- if alpha {
- V("_".into(), self.alpha.idx())
- } else {
- self.normal.clone()
- }
+ pub(crate) fn idx(&self) -> usize {
+ self.alpha.idx()
}
pub(crate) fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
Some(AlphaVar {
- normal: self.normal.shift(delta, &var.normal)?,
alpha: self.alpha.shift(delta, &var.alpha)?,
})
}
@@ -48,7 +40,6 @@ impl AlphaVar {
shift_map: &HashMap<Label, usize>,
) -> Self {
AlphaVar {
- normal: self.normal.under_multiple_binders(shift_map),
alpha: self.alpha.under_multiple_binders(shift_map),
}
}
@@ -68,6 +59,9 @@ impl Binder {
pub(crate) fn to_label(&self) -> Label {
self.clone().into()
}
+ pub(crate) fn name(&self) -> &Label {
+ &self.name
+ }
}
/// Equality up to alpha-equivalence
@@ -85,7 +79,7 @@ impl std::cmp::PartialEq for Binder {
impl std::fmt::Debug for AlphaVar {
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
- write!(f, "AlphaVar({}, {})", self.normal, self.alpha.1)
+ write!(f, "AlphaVar({})", self.alpha.1)
}
}
@@ -97,18 +91,12 @@ impl std::fmt::Debug for Binder {
impl<'a> From<&'a Label> for AlphaVar {
fn from(x: &'a Label) -> AlphaVar {
- AlphaVar {
- normal: V(x.clone(), 0),
- alpha: V((), 0),
- }
+ AlphaVar { alpha: V((), 0) }
}
}
impl From<Binder> for AlphaVar {
fn from(x: Binder) -> AlphaVar {
- AlphaVar {
- normal: V(x.into(), 0),
- alpha: V((), 0),
- }
+ AlphaVar { alpha: V((), 0) }
}
}
impl<'a> From<&'a Binder> for AlphaVar {
diff --git a/dhall/src/semantics/to_expr.rs b/dhall/src/semantics/to_expr.rs
index 1adfd49..612f794 100644
--- a/dhall/src/semantics/to_expr.rs
+++ b/dhall/src/semantics/to_expr.rs
@@ -1,8 +1,9 @@
+use crate::semantics::core::var::Binder;
use crate::semantics::phase::typecheck::rc;
use crate::semantics::phase::NormalizedExpr;
use crate::semantics::{Value, ValueKind};
use crate::syntax;
-use crate::syntax::{Builtin, ExprKind};
+use crate::syntax::{Builtin, ExprKind, V};
/// Controls conversion from `Value` to `Expr`
#[derive(Copy, Clone)]
@@ -14,19 +15,37 @@ pub(crate) struct ToExprOptions {
}
/// Converts a value back to the corresponding AST expression.
-pub(crate) fn value_to_expr(
- val: &Value,
+pub(crate) fn value_to_expr<'a>(
+ val: &'a Value,
opts: ToExprOptions,
+ ctx: &Vec<&'a Binder>,
) -> NormalizedExpr {
if opts.normalize {
val.normalize_whnf();
}
let kind = val.as_kind();
- let kind = kind.map_ref(|v| value_to_expr(v, opts));
+ let kind = kind.map_ref_with_special_handling_of_binders(
+ |v| value_to_expr(v, opts, ctx),
+ |b, _, v| {
+ let mut ctx = ctx.clone();
+ ctx.push(b);
+ value_to_expr(v, opts, &ctx)
+ },
+ );
match kind {
+ ValueKind::Var(v) if opts.alpha => {
+ rc(ExprKind::Var(V("_".into(), v.idx())))
+ }
ValueKind::Var(v) => {
- rc(ExprKind::Var(v.to_var_maybe_alpha(opts.alpha)))
+ let name = ctx[ctx.len() - 1 - v.idx()].to_label();
+ let mut idx = 0;
+ for b in ctx.iter().rev().take(v.idx()) {
+ if b.name() == &name {
+ idx += 1;
+ }
+ }
+ rc(ExprKind::Var(V(name, idx)))
}
ValueKind::Lam(x, t, e) => {
rc(ExprKind::Lam(x.to_label_maybe_alpha(opts.alpha), t, e))