diff options
Diffstat (limited to '')
-rw-r--r-- | dhall/src/semantics/core/context.rs | 12 | ||||
-rw-r--r-- | dhall/src/semantics/core/value.rs | 26 | ||||
-rw-r--r-- | dhall/src/semantics/core/var.rs | 21 |
3 files changed, 19 insertions, 40 deletions
diff --git a/dhall/src/semantics/core/context.rs b/dhall/src/semantics/core/context.rs index 47d2d2d..8c64c26 100644 --- a/dhall/src/semantics/core/context.rs +++ b/dhall/src/semantics/core/context.rs @@ -6,7 +6,9 @@ use crate::syntax::{Label, V}; #[derive(Debug, Clone)] enum CtxItem { - Kept(AlphaVar, Value), + // Variable is bound with given type + Kept(Value), + // Variable has been replaced by corresponding value Replaced(Value), } @@ -24,7 +26,7 @@ impl TyCtx { } pub fn insert_type(&self, x: &Binder, t: Value) -> Self { let mut vec = self.ctx.clone(); - vec.push((x.clone(), CtxItem::Kept(x.into(), t.under_binder(x)))); + vec.push((x.clone(), CtxItem::Kept(t.under_binder()))); self.with_vec(vec) } pub fn insert_value( @@ -47,7 +49,7 @@ impl TyCtx { Some(newvar) => newvar, None => break item, }; - if let CtxItem::Kept(_, _) = item { + if let CtxItem::Kept(_) = item { shift_delta += 1; } } else { @@ -57,8 +59,8 @@ impl TyCtx { }; let v = match found_item { - CtxItem::Kept(newvar, t) => Value::from_kind_and_type( - ValueKind::Var(newvar.clone()), + CtxItem::Kept(t) => Value::from_kind_and_type( + ValueKind::Var(AlphaVar::default()), t.clone(), ), CtxItem::Replaced(v) => v.clone(), diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs index 6ae0a90..8b3ada1 100644 --- a/dhall/src/semantics/core/value.rs +++ b/dhall/src/semantics/core/value.rs @@ -209,9 +209,9 @@ impl Value { pub(crate) fn app(&self, v: Value) -> Value { let body_t = match &*self.get_type_not_sort().as_whnf() { - ValueKind::Pi(x, t, e) => { + ValueKind::Pi(_, t, e) => { v.check_type(t); - e.subst_shift(&x.into(), &v) + e.subst_shift(&AlphaVar::default(), &v) } _ => unreachable!("Internal type error"), }; @@ -242,18 +242,12 @@ impl Value { pub(crate) fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { Some(self.as_internal().shift(delta, var)?.into_value()) } - pub(crate) fn over_binder<T>(&self, x: T) -> Option<Self> - where - T: Into<AlphaVar>, - { - self.shift(-1, &x.into()) + pub(crate) fn over_binder(&self) -> Option<Self> { + self.shift(-1, &AlphaVar::default()) } - pub(crate) fn under_binder<T>(&self, x: T) -> Self - where - T: Into<AlphaVar>, - { + pub(crate) fn under_binder(&self) -> Self { // Can't fail since delta is positive - self.shift(1, &x.into()).unwrap() + self.shift(1, &AlphaVar::default()).unwrap() } pub(crate) fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { match &*self.as_kind() { @@ -456,18 +450,18 @@ impl ValueKind<Value> { ValueKind::Var(v) => ValueKind::Var(v.shift(delta, var)?), _ => self.traverse_ref_with_special_handling_of_binders( |x| Ok(x.shift(delta, var)?), - |b, _, x| Ok(x.shift(delta, &var.under_binder(b))?), + |_, _, x| Ok(x.shift(delta, &var.under_binder())?), )?, }) } fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { match self { ValueKind::Var(v) if v == var => val.to_whnf_ignore_type(), - ValueKind::Var(v) => ValueKind::Var(v.over_binder(var).unwrap()), + ValueKind::Var(v) => ValueKind::Var(v.shift(-1, var).unwrap()), _ => self.map_ref_with_special_handling_of_binders( |x| x.subst_shift(var, val), - |b, _, x| { - x.subst_shift(&var.under_binder(b), &val.under_binder(b)) + |_, _, x| { + x.subst_shift(&var.under_binder(), &val.under_binder()) }, ), } diff --git a/dhall/src/semantics/core/var.rs b/dhall/src/semantics/core/var.rs index 93776bf..b336c66 100644 --- a/dhall/src/semantics/core/var.rs +++ b/dhall/src/semantics/core/var.rs @@ -26,15 +26,9 @@ impl AlphaVar { alpha: self.alpha.shift(delta, &var.alpha)?, }) } - pub(crate) fn under_binder<T>(&self, x: T) -> Self - where - T: Into<AlphaVar>, - { + pub(crate) fn under_binder(&self) -> Self { // Can't fail since delta is positive - self.shift(1, &x.into()).unwrap() - } - pub(crate) fn over_binder(&self, x: &AlphaVar) -> Option<Self> { - self.shift(-1, x) + self.shift(1, &AlphaVar::default()).unwrap() } } @@ -82,17 +76,6 @@ impl std::fmt::Debug for Binder { } } -impl From<Binder> for AlphaVar { - fn from(x: Binder) -> AlphaVar { - AlphaVar { alpha: V((), 0) } - } -} -impl<'a> From<&'a Binder> for AlphaVar { - fn from(x: &'a Binder) -> AlphaVar { - AlphaVar { alpha: V((), 0) } - } -} - impl From<Binder> for Label { fn from(x: Binder) -> Label { x.name |