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 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 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.)

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.

Get the internal QName for the name of a record constructor. If the name does not refer to a record type, Nothing is returned.

Create a ImportedNameMap.

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

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

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.

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.)

Record (ha) that a given record has the specified constructor name.

Clear the scope of any no names.

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

Check that an import directive doesn't contain repeated names.

Check that the newly added variable have unique names.

Run a computation without changing the local variables.

A finite map for ImportedNames.