Agda-2.2.6: A dependently typed functional programming language and proof assistant Source code Contents Index

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 :: NameSpace public opened names scopeImports :: Map QName ModuleName

data NameSpaceId Source

Constructors PrivateNS PublicNS ImportedNS

localNameSpace :: Access -> NameSpaceId Source

importedNameSpace :: Access -> NameSpaceId Source

scopeNameSpace :: NameSpaceId -> Scope -> NameSpace Source

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

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

type ThingsInScope a = Map Name [a] Source

type NamesInScope = ThingsInScope AbstractName Source

type ModulesInScope = ThingsInScope AbstractModule Source

data InScopeTag a where Source

Constructors NameTag :: InScopeTag AbstractName ModuleTag :: InScopeTag AbstractModule

class Eq a => InScope a where Source

Methods inScopeTag :: InScopeTag a Source

inNameSpace :: forall a. InScope a => NameSpace -> ThingsInScope a Source

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 anameName :: QName anameKind :: KindOfName

data AbstractModule Source

For modules we record the arity. I'm not sure that it's every used anywhere. Constructors AbsModule amodName :: ModuleName

blockOfLines :: String -> [String] -> [String] Source

Operations on names

Operations on name and module maps.

mergeNames :: InScope a => ThingsInScope a -> ThingsInScope a -> ThingsInScope a Source

Operations on name spaces

emptyNameSpace :: NameSpace Source

The empty name space.

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

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

zipNameSpace :: (NamesInScope -> NamesInScope -> NamesInScope) -> (ModulesInScope -> ModulesInScope -> ModulesInScope) -> NameSpace -> NameSpace -> NameSpace Source

Zip together two name spaces.

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

Map monadic function over a namespace.

General operations on scopes

emptyScope :: Scope Source

The empty scope.

emptyScopeInfo :: ScopeInfo Source

The empty scope info.

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

Map functions over the names and modules in a scope.

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

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

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

mapScopeM_ :: Monad m => (NamesInScope -> m NamesInScope) -> (ModulesInScope -> m ModulesInScope) -> Scope -> m Scope Source

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 Source

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 Source

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

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

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 Source

Return all names in a scope.

namesInScope :: InScope a => [Scope -> NameSpace] -> Scope -> ThingsInScope a Source

allThingsInScope :: Scope -> NameSpace Source

thingsInScope :: [Scope -> NameSpace] -> Scope -> NameSpace Source

mergeScope :: Scope -> Scope -> Scope Source

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

mergeScopes :: [Scope] -> Scope Source

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 Source

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

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

Add names to a scope.

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

Add a name to a scope.

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

Add a module to a scope.

applyImportDirective :: ImportDirective -> Scope -> Scope Source

Apply an ImportDirective to a scope.

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

Rename the abstract names in a scope.

restrictPrivate :: Scope -> Scope Source

Restrict the private name space of a scope

publicModules :: ScopeInfo -> Map ModuleName Scope Source

Get the public parts of the public modules of a scope

everythingInScope :: ScopeInfo -> NameSpace Source

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

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

inverseScopeLookupName :: QName -> ScopeInfo -> Maybe QName Source

Takes the first component of inverseScopeLookup.

inverseScopeLookupModule :: ModuleName -> ScopeInfo -> Maybe QName Source

Takes the second component of inverseScopeLookup.

Produced by Haddock version 2.6.0