What the machinery here can report. The type is parametric in the spelling, as the tables are, and a Functor over it.

Since: 0.4.0

Render an error, given a renderer for the spellings.

Since: 0.4.0

A term as stored: canonical bytes. Equality of stored terms is byte equality, which is what a canonical-artifact property tests.

Since: 0.4.0

Store a term verbatim, through the instances of Control.Monad.Free.Foil.Binary.

The disjoint layout is what makes verbatim enough. A constant's spelling goes into the unit's table (termSpellings), and a local needs no table: its id is expected to be canonical, which it is when elaboration allocates locals in a region of their own.

Since: 0.4.0

Decode a stored term's bytes: the instances alone, no meaning yet. Meaning is given per unit, by constantRelocation and relocateConstants.

Since: 0.4.0

The spelling-table entries a term needs. Its free variables are exactly its constants, provided the stored declaration is closed over everything local. Each is mapped to its spelling from the display table.

Note that the table should cover the referenced constants and only those. A table of everything in scope would let an unused import dirty a dependant's content hash, and would differ between build schedules.

Since: 0.4.0

The names a term's binders bind: what a unit's locals range covers. Note that supportOf cannot see them, since they are bound and not free.

Since: 0.4.0

The tightest range covering the given names, or Nothing for none. The caller picks its own convention for the empty range.

>>> spanOfNames [7, 3, 5]
Just (NameRange {nameRangeLo = 3, nameRangeHi = 7})

Since: 0.4.0

A unit's recorded name layout: the actual names of its own constants, and of its locals. The two travel together, so that they cannot be mixed up with the ranges of the loading world. An artifact records them as one field, and the checks and the relocation consume them as one value.

Since: 0.4.0

How many names a range holds.

>>> nameRangeSize (NameRange 3 5)
3

Since: 0.4.0

Whether a raw name lies in a range.

Since: 0.4.0

Whether two ranges share a name. An empty range overlaps nothing.

>>> nameRangesOverlap (NameRange 0 4) (NameRange 4 9)
True
>>> nameRangesOverlap (NameRange 0 4) (NameRange 5 9)
False

Since: 0.4.0

The checks a unit's recorded layout admits, judged from metadata alone. The constants and locals ranges must not overlap, no spelling may be recorded for a local, and the constants range must hold exactly one name per declaration, since allocation is dense from the range's low end.

>>> layout = StoredLayout (NameRange (-10) (-9)) (NameRange 0 5)
>>> checkStoredLayout layout (Map.fromList [(-20, "P.base")]) 2
Right ()
>>> checkStoredLayout layout (Map.fromList [(3, "q")]) 2
Left (SpellingForLocal 3)

Since: 0.4.0

What a unit's constants need in the loading world, judged once, from the spelling table alone. Nothing says every constant already has the id its spelling means here, which is the fast path, on which no term is walked at all. Otherwise the result is the renaming to apply. Its domain is a scope of the unit's world, which no longer exists, so its index is the caller's phantom.

The unit's own constants (table entries inside the recorded range) do not consult the world: they are being loaded right now, in the same order they were allocated, so their relocation is the affine shift between the recorded range and the one this run assigned. Their new names are thereby minted ahead of their allocation, which the caller's trust covers. An imported constant resolves by its spelling, and one this world does not know is reported. Finally, no relocation target may land among the locals, since verbatim locals rest on the two never meeting.

Since: 0.4.0

Rename every constant reference through the map, moving the term from the unit's world into the loading one. This is the restriction to constants of a general renaming Name n -> Name n'. sinkabilityProof embodies the general renaming, but its efficient implementations degenerate the renaming to a coercion under binders, which is sound only for inclusions, whereas this walk carries an arbitrary map through.

The invariant that lets the walk ignore the binders is the disjointness the recorded layout certifies: every name in the map's domain is a constant, and a binder binds locals, so no binder can shadow a name in the domain and no local can be in it. Note that this covers imported constants too, since checkStoredLayout refuses a spelling for any name among the locals. Thus the map never needs extending under a binder, and locals and patterns cross by coercion. A constant outside the map (bytes referencing something the spelling table does not cover) is re-minted unchanged, trusted like everything else about the term. Note that a map that is the identity on raw ids would make the whole walk a coercion, which is why constantRelocation reports it as no relocation at all.

Since: 0.4.0