| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

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
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 ()
renamedCanonicalNames :: ModuleName -> ModuleName -> Scope -> ScopeM (Map QName QName, Map ModuleName ModuleName)
type Ren a = Map a a
type Out = [Either (Ren ModuleName) (Ren QName)]
type WSM = WriterT 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 = TCM | Source

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

notInScope :: QName -> ScopeM a | Source

General operations

getCurrentModule :: ScopeM ModuleName | Source

setCurrentModule :: ModuleName -> ScopeM () | Source

withCurrentModule :: ModuleName -> ScopeM a -> ScopeM a | Source

getNamedScope :: ModuleName -> ScopeM Scope | Source

getCurrentScope :: ScopeM Scope | Source

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

Set context precedence

getContextPrecedence :: ScopeM Precedence | Source

withContextPrecedence :: Precedence -> ScopeM a -> ScopeM a | Source

getLocalVars :: ScopeM LocalVars | Source

setLocalVars :: LocalVars -> ScopeM () | Source

withLocalVars :: ScopeM a -> ScopeM a | Source

Run a computation without changing the local variables.
Names

freshAbstractName :: Fixity -> Name -> ScopeM Name | Source

Create a fresh abstract name from a concrete name.

freshAbstractName_ :: Name -> ScopeM Name | Source

    freshAbstractName_ = freshAbstractName defaultFixity

freshAbstractQName :: Fixity -> Name -> ScopeM QName | Source

Create a fresh abstract qualified name.
Resolving names

data ResolvedName | Source

Constructors

VarName Name |
DefinedName AbstractName |
ConstructorName [AbstractName] |
UnknownName |

Instances

Show ResolvedName

resolveName :: QName -> ScopeM ResolvedName | Source

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

resolveModule :: QName -> ScopeM AbstractModule | Source

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.

renamedCanonicalNames :: ModuleName -> ModuleName -> Scope -> ScopeM (Map QName QName, Map ModuleName ModuleName) | Source

`renamedCanonicalNames old new s` returns a renaming replacing all (abstract) names `old.m.x` with `new.m.x`. Any other names are left untouched.

type Ren a = Map a a | Source

type Out = [Either (Ren ModuleName) (Ren QName)] | Source

type WSM = WriterT Out ScopeM | Source

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 Scope | Source

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