Eval

Pure evaluator: interprets kernel terms in an environment of values. Zero effect system imports — part of the trusted computing base (TCB).

Core Functions

eval : Env → Tm → Val — evaluate with default fuel (10M steps)
evalF : Int → Env → Tm → Val — evaluate with explicit fuel budget
instantiate : Closure → Val → Val — apply a closure to an argument

Elimination Helpers

vApp : Val → Val → Val — apply a function value (beta-reduces VLam, extends spine for VNe)
vFst, vSnd — pair projections
vBootSumElim — sum elimination
vBootJ — identity elimination (computes to base on VBootRefl)

Trampolining

Generated desc-con chains use builtins.genericClosure to flatten recursive structures iteratively, guaranteeing O(1) stack depth on deep generated recursive data.

Each evalF call decrements a fuel counter. When fuel reaches 0, evaluation throws "normalization budget exceeded". This bounds total work and prevents unbounded computation in the Nix evaluator. Default budget: 10,000,000 steps.

`descView`

descView: default-fuel one-step semantic view of a description value — return { tag = "DView{Ret,Arg,Rec,Pi,Plus}"; idx; ...payload } selecting the description's outer constructor.

descView : Val -> { tag : DViewTag; idx : Int; ... } | null

Dispatches on both primitive VDescX shapes and encoded VDescCon shapes uniformly. The idx field gives the summand position (0 = ret, 1 = arg, 2 = rec, 3 = pi, 4 = plus). Primary consumer is check.nix's desc-con trampoline, which uses the view to detect plus-coproduct shapes with linear recursion. Returns null for VNe or values whose _canonRef is opaque.

`eval`

eval: default-fuel wrapper around evalF; spends from the defaultFuel (10M-step) budget. The canonical evaluator entry for kernel consumers.

eval : Env -> Tm -> Val

`evalF`

evalF: kernel-term evaluator. Routes through the depth-budgeted hybrid in tc/eval/direct.nix: direct mkValueF recursion for shallow structural terms, the CEK machine (tc/eval/machine.nix) at budget exhaustion and for the tags that must see machine-internal Val tags (notably VLazyDescIndAccLayer). mkValueF remains exported for overlays (notably tc/elaborate/eval-overlay.nix) that compose their own self-table with VMeta-aware dispatch.

evalF : Int -> Env -> Tm -> Val

`instantiate`

instantiate: default-fuel closure application — given Closure { env; body; } and an argument Val, evaluate the body in the extended environment.

instantiate : Closure -> Val -> Val

`linearProfile`

linearProfile: default-fuel linear-recursion classifier — given a description value D, return a list of pre-rec field types if D is a descArg-chain ending in descRec descRet; null if D is non-linear (tree, multi-rec, or non-plus).

linearProfile : Val -> [{ S : Val; ... }] | null

Walks the descArg/descRec chain via descView; succeeds when every pre-rec field is descArg and the tail is exactly descRec descRet. Used by check.nix's desc-con trampoline to detect when a plus-coproduct A + B has exactly one linear-recursive summand — the case where chain peeling applies and 5000+ layers can be checked without recursion.

`machine`

fx.tc.eval.machine: CEK abstract machine. runMachineF is the defunctionalized form of evalF; runQuoteF is the symmetric read-back driver consumed by tc/quote.nix.

`mkDescDescAppV`

mkDescDescAppV: default-fuel canonical descDesc iLev I L-value constructor — produces the levitated description-of-descriptions value, cached and shared across the kernel for index I at universe iLev and level L.

mkDescDescAppV : Val -> Val -> Val -> Val  -- iLev, I, L

`mkValueF`

mkValueF: dispatch-algebra-parameterized core evaluator body. Kernel instantiates mkValueF self; overlays (notably tc/elaborate/eval-overlay.nix) instantiate with their own self-table to thread VMeta-aware dispatch through closure bodies, preserving kernel-purity (Abel-Pientka 2011, section 2; see tc/elaborate/value.nix:13-17).

mkValueF : Self -> Int -> Env -> Tm -> Val

`sumPayloadTmView`

sumPayloadTmView: term-level sum-payload view — given a Tm that is boot-inl/boot-inr or a sum-shaped desc-con with _descConCert, return { side; value; rebuild; rebuildVal; } to drive the desc-con trampoline's payload walker; null for non-sum shapes.

sumPayloadTmView : Tm -> { side : "inl" | "inr"; value : Tm; rebuild : Tm -> Tm; rebuildVal : (Tm -> Val) -> Val -> Val; } | null

`sumPayloadValView`

