From cc0c6cc420ca8019665e745797758c997cc35358 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 16 Aug 2019 22:33:16 +0200 Subject: Use generic Shift/Subst impls --- dhall/src/core/var.rs | 175 +++++++++++++++++++++++++++++++++++++++----------- 1 file changed, 138 insertions(+), 37 deletions(-) (limited to 'dhall/src/core/var.rs') 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 { - Some(()) - } -} - -impl Shift for Option { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option { - Some(match self { - None => None, - Some(x) => Some(x.shift(delta, var)?), - }) - } -} - -impl Shift for Box { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option { - Some(Box::new(self.as_ref().shift(delta, var)?)) - } -} - -impl Subst for () { - fn subst_shift(&self, _var: &AlphaVar, _val: &S) -> Self {} -} - -impl> Subst for Option { - fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self { - self.as_ref().map(|x| x.subst_shift(var, val)) - } -} - -impl> Subst for Box { - 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 for Label { x.0 } } +impl Shift for () { + fn shift(&self, _delta: isize, _var: &AlphaVar) -> Option { + Some(()) + } +} + +impl Shift for Option { + fn shift(&self, delta: isize, var: &AlphaVar) -> Option { + Some(match self { + None => None, + Some(x) => Some(x.shift(delta, var)?), + }) + } +} + +impl Shift for Box { + fn shift(&self, delta: isize, var: &AlphaVar) -> Option { + Some(Box::new(self.as_ref().shift(delta, var)?)) + } +} + +impl Shift for std::rc::Rc { + fn shift(&self, delta: isize, var: &AlphaVar) -> Option { + Some(std::rc::Rc::new(self.as_ref().shift(delta, var)?)) + } +} + +impl Shift for std::cell::RefCell { + fn shift(&self, delta: isize, var: &AlphaVar) -> Option { + Some(std::cell::RefCell::new(self.borrow().shift(delta, var)?)) + } +} + +impl Shift for dhall_syntax::ExprF { + fn shift(&self, delta: isize, var: &AlphaVar) -> Option { + 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 Shift for Vec { + fn shift(&self, delta: isize, var: &AlphaVar) -> Option { + Some( + self.iter() + .map(|v| Ok(v.shift(delta, var)?)) + .collect::>()?, + ) + } +} + +impl Shift for HashMap +where + K: Clone + std::hash::Hash + Eq, +{ + fn shift(&self, delta: isize, var: &AlphaVar) -> Option { + Some( + self.iter() + .map(|(k, v)| Ok((k.clone(), v.shift(delta, var)?))) + .collect::>()?, + ) + } +} + +impl Shift for dhall_syntax::InterpolatedTextContents { + fn shift(&self, delta: isize, var: &AlphaVar) -> Option { + use dhall_syntax::InterpolatedTextContents::{Expr, Text}; + Some(match self { + Expr(x) => Expr(x.shift(delta, var)?), + Text(s) => Text(s.clone()), + }) + } +} + +impl Subst for () { + fn subst_shift(&self, _var: &AlphaVar, _val: &S) -> Self {} +} + +impl> Subst for Option { + fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self { + self.as_ref().map(|x| x.subst_shift(var, val)) + } +} + +impl> Subst for Box { + fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self { + Box::new(self.as_ref().subst_shift(var, val)) + } +} + +impl> Subst for std::rc::Rc { + fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self { + std::rc::Rc::new(self.as_ref().subst_shift(var, val)) + } +} + +impl> Subst for std::cell::RefCell { + fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self { + std::cell::RefCell::new(self.borrow().subst_shift(var, val)) + } +} + +impl, E: Clone> Subst for dhall_syntax::ExprF { + 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> Subst for Vec { + fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self { + self.iter().map(|v| v.subst_shift(var, val)).collect() + } +} + +impl> Subst for dhall_syntax::InterpolatedTextContents { + 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> Subst for HashMap +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() + } +} -- cgit v1.2.3