rocq/backend/EmitModule.v
# The lines of a module
As filc_amd64.pl's module_emit/4 with every temporary in its stack slot: the lines of each item in order, then those of each weak thunk, then the end of the file. The gate (emit.sh) holds each list to the Prolog compiler's.
The lines of an item, a function's with selected branches or not. Nothing for a function the model keeps outside the core subset, or one the backend builds no plan for.
The end of the file: the stack is not executable.
The last piece of every module. It stands alone, with its type written out, because a C++ extraction cannot type a Some inside a function that is an element of a list.
A module's lists of lines, a piece at a time, in the order module_emit/4 gives them: a piece for each item, one for all the weak thunks and one for the end of the file. A driver asks for a piece, prints its lists and drops them before it asks for the next, so the lines of a whole module are never all alive. A piece is nothing if its item or a thunk has no lines.
The reference: no branch is selected.
The lists of lines of a module: every piece's. Nothing if some piece is nothing.