Agda-2.2.10: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.Syntax.Scope.Monad
Contents
The scope checking monad
Errors
General operations
Names
Resolving names
Binding names
Module manipulation operations
Description
The scope monad with operations.
Synopsis
type ScopeM = TCM
notInScope :: QName -> ScopeM a
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 :: ModuleName -> ScopeM ()
modifyScopeInfo :: (ScopeInfo -> ScopeInfo) -> ScopeM ()
modifyScopes :: (Map ModuleName Scope -> Map ModuleName Scope) -> ScopeM ()
modifyNamedScope :: ModuleName -> (Scope -> Scope) -> ScopeM ()
modifyCurrentScope :: (Scope -> Scope) -> ScopeM ()
modifyNamedScopeM :: ModuleName -> (Scope -> ScopeM Scope) -> ScopeM ()
modifyCurrentScopeM :: (Scope -> ScopeM Scope) -> ScopeM ()
modifyCurrentNameSpace :: NameSpaceId -> (NameSpace -> NameSpace) -> ScopeM ()
setContextPrecedence :: Precedence -> ScopeM ()
getContextPrecedence :: ScopeM Precedence
withContextPrecedence :: Precedence -> ScopeM a -> ScopeM a
getLocalVars :: ScopeM LocalVars
setLocalVars :: LocalVars -> ScopeM ()
withLocalVars :: ScopeM a -> ScopeM a
freshAbstractName :: Fixity' -> Name -> ScopeM Name
freshAbstractName_ :: Name -> ScopeM Name
freshAbstractQName :: Fixity' -> Name -> ScopeM QName
data ResolvedName
= VarName Name
| DefinedName AbstractName
| ConstructorName [AbstractName]
| UnknownName
resolveName :: QName -> ScopeM ResolvedName
resolveModule :: QName -> ScopeM AbstractModule
getFixity :: QName -> ScopeM Fixity'
bindVariable :: Name -> Name -> ScopeM ()
bindName :: Access -> KindOfName -> Name -> QName -> ScopeM ()
bindModule :: Access -> Name -> ModuleName -> ScopeM ()
bindQModule :: Access -> QName -> ModuleName -> ScopeM ()
stripNoNames :: ScopeM ()
type Ren a = Map a a
type Out = (Ren ModuleName, Ren QName)
type WSM = StateT Out ScopeM
copyScope :: ModuleName -> Scope -> ScopeM (Scope, (Ren ModuleName, Ren QName))
applyImportDirectiveM :: QName -> ImportDirective -> Scope -> ScopeM Scope
openModule_ :: QName -> ImportDirective -> ScopeM ()
The scope checking monad
type ScopeM = TCMSource
To simplify interaction between scope checking and type checking (in particular when chasing imports), we use the same monad.
Errors
notInScope :: QName -> ScopeM aSource
General operations
getCurrentModule :: ScopeM ModuleNameSource
setCurrentModule :: ModuleName -> ScopeM ()Source
withCurrentModule :: ModuleName -> ScopeM a -> ScopeM aSource
withCurrentModule' :: (MonadTrans t, Monad (t ScopeM)) => ModuleName -> t ScopeM a -> t ScopeM aSource
getNamedScope :: ModuleName -> ScopeM ScopeSource
getCurrentScope :: ScopeM ScopeSource
createModule :: ModuleName -> ScopeM ()Source
Create a new module with an empty scope
modifyScopeInfo :: (ScopeInfo -> ScopeInfo) -> ScopeM ()Source
Apply a function to the scope info.
modifyScopes :: (Map ModuleName Scope -> Map ModuleName Scope) -> ScopeM ()Source
Apply a function to the scope map.
modifyNamedScope :: ModuleName -> (Scope -> Scope) -> ScopeM ()Source
Apply a function to the given scope.
modifyCurrentScope :: (Scope -> Scope) -> ScopeM ()Source
Apply a function to the current scope.
modifyNamedScopeM :: ModuleName -> (Scope -> ScopeM Scope) -> ScopeM ()Source
Apply a monadic function to the top scope.
modifyCurrentScopeM :: (Scope -> ScopeM Scope) -> ScopeM ()Source
modifyCurrentNameSpace :: NameSpaceId -> (NameSpace -> NameSpace) -> ScopeM ()Source
Apply a function to the public or private name space.
setContextPrecedence :: Precedence -> ScopeM ()Source
getContextPrecedence :: ScopeM PrecedenceSource
withContextPrecedence :: Precedence -> ScopeM a -> ScopeM aSource
getLocalVars :: ScopeM LocalVarsSource
setLocalVars :: LocalVars -> ScopeM ()Source
withLocalVars :: ScopeM a -> ScopeM aSource
Run a computation without changing the local variables.
Names
freshAbstractName :: Fixity' -> Name -> ScopeM NameSource
Create a fresh abstract name from a concrete name.
freshAbstractName_ :: Name -> ScopeM NameSource
freshAbstractName_ = freshAbstractName defaultFixity
freshAbstractQName :: Fixity' -> Name -> ScopeM QNameSource
Create a fresh abstract qualified name.
Resolving names
data ResolvedName Source
Constructors
VarName Name
DefinedName AbstractName
ConstructorName [AbstractName]
UnknownName
resolveName :: QName -> ScopeM ResolvedNameSource
Look up the abstract name referred to by a given concrete name.
resolveModule :: QName -> ScopeM AbstractModuleSource
Look up a module in the scope.
getFixity :: QName -> ScopeM Fixity'Source
Get the fixity of a name. The name is assumed to be in scope.
Binding names
bindVariable :: Name -> Name -> ScopeM ()Source
Bind a variable. The abstract name is supplied as the second argument.
bindName :: Access -> KindOfName -> Name -> QName -> ScopeM ()Source
Bind a defined name. Must not shadow anything.
bindModule :: Access -> Name -> ModuleName -> ScopeM ()Source
Bind a module name.
bindQModule :: Access -> QName -> ModuleName -> ScopeM ()Source
Bind a qualified module name. Adds it to the imports field of the scope.
Module manipulation operations
stripNoNames :: ScopeM ()Source
Clear the scope of any no names.
type Ren a = Map a aSource
type Out = (Ren ModuleName, Ren QName)Source
type WSM = StateT Out ScopeMSource
copyScope :: ModuleName -> Scope -> ScopeM (Scope, (Ren ModuleName, Ren QName))Source
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.
applyImportDirectiveM :: QName -> ImportDirective -> Scope -> ScopeM ScopeSource
Apply an importdirective and check that all the names mentioned actually exist.
openModule_ :: QName -> ImportDirective -> ScopeM ()Source
Open a module.
Produced by Haddock version 2.6.1