| 2337 | &decl.domain, |
| 2338 | &self.fvar_levels, |
| 2339 | depth + i, |
| 2340 | self.param_names, |
| 2341 | self.stt, |
| 2342 | ); |
| 2343 | self.tc.push_local(kty); |
| 2344 | } |
| 2345 | self.extra_locals += decls.len(); |
| 2346 | } |
| 2347 | |
| 2348 | /// Pop locals pushed by `push_locals`. |
| 2349 | pub(super) fn pop_locals(&mut self, decls: &[LocalDecl]) { |
| 2350 | for decl in decls.iter().rev() { |
| 2351 | self.tc.pop_local(); |
| 2352 | self.fvar_levels.remove(&decl.fvar_name); |
| 2353 | } |
| 2354 | self.extra_locals -= decls.len(); |
| 2355 | } |
| 2356 | |
| 2357 | fn fault_in_direct_expr_consts(&mut self, expr: &LeanExpr) { |
| 2358 | let mut refs = FxHashSet::default(); |
| 2359 | collect_lean_const_refs(expr, &mut refs); |
| 2360 | for name in refs { |
| 2361 | self.fault_in_name(&name); |
| 2362 | } |
| 2363 | } |
| 2364 | |
| 2365 | fn fault_in_name(&mut self, name: &Name) -> bool { |
| 2366 | let Some(lean_env) = self.stt.lean_env.as_deref() else { |
| 2367 | return false; |
| 2368 | }; |
| 2369 | ensure_full_in_tc_env(name, lean_env, self.stt, self.tc.env); |
| 2370 | let addr = resolve_lean_name_addr( |
| 2371 | name, |
| 2372 | Some(&self.stt.name_to_addr), |
| 2373 | Some(&self.stt.aux_name_to_addr), |
| 2374 | ); |
| 2375 | self.addr_present(&addr) |
| 2376 | } |
| 2377 | |
| 2378 | fn fault_in_addr(&mut self, addr: &Address) -> bool { |
| 2379 | if self.addr_present(addr) { |
| 2380 | return true; |
| 2381 | } |
| 2382 | let Some(name) = self.name_for_addr(addr) else { |
| 2383 | return false; |
| 2384 | }; |
| 2385 | self.fault_in_name(&name) && self.addr_present(addr) |
| 2386 | } |
| 2387 | |
| 2388 | fn addr_present(&self, addr: &Address) -> bool { |
| 2389 | self.tc.env.consts.keys().any(|id| &id.addr == addr) |
| 2390 | } |
| 2391 | |
| 2392 | fn name_for_addr(&self, addr: &Address) -> Option<Name> { |
| 2393 | for entry in self.stt.name_to_addr.iter() { |
| 2394 | if entry.value() == addr { |
| 2395 | return Some(entry.key().clone()); |