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<'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 set_transparency(&mut self, mode: TransparencyMode)

Set the transparency mode.

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.

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 infer_type(&mut self, expr: &Expr) -> Result<Expr, KernelError>

Infer the type of an expression.

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.