Class CompileState

crates/compile/src/compile.rs:108–171

Compile state for building the Ixon environment.

pub struct KernelCtx {
  /// Worker-local **canonical** kernel environment. Populated incrementally by
  /// aux_gen's Phase 1+ (`compute_is_large_and_k`, `ingress_field_deps`,
  /// etc.) with aux-substituted types at `resolve_lean_name_addr`-derived
  /// addresses that may shift as alpha-collapse reassigns addresses over
  /// the course of compilation.
  pub kenv: ix_kernel::env::KEnv<ix_kernel::mode::Meta>,
  /// Ids whose `ingress_aux_gen_dep` dispatch has already run against
  /// `kenv`. The dispatch is a deterministic function of the constant's
  /// kind, so once an id is here its kenv entry is at final fidelity and
  /// the walkers skip re-expanding its whole reference closure (that
  /// re-expansion was Θ(blocks × closure) when the set lived per call).
  /// Keyed by resolved `KId` — not bare `Name` — so an address shifted
  /// by later aux registration reads as unseen and re-ingresses under
  /// the new id, exactly as the per-call sets healed it. Must be cleared
  /// together with `kenv` (the entries it vouches for die with it).
  pub aux_ingress_seen: FxHashSet<ix_kernel::id::KId<ix_kernel::mode::Meta>>,
}

impl Default for KernelCtx {
  fn default() -> Self {
    Self::new()
  }
}

impl KernelCtx {
  pub fn new() -> Self {
    KernelCtx {
      kenv: ix_kernel::env::KEnv::new(),
      aux_ingress_seen: FxHashSet::default(),
    }
  }
}

/// Compile state for building the Ixon environment.
pub struct CompileState {
  /// Ixon environment being built
  pub env: IxonEnv,
  /// Map from Lean constant name to Ixon address
  pub name_to_addr: DashMap<Name, Address>,
  /// Mutual block canonical class ordering, keyed by any inductive name in the
  /// block. Each entry is the list of equivalence classes (in `sort_consts` order),
  /// where each class is a list of names.
  pub blocks: DashMap<Name, Vec<Vec<Name>>>,
  /// Per-block size statistics (keyed by low-link name)
  pub block_stats: DashMap<Name, BlockSizeStats>,
  /// Constants that couldn't be compiled (name -> error description).
  ///
  /// Populated in two phases:
  /// 1. Pre-compile grounding: `ground_consts` identifies constants unreachable
  ///    from axioms/primitives.
  /// 2. During scheduling: per-block compile failures (e.g. `compute_is_large_and_k`
  ///    rejecting an ill-formed inductive) are recorded here instead of
  ///    aborting the scheduler, so the rest of the env still compiles and
  ///    callers can report each failure per-constant.
  ///
  /// `DashMap` (rather than `FxHashMap`) because scheduler workers insert
  /// concurrently on per-block failure paths.
  pub ungrounded: DashMap<Name, String>,
  /// Persistent set of names compiled by aux_gen. Used for membership