summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorNadrieril2019-04-23 22:37:05 +0200
committerNadrieril2019-04-23 22:38:33 +0200
commitd1ad0a2036ce689d4a6b5f38a1641b9ce475df9e (patch)
treecc053df9adbe5fcfb19a04c4d5b58d2cd28f03b0
parent4b1ad84cb2dad533069d685e212894d517d8fa57 (diff)
Fix shifting under Pi
-rw-r--r--dhall/src/typecheck.rs42
1 files changed, 29 insertions, 13 deletions
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index d45b93c..0ee481f 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -57,6 +57,13 @@ impl<'a> Normalized<'a> {
self.2,
)
}
+ fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+ Normalized(
+ shift(delta, var, &self.0),
+ self.1.as_ref().map(|t| t.shift(delta, var)),
+ self.2,
+ )
+ }
pub(crate) fn into_type(self) -> Result<Type<'a>, TypeError> {
self.into_type_ctx(&TypecheckContext::new())
}
@@ -118,19 +125,10 @@ impl<'a> Type<'a> {
&self.0
}
fn shift0(&self, delta: isize, label: &Label) -> Self {
- use TypeInternal::*;
- Type(match &self.0 {
- Expr(e) => Expr(Box::new(e.shift0(delta, label))),
- Pi(ctx, c, x, t, e) => Pi(
- ctx.clone(),
- *c,
- x.clone(),
- Box::new(t.shift0(delta, label)),
- Box::new(e.shift0(delta, label)),
- ),
- Const(c) => Const(*c),
- SuperType => SuperType,
- })
+ Type(self.0.shift0(delta, label))
+ }
+ fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+ Type(self.0.shift(delta, var))
}
fn const_sort() -> Self {
@@ -192,6 +190,24 @@ impl<'a> TypeInternal<'a> {
)),
}
}
+ fn shift0(&self, delta: isize, label: &Label) -> Self {
+ self.shift(delta, &V(label.clone(), 0))
+ }
+ fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+ use TypeInternal::*;
+ match self {
+ Expr(e) => Expr(Box::new(e.shift(delta, var))),
+ Pi(ctx, c, x, t, e) => Pi(
+ ctx.clone(),
+ *c,
+ x.clone(),
+ Box::new(t.shift(delta, var)),
+ Box::new(e.shift(delta, &var.shift0(1, x))),
+ ),
+ Const(c) => Const(*c),
+ SuperType => SuperType,
+ }
+ }
}
#[derive(Debug, Clone)]