rocq/backend/Compile.v
# From an unchecked module to its lines
As main.pl's compile command for a Fil-C module, without -O: the module is pizlonated (Pizlonate.v), read as the model's syntax (Transport.v), judged by the model's validator (Validate.v), and its lines are those of EmitModule.v. Nothing of Prolog is in the path; the gate (tests/compile.sh) holds the printed lines to those of nanofilcompile.
Two things the Prolog compiler does are not done here, so it refuses some modules that compile takes:
- It runs
valid_module/1on the module as written, before pizlonation. Here only the checked module is judged. - It checks the
context/2items (provenance's records), which pizlonation drops here.
The lines of a module both take are the same.
compile_promoted is main.pl's compile − promoted command: before pizlonation the module is promoted (Promote.v) and its copies are propagated (Copy.v), and the emission selects its branches (Emit.v). The same gate, with COMMAND=compile-promoted, holds its lines to those of nanofilcompile − promoted.
What becomes of a module.
| | | Refused | why : string | |
Not a valid module: the Prolog compiler refuses it too. | |||
| | | Outside | why : string | |
A module this compiler does not take, though it may be valid. | |||
| | | Pieces | ps : listunit → optionlistlistline | |
Its lines, a piece at a time (module_pieces). A piece is nothing for a function the backend builds no plan for.
Whether the item is not a function, or is one named by an atom. ir.pl's validator takes any term as a name, and the Prolog emission throws at a function whose name is not an atom, since the name is also a string of the function's origin.
The lines of the unchecked Fil-C module m, its branches selected or not: pizlonated, read as the model's syntax, judged and emitted. Outside if it has a function outside the core subset, which the validator cannot judge.
The module m, as read, compiled. A plain module is outside: its backend (amd64.pl) is not ported.
With promoted, as optimize(passes([promote, copy])) and emit(stack, selected, call): the module is promoted (Promote.v), its copies are propagated (Copy.v), and its branches are selected (Emit.v). Whether the module is plain is asked of the module as read, as main.pl's compile asks it, since promotion can remove every pointer.
As nanofilcompile without -O.
With promotion, copy propagation and selected branches.
The lines of an unchecked Fil-C module compiled with whole-function register allocation and direct register selection (Regs.v).
A module of one function that returns its argument is taken, and one with no pointer and no outside call is plain.
Proof 1 step Qed
Proof 1 step Qed
A use with no definition is refused.
Proof 1 step Qed
A function named by a term that is not an atom is refused.