diff options
author | Nadrieril | 2019-04-18 19:34:38 +0200 |
---|---|---|
committer | Nadrieril | 2019-04-18 19:34:38 +0200 |
commit | 588127bf4105d8d4629304521abc3d992326a63a (patch) | |
tree | 57c8c0255ed21cba0f6f6229e4207d6d6582175c /dhall/src | |
parent | f4a50a5da10eb2de1d7cf00ad6f6765605da366d (diff) |
subst_shift in a single pass
Diffstat (limited to '')
-rw-r--r-- | dhall/src/typecheck.rs | 17 |
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()?, |