Dispatch

fx.tc.eval.dispatch: full kernel evaluator self-fixpoint. Consumed by overlay constructions (notably tc/elaborate/eval-overlay.nix) that need to build a meta-aware self-table replacing selected dispatch attrs while inheriting the rest.

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: core kernel-term evaluator — interpret a Tm in an environment of values to produce a Val, fuel-threaded so each step decrements until exhaustion throws "normalization budget exceeded".

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

Dispatches per tm.tag over the kernel-term ADT: variables, let, ann, all type formers (pi, sigma, boot-sum, boot-eq, mu, squash, primitives, universe), introduction forms (lam, pair, tt, boot-inl/boot-inr, boot-refl, squash-intro, literals, desc-con), and elimination forms (app, fst/snd, boot-sum-elim, boot-j, squash-elim, desc-ind, lift-elim).

Mutual recursion with vAppF / instantiateF (this file) and the description walkers vDescIndF / vInterpDF / vAllDF / vEverywhereDF (desc.nix) is closed by the kernel fixpoint through self. desc-con chains are trampolined via builtins.genericClosure so deep recursive data (5000+ layers) never blows the Nix evaluator stack.

Fuel is decremented once per recursive self.evalF call. The budget threads through all sub-evaluations; partial spending is bounded by the budget at the call site. Default budget (defaultFuel = 10000000) covers all in-repo workloads; tune only for experimental kernel-stress benchmarks.

Returns a Val with one of the kernel's value tags (VLam, VPi, VSigma, VPair, VTt, VBootSum, VBootInl, VBootInr, VBootEq, VBootRefl, VFunext, VSquash, VSquashIntro, VLift, VLiftIntro, VDesc, VMu, VDescCon, VU, primitive VString/VInt/..., VStringLit/..., VNe for stuck applications, VOpaqueLam for axiomatized lambdas). Unknown tags throw an internal error.

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.

mkCanonAppVF

mkCanonAppVF: value-level constructor for canon-app id params body-as-tagged-VDescCon — currying-applies body to params and stamps the result with _canonRef = { id; params; } so conv/quote short-circuit on the canonical identity instead of forcing .D.

mkCanonAppVF : Int -> String -> [Val] -> Val -> Val

Generic counterpart of mkDescDescAppVF for user-registered canonical descriptions. bodyVal is expected to be a curried chain of VLams that, after applying every element of paramVals, yields a VDescCon. The raw result's .D/.i/.d fields are reused; the _canonRef stamp takes precedence in conv and quote so the recursive .D slot is never forced.

Throws if the curried application does not produce a VDescCon — the smart-form's static contract.

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

mkDescDescAppVF

mkDescDescAppVF: value-level constructor for descDesc I L-as-tagged-VDescCon — builds the tagged shell before forcing the recursively computed fields so conv/quote can recognise the canonical reference without descending into the strong-levitation spiral.

mkDescDescAppVF : Int -> Val -> Val -> Val

Returns a VDescCon whose _canonRef = { id = "descDesc"; I; L; } marker lets conv/quote treat the value opaquely. Eliminators (descView, vInterpDF, ...) walk through descViewF's one-step semantic view of the same reference rather than forcing .D directly.

The underlying raw value is descDescVal I L evaluated via vAppF; its fields are reused but the canonical marker takes precedence in conv and quote. This separation enables sharing a single descDesc value across every recursive position in the kernel without re-evaluating the spiral.

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