summaryrefslogtreecommitdiff
path: root/dhall/src/core/thunk.rs
diff options
context:
space:
mode:
authorNadrieril2019-05-09 16:32:30 +0200
committerNadrieril2019-05-09 16:32:30 +0200
commit7538e29275720407ac172bb05cdbc028d95ff921 (patch)
tree79ad968a7ef6e36e5a4e7fc19df281c46ac68f6c /dhall/src/core/thunk.rs
parent2020d41874f7681ba948a40d8e8f8993d651a81c (diff)
Make shift fallible and improve shift ergonomics
Diffstat (limited to 'dhall/src/core/thunk.rs')
-rw-r--r--dhall/src/core/thunk.rs40
1 files changed, 20 insertions, 20 deletions
diff --git a/dhall/src/core/thunk.rs b/dhall/src/core/thunk.rs
index a02d7ae..51922e1 100644
--- a/dhall/src/core/thunk.rs
+++ b/dhall/src/core/thunk.rs
@@ -264,38 +264,38 @@ impl TypeThunk {
}
impl Shift for Thunk {
- fn shift(&self, delta: isize, var: &AlphaVar) -> Self {
- self.0.borrow().shift(delta, var).into_thunk()
+ fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
+ Some(self.0.borrow().shift(delta, var)?.into_thunk())
}
}
impl Shift for ThunkInternal {
- fn shift(&self, delta: isize, var: &AlphaVar) -> Self {
- match self {
+ fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
+ Some(match self {
ThunkInternal::Unnormalized(ctx, e) => {
- ThunkInternal::Unnormalized(ctx.shift(delta, var), e.clone())
+ ThunkInternal::Unnormalized(ctx.shift(delta, var)?, e.clone())
}
ThunkInternal::PartialExpr(e) => ThunkInternal::PartialExpr(
- e.map_ref_with_special_handling_of_binders(
- |v| v.shift(delta, var),
- |x, v| v.shift(delta, &var.shift(1, &x.into())),
- X::clone,
- Label::clone,
- ),
+ e.traverse_ref_with_special_handling_of_binders(
+ |v| Ok(v.shift(delta, var)?),
+ |x, v| Ok(v.shift(delta, &var.under_binder(x))?),
+ |x| Ok(X::clone(x)),
+ |l| Ok(Label::clone(l)),
+ )?,
),
ThunkInternal::Value(m, v) => {
- ThunkInternal::Value(*m, v.shift(delta, var))
+ ThunkInternal::Value(*m, v.shift(delta, var)?)
}
- }
+ })
}
}
impl Shift for TypeThunk {
- fn shift(&self, delta: isize, var: &AlphaVar) -> Self {
- match self {
- TypeThunk::Thunk(th) => TypeThunk::Thunk(th.shift(delta, var)),
- TypeThunk::Type(t) => TypeThunk::Type(t.shift(delta, var)),
- }
+ fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
+ Some(match self {
+ TypeThunk::Thunk(th) => TypeThunk::Thunk(th.shift(delta, var)?),
+ TypeThunk::Type(t) => TypeThunk::Type(t.shift(delta, var)?),
+ })
}
}
@@ -317,8 +317,8 @@ impl Subst<Typed> for ThunkInternal {
|v| v.subst_shift(var, val),
|x, v| {
v.subst_shift(
- &var.shift(1, &x.into()),
- &val.shift(1, &x.into()),
+ &var.under_binder(x),
+ &val.under_binder(x),
)
},
X::clone,