Function build_collapse_const_map

crates/ffi/src/lean_env.rs:262–322

Build the `B → A` rename map for an alpha-collapsed mutual block. When two primary inductives (e.g. `A` and `B`) compile to the same canonical address, the original Lean env still emits separate `B`/`B.below`/`B.rec`/`B.b`/... declarations whose bodies reference `A`/`B` as distinct names. The decompiled (canonical) form, however, has those references collapsed onto a single representative — typic

(
  all: &[Name],
  env: &Env,
  stt: &ix_compile::compile::CompileState,
)

/// representatives so [`const_alpha_eq_with_perm`] can compare the two
/// sides structurally.
fn build_collapse_const_map(
  all: &[Name],
  env: &Env,
  stt: &ix_compile::compile::CompileState,
) -> FxHashMap<Name, Name> {
  use ix_common::env::ConstantInfo as LeanCI;
  let mut map: FxHashMap<Name, Name> = FxHashMap::default();
  // Group primary members by canonical address; the first member with a
  // given address is the representative.
  let mut rep_by_addr: FxHashMap<ix_common::address::Address, &Name> =
    FxHashMap::default();
  for member in all {
    let Some(addr) = stt.resolve_addr(member) else {
      continue;
    };
    rep_by_addr.entry(addr).or_insert(member);
  }
  for member in all {
    let Some(addr) = stt.resolve_addr(member) else {
      continue;
    };
    let Some(&rep) = rep_by_addr.get(&addr) else {
      continue;
    };
    if rep == member {
      continue;
    }
    map.insert(member.clone(), rep.clone());
    // Derived names: `.rec`, `.below`, `.brecOn`, `.brecOn.go`,
    // `.brecOn.eq`, `.casesOn`, `.recOn`.
    for suffix in ["rec", "below", "brecOn", "casesOn", "recOn"] {
      let from = Name::str(member.clone(), suffix.to_string());
      let to = Name::str(rep.clone(), suffix.to_string());
      map.insert(from, to);
    }
    for suffix in ["go", "eq"] {
      let from = Name::str(
        Name::str(member.clone(), "brecOn".to_string()),
        suffix.to_string(),
      );
      let to = Name::str(
        Name::str(rep.clone(), "brecOn".to_string()),
        suffix.to_string(),
      );
      map.insert(from, to);
    }
    // Constructors: positional mapping. Both members are alpha-collapsed,
    // so they have the same number of constructors in the same order.
    if let (Some(LeanCI::InductInfo(m_ind)), Some(LeanCI::InductInfo(r_ind))) =
      (env.get(member).as_deref(), env.get(rep).as_deref())
      && m_ind.ctors.len() == r_ind.ctors.len()
    {
      for (m_ctor, r_ctor) in m_ind.ctors.iter().zip(r_ind.ctors.iter()) {
        if m_ctor != r_ctor {
          map.insert(m_ctor.clone(), r_ctor.clone());
        }
      }
    }