Skip to main content

Module lower

Module lower 

Source
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.name can reach.
lower_roots
Lowers only the declarations roots can reach.