(ci: &LeanConstantInfo)
| 2287 | idx: u64, |
| 2288 | other: Option<&MutConst>, |
| 2289 | mutuals_len: usize, |
| 2290 | stt: &CompileState, |
| 2291 | ) -> DecompileError { |
| 2292 | let has_addr = stt.name_to_addr.contains_key(name); |
| 2293 | let has_aux = stt.aux_name_to_addr.contains_key(name); |
| 2294 | let has_original = stt.env.named.get(name).is_some_and(|n| n.has_original()); |
| 2295 | DecompileError::BadConstantFormat { |
| 2296 | msg: format!( |
| 2297 | "{kind} '{}' idx={idx} landed on {:?} (mutuals.len={mutuals_len}, \ |
| 2298 | addr={has_addr}, aux={has_aux}, has_original={has_original})", |
| 2299 | name.pretty(), |
| 2300 | other.map(std::mem::discriminant), |
| 2301 | ), |
| 2302 | } |
| 2303 | } |
| 2304 | |
| 2305 | /// Decompile a single constant (non-mutual). |
| 2306 | fn decompile_const( |
| 2307 | name: &Name, |
| 2308 | named: &Named, |
| 2309 | stt: &CompileState, |
| 2310 | dstt: &DecompileState, |
| 2311 | ) -> Result<(), DecompileError> { |
| 2312 | let cnst = read_const(&named.addr, stt)?; |
| 2313 | |
| 2314 | // Build ctx from metadata's all field |
| 2315 | let named_meta = named.meta(); |
| 2316 | let all_addrs = get_all_from_meta(&named_meta); |
| 2317 | let all_names: Vec<Name> = all_addrs |
| 2318 | .iter() |
| 2319 | .map(|a| decompile_name(a, stt)) |
| 2320 | .collect::<Result<Vec<_>, _>>()?; |
| 2321 | let ctx = all_to_ctx(&all_names); |
| 2322 | let current_const = name.pretty(); |
| 2323 | |
| 2324 | match cnst.as_ref() { |
| 2325 | Constant { info: ConstantInfo::Defn(def), sharing, refs, univs } => { |
| 2326 | let mut cache = BlockCache { |
| 2327 | sharing: sharing.clone(), |
| 2328 | refs: refs.clone(), |
| 2329 | univ_table: univs.clone(), |
| 2330 | ctx: ctx.clone(), |
| 2331 | current_const: current_const.clone(), |
| 2332 | ..Default::default() |
| 2333 | }; |
| 2334 | cache.load_meta_extensions(&named_meta); |
| 2335 | let info = decompile_definition(def, &named_meta, &mut cache, stt, dstt)?; |
| 2336 | dstt.insert_interned(name.clone(), info); |
| 2337 | }, |
| 2338 | |
| 2339 | Constant { info: ConstantInfo::Recr(rec), sharing, refs, univs } => { |
| 2340 | let mut cache = BlockCache { |
| 2341 | sharing: sharing.clone(), |
| 2342 | refs: refs.clone(), |
| 2343 | univ_table: univs.clone(), |
| 2344 | ctx: ctx.clone(), |
| 2345 | current_const: current_const.clone(), |
| 2346 | ..Default::default() |
no test coverage detected