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

Agda.Syntax.Scope.Base

Contents

Description

This module defines the notion of a scope and operations on scopes.

Synopsis

Scope representation

data Scope Source

A scope is a named collection of names partitioned into public and private names.

data ScopeInfo Source

The complete information about the scope at a particular program point includes the scope stack, the local variables, and the context precedence.

type LocalVars = [(Name, Name)]Source

Local variables

data NameSpace Source

A NameSpace contains the mappings from concrete names that the user can write to the abstract fully qualified names that the type checker wants to read.

data KindOfName Source

We distinguish constructor names from other names.

Constructors

ConName 
DefName 

data AbstractName Source

Apart from the name, we also record whether it's a constructor or not and what the fixity is.

Constructors

AbsName 

data AbstractModule Source

For modules we record the arity. I'm not sure that it's every used anywhere.

Constructors

AbsModule 

Fields

amodName :: ModuleName
 

Operations on names

Operations on name and module maps.

Operations on name spaces

emptyNameSpace :: NameSpaceSource

The empty name space.

mapNameSpace :: (NamesInScope -> NamesInScope) -> (ModulesInScope -> ModulesInScope) -> NameSpace -> NameSpaceSource

Map functions over the names and modules in a name space.

mapNameSpaceM :: Monad m => (NamesInScope -> m NamesInScope) -> (ModulesInScope -> m ModulesInScope) -> NameSpace -> m NameSpaceSource

Map monadic function over a namespace.

General operations on scopes

emptyScope :: ScopeSource

The empty scope.

emptyScopeInfo :: ScopeInfoSource

The empty scope info.

mapScope :: (NameSpaceId -> NamesInScope -> NamesInScope) -> (NameSpaceId -> ModulesInScope -> ModulesInScope) -> Scope -> ScopeSource

Map functions over the names and modules in a scope.

mapScope_ :: (NamesInScope -> NamesInScope) -> (ModulesInScope -> ModulesInScope) -> Scope -> ScopeSource

Same as mapScope but applies the same function to all name spaces.

mapScopeM :: (Functor m, Monad m) => (NameSpaceId -> NamesInScope -> m NamesInScope) -> (NameSpaceId -> ModulesInScope -> m ModulesInScope) -> Scope -> m ScopeSource

Map monadic functions over the names and modules in a scope.

mapScopeM_ :: (Functor m, Monad m) => (NamesInScope -> m NamesInScope) -> (ModulesInScope -> m ModulesInScope) -> Scope -> m ScopeSource

Same as mapScopeM but applies the same function to both the public and private name spaces.

zipScope :: (NameSpaceId -> NamesInScope -> NamesInScope -> NamesInScope) -> (NameSpaceId -> ModulesInScope -> ModulesInScope -> ModulesInScope) -> Scope -> Scope -> ScopeSource

Zip together two scopes. The resulting scope has the same name as the first scope.

zipScope_ :: (NamesInScope -> NamesInScope -> NamesInScope) -> (ModulesInScope -> ModulesInScope -> ModulesInScope) -> Scope -> Scope -> ScopeSource

Same as zipScope but applies the same function to both the public and private name spaces.

filterScope :: (Name -> Bool) -> (Name -> Bool) -> Scope -> ScopeSource

Filter a scope keeping only concrete names matching the predicates. The first predicate is applied to the names and the second to the modules.

allNamesInScope :: InScope a => Scope -> ThingsInScope aSource

Return all names in a scope.

exportedNamesInScope :: InScope a => Scope -> ThingsInScope aSource

Returns the scope's non-private names.

mergeScope :: Scope -> Scope -> ScopeSource

Merge two scopes. The result has the name of the first scope.

mergeScopes :: [Scope] -> ScopeSource

Merge a non-empty list of scopes. The result has the name of the first scope in the list.

Specific operations on scopes

setScopeAccess :: NameSpaceId -> Scope -> ScopeSource

Move all names in a scope to the given name space (except never move from Imported to Public).

addNamesToScope :: NameSpaceId -> Name -> [AbstractName] -> Scope -> ScopeSource

Add names to a scope.

addNameToScope :: NameSpaceId -> Name -> AbstractName -> Scope -> ScopeSource

Add a name to a scope.

addModuleToScope :: NameSpaceId -> Name -> AbstractModule -> Scope -> ScopeSource

Add a module to a scope.

renameCanonicalNames :: Map QName QName -> Map ModuleName ModuleName -> Scope -> ScopeSource

Rename the abstract names in a scope.

restrictPrivate :: Scope -> ScopeSource

Restrict the private name space of a scope

removeOnlyQualified :: Scope -> ScopeSource

Remove names that can only be used qualified (when opening a scope)

publicModules :: ScopeInfo -> Map ModuleName ScopeSource

Get the public parts of the public modules of a scope

scopeLookup :: InScope a => QName -> ScopeInfo -> [a]Source

Look up a name in the scope

scopeLookup' :: forall a. InScope a => QName -> ScopeInfo -> [(a, Access)]Source

Inverse look-up

inverseScopeLookup :: Either ModuleName QName -> ScopeInfo -> Maybe QNameSource

Find the shortest concrete name that maps (uniquely) to a given abstract name.