Documentation

Staying names.

Changing names.

A name either stays or disappears.

Annotation for a binding saying "supposed to disappear".

Annotation for a bound variable saying "supposed to disappear".

Annotation for an out-of-scope variable saying "supposed to stay out of scope".

Annotation for a free variable saying "supposed to stay free".

Reference the provided variable in the provided type/term as an in-scope one.

Reference the provided variable in the provided type/term as an out-of-scope one.

Each kind of old and new names.

A ScopeInfo is a set of ScopedNames for each of the ScopeEntry. If a ScopeEntry is not present in the map, the corresponding set of ScopeNames is considered to be empty.

Extract the set stored in the provided ScopeInfo at the provided ScopeEntry.

Check if a set is empty and report an error with the set embedded in it otherwise.

Merge two ScopeInfos checking that binders in them do not intersect along the way.

Whether it's OK if the pass removes bindings. A renamer isn't supposed to do that, but for example an inliner may do it, since it's basically the entire point of an inliner.

Take a constructor for a binder, a name bound by it, a sort (kind/type), a value of that sort (type/term) and call establishScoping on both the sort and its value and reassemble the original binder with the annotated sort and its value, but also decorate the reassembled binder with one out-of-scope variable and one in-scope one.

Every kind of error thrown by the scope checking machinery at different stages.

Override the set at the provided ScopeEntry to contain only the provided ScopedName.

Use a Stays to handle an unchanged old name.

Use a Disappears to handle differing old and new names.

Use a NameAction to handle an old and a new name.

Use a NameAnn to handle a new name.

Check that each kind of Set from ScopeInfo relates to all other ones in a certain way. We start with these three relations that are based on the assumption that for each binder we add at least one out-of-scope variable and at least one in-scope one:

1. disappeared bindings should be the same as stayed out of scope variables (ensures that old bindings disappear via renaming and not via removal)
2. disappeared bindings should be the same as disappeared variables (ensures that old names consistently disappear at the binding and use sites)
3. appeared bindings should be the same as appeared variables (ensures that new names consistently appear at the binding and use sites)

Once we've ensured all of that, we're left with only three sets and 3C2 equals 3, so we only need to consider three more relations:

1. disappeared bindings should not intersect with free variables (an internal sanity check)
2. appeared bindings should not intersect with disappeared bindings
3. appeared bindings should not intersect with free variables

The last two ensure that no new name has an old name's unique.

The type of errors that the scope checking machinery returns.

Check if a pass respects scoping.

Returns the thing that the scoping tests run on, the result of the pass and the scope checking outcome, respectively.