Function simul_subst

crates/kernel/src/subst.rs:235–252

Perform simultaneous substitution: replace `Var(depth)..Var(depth+n-1)` with `substs[0]..substs[n-1]`, shifting free variables above by `-n`. Uses the same per-call pointer-identity memoization as `subst` so shared sub-expressions are traversed once per depth level (see the module-level docs).

(
  env: &mut InternTable<M>,
  body: &KExpr<M>,
  substs: &[KExpr<M>],
  depth: u64,
)

/// with `substs[0]..substs[n-1]`, shifting free variables above by `-n`.
///
/// Uses the same per-call pointer-identity memoization as `subst` so
/// shared sub-expressions are traversed once per depth level (see the
/// module-level docs).
pub fn simul_subst<M: KernelMode>(
  env: &mut InternTable<M>,
  body: &KExpr<M>,
  substs: &[KExpr<M>],
  depth: u64,
) -> KExpr<M> {
  if body.lbr() <= depth {
    return body.clone();
  }
  // See `subst` for the mem::take/restore pattern. `simul_subst_cached`
  // does not call into `subst`/`simul_subst`, so it is safe to share the
  // single `subst_scratch` between them.
  let mut cache = std::mem::take(&mut env.subst_scratch);
  cache.clear();
  let result = simul_subst_cached(env, body, substs, depth, &mut cache);
  env.subst_scratch = cache;
  result
}