summaryrefslogtreecommitdiff
path: root/dhall/src/semantics/core/var.rs
diff options
context:
space:
mode:
authorNadrieril2020-01-17 11:03:40 +0000
committerNadrieril2020-01-17 11:18:57 +0000
commit72d1e3c339cf550fa5af9981af6078a813feb80a (patch)
treeb6dc162bf0af9ce8e2cd7dbe0443b302ef071f0e /dhall/src/semantics/core/var.rs
parentf7a8d967b02bc20c093d501746ed3de53cc7da13 (diff)
Remove Shift/Subst traits
Diffstat (limited to '')
-rw-r--r--dhall/src/semantics/core/var.rs63
1 files changed, 14 insertions, 49 deletions
diff --git a/dhall/src/semantics/core/var.rs b/dhall/src/semantics/core/var.rs
index c21e53e..a110632 100644
--- a/dhall/src/semantics/core/var.rs
+++ b/dhall/src/semantics/core/var.rs
@@ -1,5 +1,3 @@
-use std::collections::HashMap;
-
use crate::syntax::{Label, V};
/// Stores a pair of variables: a normal one and one
@@ -18,44 +16,6 @@ pub struct Binder {
name: Label,
}
-pub(crate) trait Shift: Sized {
- // Shift an expression to move it around binders without changing the meaning of its free
- // variables. Shift by 1 to move an expression under a binder. Shift by -1 to extract an
- // expression from under a binder, if the expression does not refer to that bound variable.
- // Returns None if delta was negative and the variable was free in the expression.
- fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self>;
-
- fn over_binder<T>(&self, x: T) -> Option<Self>
- where
- T: Into<AlphaVar>,
- {
- self.shift(-1, &x.into())
- }
-
- fn under_binder<T>(&self, x: T) -> Self
- where
- T: Into<AlphaVar>,
- {
- // Can't fail since delta is positive
- self.shift(1, &x.into()).unwrap()
- }
-
- fn under_multiple_binders(&self, shift_map: &HashMap<Label, usize>) -> Self
- where
- Self: Clone,
- {
- let mut v = self.clone();
- for (x, n) in shift_map {
- v = v.shift(*n as isize, &x.into()).unwrap();
- }
- v
- }
-}
-
-pub(crate) trait Subst<S> {
- fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self;
-}
-
impl AlphaVar {
pub(crate) fn to_var_maybe_alpha(&self, alpha: bool) -> V<Label> {
if alpha {
@@ -64,6 +24,20 @@ impl AlphaVar {
self.normal.clone()
}
}
+
+ 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)?,
+ })
+ }
+ pub(crate) fn under_binder<T>(&self, x: T) -> Self
+ where
+ T: Into<AlphaVar>,
+ {
+ // Can't fail since delta is positive
+ self.shift(1, &x.into()).unwrap()
+ }
}
impl Binder {
@@ -82,15 +56,6 @@ impl Binder {
}
}
-impl Shift for AlphaVar {
- 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)?,
- })
- }
-}
-
/// Equality up to alpha-equivalence
impl std::cmp::PartialEq for AlphaVar {
fn eq(&self, other: &Self) -> bool {