Agda-2.2.6: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.Syntax.Scope.Base
Contents
Scope representation
Operations on names
Operations on name and module maps.
Operations on name spaces
General operations on scopes
Specific operations on scopes
Inverse look-up
Description
This module defines the notion of a scope and operations on scopes.
Synopsis
data Scope = Scope {
scopeName :: ModuleName
scopeParents :: [ModuleName]
scopePrivate :: NameSpace
scopePublic :: NameSpace
scopeImported :: NameSpace
scopeImports :: Map QName ModuleName
}
data NameSpaceId
= PrivateNS
| PublicNS
| ImportedNS
localNameSpace :: Access -> NameSpaceId
importedNameSpace :: Access -> NameSpaceId
scopeNameSpace :: NameSpaceId -> Scope -> NameSpace
data ScopeInfo = ScopeInfo {
scopeCurrent :: ModuleName
scopeModules :: Map ModuleName Scope
scopeLocals :: LocalVars
scopePrecedence :: Precedence
}
type LocalVars = [(Name, Name)]
data NameSpace = NameSpace {
nsNames :: NamesInScope
nsModules :: ModulesInScope
}
type ThingsInScope a = Map Name [a]
type NamesInScope = ThingsInScope AbstractName
type ModulesInScope = ThingsInScope AbstractModule
data InScopeTag a where
NameTag :: InScopeTag AbstractName
ModuleTag :: InScopeTag AbstractModule
class Eq a => InScope a where
inScopeTag :: InScopeTag a
inNameSpace :: forall a. InScope a => NameSpace -> ThingsInScope a
data KindOfName
= ConName
| DefName
data AbstractName = AbsName {
anameName :: QName
anameKind :: KindOfName
}
data AbstractModule = AbsModule {
amodName :: ModuleName
}
blockOfLines :: String -> [String] -> [String]
mergeNames :: InScope a => ThingsInScope a -> ThingsInScope a -> ThingsInScope a
emptyNameSpace :: NameSpace
mapNameSpace :: (NamesInScope -> NamesInScope) -> (ModulesInScope -> ModulesInScope) -> NameSpace -> NameSpace
zipNameSpace :: (NamesInScope -> NamesInScope -> NamesInScope) -> (ModulesInScope -> ModulesInScope -> ModulesInScope) -> NameSpace -> NameSpace -> NameSpace
mapNameSpaceM :: Monad m => (NamesInScope -> m NamesInScope) -> (ModulesInScope -> m ModulesInScope) -> NameSpace -> m NameSpace
emptyScope :: Scope
emptyScopeInfo :: ScopeInfo
mapScope :: (NameSpaceId -> NamesInScope -> NamesInScope) -> (NameSpaceId -> ModulesInScope -> ModulesInScope) -> Scope -> Scope
mapScope_ :: (NamesInScope -> NamesInScope) -> (ModulesInScope -> ModulesInScope) -> Scope -> Scope
mapScopeM :: Monad m => (NameSpaceId -> NamesInScope -> m NamesInScope) -> (NameSpaceId -> ModulesInScope -> m ModulesInScope) -> Scope -> m Scope
mapScopeM_ :: Monad m => (NamesInScope -> m NamesInScope) -> (ModulesInScope -> m ModulesInScope) -> Scope -> m Scope
zipScope :: (NameSpaceId -> NamesInScope -> NamesInScope -> NamesInScope) -> (NameSpaceId -> ModulesInScope -> ModulesInScope -> ModulesInScope) -> Scope -> Scope -> Scope
zipScope_ :: (NamesInScope -> NamesInScope -> NamesInScope) -> (ModulesInScope -> ModulesInScope -> ModulesInScope) -> Scope -> Scope -> Scope
filterScope :: (Name -> Bool) -> (Name -> Bool) -> Scope -> Scope
allNamesInScope :: InScope a => Scope -> ThingsInScope a
namesInScope :: InScope a => [Scope -> NameSpace] -> Scope -> ThingsInScope a
allThingsInScope :: Scope -> NameSpace
thingsInScope :: [Scope -> NameSpace] -> Scope -> NameSpace
mergeScope :: Scope -> Scope -> Scope
mergeScopes :: [Scope] -> Scope
setScopeAccess :: NameSpaceId -> Scope -> Scope
addNamesToScope :: NameSpaceId -> Name -> [AbstractName] -> Scope -> Scope
addNameToScope :: NameSpaceId -> Name -> AbstractName -> Scope -> Scope
addModuleToScope :: NameSpaceId -> Name -> AbstractModule -> Scope -> Scope
applyImportDirective :: ImportDirective -> Scope -> Scope
renameCanonicalNames :: Map QName QName -> Map ModuleName ModuleName -> Scope -> Scope
restrictPrivate :: Scope -> Scope
publicModules :: ScopeInfo -> Map ModuleName Scope
everythingInScope :: ScopeInfo -> NameSpace
scopeLookup :: forall a. InScope a => QName -> ScopeInfo -> [a]
inverseScopeLookup :: Either ModuleName QName -> ScopeInfo -> Maybe QName
inverseScopeLookupName :: QName -> ScopeInfo -> Maybe QName
inverseScopeLookupModule :: ModuleName -> ScopeInfo -> Maybe QName
Scope representation
data Scope Source
A scope is a named collection of names partitioned into public and private names.
Constructors
Scope
scopeName :: ModuleName
scopeParents :: [ModuleName]
scopePrivate :: NameSpace
scopePublic :: NameSpace
scopeImported :: NameSpacepublic opened names
scopeImports :: Map QName ModuleName
show/hide Instances
data NameSpaceId Source
Constructors
PrivateNS
PublicNS
ImportedNS
show/hide Instances
localNameSpace :: Access -> NameSpaceIdSource
importedNameSpace :: Access -> NameSpaceIdSource
scopeNameSpace :: NameSpaceId -> Scope -> NameSpaceSource
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.
Constructors
ScopeInfo
scopeCurrent :: ModuleName
scopeModules :: Map ModuleName Scope
scopeLocals :: LocalVars
scopePrecedence :: Precedence
show/hide Instances
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.
Constructors
NameSpace
nsNames :: NamesInScope
nsModules :: ModulesInScope
show/hide Instances
type ThingsInScope a = Map Name [a]Source
type NamesInScope = ThingsInScope AbstractNameSource
type ModulesInScope = ThingsInScope AbstractModuleSource
data InScopeTag a whereSource
Constructors
NameTag :: InScopeTag AbstractName
ModuleTag :: InScopeTag AbstractModule
class Eq a => InScope a whereSource
Methods
inScopeTag :: InScopeTag aSource
show/hide Instances
inNameSpace :: forall a. InScope a => NameSpace -> ThingsInScope aSource
data KindOfName Source
We distinguish constructor names from other names.
Constructors
ConName
DefName
show/hide Instances
data AbstractName Source
Apart from the name, we also record whether it's a constructor or not and what the fixity is.
Constructors
AbsName
anameName :: QName
anameKind :: KindOfName
show/hide Instances
data AbstractModule Source
For modules we record the arity. I'm not sure that it's every used anywhere.
Constructors
AbsModule
amodName :: ModuleName
show/hide Instances
blockOfLines :: String -> [String] -> [String]Source
Operations on names
Operations on name and module maps.
mergeNames :: InScope a => ThingsInScope a -> ThingsInScope a -> ThingsInScope aSource
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.
zipNameSpace :: (NamesInScope -> NamesInScope -> NamesInScope) -> (ModulesInScope -> ModulesInScope -> ModulesInScope) -> NameSpace -> NameSpace -> NameSpaceSource
Zip together two name spaces.
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 :: 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_ :: 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.
namesInScope :: InScope a => [Scope -> NameSpace] -> Scope -> ThingsInScope aSource
allThingsInScope :: Scope -> NameSpaceSource
thingsInScope :: [Scope -> NameSpace] -> Scope -> NameSpaceSource
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.
applyImportDirective :: ImportDirective -> Scope -> ScopeSource
Apply an ImportDirective 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
publicModules :: ScopeInfo -> Map ModuleName ScopeSource
Get the public parts of the public modules of a scope
everythingInScope :: ScopeInfo -> NameSpaceSource
scopeLookup :: forall a. InScope a => QName -> ScopeInfo -> [a]Source
Look up a name in the scope
Inverse look-up
inverseScopeLookup :: Either ModuleName QName -> ScopeInfo -> Maybe QNameSource
Find the shortest concrete name that maps (uniquely) to a given abstract name.
inverseScopeLookupName :: QName -> ScopeInfo -> Maybe QNameSource
Takes the first component of inverseScopeLookup.
inverseScopeLookupModule :: ModuleName -> ScopeInfo -> Maybe QNameSource
Takes the second component of inverseScopeLookup.
Produced by Haddock version 2.4.2