summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
authorNadrieril2019-04-18 19:34:38 +0200
committerNadrieril2019-04-18 19:34:38 +0200
commit588127bf4105d8d4629304521abc3d992326a63a (patch)
tree57c8c0255ed21cba0f6f6229e4207d6d6582175c /dhall
parentf4a50a5da10eb2de1d7cf00ad6f6765605da366d (diff)
subst_shift in a single pass
Diffstat (limited to 'dhall')
-rw-r--r--dhall/src/typecheck.rs17
1 files changed, 7 insertions, 10 deletions
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 5aaeb08..186384d 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -44,9 +44,9 @@ impl<'a> Normalized<'a> {
fn unroll_ref(&self) -> &Expr<X, X> {
self.as_expr().as_ref()
}
- fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+ fn shift0(&self, delta: isize, label: &Label) -> Self {
// shift the type too ?
- Normalized(shift(delta, var, &self.0), self.1.clone(), self.2)
+ Normalized(shift0(delta, label, &self.0), self.1.clone(), self.2)
}
}
impl Normalized<'static> {
@@ -86,10 +86,10 @@ impl<'a> Type<'a> {
Cow::Owned(e) => Ok(Cow::Owned(e.into_expr().unroll())),
}
}
- fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+ fn shift0(&self, delta: isize, label: &Label) -> Self {
use TypeInternal::*;
Type(match &self.0 {
- Expr(e) => Expr(Box::new(e.shift(delta, var))),
+ Expr(e) => Expr(Box::new(e.shift0(delta, label))),
Const(c) => Const(*c),
SuperType => SuperType,
})
@@ -378,9 +378,7 @@ fn type_with(
let ret = match e.as_ref() {
Lam(x, t, b) => {
let t = mktype(ctx, t.clone())?;
- let ctx2 = ctx
- .insert(x.clone(), t.clone())
- .map(|e| e.shift(1, &V(x.clone(), 0)));
+ let ctx2 = ctx.insert(x.clone(), t.clone()).map(|e| e.shift0(1, x));
let b = type_with(&ctx2, b.clone())?;
Ok(RetExpr(Pi(
x.clone(),
@@ -395,9 +393,8 @@ fn type_with(
mkerr(InvalidInputType(ta.into_normalized()?)),
);
- let ctx2 = ctx
- .insert(x.clone(), ta.clone())
- .map(|e| e.shift(1, &V(x.clone(), 0)));
+ let ctx2 =
+ ctx.insert(x.clone(), ta.clone()).map(|e| e.shift0(1, x));
let tb = type_with(&ctx2, tb.clone())?;
let kB = ensure_is_const!(
&tb.get_type()?,