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

Instances

Data Scope
Show Scope
Typeable Scope
EmbPrj Scope
InstantiateFull Scope

data NameSpaceId | Source

Constructors

PrivateNS |
PublicNS |
ImportedNS |

Instances

Eq NameSpaceId
Data NameSpaceId
Typeable NameSpaceId

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 |

Instances

Data ScopeInfo
Show ScopeInfo
Typeable ScopeInfo
EmbPrj ScopeInfo

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 |

Instances

Data NameSpace
Show NameSpace
Typeable NameSpace
EmbPrj NameSpace

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

Instances

InScope AbstractModule
InScope AbstractName

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

data KindOfName | Source

We distinguish constructor names from other names.
Constructors

ConName |
DefName |

Instances

Eq KindOfName
Data KindOfName
Show KindOfName
Typeable KindOfName
EmbPrj KindOfName

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 |

Instances

Eq AbstractName
Data AbstractName
Ord AbstractName
Show AbstractName
Typeable AbstractName
SetRange AbstractName
HasRange AbstractName
InScope AbstractName
EmbPrj AbstractName

data AbstractModule | Source

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

AbsModule |

amodName :: ModuleName |

Instances

Eq AbstractModule
Data AbstractModule
Ord AbstractModule
Show AbstractModule
Typeable AbstractModule
InScope AbstractModule
EmbPrj AbstractModule

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.4.2