| 2704 | |
| 2705 | /// Name → Address for KId construction from Lean Names. |
| 2706 | pub fn lean_name_to_addr(name: &Name) -> Address { |
| 2707 | Address::from_blake3_hash(*name.get_hash()) |
| 2708 | } |
| 2709 | |
| 2710 | /// Incrementally ingress a set of just-compiled constants into a KEnv. |
| 2711 | /// |
| 2712 | /// Called after each block compiles in the topological compilation loop. |
| 2713 | /// `names` are the Lean names of constants in the block. For each name, |
| 2714 | /// we look up its Ixon address and constant, convert to KConst, and insert. |
| 2715 | /// Build the address → name + name → address lookup tables for |
| 2716 | /// `ingress_compiled_names`. Call once at compile start, then pass to each |
| 2717 | /// incremental ingress call. |
| 2718 | /// |
| 2719 | /// Two maps: |
| 2720 | /// - `name_map`: `ixon_env.names` inverted — address of a `Lean.Name` → |
| 2721 | /// the name itself. Used in Meta mode to recover names from arena |
| 2722 | /// metadata. |
| 2723 | /// - `addr_map`: `ixon_env.named` — each registered Lean name → the |
| 2724 | /// content address at which its compiled `Constant` is stored |
| 2725 | /// (projection address for Muts members, or direct block address for |
| 2726 | /// singletons). This is the kernel-addressing map: `KId`s for sibling |
| 2727 | /// references inside Muts blocks MUST use these addresses (the raw |
| 2728 | /// name-hash address is insufficient because an alpha-collapsed block |