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

Safe Haskell | None

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
- isDatatypeModule :: ModuleName -> ScopeM Bool
- 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 ()
- 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 Access AbstractName
  - | FieldName AbstractName
  - | ConstructorName [AbstractName]
  - | PatternSynResName 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 = TCM

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

# Errors

notInScope :: QName -> ScopeM a

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.

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

Apply a function to the current scope.

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

Apply a monadic function to the top 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

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.

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.

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.

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 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))

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

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

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

Open a module.