Agda.Syntax.Scope.Monad

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

Source code

Contents

Index

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

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