Trampoline

fx.experimental.desc-interp.trampoline: qApp/run/handle interpreters trampolining FreeFx Desc values via genericClosure for O(1) stack depth on long chains.

handle

handle Eff Resp A { return?; handler; dispatch; state } prog — thin wrapper over run with a custom return clause folding the final (value, state) pair.

handle : Hoas U -> Hoas (U -> U) -> Hoas U -> { return?, handler, dispatch, state } -> Hoas (μ freeFxApp Eff Resp A) -> b

qApp

qApp Eff Resp q x — apply queue q to value x : Hoas q._index.X; trampolines Pure-returning leaves via genericClosure; on Impure splices the inner queue with the remaining tail. The queue's _index sidecar carries the (X, A) indexing that the kernel's μI U² slot witnesses.

qApp : Hoas U -> Hoas (U -> U) -> Hoas (μI U² kontQueueApp …) -> Hoas X -> Hoas (μ freeFxApp Eff Resp A)

qAppend

qAppend Eff Resp l r — concatenate two queues. Identity short-circuits on either side mirror queue.nix:append; otherwise builds qNode l r with the seam M = l._index.A (= r._index.X, asserted host-level by qNode). The composite queue inhabits μI U² kontQueueApp (l._index.X, r._index.A).

qAppend : Hoas U -> Hoas (U -> U) -> Hoas (μI U² kontQueueApp …) -> Hoas (μI U² kontQueueApp …) -> Hoas (μI U² kontQueueApp …)

run

run Eff Resp A { handler; dispatch } prog initialState — drive prog : μ(freeFxApp Eff Resp A) to completion via a genericClosure worklist; per Impure node, the kernel-resident handler term is applied to the op + threaded state via vApp, and the Nix-side dispatch interpreter reads the kernel-eval'd result to produce a step decision.

run : Hoas U -> Hoas (U -> U) -> Hoas U -> { handler; dispatch } -> Hoas (μ freeFxApp Eff Resp A) -> Hoas State -> { value; state }