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

Safe HaskellNone
LanguageHaskell98

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.

Constructors

Scope 

Fields

scopeName :: ModuleName
 
scopeParents :: [ModuleName]
 
scopeNameSpaces :: [(NameSpaceId, NameSpace)]
 
scopeImports :: Map QName ModuleName
 
scopeDatatypeModule :: Bool
 

Instances

data NameSpaceId Source

Constructors

PrivateNS 
PublicNS 
ImportedNS 
OnlyQualifiedNS 

Instances

localNameSpace :: Access -> NameSpaceId Source

nameSpaceAccess :: NameSpaceId -> Access Source

scopeNameSpace :: NameSpaceId -> Scope -> NameSpace Source

Get a NameSpace from Scope.

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 

Fields

scopeCurrent :: ModuleName
 
scopeModules :: Map ModuleName Scope
 
scopeLocals :: LocalVars
 
scopePrecedence :: Precedence
 

Instances

type LocalVars = [(Name, Name)] Source

Local variables.

modifyScopeLocals :: (LocalVars -> LocalVars) -> ScopeInfo -> ScopeInfo Source

Lens for scopeLocals.

setScopeLocals :: LocalVars -> ScopeInfo -> ScopeInfo Source

Name spaces

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 

Fields

nsNames :: NamesInScope

Maps concrete names to a list of abstract names.

nsModules :: ModulesInScope

Maps concrete module names to a list of abstract module names.

Instances

type ThingsInScope a = Map Name [a] Source

type NamesInScope = ThingsInScope AbstractName Source

type ModulesInScope = ThingsInScope AbstractModule Source

data InScopeTag a where Source

Set of types consisting of exactly AbstractName and AbstractModule.

A GADT just for some dependent-types trickery.

Constructors

NameTag :: InScopeTag AbstractName 
ModuleTag :: InScopeTag AbstractModule 

class Eq a => InScope a where Source

Type class for some dependent-types trickery.

Methods

inScopeTag :: InScopeTag a Source

Instances

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

inNameSpace selects either the name map or the module name map from a NameSpace. What is selected is determined by result type (using the dependent-type trickery).

Decorated names

data KindOfName Source

For the sake of parsing left-hand sides, we distinguish constructor and record field names from defined names.

Constructors

ConName

Constructor name.

FldName

Record field name.

DefName

Ordinary defined name.

PatternSynName

Name of a pattern synonym.

Instances

allKindsOfNames :: [KindOfName] Source

A list containing all name kinds.

data WhyInScope Source

Where does a name come from?

This information is solely for reporting to the user, see whyInScope.

Constructors

Defined

Defined in this module.

Opened QName WhyInScope

Imported from another module.

Applied QName WhyInScope

Imported by a module application.

Instances

data AbstractName Source

A decoration of QName.

Constructors

AbsName 

Fields

anameName :: QName

The resolved qualified name.

anameKind :: KindOfName

The kind (definition, constructor, record field etc.).

anameLineage :: WhyInScope

Explanation where this name came from.

Instances

data AbstractModule Source

A decoration of abstract syntax module names.

Constructors

AbsModule 

Fields

amodName :: ModuleName

The resolved module name.

amodLineage :: WhyInScope

Explanation where this name came from.

Instances

Operations on name and module maps.

mergeNames :: Eq 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 :: (Functor m, 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_ :: (Functor m, 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.

allNamesInScope' :: InScope a => Scope -> ThingsInScope (a, Access) Source

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

Returns the scope's non-private names.

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

allThingsInScope :: Scope -> NameSpace Source

thingsInScope :: [NameSpaceId] -> 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).

setNameSpace :: NameSpaceId -> NameSpace -> Scope -> Scope Source

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

removeOnlyQualified :: Scope -> Scope Source

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

inScopeBecause :: (WhyInScope -> WhyInScope) -> Scope -> Scope Source

Add an explanation to why things are in scope.

publicModules :: ScopeInfo -> Map ModuleName Scope Source

Get the public parts of the public modules of a scope

everythingInScope :: ScopeInfo -> NameSpace Source

flattenScope :: [[Name]] -> ScopeInfo -> Map QName [AbstractName] Source

Compute a flattened scope. Only include unqualified names or names qualified by modules in the first argument.

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

(Debug) printing

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

Add first string only if list is non-empty.

Boring instances