Agda.Syntax.Scope.Monad

The scope monad with operations.

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

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)

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.

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

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

Apply a monadic function to the top scope.

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

Apply a function to the current scope.

modifyCurrentScopeM :: (Scope -> ScopeM (a, Scope)) -> ScopeM a

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

modifyLocalVars :: (LocalVars -> LocalVars) -> ScopeM ()

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.

This function is used when we translate a concrete name in a binder. The Range of the concrete name is saved as the nameBindingSite of the abstract name.

freshAbstractName_ :: Name -> ScopeM Name

freshAbstractName_ = freshAbstractName noFixity'

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

Eq ResolvedName

Show ResolvedName

resolveName :: QName -> ScopeM ResolvedName

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

resolveName' :: [KindOfName] -> Maybe (Set Name) -> QName -> ScopeM ResolvedName

Look up the abstract name corresponding to a concrete name of a certain kind and/or from a given set of names. Sometimes we know already that we are dealing with a constructor or pattern synonym (e.g. when we have parsed a pattern). Then, we can ignore conflicting definitions of that name of a different kind. (See issue 822.)

resolveModule :: QName -> ScopeM AbstractModule

Look up a module in the scope.

getNotation

Arguments

:: QName

-> Set Name

The name must correspond to one of the names in this set.

-> ScopeM NewNotation

Get the notation 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.

rebindName :: Access -> KindOfName -> Name -> QName -> ScopeM ()

Rebind a name. Use with care! Ulf, 2014-06-29: Currently used to rebind the name defined by an unquoteDecl, which is a QuotableName in the body, but a DefinedName later on.

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 Out = (Ren ModuleName, Ren QName)

type WSM = StateT Out ScopeM

copyScope :: QName -> 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 (ImportDirective, Scope)

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

lookupImportedName :: (Eq a, Eq b) => ImportedName' a b -> [ImportedName' (a, c) (b, d)] -> ImportedName' c d

A finite map for ImportedNames.

mapImportDir

Arguments

:: (Eq a, Eq b)

=> [ImportedName' (a, c) (b, d)]

Translation of imported names.

-> [ImportedName' (a, c) (b, d)]

Translation of names defined by this import.

-> ImportDirective' a b

-> ImportDirective' c d

Translation of ImportDirective.

mapUsing

Arguments

:: (Eq a, Eq b)

=> [ImportedName' (a, c) (b, d)]

Translation of names in using or hiding list.

-> Using' a b

-> Using' c d

Translation of Using or Hiding.

mapRenaming

Arguments

:: (Eq a, Eq b)

=> [ImportedName' (a, c) (b, d)]

Translation of renFrom names.

-> [ImportedName' (a, c) (b, d)]

Translation of rento names.

-> Renaming' a b

-> Renaming' c d

Translation of Renaming.

openModule_ :: QName -> ImportDirective -> ScopeM ImportDirective

Open a module.