Function expr_mentions_addr

crates/kernel/src/tc.rs:1064–1100

Check whether an expression mentions a constant with the given address. Iterative (stack-based) — immune to stack overflow on deeply nested input.

(e: &KExpr<M>, addr: &Address)

  ///
  /// Primitives are resolved by address only — `Primitives::from_addr_names`
  /// receives a closure that always returns `None`, so the
  /// `M::MField<Name>` slot ends up as `()` (always, in Anon mode).
  pub fn new_with_lazy_anon(
    env: &'a mut KEnv<super::mode::Anon>,
    anon_env: &'a IxonEnv,
  ) -> Self {
    if !env.has_prims() {
      let prims = Primitives::from_addr_names(|_addr| None);
      let _ = env.set_prims(prims);
    }
    let mut tc = Self::new(env);
    tc.lazy_anon =
      Some(LazyAnonIngress { anon_env, faulted_addrs: FxHashSet::default() });
    tc
  }
}

// -----------------------------------------------------------------------
// Free-standing helpers
// -----------------------------------------------------------------------

/// Check whether an expression mentions a constant with the given address.
/// Iterative (stack-based) — immune to stack overflow on deeply nested input.
pub fn expr_mentions_addr<M: KernelMode>(e: &KExpr<M>, addr: &Address) -> bool {
  let mut stack: Vec<&KExpr<M>> = vec![e];
  while let Some(e) = stack.pop() {
    match e.data() {
      ExprData::Const(id, _, _) => {
        if id.addr == *addr {
          return true;
        }
      },
      ExprData::App(f, a, _) => {
        stack.push(f);
        stack.push(a);
      },
      ExprData::Lam(_, _, ty, body, _) | ExprData::All(_, _, ty, body, _) => {
        stack.push(ty);
        stack.push(body);
      },