Compile a Constructor. Each constructor gets its own arena.
( ctor: &ConstructorVal, mut_ctx: &MutCtx, cache: &mut BlockCache, stt: &CompileState, )
| 2109 | structural_overhead += 32 + ind.ctors.len() * 32; |
| 2110 | }, |
| 2111 | IxonMutConst::Recr(rec) => { |
| 2112 | // Recursor: 32-byte key + (k + flags + lvls + params + indices + motives + minors + typ_ref + rules_array_ref) |
| 2113 | // = 32 + (1 + 1 + 8 + 8 + 8 + 8 + 8 + 32 + 32) = 138 bytes |
| 2114 | structural_overhead += 138; |
| 2115 | // Each RecursorRule: 32-byte key + (fields + rhs_ref) = 32 + (8 + 32) = 72 bytes |
| 2116 | structural_overhead += rec.rules.len() * 72; |
| 2117 | // Rules array: 32-byte key + N * 32-byte refs |
| 2118 | structural_overhead += 32 + rec.rules.len() * 32; |
| 2119 | }, |
| 2120 | } |
| 2121 | } |
| 2122 | // Refs: each is a 32-byte address (already content-addressed, no extra overhead) |
| 2123 | // Univs: each unique univ needs storage. Estimate 32 + 8 bytes per univ. |
| 2124 | structural_overhead += univs.len() * 40; |
| 2125 | |
| 2126 | let hash_consed_size = expr_hash_consed_size + structural_overhead; |
| 2127 | |
| 2128 | // Rebuild the constants with rewritten expressions |
| 2129 | let mut new_consts = Vec::with_capacity(mut_consts.len()); |
| 2130 | for (i, mc) in mut_consts.into_iter().enumerate() { |
| 2131 | let (kind, indices) = &layout[i]; |
| 2132 | let new_mc = match (kind, mc) { |
| 2133 | (MutConstKind::Defn, IxonMutConst::Defn(def)) => { |
| 2134 | IxonMutConst::Defn(Definition { |
| 2135 | kind: def.kind, |
| 2136 | safety: def.safety, |
| 2137 | lvls: def.lvls, |
| 2138 | typ: rewritten[indices[0]].clone(), |
| 2139 | value: rewritten[indices[1]].clone(), |
| 2140 | }) |
| 2141 | }, |
| 2142 | (MutConstKind::Indc, IxonMutConst::Indc(ind)) => { |
| 2143 | let new_ctors: Vec<Constructor> = ind |
| 2144 | .ctors |
| 2145 | .into_iter() |
| 2146 | .enumerate() |
| 2147 | .map(|(ci, ctor)| Constructor { |
| 2148 | is_unsafe: ctor.is_unsafe, |
| 2149 | lvls: ctor.lvls, |
| 2150 | cidx: ctor.cidx, |
| 2151 | params: ctor.params, |
| 2152 | fields: ctor.fields, |
| 2153 | typ: rewritten[indices[ci + 1]].clone(), |
| 2154 | }) |
| 2155 | .collect(); |
| 2156 | IxonMutConst::Indc(Inductive { |
| 2157 | is_unsafe: ind.is_unsafe, |
| 2158 | lvls: ind.lvls, |
| 2159 | params: ind.params, |
| 2160 | indices: ind.indices, |
no test coverage detected