diff options
author | Nadrieril | 2019-05-04 19:51:26 +0200 |
---|---|---|
committer | Nadrieril | 2019-05-04 19:51:26 +0200 |
commit | 6792d3da32d11b5303b00d1cc667f6f946d8bf33 (patch) | |
tree | 03489613ec26f5a5559bb5b015a2d29a1bf15c53 /dhall | |
parent | ab100be616932dab22a5309df86107b66e93db37 (diff) |
We actually don't need SubExpr::shift anymore
Diffstat (limited to '')
-rw-r--r-- | dhall/src/normalize.rs | 9 | ||||
-rw-r--r-- | dhall_syntax/src/core.rs | 81 |
2 files changed, 5 insertions, 85 deletions
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs index 8ae746d..d84c2d5 100644 --- a/dhall/src/normalize.rs +++ b/dhall/src/normalize.rs @@ -187,17 +187,18 @@ impl Value { let a = n.normalize_to_expr(); dhall::subexpr!(λ(x: a) -> Some x) } - Value::ListConsClosure(n, None) => { - let a = n.normalize_to_expr(); + Value::ListConsClosure(a, None) => { // Avoid accidental capture of the new `x` variable let a1 = a.shift(1, &Label::from("x").into()); + let a1 = a1.normalize_to_expr(); + let a = a.normalize_to_expr(); 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.shift(1, &Label::from("xs").into()); + let v = v.normalize_to_expr(); + let a = n.normalize_to_expr(); dhall::subexpr!(λ(xs : List a) -> [ v ] # xs) } Value::NaturalSuccClosure => { diff --git a/dhall_syntax/src/core.rs b/dhall_syntax/src/core.rs index a186d19..7cdda64 100644 --- a/dhall_syntax/src/core.rs +++ b/dhall_syntax/src/core.rs @@ -1,9 +1,7 @@ #![allow(non_snake_case)] use std::collections::BTreeMap; -use std::collections::HashMap; use std::rc::Rc; -use crate::context::Context; use crate::visitor; use crate::*; @@ -436,36 +434,6 @@ impl<N: Clone, E> SubExpr<N, E> { )), } } - - /// `shift` is used by both normalization and type-checking to avoid variable - /// capture by shifting variable indices - /// See https://github.com/dhall-lang/dhall-lang/blob/master/standard/semantics.md#shift - /// for details - pub fn shift(&self, delta: isize, var: &V<Label>) -> Self { - match self.as_ref() { - ExprF::Var(v) => self.rewrap(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.shift(1, &x.into())), - ), - } - } - - pub fn subst_shift(&self, var: &V<Label>, val: &Self) -> Self { - match self.as_ref() { - ExprF::Var(v) if v == var => val.clone(), - ExprF::Var(v) => self.rewrap(ExprF::Var(v.shift(-1, var))), - _ => self.map_subexprs_with_special_handling_of_binders( - |e| e.subst_shift(var, val), - |x: &Label, e| { - e.subst_shift( - &var.shift(1, &x.into()), - &val.shift(1, &x.into()), - ) - }, - ), - } - } } impl<N: Clone> SubExpr<N, X> { @@ -512,52 +480,3 @@ impl<Label: PartialEq + Clone> V<Label> { } } } - -/// `shift` is used by both normalization and type-checking to avoid variable -/// capture by shifting variable indices -/// See https://github.com/dhall-lang/dhall-lang/blob/master/standard/semantics.md#shift -/// for details -/// -pub fn shift<N, E>( - delta: isize, - var: &V<Label>, - in_expr: &SubExpr<N, E>, -) -> SubExpr<N, E> -where - N: Clone, -{ - in_expr.shift(delta, var) -} - -pub fn shift0_multiple<N, E>( - deltas: &HashMap<Label, isize>, - in_expr: &SubExpr<N, E>, -) -> SubExpr<N, E> -where - N: Clone, -{ - shift0_multiple_inner(&Context::new(), deltas, in_expr) -} - -fn shift0_multiple_inner<N, E>( - ctx: &Context<Label, ()>, - deltas: &HashMap<Label, isize>, - in_expr: &SubExpr<N, E>, -) -> SubExpr<N, E> -where - N: Clone, -{ - use crate::ExprF::*; - match in_expr.as_ref() { - Var(V(y, m)) if ctx.lookup(y, *m).is_none() => { - let delta = deltas.get(y).unwrap_or(&0); - in_expr.rewrap(Var(V(y.clone(), add_ui(*m, *delta)))) - } - _ => in_expr.map_subexprs_with_special_handling_of_binders( - |e| shift0_multiple_inner(ctx, deltas, e), - |x: &Label, e| { - shift0_multiple_inner(&ctx.insert(x.clone(), ()), deltas, e) - }, - ), - } -} |