Agda-2.2.6: A dependently typed functional programming language and proof assistant




The scope monad with operations.


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.


General operations

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.

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

Apply a function to the public or private name space.

setContextPrecedence :: Precedence -> ScopeM ()Source

Set context precedence

withLocalVars :: ScopeM a -> ScopeM aSource

Run a computation without changing the local variables.


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

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 FixitySource

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 aSource

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.