Module sem 

The value engine: type checking and definitional equality by evaluation into closures.

The substitution checker (crate::dag::tc) crosses a binder by substituting a free variable into the body and β-reduces by substituting an argument into a body — each a copy of everything the variable is under. Here nothing is ever substituted. A term is evaluated in an environment that gives each bound variable a value: β extends the environment, a binder is crossed by binding a fresh variable, δ evaluates a definition’s body once per universe instantiation and applies it to the arguments. Evaluation performs β only; δ and ι wait in neutral values (a head and its arguments) until conversion or inference demands a weak head, and each such step is remembered on the value that asked for it.

Types are values too: inferring an application instantiates its function type’s closure with the argument’s value, and a lambda’s type is a closure whose codomain is inferred only when someone asks for it. The judgment is the substitution checker’s rule for rule, and conversion is Lean’s algorithm (lazy δ by definitional height, proof irrelevance, η, struct-η, unit-like types, K, quotients, Nat/String literals) — only the objects differ.

Values live for a session of many declarations: a constant’s type, its unfolded body, the weak-head normal form of a closed application are computed once and shared by every later declaration, until the session’s arena outgrows its budget or the environment changes the meaning of something already evaluated (see Kernel::sem_epoch).

A variable is identified by its binder depth and its type, so the variable a check binds and the variable a later comparison binds at the same depth with the same type are one value, and everything known about one is known about the other. That identification is sound exactly when no two variables in scope share a depth — the one invariant Sem::bind keeps.

Modules

conv

Definitional equality of values: Lean’s algorithm, in the classic engine’s order of attempts.

eval

Evaluation: terms to values, application, and the values of constants.

infer

Type inference and checking over values.

table

The value engine’s hash tables: open addressing with linear probing over small Copy keys and u32 values, one slot per cache line access, Fibonacci-hashed.

types

The types of values, for the parts of conversion and reduction that look at types — proof irrelevance, η, struct-η, unit-like types, K — and for projections. Values reaching here are well-typed, so this is inference without checking: a head’s type followed along the spine.

value

Semantic values and the arena that interns them.

whnf

Weak-head reduction of values: ι (recursors, with K and struct-η), quotients, projections, validated Nat literal operations, and δ through constant heads.

Structs

Counters

How the session’s caches are doing (reported by logos_kernel --stats).

Sem

The engine: the kernel (environment, stores, well-known names) and the session state.

State

One session’s values and caches.