Function build_ref_graph

crates/compile/src/graph.rs:50–98

Builds a [`RefGraph`] from a Lean [`Env`] by collecting all constant references in parallel. For each constant, extracts the set of names it references (from types, values, constructors, and recursor rules), then assembles both the forward and reverse edge maps.

(env: &Env)

/// For each constant, extracts the set of names it references (from types, values, constructors,
/// and recursor rules), then assembles both the forward and reverse edge maps.
/// Everything the compile-env setup needs from a whole-env pass: the
/// reference graph, the immediately-ungrounded set (before transitive
/// proliferation), and the inductive mutual-block groups
/// (`all[0] → all`, for flag validation).
pub struct SetupScan {
  pub graph: RefGraph,
  pub immediate_ungrounded: FxHashMap<Name, crate::ground::GroundError>,
  pub ind_groups: FxHashMap<Name, Vec<Name>>,
}

/// Fused whole-env setup pass: one decode per constant feeding the ref
/// graph, the groundedness check, and inductive-group collection.
/// One pass instead of separate `build_ref_graph` /
/// `ground_consts`' scan, `validate_lean_ind_flags`' scan) — under
/// (the compile path'''s default) decodes a constant per access, so
/// visiting the whole env once instead of three times cuts the setup
/// decode count to a third. Outputs are identical to the separate passes.
pub fn setup_scan(env: &Env) -> SetupScan {
  #[derive(Default)]
  struct Acc {
    out_refs: RefMap,
    in_refs: RefMap,
    ungrounded: FxHashMap<Name, crate::ground::GroundError>,
    ind_groups: FxHashMap<Name, Vec<Name>>,
  }

  let names: Vec<&Name> = env.keys().collect();
  let acc = names
    .into_par_iter()
    .filter_map(|name| {
      let constant = env.get(name)?;
      let deps = get_constant_info_references(&constant);
      let mut acc = Acc {
        in_refs: mk_in_refs(name, &deps),
        out_refs: RefMap::from_iter([(name.clone(), deps)]),
        ..Acc::default()
      };
      if let Err(err) = crate::ground::ground_const_check(&constant, env) {
        acc.ungrounded.insert(name.clone(), err);
      }
      // Members of one mutual family share the same `all`, so
      // first-wins insertion is value-identical regardless of which
      // member lands first.
      if let ConstantInfo::InductInfo(v) = &*constant
        && let Some(first) = v.all.first()
      {
        acc.ind_groups.entry(first.clone()).or_insert_with(|| v.all.clone());
      }
      Some(acc)
    })
    .reduce(Acc::default, |mut l, r| {
      l.out_refs = merge_ref_maps(l.out_refs, r.out_refs);