Agda.Syntax.Scope.Monad

The scope monad with operations.

The scope checking monad

type ScopeM = TCM

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

Errors

isDatatypeModule :: ModuleName -> ScopeM Bool

General operations

getCurrentModule :: ScopeM ModuleName

setCurrentModule :: ModuleName -> ScopeM ()

withCurrentModule :: ModuleName -> ScopeM a -> ScopeM a

withCurrentModule' :: (MonadTrans t, Monad (t ScopeM)) => ModuleName -> t ScopeM a -> t ScopeM a

getNamedScope :: ModuleName -> ScopeM Scope

getCurrentScope :: ScopeM Scope

createModule :: Bool -> ModuleName -> ScopeM ()

Create a new module with an empty scope (Bool is True if it is a datatype module)

modifyScopeInfo :: (ScopeInfo -> ScopeInfo) -> ScopeM ()

Apply a function to the scope info.

modifyScopes :: (Map ModuleName Scope -> Map ModuleName Scope) -> ScopeM ()

Apply a function to the scope map.

modifyNamedScope :: ModuleName -> (Scope -> Scope) -> ScopeM ()

Apply a function to the given scope.

setNamedScope :: ModuleName -> Scope -> ScopeM ()

modifyNamedScopeM :: ModuleName -> (Scope -> ScopeM Scope) -> ScopeM ()

Apply a monadic function to the top scope.

modifyCurrentScope :: (Scope -> Scope) -> ScopeM ()

Apply a function to the current scope.

modifyCurrentScopeM :: (Scope -> ScopeM Scope) -> ScopeM ()

modifyCurrentNameSpace :: NameSpaceId -> (NameSpace -> NameSpace) -> ScopeM ()

Apply a function to the public or private name space.

setContextPrecedence :: Precedence -> ScopeM ()

getContextPrecedence :: ScopeM Precedence

withContextPrecedence :: Precedence -> ScopeM a -> ScopeM a

getLocalVars :: ScopeM LocalVars

modifyLocalVars :: (LocalVars -> LocalVars) -> ScopeM ()

setLocalVars :: LocalVars -> ScopeM ()

withLocalVars :: ScopeM a -> ScopeM a

Run a computation without changing the local variables.

Names

freshAbstractName :: Fixity' -> Name -> ScopeM Name

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_ :: Name -> ScopeM Name

freshAbstractName_ = freshAbstractName defaultFixity

freshAbstractQName :: Fixity' -> Name -> ScopeM QName

Create a fresh abstract qualified name.

Resolving names

data ResolvedName

Constructors

VarName Name

DefinedName Access AbstractName

FieldName AbstractName

record fields names need to be distinguished to parse copatterns

ConstructorName [AbstractName]

PatternSynResName AbstractName

UnknownName

Instances

Show ResolvedName

resolveName :: QName -> ScopeM ResolvedName

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

resolveName' :: [KindOfName] -> QName -> ScopeM ResolvedName

Look up the abstract name corresponding to a concrete name of a certain kind. 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.)

resolveModule :: QName -> ScopeM AbstractModule

Look up a module in the scope.

getFixity :: QName -> ScopeM Fixity'

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

Binding names

bindVariable :: Name -> Name -> ScopeM ()

Bind a variable. The abstract name is supplied as the second argument.

bindName :: Access -> KindOfName -> Name -> QName -> ScopeM ()

Bind a defined name. Must not shadow anything.

rebindName :: Access -> KindOfName -> Name -> QName -> ScopeM ()

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.

bindModule :: Access -> Name -> ModuleName -> ScopeM ()

Bind a module name.

bindQModule :: Access -> QName -> ModuleName -> ScopeM ()

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

Module manipulation operations

stripNoNames :: ScopeM ()

Clear the scope of any no names.

type Out = (Ren ModuleName, Ren QName)

type WSM = StateT Out ScopeM

copyScope :: QName -> ModuleName -> Scope -> ScopeM (Scope, (Ren ModuleName, Ren QName))

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.

Data and record types share a common abstract name with their module. This invariant needs to be preserved by copyScope, since constructors (fields) can be qualified by their data (record) type name (as an alternative to qualification by their module). (See Issue 836).

applyImportDirectiveM :: QName -> ImportDirective -> Scope -> ScopeM Scope

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

openModule_ :: QName -> ImportDirective -> ScopeM ()

Open a module.