Agda-2.6.2.1.20220320: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.Syntax.Scope.Monad

Description

The scope monad with operations.

Synopsis

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.

General operations

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

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

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 () Source #

Apply a function to the scope map.

modifyNamedScope :: ModuleName -> (Scope -> Scope) -> ScopeM () Source #

Apply a function to the given scope.

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

Apply a monadic function to the top scope.

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

Apply a function to the current scope.

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

Apply a function to the public or private name space.

withLocalVars :: ScopeM a -> ScopeM a Source #

Run a computation without changing the local variables.

outsideLocalVars :: Int -> ScopeM a -> ScopeM a Source #

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 Source #

Check that the newly added variable have unique names.

checkNoShadowing Source #

Arguments

:: LocalVars

Old local scope

-> LocalVars

New local scope

-> ScopeM () 

bindVarsToBind :: ScopeM () Source #

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

Names

freshAbstractName :: Fixity' -> Name -> ScopeM Name Source #

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 Source #

freshAbstractName_ = freshAbstractName noFixity'

freshAbstractQName :: Fixity' -> Name -> ScopeM QName Source #

Create a fresh abstract qualified name.

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

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 Source #

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

resolveName' :: KindsOfNames -> Maybe (Set Name) -> QName -> ScopeM ResolvedName Source #

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 Source #

Arguments

:: (ReadTCState m, HasBuiltins m, MonadError (List1 QName) 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) Source #

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

resolveModule :: QName -> ScopeM AbstractModule Source #

Look up a module in the scope.

getConcreteFixity :: Name -> ScopeM Fixity' Source #

Get the fixity of a not yet bound name.

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

Get the polarities of a not yet bound name.

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

Collect the fixity/syntax declarations and polarity pragmas from the list of declarations and store them in the scope.

getNotation Source #

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 Source #

Arguments

:: BindingSource

λ, Π, let, ...?

-> Name

Concrete name.

-> Name

Abstract name.

-> ScopeM () 

Bind a variable.

unbindVariable :: Name -> ScopeM a -> ScopeM a Source #

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

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

Bind a defined name. Must not shadow anything.

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

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

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

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

type WSM = StateT ScopeMemo ScopeM Source #

data ScopeMemo Source #

Constructors

ScopeMemo 

Fields

copyScope :: QName -> ModuleName -> Scope -> ScopeM (Scope, ScopeCopyInfo) 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.

Import directives

checkNoFixityInRenamingModule :: [Renaming] -> ScopeM () Source #

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

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

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

applyImportDirectiveM Source #

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 Source #

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 Source #

A finite map for ImportedNames.

Constructors

ImportedNameMap 

Fields

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

Create a ImportedNameMap.

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

mapRenaming Source #

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

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

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

Orphan instances