diff options
author | Nadrieril | 2019-05-02 17:18:52 +0200 |
---|---|---|
committer | Nadrieril | 2019-05-02 17:18:52 +0200 |
commit | 17ab417aeb5aea6cd21240a491607b9017194737 (patch) | |
tree | d657fd50678dd8a562621d91c3caecbb2396fc7a /dhall_core/src | |
parent | db3ca819283f9bd99d197de464717f0b58b52fe4 (diff) |
Remove shift0
Diffstat (limited to 'dhall_core/src')
-rw-r--r-- | dhall_core/src/core.rs | 40 |
1 files changed, 17 insertions, 23 deletions
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>, |