summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--dhall/src/semantics/core/context.rs33
-rw-r--r--dhall/src/semantics/core/value.rs26
-rw-r--r--dhall/src/semantics/core/var.rs16
3 files changed, 42 insertions, 33 deletions
diff --git a/dhall/src/semantics/core/context.rs b/dhall/src/semantics/core/context.rs
index 16ea48f..a6ab79e 100644
--- a/dhall/src/semantics/core/context.rs
+++ b/dhall/src/semantics/core/context.rs
@@ -17,27 +17,6 @@ pub(crate) struct TyCtx {
ctx: Vec<(Binder, CtxItem)>,
}
-impl CtxItem {
- fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
- Some(match self {
- CtxItem::Kept(v, t) => {
- CtxItem::Kept(v.shift(delta, var)?, t.shift(delta, var)?)
- }
- CtxItem::Replaced(e) => CtxItem::Replaced(e.shift(delta, var)?),
- })
- }
- 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 {
- v = v.shift(*n as isize, &x.into()).unwrap();
- }
- v
- }
-}
-
impl TyCtx {
pub fn new() -> Self {
TyCtx { ctx: Vec::new() }
@@ -66,12 +45,16 @@ impl TyCtx {
let l = b.to_label();
match var.over_binder(&l) {
None => {
- let i = i.under_multiple_binders(&shift_map);
return Some(match i {
- CtxItem::Kept(newvar, t) => {
- Value::from_kind_and_type(ValueKind::Var(newvar), t)
+ CtxItem::Kept(newvar, t) => Value::from_kind_and_type(
+ ValueKind::Var(
+ newvar.under_multiple_binders(&shift_map),
+ ),
+ t.under_multiple_binders(&shift_map),
+ ),
+ CtxItem::Replaced(v) => {
+ v.under_multiple_binders(&shift_map)
}
- CtxItem::Replaced(v) => v,
});
}
Some(newvar) => var = newvar,
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()),
diff --git a/dhall/src/semantics/core/var.rs b/dhall/src/semantics/core/var.rs
index a110632..7c2c4de 100644
--- a/dhall/src/semantics/core/var.rs
+++ b/dhall/src/semantics/core/var.rs
@@ -1,3 +1,5 @@
+use std::collections::HashMap;
+
use crate::syntax::{Label, V};
/// Stores a pair of variables: a normal one and one
@@ -38,6 +40,20 @@ impl AlphaVar {
// 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
+ }
}
impl Binder {