diff options
Diffstat (limited to '')
-rw-r--r-- | dhall/src/core/var.rs | 175 |
1 files changed, 138 insertions, 37 deletions
diff --git a/dhall/src/core/var.rs b/dhall/src/core/var.rs index 3af12ec..8d02171 100644 --- a/dhall/src/core/var.rs +++ b/dhall/src/core/var.rs @@ -92,43 +92,6 @@ impl Shift for AlphaVar { } } -impl Shift for () { - fn shift(&self, _delta: isize, _var: &AlphaVar) -> Option<Self> { - Some(()) - } -} - -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 impl std::cmp::PartialEq for AlphaVar { fn eq(&self, other: &Self) -> bool { @@ -188,3 +151,141 @@ impl From<AlphaLabel> for Label { x.0 } } +impl Shift for () { + fn shift(&self, _delta: isize, _var: &AlphaVar) -> Option<Self> { + Some(()) + } +} + +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<T: Shift> Shift for std::rc::Rc<T> { + fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { + Some(std::rc::Rc::new(self.as_ref().shift(delta, var)?)) + } +} + +impl<T: Shift> Shift for std::cell::RefCell<T> { + fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { + Some(std::cell::RefCell::new(self.borrow().shift(delta, var)?)) + } +} + +impl<T: Shift, E: Clone> Shift for dhall_syntax::ExprF<T, E> { + fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { + Some(self.traverse_ref_with_special_handling_of_binders( + |v| Ok(v.shift(delta, var)?), + |x, v| Ok(v.shift(delta, &var.under_binder(x))?), + )?) + } +} + +impl<T: Shift> Shift for Vec<T> { + fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { + Some( + self.iter() + .map(|v| Ok(v.shift(delta, var)?)) + .collect::<Result<_, _>>()?, + ) + } +} + +impl<K, T: Shift> Shift for HashMap<K, T> +where + K: Clone + std::hash::Hash + Eq, +{ + fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { + Some( + self.iter() + .map(|(k, v)| Ok((k.clone(), v.shift(delta, var)?))) + .collect::<Result<_, _>>()?, + ) + } +} + +impl<T: Shift> Shift for dhall_syntax::InterpolatedTextContents<T> { + fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { + use dhall_syntax::InterpolatedTextContents::{Expr, Text}; + Some(match self { + Expr(x) => Expr(x.shift(delta, var)?), + Text(s) => Text(s.clone()), + }) + } +} + +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)) + } +} + +impl<S, T: Subst<S>> Subst<S> for std::rc::Rc<T> { + fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self { + std::rc::Rc::new(self.as_ref().subst_shift(var, val)) + } +} + +impl<S, T: Subst<S>> Subst<S> for std::cell::RefCell<T> { + fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self { + std::cell::RefCell::new(self.borrow().subst_shift(var, val)) + } +} + +impl<S: Shift, T: Subst<S>, E: Clone> Subst<S> for dhall_syntax::ExprF<T, E> { + fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self { + self.map_ref_with_special_handling_of_binders( + |v| v.subst_shift(var, val), + |x, v| v.subst_shift(&var.under_binder(x), &val.under_binder(x)), + ) + } +} + +impl<S, T: Subst<S>> Subst<S> for Vec<T> { + fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self { + self.iter().map(|v| v.subst_shift(var, val)).collect() + } +} + +impl<S, T: Subst<S>> Subst<S> for dhall_syntax::InterpolatedTextContents<T> { + fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self { + use dhall_syntax::InterpolatedTextContents::{Expr, Text}; + match self { + Expr(x) => Expr(x.subst_shift(var, val)), + Text(s) => Text(s.clone()), + } + } +} + +impl<S, K, T: Subst<S>> Subst<S> for HashMap<K, T> +where + K: Clone + std::hash::Hash + Eq, +{ + fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self { + self.iter() + .map(|(k, v)| (k.clone(), v.subst_shift(var, val))) + .collect() + } +} |