summaryrefslogtreecommitdiff
path: root/dhall/src/core/var.rs
diff options
context:
space:
mode:
authorNadrieril2019-08-16 21:59:11 +0200
committerNadrieril2019-08-16 21:59:58 +0200
commit961dbc0e9d52691de590568c01a22d28c04fe2f5 (patch)
treeedf1cdcfa39eec402bf15b8aeb52f8e739fb95dd /dhall/src/core/var.rs
parent9383d55718b86faf4c1734fe8fee3f99730499d4 (diff)
Store type in Thunk
Diffstat (limited to '')
-rw-r--r--dhall/src/core/var.rs35
1 files changed, 31 insertions, 4 deletions
diff --git a/dhall/src/core/var.rs b/dhall/src/core/var.rs
index 296e968..3af12ec 100644
--- a/dhall/src/core/var.rs
+++ b/dhall/src/core/var.rs
@@ -50,8 +50,8 @@ pub(crate) trait Shift: Sized {
}
}
-pub(crate) trait Subst<T> {
- fn subst_shift(&self, var: &AlphaVar, val: &T) -> Self;
+pub(crate) trait Subst<S> {
+ fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self;
}
impl AlphaVar {
@@ -98,8 +98,35 @@ impl Shift for () {
}
}
-impl<T> Subst<T> for () {
- fn subst_shift(&self, _var: &AlphaVar, _val: &T) -> Self {}
+impl<T: Shift> Shift for Option<T> {
+ fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
+ Some(match self {
+ None => None,
+ Some(x) => Some(x.shift(delta, var)?),
+ })
+ }
+}
+
+impl<T: Shift> Shift for Box<T> {
+ fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
+ Some(Box::new(self.as_ref().shift(delta, var)?))
+ }
+}
+
+impl<S> Subst<S> for () {
+ fn subst_shift(&self, _var: &AlphaVar, _val: &S) -> Self {}
+}
+
+impl<S, T: Subst<S>> Subst<S> for Option<T> {
+ fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self {
+ self.as_ref().map(|x| x.subst_shift(var, val))
+ }
+}
+
+impl<S, T: Subst<S>> Subst<S> for Box<T> {
+ fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self {
+ Box::new(self.as_ref().subst_shift(var, val))
+ }
}
/// Equality up to alpha-equivalence