diff options
author | Nadrieril | 2019-05-08 00:45:59 +0200 |
---|---|---|
committer | Nadrieril | 2019-05-08 00:45:59 +0200 |
commit | 03de1d323107916b57def2a39238da14ba23291b (patch) | |
tree | 98be43d74185f6b30a6a976b44e61b64046c1c51 | |
parent | 7680ff4d5ebe7b98cdc54bd0e90a8d22395f715f (diff) |
Fix Context shifting
Diffstat (limited to '')
-rw-r--r-- | dhall/src/core/context.rs | 39 |
1 files changed, 24 insertions, 15 deletions
diff --git a/dhall/src/core/context.rs b/dhall/src/core/context.rs index f07c638..0483c4d 100644 --- a/dhall/src/core/context.rs +++ b/dhall/src/core/context.rs @@ -62,27 +62,24 @@ impl<T> Context<T> { } None } - fn shift(&self, delta: isize, var: &AlphaVar) -> Self - where - T: Shift, - { - Context(Rc::new( - self.0 - .iter() - .map(|(l, i)| (l.clone(), i.shift(delta, var))) - .collect(), - )) - } - fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self + /// Given a var that makes sense in the current context, map the given function in such a way + /// that the passed variable always makes sense in the context of the passed item. + /// Once we pass the variable definition, the variable doesn't make sense anymore so we just + /// copy the remaining items. + fn do_with_var( + &self, + var: &AlphaVar, + mut f: impl FnMut(&AlphaVar, &CtxItem<T>) -> CtxItem<T>, + ) -> Self where - T: Clone + Subst<Typed>, + T: Clone, { let mut vec = Vec::new(); vec.reserve(self.0.len()); let mut var = var.clone(); let mut iter = self.0.iter().rev(); for (l, i) in iter.by_ref() { - vec.push((l.clone(), i.subst_shift(&var, val))); + vec.push((l.clone(), f(&var, i))); if let CtxItem::Kept(_, _) = i { if var == l.into() { break; @@ -97,6 +94,18 @@ impl<T> Context<T> { vec.reverse(); Context(Rc::new(vec)) } + fn shift(&self, delta: isize, var: &AlphaVar) -> Self + where + T: Clone + Shift, + { + self.do_with_var(var, |var, i| i.shift(delta, &var)) + } + fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self + where + T: Clone + Subst<Typed>, + { + self.do_with_var(var, |var, i| i.subst_shift(&var, val)) + } } impl NormalizationContext { @@ -161,7 +170,7 @@ impl<T: Shift> Shift for CtxItem<T> { } } -impl<T: Shift> Shift for Context<T> { +impl<T: Clone + Shift> Shift for Context<T> { fn shift(&self, delta: isize, var: &AlphaVar) -> Self { self.shift(delta, var) } |