| 39 | |
| 40 | impl<M: KernelMode> TypeChecker<'_, M> { |
| 41 | pub fn infer(&mut self, e: &KExpr<M>) -> Result<KExpr<M>, TcError<M>> { |
| 42 | if *IX_INFER_COUNT_LOG { |
| 43 | let n = INFER_COUNT.fetch_add(1, std::sync::atomic::Ordering::Relaxed); |
| 44 | if n.is_multiple_of(100_000) && n > 0 { |
| 45 | log::info!("[infer] count={n}"); |
| 46 | } |
| 47 | } |
| 48 | let infer_only = self.infer_only; |
| 49 | |
| 50 | let cache_key = self.infer_key(e); |
| 51 | // Full-mode results are validated and may be consumed by either mode. |
| 52 | if let Some(cached) = self.env.infer_cache.get(&cache_key) { |
| 53 | self.env.perf.record_infer_hit(); |
| 54 | return Ok(cached.clone()); |
| 55 | } |
| 56 | self.env.perf.record_infer_miss(); |
| 57 | if !infer_only { |
| 58 | self.record_hot_miss("infer", e); |
| 59 | } |
| 60 | // Infer-only results skipped argument/let validation, so only infer-only |
| 61 | // callers may reuse them. |
| 62 | if infer_only { |
| 63 | if let Some(cached) = self.env.infer_only_cache.get(&cache_key) { |
| 64 | self.env.perf.record_infer_only_hit(); |
| 65 | return Ok(cached.clone()); |
| 66 | } |
| 67 | self.env.perf.record_infer_only_miss(); |
| 68 | self.record_hot_miss("infer-only", e); |
| 69 | } |
| 70 | |
| 71 | let ty = match e.data() { |
| 72 | // Legacy de Bruijn lookup: still used by inductive validation paths |
| 73 | // that push types via `push_local`/`push_let` rather than opening |
| 74 | // binders into fvars. Keeps the dual-bookkeeping correctness during |
| 75 | // the partial fvar transition (Stage B of the plan). |
| 76 | ExprData::Var(i, _, _) => self.lookup_var(*i)?, |
| 77 | |
| 78 | // Free variable: look up the type stored in the active local |
| 79 | // context. No lift is needed: every type pushed to `lctx` is closed |
| 80 | // under fvar identity (its outer Vars/FVars were already |
| 81 | // instantiate_rev'd or were absent), so the stored type is depth- |
| 82 | // invariant. Mirrors lean4lean's `inferType` `.fvar` branch. |
| 83 | ExprData::FVar(id, _, _) => match self.lctx.find(*id) { |
| 84 | Some(decl) => decl.ty().clone(), |
| 85 | None => { |
| 86 | return Err(TcError::Other(format!( |
| 87 | "infer: unknown FVar({id}); not bound in the active local context" |
| 88 | ))); |
| 89 | }, |
| 90 | }, |
| 91 | |
| 92 | ExprData::Sort(u, _) => { |
| 93 | let u2 = KUniv::succ(u.clone()); |
| 94 | self.intern(KExpr::sort(u2)) |
| 95 | }, |
| 96 | |
| 97 | ExprData::Const(id, us, _) => { |
| 98 | let c = self.get_const(id)?; |