Expand description
Turning a checked package into the executable IR.
This reads the answers cove-sema already settled and writes them down
as slots and instructions. It re-derives nothing: an expression’s type
comes from Facts::ty, a declaration’s boundary
from Facts::signature, and where the two
could disagree the checker is right by construction because this asked it
rather than working it out again.
§There is no refusal
A valid checked program lowers. That is the whole contract, and it is
what ADR 0034
replaces the predecessor’s admission predicate with. The two ways this
can answer Err are the two gap module builds — an unsettled type and
a construct this crate has not been taught yet — and neither is a
judgement about the program.
§A value is a run of words, and the lowering is what knows how many
docs/LINEAR_VM.md puts the fields of a struct where the value is, so
l.from.x is a slot number this module computes and not an instruction
the machine runs. A field access on an inline value is arithmetic on a
slot, and only a field of a heap object is a load. That is why
Val is a base slot and a layout rather than a slot and a Repr: the
layout is what a copy’s width, a location’s reference words and a field’s
offset are all read off.
§A generic is one function per instantiation
docs/LINEAR_VM.md says why there was no choice: a slot’s Repr is fixed
for the whole function, that is what makes one static reference map
correct at every program counter, and a generic value’s width is a fact
about the type argument — Cell<Int> is one word and Cell<Point> is
two. Carrying layouts at run time would make widths dynamic and take the
map with them; boxing every generic value would allocate on f(1) and
make a type parameter mean what dyn Trait already means. So f<Int> and
f<Point> are two functions and two frames, and a generic struct at two
instantiations is two layouts.
It costs one substitution and no second walk. The checker walked the
generic body once with its type parameters rigid, so every fact in it is
recorded in terms of them, and Body::ty completes one as it is read.
Which arguments a call site asks for is read off the facts the checker
settled there — Body::instantiation is that reading, and it is also why
an explicit type argument needs no path of its own: the checker applied
it before this crate saw anything.
§The shape of a lowered body
Control flow is flat. There are no basic blocks and no block arguments:
an if is a Inst::BranchFalse over a run of instructions, a while
is a backward Inst::Jump, and both are emitted with an unpatchable
target that is filled in once the destination is known. A loop keeps the
jumps its breaks left behind and patches them when it learns where its
end is.
Every function ends in Inst::Return, and it is emitted
unconditionally — even after a body that already returned on every path.
That is one dead word, and what it buys is that every patched target
lands on an instruction: a branch whose destination is “after everything”
has something to be after. Tracking reachability well enough to drop it
would mean tracking which pending patches point past the end, which is
more machinery than the word is worth.
Functions§
- lower
- Lowers a checked package: every declaration it has, whether or not anything reaches it.
- lower_
entry - Lowers only the declarations
module.namecan reach. - lower_
roots - Lowers only the declarations
rootscan reach.