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.

printLocals :: Int -> String -> ScopeM ()

scopeWarning' :: CallStack -> DeclarationWarning' -> ScopeM ()

scopeWarning :: HasCallStack => DeclarationWarning' -> ScopeM ()

General operations

isDatatypeModule :: ReadTCState m => ModuleName -> m (Maybe DataOrRecordModule)

getCurrentModule :: ReadTCState m => m ModuleName

setCurrentModule :: MonadTCState m => ModuleName -> m ()

withCurrentModule :: (ReadTCState m, MonadTCState m) => ModuleName -> m a -> m a

withCurrentModule' :: (MonadTrans t, Monad (t ScopeM)) => ModuleName -> t ScopeM a -> t ScopeM a

getNamedScope :: ModuleName -> ScopeM Scope

getCurrentScope :: ScopeM Scope

createModule :: Maybe DataOrRecordModule -> ModuleName -> ScopeM ()

Create a new module with an empty scope. If the module is not new (e.g. duplicate import), don't erase its contents. (Just if it is a datatype or record 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 :: PrecedenceStack -> ScopeM ()

withContextPrecedence :: ReadTCState m => Precedence -> m a -> m a

getLocalVars :: ReadTCState m => m LocalVars

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

setLocalVars :: LocalVars -> ScopeM ()

withLocalVars :: ScopeM a -> ScopeM a

Run a computation without changing the local variables.

outsideLocalVars :: Int -> ScopeM a -> ScopeM a

