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

Safe HaskellNone

Agda.Syntax.Scope.Base

Contents

Description

This module defines the notion of a scope and operations on scopes.

Synopsis

Scope representation

data Scope

A scope is a named collection of names partitioned into public and private names.

data ScopeInfo

The complete information about the scope at a particular program point includes the scope stack, the local variables, and the context precedence.

type LocalVars = [(Name, Name)]

Local variables

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.

type ThingsInScope a = Map Name [a]

class Eq a => InScope a where

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 

data AbstractModule

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

Constructors

AbsModule 

Fields

amodName :: ModuleName
 

Operations on names

Operations on name and module maps.

Operations on name spaces

emptyNameSpace :: NameSpace

The empty name space.

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

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

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.

emptyScopeInfo :: ScopeInfo

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.

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

Returns the scope's non-private names.

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

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.

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

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

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

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.