sumPayloadValView: value-level sum-payload view — given a Val that is VBootInl/VBootInr or a sum-shaped VDescCon with _descRef, return { side; value; rebuild; } for use in the desc-con trampoline; null for non-sum shapes.

sumPayloadValView : Val -> { side : "inl" | "inr"; value : Val; rebuild : Val -> Val; } | null

`vAllD`

vAllD: default-fuel allD L I D K X M i d — the type expressing that every recursive position in description-payload d (at index i) satisfies motive M.

vAllD : Val -> Val -> Val -> Val -> Val -> Val -> Val -> Val -> Val

`vApp`

vApp: default-fuel kernel function-application value — beta-reduces VLam, extends the spine for VNe, threads through VDescViewFn.

vApp : Val -> Val -> Val

`vBootJ`

vBootJ: J-eliminator over VBootEq — on VBootRefl returns the base case (checker has already verified the sides match); on VNe extends the spine with an eBootJ frame.

vBootJ : Val -> Val -> Val -> Val -> Val -> Val -> Val

Arguments are type lhs motive base rhs eq. When eq is VBootRefl, returns base directly — the checker has already verified lhs ≡ rhs, so rhs is unused. When eq is VNe, preserves rhs in the EBootJ spine frame so quotation can reconstruct the stuck term. Any other shape is rejected with an internal error.

`vBootSumElim`

vBootSumElim: default-fuel boot-sum eliminator — dispatches VBootInl to onLeft and VBootInr to onRight; extends the spine on VNe.

vBootSumElim : Val -> Val -> Val -> Val -> Val -> Val -> Val

`vDescInd`

vDescInd: default-fuel generic eliminator for description-based indexed inductives — ind D P step i (con d) = step i d (everywhere D D P (lam j x. ind D P step j x) i d).

vDescInd : Val -> Val -> Val -> Val -> Val -> Val

Arguments: description D, motive P : (i:I) -> mu D i -> U, step function step, target index i, scrutinee (a VDescCon or VNe). On VDescCon, builds the inductive hypothesis as a self-reference closure over step/motive/D/I, feeds the canonical mu D family to vEverywhereDF, and applies step i d (everywhereResult). On VNe, extends the spine with eDescInd D motive step i. The motive must be a VLam so I is recoverable from its domain annotation.

`vEverywhereD`

vEverywhereD: default-fuel everywhereD L I D K X M ih i d — apply inductive hypothesis ih at every recursive position of d, producing the allD witness consumed by vDescInd.

vEverywhereD : Val -> Val -> Val -> Val -> Val -> Val -> Val -> Val -> Val -> Val

`vFst`

vFst: kernel pair-projection — return the first component of a VPair; extend the spine with eFst on a stuck VNe.

vFst : Val -> Val

`vInterpD`

vInterpD: default-fuel description interpretation — given L_val I_val D X i, compute the type interp I D X i whose values are layers of the recursive datatype determined by D.

vInterpD : Val -> Val -> Val -> Val -> Val -> Val

`vLiftElimF`

vLiftElimF: kernel lower eliminator — idempotent at convLevel l m; β-reduces lower _ (lift _ a) -> a on VLiftIntro; appends ELiftElim to a stuck VNe spine.

vLiftElimF : Val -> Val -> Val -> Val -> Val -> Val

`vLiftF`

vLiftF: kernel Lift l m eq A type-former value — the type of values of A : U(l) transported up to U(m); collapses idempotently when convLevel l m and composes nested Lifts.

vLiftF : Val -> Val -> Val -> Val -> Val

Idempotence: Lift l l _ A ≡ A for homogeneous code — returns A directly when convLevel l m. Composition: Lift l m _ (Lift l' l _ A') ≡ Lift l' m _ A' — flattens by lowering the inner level. The witness slot eq is irrelevant on collapse since both bound conditions hold by transitivity; emit vBootRefl for the composed form.

`vLiftIntroF`

vLiftIntroF: kernel liftIntro value former — wraps a : A as a VLift l m _ A-typed value; idempotent at convLevel l m, and η-reduces a stuck lower-spine via lift _ (lower _ x) ≡ x.

vLiftIntroF : Val -> Val -> Val -> Val -> Val -> Val

Witness-irrelevance is enforced structurally: levels are compared via convLevel and the carried A via syntactic equality. The spine's eq field is not consulted. The η-reduction inspects the tail of a VNe spine for an ELiftElim frame whose parameters match; on hit, drops the frame to yield the inner stuck term.

`vSnd`

vSnd: kernel pair-projection — return the second component of a VPair; extend the spine with eSnd on a stuck VNe.

vSnd : Val -> Val