Function subst

crates/kernel/src/subst.rs:45–67

Perform single substitution: `body[arg/Var(depth)]`. Replaces `Var(depth)` with `arg` (lifted by `depth`), shifts free variables above `depth` down by 1. Uses `lbr()` for fast-path skipping. The internal traversal is memoized by content hash so shared sub-expressions within `body` are walked once per depth. Memoization scratch is borrowed from `env.subst_scratch` to avoid allocating a fresh `FxH

(
  env: &mut InternTable<M>,
  body: &KExpr<M>,
  arg: &KExpr<M>,
  depth: u64,
)

/// allocating a fresh `FxHashMap` per call. We `mem::take` it out
/// (replacing with an empty placeholder) so the borrow checker lets us
/// thread `&mut env` and `&mut scratch` separately into `subst_cached`,
/// then put it back on the way out. `subst_cached` does not call back
/// into `subst`, so there is no risk of recursive scratch use.
pub fn subst<M: KernelMode>(
  env: &mut InternTable<M>,
  body: &KExpr<M>,
  arg: &KExpr<M>,
  depth: u64,
) -> KExpr<M> {
  if *IX_SUBST_COUNT_LOG && depth == 0 {
    let n = SUBST_COUNT.fetch_add(1, std::sync::atomic::Ordering::Relaxed);
    if n.is_multiple_of(100_000) && n > 0 {
      log::info!("[subst] count={n}");
    }
  }
  // Fast path: no loose bound vars at or below `depth` means nothing to
  // substitute; returning the original Arc is cheap and cache-free.
  if body.lbr() <= depth {
    return body.clone();
  }
  let mut cache = std::mem::take(&mut env.subst_scratch);
  cache.clear();
  let result = subst_cached(env, body, arg, depth, &mut cache);
  env.subst_scratch = cache;
  result
}