Module value 

Semantic values and the arena that interns them.

A value is what an expression means once its bound variables have values: a closure for a function or a Π, a neutral (a head and the arguments applied to it) for anything whose head cannot reduce further by β, a sort, or a literal. Nothing in a value is ever substituted.

Every value is interned. A neutral application f a is built once per pair of ids, a variable once per (level, type), a constant once per universe instantiation, an environment once per (parent, value): so two values built the same way from the same parts are the same id, and a result remembered for an id — its weak-head normal form, its type, a conversion answer — serves every place that builds it again. The per-value memos are plain arrays indexed by id, not hash maps.

Structs

Arena

All values of a checking session, their memos, and the tables that intern them.

CtxId

The types of the enclosing bound variables, innermost first (for inference under binders).

CtxNode

EnvId

An environment: the values of the enclosing bound variables, innermost first.

EnvNode

An environment node: either one entry consed onto a parent environment, or a frame — a pruned environment of len entries holding only the entries an expression can see, stored contiguously from val (an index into the frame slots). A narrow frame (every live index below 64) finds an entry by its rank in live; a wide frame keeps its live indices as a sorted list (wide, an index into the wide-index table) and finds an entry by search.

HeadId

Sp

The arguments applied to a neutral head, as a snoc list.

SpNode

V

Enums

Head

Kind

What a neutral’s head does under reduction.

Val

Constants

DEAD

The placeholder for an environment entry an expression cannot see: value 0 of every session, closed and inert (a neutral headed by the anonymous constant, which no declaration can be).

OPEN

The value mentions a variable bound by a binder being checked or compared.