Agda.Syntax.Scope.Base

A scope is a named collection of names partitioned into public and private names.

See Access.

Get a NameSpace from Scope.

A lens for scopeNameSpaces

`Monadic' lens (Functor sufficient).

The complete information about the scope at a particular program point includes the scope stack, the local variables, and the context precedence.

For the sake of highlighting, the _scopeInverseName map also stores the KindOfName of an A.QName.

Local variables.

For each bound variable, we want to know whether it was bound by a λ, Π, module telescope, pattern, or let.

A local variable can be shadowed by an import. In case of reference to a shadowed variable, we want to report a scope error.

Shadow a local name by a non-empty list of imports.

Treat patternBound variable as a module parameter

Project name of unshadowed local variable.

Get all locals that are not shadowed by imports.

Lenses for ScopeInfo components

Lens for scopeVarsToBind.

Lens for scopeLocals.

A NameSpace contains the mappings from concrete names that the user can write to the abstract fully qualified names that the type checker wants to read.

Set of types consisting of exactly AbstractName and AbstractModule.

A GADT just for some dependent-types trickery.

Type class for some dependent-types trickery.

inNameSpace selects either the name map or the module name map from a NameSpace. What is selected is determined by result type (using the dependent-type trickery).

Non-dependent tag for name or module.

For the sake of parsing left-hand sides, we distinguish constructor and record field names from defined names.

For ambiguous constructors, we might have both alternatives of Induction. In this case, we default to ConName.

For ambiguous constructors, we might have both alternatives of Induction. In this case, we default to Inductive.

Only return [Co]ConName if no ambiguity.

A set of KindOfName, for the sake of elemKindsOfNames.

Decorate something with KindOfName

Where does a name come from?

This information is solely for reporting to the user, see whyInScope.

A decoration of QName.

A decoration of abstract syntax module names.

Van Laarhoven lens on anameName.

Van Laarhoven lens on amodName.

Why is a resolved name ambiguous? What did it resolve to?

Invariant (statically enforced): At least two resolvents in total.

The flat list of ambiguous names in AmbiguousNameReason.

The empty name space.

Map functions over the names and modules in a name space.

Zip together two name spaces.

Map monadic function over a namespace.

The empty scope.

The empty scope info.

Map functions over the names and modules in a scope.

Same as mapScope but applies the same function to all name spaces.

Same as mapScope but applies the function only on the given name space.

Map monadic functions over the names and modules in a scope.

Same as mapScopeM but applies the same function to both the public and private name spaces.

Zip together two scopes. The resulting scope has the same name as the first scope.

Same as zipScope but applies the same function to both the public and private name spaces.

Recompute the inScope sets of a scope.

Filter a scope keeping only concrete names matching the predicates. The first predicate is applied to the names and the second to the modules.

Return all names in a scope.

Look up a single name in the current scope.

This is equivalent to Map.lookup n . allNamesInScope', but more efficient when only a single name needs to be looked up.

Returns the scope's non-private names.

Merge two scopes. The result has the name of the first scope.

Merge a non-empty list of scopes. The result has the name of the first scope in the list.

Move all names in a scope to the given name space (except never move from Imported to Public).

Update a particular name space.

Modify a particular name space.

Add a name to a scope.

Remove a name from a scope. Caution: does not update the nsInScope set. This is only used by rebindName and in that case we add the name right back (but with a different kind).

Add a module to a scope.

When we get here we cannot have both using and hiding.

Apply an ImportDirective to a scope:

1. rename keys (C.Name) according to renaming;

2. for untouched keys, either of

a) remove keys according to hiding, or b) filter keys according to using.

Both steps could be done in one pass, by first preparing key-filtering functions C.Name -> Maybe C.Name for defined names and module names. However, the penalty of doing it in two passes should not be too high. (Doubling the run time.)

Version of applyImportDirective that also returns sets of name and module name clashes introduced by renaming to identifiers that are already imported by using or lack of hiding.

Rename the abstract names in a scope.

Remove private name space of a scope.

Should be a right identity for exportedNamesInScope. exportedNamesInScope . restrictPrivate == exportedNamesInScope.

Remove private things from the given module from a scope.

Filter privates out of a ScopeInfo

Disallow using generalized variables from the scope

Add an explanation to why things are in scope.

Get the public parts of the public modules of a scope

Get all concrete names in scope. Includes bound variables.

Look up a name in the scope

Find the concrete names that map (uniquely) to a given abstract qualified name. Sort by number of modules in the qualified name, unqualified names first.

A version of inverseScopeLookupName that also delivers the KindOfName. Used in highlighting.

Find the concrete names that map (uniquely) to a given abstract module name. Sort by length, shortest first.

Set the nameBindingSite in an abstract name.

Add first string only if list is non-empty.