diff options
Diffstat (limited to 'dhall/src/semantics/core/value.rs')
-rw-r--r-- | dhall/src/semantics/core/value.rs | 26 |
1 files changed, 18 insertions, 8 deletions
diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs index ad03187..049c2a9 100644 --- a/dhall/src/semantics/core/value.rs +++ b/dhall/src/semantics/core/value.rs @@ -240,9 +240,7 @@ impl Value { } pub(crate) fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { - Some(Value(Rc::new(RefCell::new( - self.0.borrow().shift(delta, var)?, - )))) + Some(self.0.borrow().shift(delta, var)?.into_value()) } pub(crate) fn over_binder<T>(&self, x: T) -> Option<Self> where @@ -257,6 +255,20 @@ impl Value { // Can't fail since delta is positive self.shift(1, &x.into()).unwrap() } + pub(crate) 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 { + // Can't fail since delta is positive + v = v.shift(*n as isize, &x.into()).unwrap(); + } + v + } pub(crate) fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { match &*self.as_kind() { // If the var matches, we can just reuse the provided value instead of copying it. @@ -267,9 +279,7 @@ impl Value { } val.clone() } - _ => Value(Rc::new(RefCell::new( - self.0.borrow().subst_shift(var, val), - ))), + _ => self.0.borrow().subst_shift(var, val).into_value(), } } } @@ -434,7 +444,7 @@ impl ValueKind<Value> { ValueKind::AppliedBuiltin(b, vec![]) } - pub(crate) fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { + fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { Some(match self { ValueKind::Var(v) => ValueKind::Var(v.shift(delta, var)?), _ => self.traverse_ref_with_special_handling_of_binders( @@ -443,7 +453,7 @@ impl ValueKind<Value> { )?, }) } - pub(crate) fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { + fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { match self { ValueKind::Var(v) if v == var => val.to_whnf_ignore_type(), ValueKind::Var(v) => ValueKind::Var(v.shift(-1, var).unwrap()), |