Apply an import directive and check that all the names mentioned actually exist.

Monadic for the sake of error reporting.

Bind a module name.

Bind a defined name. Must not shadow anything.

Bind a name. Returns the TypeError if exists, but does not throw it.

Bind a qualified module name. Adds it to the imports field of the scope.

Bind the pseudo-name constructor in the scope of the record module, mapping it to the (possibly anonymous) constructor of the record.

This is what makes R.constructor resolve: R is the record module and constructor an ordinary name in it, so no special treatment is needed when resolving the qualified name R.constructor.

Note that constructor is a keyword, thus, it can never be parsed as an unqualified name. In particular, open R does not make the record constructor accessible under the name constructor, and constructor cannot be mentioned in using, hiding or renaming.

This does not put the record constructor itself into the record module (which would be wrong, see issue #4189, since the record module is parameterized over the record value, but the constructor is not); it only adds this alias for it.

Bind a variable.

After collecting some variable names in the scopeVarsToBind, bind them all simultaneously.

Test if a given abstract name can appear with a suffix. Currently only true for the names of builtin sorts.

Warn about fixity declarations for targets that are non-operators or closed operators:

Warn about useless fixity declarations in renaming directives. Monadic for the sake of error reporting.

Collect the fixity/syntax declarations and polarity pragmas from the list of declarations and store them in the scope.

Mark a name as being a copy in the TC state, associating it with the given ScopeCopyRef for liveness information.

Create a new scope with the given name from an old scope. Renames public names in the old scope to match the new name and returns the renamings.

Create a new module with an empty scope. If the module is not new (e.g. duplicate import), don't erase its contents. (Just if it is a datatype or record module.)

Remove the record constructor pseudo-name from the scope of a record module.

The alias constructor is only meant to be used in the qualified form R.constructor, where R is the record module. Thus, it is not brought into scope by open R.

It is also not copied when the record module R itself is applied to arguments (as in module M = R): the record module is parameterized over the record value, but the record constructor is not (issue #4189). (When R is only copied as a submodule of the applied module, the constructor is copied correctly, since the arguments are then taken from the enclosing module.)

Create a fresh abstract name from a concrete name.

This function is used when we translate a concrete name in a binder. The Range of the concrete name is saved as the nameBindingSite of the abstract name.

freshAbstractName_ = freshAbstractName noFixity'

Create a fresh abstract qualified name.

Create a concrete name that is not yet in scope. | NOTE: See chooseName in Agda.Syntax.Translation.AbstractToConcrete for similar logic. | NOTE: See withName in Agda.Syntax.Translation.ReflectedToAbstract for similar logic.

Get the fixity of a not yet bound name.

Get the polarities of a not yet bound name.

Get the notation of a name. The name is assumed to be in scope.

Create a ImportedNameMap.

Is this the qualified name which refers to the constructor of a record (like Foo.constructor)?

If so, return the part of the name referring to the record (Foo).

This is only used to produce a good error message when Foo.constructor does not resolve; the resolution itself goes through the ordinary scope lookup, see bindRecordConstructorPseudoName.

Apply a ImportedNameMap.

Translation of ImportDirective.

Translation of Renaming.

Apply a function to the current scope.

Apply a function to the given scope.

Apply a function to the scope map.

Open a module, possibly given an already resolved module name.

Open a module.

Run a computation outside some number of local variables and add them back afterwards. This lets you bind variables in the middle of the context and is used when binding generalizable variables (#3735).

Rebind a name. Use with care! Ulf, 2014-06-29: Currently used to rebind the name defined by an unquoteDecl, which is a QuotableName in the body, but a DefinedName later on.

The pseudo-name constructor under which the constructor of a record is bound in the scope of the record module.

Since constructor is a keyword, this name is only reachable as the tail of a qualified name, e.g., R.constructor.

Look up a module in the scope.

Look up the abstract name referred to by a given concrete name.

Look up the abstract name corresponding to a concrete name of a certain kind and/or from a given set of names. Sometimes we know already that we are dealing with a constructor or pattern synonym (e.g. when we have parsed a pattern). Then, we can ignore conflicting definitions of that name of a different kind. (See issue 822.)

Clear the scope of any no names.

Temporarily unbind a variable. Used for non-recursive lets.

Check that the newly added variable have unique names.

Run a computation without changing the local variables.

A finite map for ImportedNames.