Struct TypeChecker 

pub struct TypeChecker<'env> { /* private fields */ }

Unified type checker state.

Owns WHNF reduction, definitional equality checking, and type inference. Mirrors LEAN 4’s type_checker class.

Implementations

impl TypeChecker<'_>

pub fn infer_type(&mut self, expr: &Expr) -> Result<Expr, KernelError>

Infer the type of an expression.

The cache

A type that was inferred is kept, by term, and returned the next time the same term is asked about (Lean’s m_infer_type). A proof term is a DAG — the terms omega and simp build reach one subterm along thousands of paths — and without the table every path inferred the subterm again: millions of inferences for a few thousand distinct subterms.

The type of a term is a function of the term, the environment and the types of the free variables in it, so an entry stays valid while those do:

• the environment is fixed for the checker’s life;
• a free variable keeps its type while it is in scope, and its id is not handed out again after its binder closes — so an entry that mentions a closed variable is simply never asked for again. Should a caller of Self::push_local bind an id a second time (to another type, or after its binder closed), the table is dropped (where the checker mirrors a local into its reducer);
• in checking mode an entry also records that the term CHECKED, which depends on the transparency mode: Self::set_transparency drops the table. The mode itself (checking / infer-only) is fixed per checker.

Only successes are kept. A failure is recomputed: it may be the per-declaration budget running out, which is not a property of the term. A success reached while the budget was running out is exact (see crate::fuel) and safe to keep.

impl<'env> TypeChecker<'env>

pub fn new(env: &'env Environment) -> Self

Create a new type checker for the given environment.

pub fn new_infer_only(env: &'env Environment) -> Self

Create a type checker in infer-only mode (skips some checks).

pub fn with_fvar_types( env: &'env Environment, locals: &HashMap<u64, Expr>, ) -> Self

Create a type checker whose local context is pre-seeded with the given free-variable types (id → type), e.g. the context a Reducer mirrors so K-like iota reduction can type majors that mention local FVars. Ids are installed in ascending order (later locals may depend on earlier ones).

Every free variable the new checker mints is distinct from every seeded one, in BOTH of its id ranges: the checker’s own locals (fresh_fvar, low ids) start past the largest seeded low id, and the binder-opening variables of its def-eq checker (ids from DEF_EQ_OPENED_FVAR_BASE) start past the largest seeded id of that range. The seeded locals of the second range are the binders the surrounding def-eq checker has opened; a def-eq checker that restarted at the base would open its first binder with the id of the surrounding checker’s first one and identify the two variables (see DefEqChecker::reserve_opened_fvars_through).

pub fn set_transparency(&mut self, mode: TransparencyMode)

Set the transparency mode.

The types inferred so far are dropped with the reduction and def-eq caches: in checking mode a cached type also records that the term CHECKED, and what checks depends on what may be unfolded.

pub fn env(&self) -> &Environment

Get the environment.

pub fn fresh_fvar(&mut self, name: Name, ty: Expr) -> FVarId

Generate a fresh free variable.

pub fn fresh_fvar_let(&mut self, name: Name, ty: Expr, val: Expr) -> FVarId

Generate a fresh free variable with a value (let-binding).

pub fn push_local(&mut self, decl: LocalDecl)

Push a local declaration onto the context.

pub fn pop_local(&mut self) -> Option<LocalDecl>

Pop a local declaration from the context.

The variable leaves scope, so its type also leaves the mirrors the def-eq checker and the reducers keep of this context (see the kernel-private local_types module) — unless an earlier declaration of the same variable is still in the context, in which case the mirrors are left as they are.

pub fn local_ctx(&self) -> &[LocalDecl]

Get the local context.

pub fn whnf(&mut self, expr: &Expr) -> Expr

Reduce an expression to WHNF.

pub fn ensure_sort(&mut self, expr: &Expr) -> Result<Level, KernelError>

Ensure an expression is a Sort, returning the level.

Infers the type, reduces to WHNF, and checks it’s a Sort.

pub fn ensure_pi(&mut self, expr: &Expr) -> Result<Expr, KernelError>

Ensure an expression’s type is a Pi type, returning it.

pub fn is_def_eq(&mut self, t: &Expr, s: &Expr) -> bool

Check if two expressions are definitionally equal.

pub fn check_type( &mut self, expr: &Expr, inferred: &Expr, expected: &Expr, ) -> Result<(), KernelError>

Check that an expression has the expected type.

pub fn is_prop(&mut self, expr: &Expr) -> bool

Check if an expression is a proposition (has type Prop).

pub fn is_proof(&mut self, expr: &Expr) -> bool

Check if an expression is a proof (its type is a proposition).

pub fn is_type(&mut self, expr: &Expr) -> bool

Check if an expression is a type (has type Sort u for some u).

pub fn get_level(&mut self, expr: &Expr) -> Result<Level, KernelError>

Get the universe level of a type expression.

pub fn unfold_definition(&mut self, expr: &Expr) -> Option<Expr>

Try to unfold a constant definition.

impl<'env> TypeChecker<'env>

pub fn infer_app_chain( &mut self, f: &Expr, args: &[Expr], ) -> Result<Expr, KernelError>

Infer the type of a chain of applications at once.

pub fn telescope_type( &mut self, ty: &Expr, max_pis: usize, ) -> (Vec<LocalDecl>, Expr)

Telescope a type, instantiating leading Pi binders with fresh free variables.

pub fn close_type_over_fvars(&mut self, fvars: &[LocalDecl], ty: Expr) -> Expr

Close a type over a list of free variables into Pi types.

pub fn close_term_over_fvars(&mut self, fvars: &[LocalDecl], term: Expr) -> Expr

Close a term over free variables into lambdas.

pub fn check(&mut self, expr: &Expr, expected: &Expr) -> Result<(), KernelError>

Check that expr has type expected.

pub fn try_check(&mut self, expr: &Expr, expected: &Expr) -> bool

Try to check; return true if the type matches.

pub fn count_pi_binders(&mut self, ty: &Expr) -> usize

Get the number of Pi binders in the WHNF of a type.

pub fn verify_declaration( &mut self, name: &Name, ty: &Expr, val: Option<&Expr>, ) -> Result<(), KernelError>

Verify a declaration’s type and optional value.

pub fn normalize(&mut self, expr: &Expr) -> Expr

Normalize an expression (full normal form).

pub fn constant_arity(&mut self, name: &Name) -> Option<usize>

Return the arity (number of Pi binders) in the type of a constant.

pub fn is_level_eq(&self, l1: &Level, l2: &Level) -> bool

Check if two universe levels are definitionally equal.

Delegates to the complete level::is_equivalent decision procedure (previously this was an essentially-syntactic stub that only recognised literally-equal or both-zero levels — a trap for callers expecting real universe defeq).