diff options
Diffstat (limited to '')
-rw-r--r-- | dhall_core/src/core.rs | 62 |
1 files changed, 57 insertions, 5 deletions
diff --git a/dhall_core/src/core.rs b/dhall_core/src/core.rs index aeb6f23..56ab66c 100644 --- a/dhall_core/src/core.rs +++ b/dhall_core/src/core.rs @@ -1,7 +1,9 @@ #![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::*; @@ -486,6 +488,7 @@ fn shift_var(delta: isize, var: &V<Label>, in_expr: &V<Label>) -> V<Label> { /// 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>, @@ -505,6 +508,41 @@ pub fn shift<N, E>( } } +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) +} + +fn shift0_multiple<N, E>( + deltas: &HashMap<Label, isize>, + in_expr: &SubExpr<N, E>, +) -> SubExpr<N, E> { + 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> { + 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); + rc(Var(V(y.clone(), add_ui(*m, *delta)))) + } + _ => in_expr.map_subexprs_with_special_handling_of_binders( + |e| shift0_multiple_inner(ctx, deltas, e), + |l: &Label, e| { + shift0_multiple_inner(&ctx.insert(l.clone(), ()), deltas, e) + }, + ), + } +} + /// Substitute all occurrences of a variable with an expression, and /// removes the variable from the environment by shifting the indices /// of other variables appropriately. @@ -518,15 +556,29 @@ pub fn subst_shift<N, E>( value: &SubExpr<N, E>, in_expr: &SubExpr<N, E>, ) -> SubExpr<N, E> { + subst_shift_inner(&HashMap::new(), var, value, in_expr) +} + +fn subst_shift_inner<N, E>( + ctx: &HashMap<Label, isize>, + var: &V<Label>, + value: &SubExpr<N, E>, + in_expr: &SubExpr<N, E>, +) -> SubExpr<N, E> { use crate::ExprF::*; + let V(x, n) = var; + let dn = ctx.get(x).unwrap_or(&0); + let actual_var = V(x.clone(), add_ui(*n, *dn)); match in_expr.as_ref() { - Var(v) if v == var => SubExpr::clone(value), - Var(v) => rc(Var(shift_var(-1, var, v))), + Var(v) if v == &actual_var => shift0_multiple(ctx, value), + Var(v) => rc(Var(shift_var(-1, &actual_var, v))), _ => in_expr.map_subexprs_with_special_handling_of_binders( - |e| subst_shift(var, &value, e), + |e| subst_shift_inner(ctx, var, value, e), |l: &Label, e| { - let vl = V(l.clone(), 0); - subst_shift(&shift_var(1, &vl, var), &shift(1, &vl, value), e) + let mut ctx = ctx.clone(); + let count = ctx.entry(l.clone()).or_insert(0); + *count += 1; + subst_shift_inner(&ctx, var, value, e) }, ), } |