rocq/backend/PlanTerm.v
A plan as the term the Prolog compiler writes for it (filc_abi.pl's abi_function/10), and a module's thunks as its thunks(List). nanofilabi − terms prints both, so the plans Abi.v builds are compared with the Prolog compiler's as terms, on every function of the corpus.
Keys, words and cells
The atom of a term with no arguments.
As A − B, a pair.
The name of a pool: scalar, pointer or wide.
A key of a frame.
A return protocol: registers or buffer(N).
The source of a fast word.
As wf(K, Source).
As cell(I, K, Source, Lower): the lower of a value is lower(V), that of a saved word the saved(W) beside it, and none if the cell holds no pointer.
The channels of a fast result.
As result(R, Channels).
What a direct call invokes.
A getter.
Actions and instructions
An ABI action.
The place of a fused access: the checked pointer, or local(X, Off).
A fused access: the raw load or store, its proof replaced by its place.
An instruction after fusion.
An instruction of a plan.
The jump of a plan's block: a jump of the IR, or abi_return(Actions).
As block(L, Phis, Insts, Jump).
Public objects and thunks
As adapter_result(R, Channel, Size, packet(Copies, Zeros)).
A public object.
As thunk(F, Ref, Sig, Words, Cells, ArgsSize, Result, Need).
As thunks(List), what nanofilabi − terms prints last.
The plan
As abi_function(Name, Linkage, Ret, Sig, Frame, Entry, Blocks, Exit, Object, Origins). The entry receives the fast words and has no setjmp sites to snapshot; the exit is the exception's; the two origins, catching and not, count the roots and the named locals.