Evidence that scope l extends scope n only within a set of reserved ranges: every name of l that is not a name of n lies inside one of them.

The evidence is built alongside allocation, with extWithinRefl at the start of a unit and extWithinStep at each binder, and composes along a chain of scopes with composeExtWithin. Its runtime content is the ranges, sorted and disjoint.

Since: 0.4.0

The reservations an ExtWithin is evidence about: sorted, disjoint, adjacent ranges coalesced, empty ones dropped.

Since: 0.4.0

A scope extends itself within any range: the extension is empty.

Note that this does not say the range is disjoint from the scope. It is withExtendScopeRange that checks that, because it allocates blindly.

Since: 0.4.0

Extend the evidence across one more binder, if its name lies inside one of the ranges. One membership test per range.

A binder allocated by withFreshIn at one of these ranges always passes. A binder allocated elsewhere, by withFresh or withRefreshed, is rejected with Nothing unless it happens to land inside them, so the evidence cannot be extended past a name that escapes the reservations.

>>> let range = NameRange 100 199
>>> withFreshIn range emptyScope (\b -> fmap extWithinRanges (extWithinStep b (extWithinRefl range)))
Just [NameRange {nameRangeLo = 100, nameRangeHi = 199}]

Since: 0.4.0

Compose evidence along a chain of scopes: if m extends n only within one set of ranges and l extends m only within another, then l extends n only within their union.

The bound is the union of the two sets and not their hull, so a reservation lying between them stays linkable. Adjacent ranges are coalesced, so a chain of units with consecutive stripes collapses back to a single range.

>>> extWithinRanges (composeExtWithin (extWithinRefl (NameRange 0 9)) (extWithinRefl (NameRange 30 39)))
[NameRange {nameRangeLo = 0, nameRangeHi = 9},NameRange {nameRangeLo = 30, nameRangeHi = 39}]
>>> extWithinRanges (composeExtWithin (extWithinRefl (NameRange 0 9)) (extWithinRefl (NameRange 10 19)))
[NameRange {nameRangeLo = 0, nameRangeHi = 19}]

Since: 0.4.0

A reservation in use: the range fresh names are allocated from, paired with the evidence that everything allocated since the base scope c lies within the unit's ranges.

The allocation range is always among the evidence's ranges, so stepping the evidence at a freshly allocated name cannot fail and withFreshInBlock is total. The two components are not redundant: the evidence is a normalised set bounding the whole extension, and once units are composed the range to allocate from can no longer be read off it.

Since: 0.0.1

Start a unit: no names allocated yet, so the evidence is trivial.

Since: 0.4.0

Resume allocating from a range once the evidence has grown past what a Block tracked by itself, after composing in a loaded unit's evidence with composeExtWithin. This is what lets an interactive unit keep allocating in its own reservation over the enlarged scope.

The allocation range must lie inside one of the evidence's ranges. The ranges are normalised, so covering is containment in a single one, and Nothing says the range is not covered.

>>> let grown = composeExtWithin (extWithinRefl (NameRange 0 9)) (extWithinRefl (NameRange 10 19))
>>> fmap blockRange (resumeBlock (NameRange 0 9) grown)
Just (NameRange {nameRangeLo = 0, nameRangeHi = 9})
>>> fmap blockRange (resumeBlock (NameRange 30 39) grown)
Nothing

Since: 0.4.0

The range withFreshInBlock allocates from.

Since: 0.4.0

The evidence accumulated so far: what a finished unit hands to withDisjointUnion, or to composeExtWithin for the next unit of a chain.

Since: 0.4.0

Allocate a fresh name in the block's range, stepping the evidence in the same motion. Fails with error only on an exhausted range, exactly as withFreshIn does.

>>> withFreshInBlock (beginBlock (NameRange 7 9)) emptyScope (\b block -> (nameId (nameOf b), extWithinRanges (blockExt block)))
(7,[NameRange {nameRangeLo = 7, nameRangeHi = 9}])

Since: 0.4.0

Extend a scope with the first k names of a range, in one step.

This is the bulk form of a unit's allocation, for loading a cached unit whose extension is known to be k consecutive names, or for pre-allocating a unit's names before checking its bodies. The range part of the scope must be empty, which is checked, so the extension is fresh by construction. Nothing reports an occupied range, and also a range with fewer than k names.

The continuation receives the extended scope, the binders in ascending order (for extending a NameMap in the same step), and the ExtWithin evidence. The scope extension is a dense fromRange, \(O(k/W)\).

>>> withExtendScopeRange emptyScope (NameRange 100 199) 3 (\_ binders _ -> rawNameBinderList binders)
Just [100,101,102]

Since: 0.4.0

Evidence that scope k is precisely the union of scopes n and m: every name of n and of m is a name of k, and nothing else is.

The extension constraints (Ext n k, Ext m k) state only the first half, since a strict superset of the union satisfies them too. The second half is what totality of a merged NameMap rests on, so unionNameMaps demands this witness. It comes from withDisjointUnion, which builds the union, or from checkScopeUnion, which tests for it.

Since: 0.4.0

Link two scopes that extend a common scope c within their respective reservations. The evidence check is one sweep over the two range sets; the scope union is one union.

Nothing when the two range sets overlap. The test is soundness and not an optimisation. The extensions n \ c and m \ c lie inside their respective range sets, so their disjointness is what guarantees that no raw name denotes two different variables in the union. The names the two scopes share are exactly the names of c, identified rather than renamed apart, which is what linking two units over a common import must do.

The continuation receives both extension facts at once, a ScopeUnion witness (which unionNameMaps requires), and the union's own ExtWithin, so that a linked unit is itself linkable and a whole build folds through this one function. It also receives Ext c k, which a caller cannot derive on the spot.

Since: 0.4.0

Test that a scope is precisely the union of two others, and produce the witness if so. \(O(n+m)\).

This is the union witness for the re-attachment path, where the union scope was rebuilt rather than handed down by withDisjointUnion. Like checkExtScope, it compares raw names across independently built scopes, and is meaningful only under a deterministic reservation policy.

Since: 0.4.0

Test that every name of one scope is a name of another, and mint the extension evidence if so. \(O(n+m)\) (isSubsetOf).

This is a trust boundary. The test compares raw names, and raw names from independently built scopes need not mean the same variable. The type system tracks meaning through binders, and this function goes around it deliberately, to re-attach a scope built elsewhere: in an earlier run, in a cache, or in a parallel session. It is sound only under the external discipline that a raw name has one global meaning, which a deterministic reservation policy provides. Nothing here checks that discipline, and the caller's allocator is what has to.

Since: 0.4.0

Union of two total maps into a map on the union of their scopes. Left-biased, like union.

The witness is what makes the result total on k. The inputs are total on n and m, and ScopeUnion says that k holds their names and no others. (It also determines k, which an extension constraint alone would leave open.)

What no witness can say is that the two maps agree on the names their scopes share. Linked units agree there when the shared part comes from the same checked imports, and the left bias then only ever chooses between equal entries.

Since: 0.4.0