# 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: 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.

## `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; body; }` 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 `VLam`s 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.

`bodyVal` is preserved on the stamp so `quote` can emit
`T.mkCanonApp id params body`. `canonRefConv` compares stamps
by `(id, params)` only; `body` is conv-irrelevant.

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`. Forces a deferred `VThunkTm` first (the VThunkTm read-site invariant), as `vAppF` does, so the direct evaluator opening a machine-built closure env never reads a thunk's `.tag`._

```
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`. Forces a deferred `VThunkTm` first (the VThunkTm read-site invariant), as `vAppF` does, so the direct evaluator opening a machine-built closure env never reads a thunk's `.tag`._

```
vSnd : Val -> Val
```