diff options
| -rw-r--r-- | dhall/src/normalize.rs | 39 | ||||
| -rw-r--r-- | dhall/src/typecheck.rs | 19 | ||||
| -rw-r--r-- | dhall_core/src/core.rs | 40 |
3 files changed, 43 insertions, 55 deletions
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs index a023d38..f991a2e 100644 --- a/dhall/src/normalize.rs +++ b/dhall/src/normalize.rs @@ -38,10 +38,6 @@ impl<'a> Typed<'a> { Normalized(internal, self.1) } - pub(crate) fn shift0(&self, delta: isize, x: &Label) -> Self { - self.shift(delta, &V(x.clone(), 0)) - } - pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self { Typed(self.0.shift(delta, var), self.1) } @@ -257,10 +253,6 @@ enum EnvItem { } impl EnvItem { - fn shift0(&self, delta: isize, x: &Label) -> Self { - self.shift(delta, &V(x.clone(), 0)) - } - fn shift(&self, delta: isize, var: &V<Label>) -> Self { use EnvItem::*; match self { @@ -297,8 +289,8 @@ impl NormalizationContext { fn skip(&self, x: &Label) -> Self { NormalizationContext(Rc::new( self.0 - .map(|_, e| e.shift0(1, x)) - .insert(x.clone(), EnvItem::Skip(V(x.clone(), 0))), + .map(|_, e| e.shift(1, &x.into())) + .insert(x.clone(), EnvItem::Skip(x.into())), )) } fn lookup(&self, var: &V<Label>) -> Value { @@ -402,14 +394,14 @@ impl Value { Value::ListConsClosure(n, None) => { let a = n.normalize_to_expr(); // Avoid accidental capture of the new `x` variable - let a1 = a.shift0(1, &"x".into()); + let a1 = a.shift(1, &Label::from("x").into()); dhall::subexpr!(λ(x : a) -> λ(xs : List a1) -> [ x ] # xs) } Value::ListConsClosure(n, Some(v)) => { let v = v.normalize_to_expr(); let a = n.normalize_to_expr(); // Avoid accidental capture of the new `xs` variable - let v = v.shift0(1, &"xs".into()); + let v = v.shift(1, &Label::from("xs").into()); dhall::subexpr!(λ(xs : List a) -> [ v ] # xs) } Value::NaturalSuccClosure => { @@ -746,7 +738,7 @@ impl Value { Value::Lam(x, t, e) => Value::Lam( x.clone(), t.shift(delta, var), - e.shift(delta, &var.shift0(1, x)), + e.shift(delta, &var.shift(1, &x.into())), ), Value::AppliedBuiltin(b, args) => Value::AppliedBuiltin( *b, @@ -763,7 +755,7 @@ impl Value { Value::Pi(x, t, e) => Value::Pi( x.clone(), t.shift(delta, var), - e.shift(delta, &var.shift0(1, x)), + e.shift(delta, &var.shift(1, &x.into())), ), Value::Var(v) => Value::Var(v.shift(delta, var)), Value::Const(c) => Value::Const(*c), @@ -830,7 +822,7 @@ impl Value { Value::PartialExpr(e) => Value::PartialExpr(Box::new( e.map_ref_with_special_handling_of_binders( |v| v.shift(delta, var), - |x, v| v.shift(delta, &var.shift0(1, x)), + |x, v| v.shift(delta, &var.shift(1, &x.into())), X::clone, X::clone, Label::clone, @@ -849,7 +841,10 @@ impl Value { Value::Lam(x, t, e) => Value::Lam( x.clone(), t.subst_shift(var, val), - e.subst_shift(&var.shift0(1, x), &val.shift0(1, x)), + e.subst_shift( + &var.shift(1, &x.into()), + &val.shift(1, &x.into()), + ), ), Value::AppliedBuiltin(b, args) => Value::AppliedBuiltin( *b, @@ -866,7 +861,10 @@ impl Value { Value::Pi(x, t, e) => Value::Pi( x.clone(), t.subst_shift(var, val), - e.subst_shift(&var.shift0(1, x), &val.shift0(1, x)), + e.subst_shift( + &var.shift(1, &x.into()), + &val.shift(1, &x.into()), + ), ), Value::Var(v) if v == var => val.to_value().clone(), Value::Var(v) => Value::Var(v.shift(-1, var)), @@ -934,7 +932,12 @@ impl Value { Value::PartialExpr(e) => Value::PartialExpr(Box::new( e.map_ref_with_special_handling_of_binders( |v| v.subst_shift(var, val), - |x, v| v.subst_shift(&var.shift0(1, x), &val.shift0(1, x)), + |x, v| { + v.subst_shift( + &var.shift(1, &x.into()), + &val.shift(1, &x.into()), + ) + }, X::clone, X::clone, Label::clone, diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index 582930b..78538aa 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -46,9 +46,6 @@ impl<'a> Typed<'a> { } impl<'a> Normalized<'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 { Normalized(self.0.shift(delta, var), self.1) } @@ -79,9 +76,6 @@ impl<'a> Type<'a> { fn internal_whnf(&self) -> Option<Value> { self.0.whnf() } - pub(crate) fn shift0(&self, delta: isize, label: &Label) -> Self { - Type(self.0.shift0(delta, label)) - } pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self { Type(self.0.shift(delta, var)) } @@ -164,9 +158,6 @@ impl<'a> TypeInternal<'a> { _ => None, } } - 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 { @@ -197,11 +188,11 @@ pub(crate) enum EnvItem { } impl EnvItem { - fn shift0(&self, delta: isize, x: &Label) -> Self { + fn shift(&self, delta: isize, var: &V<Label>) -> Self { use EnvItem::*; match self { - Type(v, e) => Type(v.shift0(delta, x), e.shift0(delta, x)), - Value(e) => Value(e.shift0(delta, x)), + Type(v, e) => Type(v.shift(delta, var), e.shift(delta, var)), + Value(e) => Value(e.shift(delta, var)), } } } @@ -215,9 +206,9 @@ impl TypecheckContext { } pub(crate) fn insert_type(&self, x: &Label, t: Type<'static>) -> Self { TypecheckContext( - self.0.map(|_, e| e.shift0(1, x)).insert( + self.0.map(|_, e| e.shift(1, &x.into())).insert( x.clone(), - EnvItem::Type(V(x.clone(), 0), t.shift0(1, x)), + EnvItem::Type(x.into(), t.shift(1, &x.into())), ), ) } diff --git a/dhall_core/src/core.rs b/dhall_core/src/core.rs index ebd95e7..3db07dd 100644 --- a/dhall_core/src/core.rs +++ b/dhall_core/src/core.rs @@ -62,6 +62,18 @@ pub enum Const { #[derive(Debug, Clone, PartialEq, Eq)] pub struct V<Label>(pub Label, pub usize); +// This is only for the specific `Label` type, not generic +impl From<Label> for V<Label> { + fn from(x: Label) -> V<Label> { + V(x, 0) + } +} +impl<'a> From<&'a Label> for V<Label> { + fn from(x: &'a Label) -> V<Label> { + V(x.clone(), 0) + } +} + // Definition order must match precedence order for // pretty-printing to work correctly #[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord)] @@ -443,15 +455,11 @@ impl<N, E> SubExpr<N, E> { ExprF::Var(v) => rc(ExprF::Var(v.shift(delta, var))), _ => self.map_subexprs_with_special_handling_of_binders( |e| e.shift(delta, var), - |x: &Label, e| e.shift(delta, &var.shift0(1, x)), + |x: &Label, e| e.shift(delta, &var.shift(1, &x.into())), ), } } - pub fn shift0(&self, delta: isize, label: &Label) -> Self { - self.shift(delta, &V(label.clone(), 0)) - } - pub fn subst_shift(&self, var: &V<Label>, val: &Self) -> Self { match self.as_ref() { ExprF::Var(v) if v == var => val.clone(), @@ -459,7 +467,10 @@ impl<N, E> SubExpr<N, E> { _ => self.map_subexprs_with_special_handling_of_binders( |e| e.subst_shift(var, val), |x: &Label, e| { - e.subst_shift(&var.shift0(1, x), &val.shift0(1, x)) + e.subst_shift( + &var.shift(1, &x.into()), + &val.shift(1, &x.into()), + ) }, ), } @@ -509,15 +520,6 @@ impl<Label: PartialEq + Clone> V<Label> { V(y.clone(), *m) } } - - pub fn shift0(&self, delta: isize, x: &Label) -> Self { - let V(y, m) = self; - if x == y { - V(y.clone(), add_ui(*m, delta)) - } else { - V(y.clone(), *m) - } - } } /// `shift` is used by both normalization and type-checking to avoid variable @@ -533,14 +535,6 @@ pub fn shift<N, E>( in_expr.shift(delta, var) } -pub fn shift0<N, E>( - delta: isize, - label: &Label, - in_expr: &SubExpr<N, E>, -) -> SubExpr<N, E> { - shift(delta, &V(label.clone(), 0), in_expr) -} - pub fn shift0_multiple<N, E>( deltas: &HashMap<Label, isize>, in_expr: &SubExpr<N, E>, |