Safe Haskell | Safe-Infered |
---|
Agda.Syntax.Scope.Base
Contents
Description
This module defines the notion of a scope and operations on scopes.
- data Scope = Scope {}
- data NameSpaceId
- = PrivateNS
- | PublicNS
- | ImportedNS
- | OnlyQualifiedNS
- localNameSpace :: Access -> NameSpaceId
- nameSpaceAccess :: NameSpaceId -> Access
- scopeNameSpace :: NameSpaceId -> Scope -> NameSpace
- data ScopeInfo = ScopeInfo {}
- type LocalVars = [(Name, Name)]
- data NameSpace = NameSpace {}
- type ThingsInScope a = Map Name [a]
- type NamesInScope = ThingsInScope AbstractName
- type ModulesInScope = ThingsInScope AbstractModule
- data InScopeTag a where
- class Eq a => InScope a where
- inScopeTag :: InScopeTag a
- inNameSpace :: forall a. InScope a => NameSpace -> ThingsInScope a
- data KindOfName
- data AbstractName = AbsName {}
- data AbstractModule = AbsModule {}
- blockOfLines :: String -> [String] -> [String]
- mergeNames :: Eq 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 :: (Functor m, Monad m) => (NameSpaceId -> NamesInScope -> m NamesInScope) -> (NameSpaceId -> ModulesInScope -> m ModulesInScope) -> Scope -> m Scope
- mapScopeM_ :: (Functor m, 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
- allNamesInScope' :: InScope a => Scope -> ThingsInScope (a, Access)
- exportedNamesInScope :: InScope a => Scope -> ThingsInScope a
- namesInScope :: InScope a => [NameSpaceId] -> Scope -> ThingsInScope a
- allThingsInScope :: Scope -> NameSpace
- thingsInScope :: [NameSpaceId] -> Scope -> NameSpace
- mergeScope :: Scope -> Scope -> Scope
- mergeScopes :: [Scope] -> Scope
- setScopeAccess :: NameSpaceId -> Scope -> Scope
- setNameSpace :: NameSpaceId -> NameSpace -> 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
- removeOnlyQualified :: Scope -> Scope
- publicModules :: ScopeInfo -> Map ModuleName Scope
- everythingInScope :: ScopeInfo -> NameSpace
- scopeLookup :: InScope a => QName -> ScopeInfo -> [a]
- scopeLookup' :: forall a. InScope a => QName -> ScopeInfo -> [(a, Access)]
- inverseScopeLookup :: Either ModuleName QName -> ScopeInfo -> Maybe QName
- inverseScopeLookupName :: QName -> ScopeInfo -> Maybe QName
- inverseScopeLookupModule :: ModuleName -> ScopeInfo -> Maybe QName
Scope representation
data Scope
A scope is a named collection of names partitioned into public and private names.
Constructors
Scope | |
Fields
|
data NameSpaceId
Constructors
PrivateNS | |
PublicNS | |
ImportedNS | |
OnlyQualifiedNS |
localNameSpace :: Access -> NameSpaceId
nameSpaceAccess :: NameSpaceId -> Access
scopeNameSpace :: NameSpaceId -> Scope -> NameSpace
data ScopeInfo
The complete information about the scope at a particular program point includes the scope stack, the local variables, and the context precedence.
Constructors
ScopeInfo | |
Fields |
data NameSpace
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 | |
Fields |
type ThingsInScope a = Map Name [a]
data InScopeTag a where
Constructors
NameTag :: InScopeTag AbstractName | |
ModuleTag :: InScopeTag AbstractModule |
Methods
inScopeTag :: InScopeTag a
Instances
inNameSpace :: forall a. InScope a => NameSpace -> ThingsInScope a
data KindOfName
We distinguish constructor names from other names.
data AbstractName
Apart from the name, we also record whether it's a constructor or not and what the fixity is.
Constructors
AbsName | |
Fields
|
data AbstractModule
For modules we record the arity. I'm not sure that it's every used anywhere.
Constructors
AbsModule | |
Fields |
blockOfLines :: String -> [String] -> [String]
Operations on names
Operations on name and module maps.
mergeNames :: Eq a => ThingsInScope a -> ThingsInScope a -> ThingsInScope a
Operations on name spaces
The empty name space.
mapNameSpace :: (NamesInScope -> NamesInScope) -> (ModulesInScope -> ModulesInScope) -> NameSpace -> NameSpace
Map functions over the names and modules in a name space.
zipNameSpace :: (NamesInScope -> NamesInScope -> NamesInScope) -> (ModulesInScope -> ModulesInScope -> ModulesInScope) -> NameSpace -> NameSpace -> NameSpace
Zip together two name spaces.
mapNameSpaceM :: Monad m => (NamesInScope -> m NamesInScope) -> (ModulesInScope -> m ModulesInScope) -> NameSpace -> m NameSpace
Map monadic function over a namespace.
General operations on scopes
emptyScope :: Scope
The empty scope.
The empty scope info.
mapScope :: (NameSpaceId -> NamesInScope -> NamesInScope) -> (NameSpaceId -> ModulesInScope -> ModulesInScope) -> Scope -> Scope
Map functions over the names and modules in a scope.
mapScope_ :: (NamesInScope -> NamesInScope) -> (ModulesInScope -> ModulesInScope) -> Scope -> Scope
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 Scope
Map monadic functions over the names and modules in a scope.
mapScopeM_ :: (Functor m, Monad m) => (NamesInScope -> m NamesInScope) -> (ModulesInScope -> m ModulesInScope) -> Scope -> m Scope
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 -> Scope
Zip together two scopes. The resulting scope has the same name as the first scope.
zipScope_ :: (NamesInScope -> NamesInScope -> NamesInScope) -> (ModulesInScope -> ModulesInScope -> ModulesInScope) -> Scope -> Scope -> Scope
Same as zipScope
but applies the same function to both the public and
private name spaces.
filterScope :: (Name -> Bool) -> (Name -> Bool) -> Scope -> Scope
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 a
Return all names in a scope.
allNamesInScope' :: InScope a => Scope -> ThingsInScope (a, Access)
exportedNamesInScope :: InScope a => Scope -> ThingsInScope a
Returns the scope's non-private names.
namesInScope :: InScope a => [NameSpaceId] -> Scope -> ThingsInScope a
allThingsInScope :: Scope -> NameSpace
thingsInScope :: [NameSpaceId] -> Scope -> NameSpace
mergeScope :: Scope -> Scope -> Scope
Merge two scopes. The result has the name of the first scope.
mergeScopes :: [Scope] -> Scope
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 -> Scope
Move all names in a scope to the given name space (except never move from Imported to Public).
setNameSpace :: NameSpaceId -> NameSpace -> Scope -> Scope
addNamesToScope :: NameSpaceId -> Name -> [AbstractName] -> Scope -> Scope
Add names to a scope.
addNameToScope :: NameSpaceId -> Name -> AbstractName -> Scope -> Scope
Add a name to a scope.
addModuleToScope :: NameSpaceId -> Name -> AbstractModule -> Scope -> Scope
Add a module to a scope.
applyImportDirective :: ImportDirective -> Scope -> Scope
Apply an ImportDirective
to a scope.
renameCanonicalNames :: Map QName QName -> Map ModuleName ModuleName -> Scope -> Scope
Rename the abstract names in a scope.
restrictPrivate :: Scope -> Scope
Restrict the private name space of a scope
removeOnlyQualified :: Scope -> Scope
Remove names that can only be used qualified (when opening a scope)
publicModules :: ScopeInfo -> Map ModuleName Scope
Get the public parts of the public modules of a scope
scopeLookup :: InScope a => QName -> ScopeInfo -> [a]
Look up a name in the scope
scopeLookup' :: forall a. InScope a => QName -> ScopeInfo -> [(a, Access)]
Inverse look-up
inverseScopeLookup :: Either ModuleName QName -> ScopeInfo -> Maybe QName
Find the shortest concrete name that maps (uniquely) to a given abstract name.
inverseScopeLookupName :: QName -> ScopeInfo -> Maybe QName
Takes the first component of inverseScopeLookup
.
inverseScopeLookupModule :: ModuleName -> ScopeInfo -> Maybe QName
Takes the second component of inverseScopeLookup
.