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

Safe Haskell | None

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]
  - scopeNameSpaces :: [(NameSpaceId, NameSpace)]
  - scopeImports :: Map QName ModuleName
  - scopeDatatypeModule :: Bool
  }
- data NameSpaceId
  - = PrivateNS
  - | PublicNS
  - | ImportedNS
  - | OnlyQualifiedNS
- localNameSpace :: Access -> NameSpaceId
- nameSpaceAccess :: NameSpaceId -> Access
- 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
  - | FldName
  - | DefName
  - | PatternSynName
- allKindsOfNames :: [KindOfName]
- data AbstractName = AbsName {
  - anameName :: QName
  - anameKind :: KindOfName
  }
- data AbstractModule = AbsModule {
  - amodName :: ModuleName
  }
- 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
- flattenScope :: [[Name]] -> ScopeInfo -> Map QName [AbstractName]
- 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 scopeName :: ModuleName scopeParents :: [ModuleName] scopeNameSpaces :: [(NameSpaceId, NameSpace)] scopeImports :: Map QName ModuleName scopeDatatypeModule :: Bool

Instances

Show Scope |
Typeable Scope |
InstantiateFull Scope |
EmbPrj Scope |

data NameSpaceId

Constructors

PrivateNS |
PublicNS |
ImportedNS |
OnlyQualifiedNS |

Instances

Bounded NameSpaceId |
Enum NameSpaceId |
Eq NameSpaceId |
Show NameSpaceId |
Typeable NameSpaceId |
EmbPrj NameSpaceId |

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 scopeCurrent :: ModuleName scopeModules :: Map ModuleName Scope scopeLocals :: LocalVars scopePrecedence :: Precedence

Instances

Show ScopeInfo |
Typeable ScopeInfo |
KillRange ScopeInfo |
EmbPrj ScopeInfo |

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.

Constructors

NameSpace |
Fields nsNames :: NamesInScope nsModules :: ModulesInScope

Instances

Show NameSpace |
Typeable NameSpace |
EmbPrj NameSpace |

type ThingsInScope a = Map Name [a]

type NamesInScope = ThingsInScope AbstractName

type ModulesInScope = ThingsInScope AbstractModule

data InScopeTag a where

Constructors

NameTag :: InScopeTag AbstractName |
ModuleTag :: InScopeTag AbstractModule |

class Eq a => InScope a where

Methods

inScopeTag :: InScopeTag a

Instances

InScope AbstractModule |
InScope AbstractName |

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

data KindOfName

We distinguish constructor names from other names.

Constructors

ConName |
FldName |
DefName |
PatternSynName |

Instances

Bounded KindOfName |
Enum KindOfName |
Eq KindOfName |
Show KindOfName |
Typeable KindOfName |
EmbPrj KindOfName |

allKindsOfNames :: [KindOfName]

data AbstractName

Apart from the name, we also record whether it's a constructor or not and what the fixity is.

Constructors

AbsName |
Fields anameName :: QName anameKind :: KindOfName

Instances

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

data AbstractModule

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

Constructors

AbsModule |
Fields amodName :: ModuleName

Instances

Eq AbstractModule |
Ord AbstractModule |
Show AbstractModule |
Typeable AbstractModule |
InScope AbstractModule |
EmbPrj AbstractModule |

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

emptyNameSpace :: NameSpace

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.

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.

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

everythingInScope :: ScopeInfo -> NameSpace

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

inverseScopeLookupModule :: ModuleName -> ScopeInfo -> Maybe QName

Takes the second component of `inverseScopeLookup`.