Agda.Syntax.Scope.Monad

To simplify interaction between scope checking and type checking (in particular when chasing imports), we use the same monad.

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

Apply a function to the scope map.

Apply a function to the given scope.

Apply a monadic function to the top scope.

Apply a function to the current scope.

Apply a function to the public or private name space.

Run a computation without changing the local variables.

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

Check that the newly added variable have unique names.

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

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.

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.

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

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

Look up a module in the scope.

Get the fixity of a not yet bound name.

Get the polarities of a not yet bound name.

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

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

Bind a variable.

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

Bind a defined name. Must not shadow anything.

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

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.

Bind a module name.

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

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

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

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

Clear the scope of any no names.

Mark a name as being a copy in the TC state.

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.

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

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

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

Monadic for the sake of error reporting.

Translation of ImportDirective.

A finite map for ImportedNames.

Create a ImportedNameMap.

Apply a ImportedNameMap.

Translation of Renaming.

Open a module.

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