oxilean_kernel/infer/
cache.rs

1//! The types a [`TypeChecker`] has inferred, remembered by term.
2
3use super::types::TypeChecker;
4use crate::error::KernelError;
5use crate::Expr;
6
7impl TypeChecker<'_> {
8    /// Infer the type of an expression.
9    ///
10    /// # The cache
11    ///
12    /// A type that was inferred is kept, by term, and returned the next time
13    /// the same term is asked about (Lean's `m_infer_type`). A proof term is
14    /// a DAG — the terms `omega` and `simp` build reach one subterm along
15    /// thousands of paths — and without the table every path inferred the
16    /// subterm again: millions of inferences for a few thousand distinct
17    /// subterms.
18    ///
19    /// The type of a term is a function of the term, the environment and
20    /// the types of the free variables in it, so an entry stays valid while
21    /// those do:
22    ///
23    /// * the environment is fixed for the checker's life;
24    /// * a free variable keeps its type while it is in scope, and its id is
25    ///   not handed out again after its binder closes — so an entry that
26    ///   mentions a closed variable is simply never asked for again. Should
27    ///   a caller of [`Self::push_local`] bind an id a second time (to
28    ///   another type, or after its binder closed), the table is dropped
29    ///   (where the checker mirrors a local into its reducer);
30    /// * in checking mode an entry also records that the term CHECKED, which
31    ///   depends on the transparency mode: [`Self::set_transparency`] drops
32    ///   the table. The mode itself (checking / infer-only) is fixed per
33    ///   checker.
34    ///
35    /// Only successes are kept. A failure is recomputed: it may be the
36    /// per-declaration budget running out, which is not a property of the
37    /// term. A success reached while the budget was running out is exact
38    /// (see [`crate::fuel`]) and safe to keep.
39    #[allow(clippy::result_large_err)]
40    pub fn infer_type(&mut self, expr: &Expr) -> Result<Expr, KernelError> {
41        // C16b: inference is the third loop (besides `whnf` and `is_def_eq`)
42        // that must observe the per-declaration fuel latch. A `let`-tower or
43        // dependent application chain grows its instantiated bodies
44        // geometrically *between* whnf/def-eq steps, so without this check a
45        // single `infer_type` call tree can allocate unboundedly while the
46        // budget is long exhausted (Init decl #3864,
47        // `Array.extract_append_extract._proof_1_1`, reached >12 GiB). The
48        // error is a typed abort, mapped by callers to the NAMED resource
49        // limit — never a rejection, and never a truncated term.
50        if crate::fuel::is_exhausted() {
51            return Err(KernelError::Other(
52                "per-declaration resource budget exhausted".to_string(),
53            ));
54        }
55        // A `Sort`, a literal and a loose bound variable are read straight
56        // off the term: nothing to look up, nothing to keep.
57        let remembered = !matches!(expr, Expr::Sort(_) | Expr::BVar(_) | Expr::Lit(_));
58        if remembered {
59            if let Some(ty) = self.infer_cache.get(expr) {
60                return Ok(ty.clone());
61            }
62        }
63        let ty = self.infer_type_uncached(expr)?;
64        if remembered {
65            self.infer_cache.insert(expr, ty.clone());
66        }
67        Ok(ty)
68    }
69}
oxilean_kernel/infer/cache.rs

oxilean_kernel/infer/
cache.rs