Run a computation outside some number of local variables and add them back afterwards. This lets you bind variables in the middle of the context and is used when binding generalizable variables (#3735).

withCheckNoShadowing :: ScopeM a -> ScopeM a

Check that the newly added variable have unique names.

checkNoShadowing

Arguments

:: LocalVars

Old local scope

-> LocalVars

New local scope

-> ScopeM ()

getVarsToBind :: ScopeM LocalVars

addVarToBind :: Name -> LocalVar -> ScopeM ()

bindVarsToBind :: ScopeM ()

After collecting some variable names in the scopeVarsToBind, bind them all simultaneously.

annotateDecls :: ReadTCState m => m [Declaration] -> m Declaration

annotateExpr :: ReadTCState m => m Expr -> m Expr

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.

freshAbstractQName' :: Name -> ScopeM QName

freshConcreteName :: Range -> Int -> String -> ScopeM Name

Create a concrete name that is not yet in scope. | NOTE: See chooseName in Agda.Syntax.Translation.AbstractToConcrete for similar logic. | NOTE: See withName in Agda.Syntax.Translation.ReflectedToAbstract for similar logic.

Resolving names

resolveName :: QName -> ScopeM ResolvedName

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

resolveName' :: KindsOfNames -> 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.)

tryResolveName

Arguments

:: (ReadTCState m, HasBuiltins m, MonadError AmbiguousNameReason m)

=> KindsOfNames

Restrict search to these kinds of names.

-> Maybe (Set Name)

Unless Nothing, restrict search to match any of these names.

-> QName

Name to be resolved

-> m ResolvedName

If illegally ambiguous, throw error with the ambiguous name.

canHaveSuffixTest :: HasBuiltins m => m (QName -> Bool)

Test if a given abstract name can appear with a suffix. Currently only true for the names of builtin sorts.

resolveModule :: QName -> ScopeM AbstractModule

Look up a module in the scope.

getConcreteFixity :: Name -> ScopeM Fixity'

Get the fixity of a not yet bound name.

getConcretePolarity :: Name -> ScopeM (Maybe [Occurrence])

Get the polarities of a not yet bound name.

computeFixitiesAndPolarities :: DoWarn -> [Declaration] -> ScopeM a -> ScopeM a

Collect the fixity/syntax declarations and polarity pragmas from the list of declarations and store them 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

Arguments

:: BindingSource

λ, Π, let, ...?

-> Name

Concrete name.

-> Name

Abstract name.

-> ScopeM ()

Bind a variable.

unbindVariable :: Name -> ScopeM a -> ScopeM a

Temporarily unbind a variable. Used for non-recursive lets.

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

Bind a defined name. Must not shadow anything.

bindName' :: Access -> KindOfName -> NameMetadata -> Name -> QName -> ScopeM ()

bindName'' :: Access -> KindOfName -> NameMetadata -> Name -> QName -> ScopeM (Maybe TypeError)

Bind a name. Returns the TypeError if exists, but does not throw it.

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 WSM = StateT ScopeMemo ScopeM

data ScopeMemo

Constructors

ScopeMemo

Fields

• memoNames :: Ren QName
• memoModules :: Map ModuleName (ModuleName, Bool)

  Bool: did we copy recursively? We need to track this because we don't copy recursively when creating new modules for reexported functions (issue1985), but we might need to copy recursively later.

memoToScopeInfo :: ScopeMemo -> ScopeCopyInfo

copyName :: QName -> QName -> ScopeM ()

Mark a name as being a copy in the TC state.

copyScope :: QName -> ModuleName -> Scope -> ScopeM (Scope, ScopeCopyInfo)

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.

Import directives

checkNoFixityInRenamingModule :: [Renaming] -> ScopeM ()

Warn about useless fixity declarations in renaming directives. Monadic for the sake of error reporting.

verifyImportDirective :: [ImportedName] -> HidingDirective -> RenamingDirective -> ScopeM ()

Check that an import directive doesn't contain repeated names.

applyImportDirectiveM

Arguments

:: QName

Name of the scope, only for error reporting.

-> ImportDirective

Description of how scope is to be modified.

-> Scope

Input scope.

-> ScopeM (ImportDirective, Scope)

Scope-checked description, output scope.

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

Monadic for the sake of error reporting.

mapImportDir

Arguments

:: (Ord n1, Ord m1)

=> [ImportedName' (n1, n2) (m1, m2)]

Translation of imported names.

-> [ImportedName' (n1, n2) (m1, m2)]

Translation of names defined by this import.

-> ImportDirective' n1 m1

-> ImportDirective' n2 m2

Translation of ImportDirective.

data ImportedNameMap n1 n2 m1 m2

A finite map for ImportedNames.

Constructors

ImportedNameMap

Fields

• inameMap :: Map n1 n2
• imoduleMap :: Map m1 m2

importedNameMapFromList :: (Ord n1, Ord m1) => [ImportedName' (n1, n2) (m1, m2)] -> ImportedNameMap n1 n2 m1 m2

Create a ImportedNameMap.

lookupImportedName :: (Ord n1, Ord m1) => ImportedNameMap n1 n2 m1 m2 -> ImportedName' n1 m1 -> ImportedName' n2 m2

Apply a ImportedNameMap.

mapRenaming

Arguments

:: (Ord n1, Ord m1)

=> ImportedNameMap n1 n2 m1 m2

Translation of renFrom names and module names.

-> ImportedNameMap n1 n2 m1 m2

Translation of rento names and module names.

-> Renaming' n1 m1

Renaming before translation (1).

-> Renaming' n2 m2

Renaming after translation (2).

Translation of Renaming.

Opening a module

data OpenKind

Constructors

LetOpenModule

TopOpenModule

noGeneralizedVarsIfLetOpen :: OpenKind -> Scope -> Scope

openModule_ :: OpenKind -> QName -> ImportDirective -> ScopeM ImportDirective

Open a module.

openModule :: OpenKind -> Maybe ModuleName -> QName -> ImportDirective -> ScopeM ImportDirective

Open a module, possibly given an already resolved module name.

Orphan instances

MonadFixityError ScopeM

Methods

throwMultipleFixityDecls :: [(Name, [Fixity'])] -> ScopeM a

throwMultiplePolarityPragmas :: [Name] -> ScopeM a

warnUnknownNamesInFixityDecl :: [Name] -> ScopeM ()

warnUnknownNamesInPolarityPragmas :: [Name] -> ScopeM ()

warnUnknownFixityInMixfixDecl :: [Name] -> ScopeM ()

warnPolarityPragmasButNotPostulates :: [Name] -> ScopeM ()