Safe Haskell	None
Language	Haskell2010

Agda.Syntax.Scope.Base

Contents

Scope representation
Name spaces
Decorated names
Operations on name and module maps.
Operations on name spaces
General operations on scopes
Specific operations on scopes
Inverse look-up
(Debug) printing
Boring instances

Description

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

Synopsis

data Scope = Scope {
- scopeName :: ModuleName
- scopeParents :: [ModuleName]
- scopeNameSpaces :: ScopeNameSpaces
- scopeImports :: Map QName ModuleName
- scopeDatatypeModule :: Maybe DataOrRecord
}
data NameSpaceId
- = PrivateNS
- | PublicNS
- | ImportedNS
- | OnlyQualifiedNS
type ScopeNameSpaces = [(NameSpaceId, NameSpace)]
localNameSpace :: Access -> NameSpaceId
nameSpaceAccess :: NameSpaceId -> Access
scopeNameSpace :: NameSpaceId -> Scope -> NameSpace
updateScopeNameSpaces :: (ScopeNameSpaces -> ScopeNameSpaces) -> Scope -> Scope
updateScopeNameSpacesM :: Functor m => (ScopeNameSpaces -> m ScopeNameSpaces) -> Scope -> m Scope
data ScopeInfo = ScopeInfo {
- scopeCurrent :: ModuleName
- scopeModules :: Map ModuleName Scope
- scopeVarsToBind :: LocalVars
- scopeLocals :: LocalVars
- scopePrecedence :: PrecedenceStack
- scopeInverseName :: Map QName [QName]
- scopeInverseModule :: Map ModuleName [QName]
- scopeInScope :: InScopeSet
}
type LocalVars = AssocList Name LocalVar
data Binder
- = LambdaBound
- | PatternBound
- | LetBound
data LocalVar = LocalVar {
- localVar :: Name
- localBinder :: Binder
- localShadowedBy :: [AbstractName]
}
shadowLocal :: [AbstractName] -> LocalVar -> LocalVar
notShadowedLocal :: LocalVar -> Maybe Name
notShadowedLocals :: LocalVars -> AssocList Name Name
updateVarsToBind :: (LocalVars -> LocalVars) -> ScopeInfo -> ScopeInfo
setVarsToBind :: LocalVars -> ScopeInfo -> ScopeInfo
updateScopeLocals :: (LocalVars -> LocalVars) -> ScopeInfo -> ScopeInfo
setScopeLocals :: LocalVars -> ScopeInfo -> ScopeInfo
mapScopeInfo :: (Scope -> Scope) -> ScopeInfo -> ScopeInfo
data NameSpace = NameSpace {
- nsNames :: NamesInScope
- nsModules :: ModulesInScope
- nsInScope :: InScopeSet
}
type ThingsInScope a = Map Name [a]
type NamesInScope = ThingsInScope AbstractName
type ModulesInScope = ThingsInScope AbstractModule
type InScopeSet = Set QName
data InScopeTag a where
- NameTag :: InScopeTag AbstractName
- ModuleTag :: InScopeTag AbstractModule
class Eq a => InScope a where
inNameSpace :: forall a. InScope a => NameSpace -> ThingsInScope a
data KindOfName
- = ConName
- | FldName
- | DefName
- | PatternSynName
- | MacroName
- | QuotableName
allKindsOfNames :: [KindOfName]
data WhyInScope
- = Defined
- | Opened QName WhyInScope
- | Applied QName WhyInScope
data AbstractName = AbsName {
- anameName :: QName
- anameKind :: KindOfName
- anameLineage :: WhyInScope
}
data AbstractModule = AbsModule {
- amodName :: ModuleName
- amodLineage :: WhyInScope
}
lensAnameName :: Functor m => (QName -> m QName) -> AbstractName -> m AbstractName
lensAmodName :: Functor m => (ModuleName -> m ModuleName) -> AbstractModule -> m AbstractModule
data ResolvedName
- = VarName {
  - resolvedVar :: Name
  - resolvedBinder :: Binder
  }
- | DefinedName Access AbstractName
- | FieldName (NonemptyList AbstractName)
- | ConstructorName (NonemptyList AbstractName)
- | PatternSynResName (NonemptyList AbstractName)
- | UnknownName
mergeNames :: Eq a => ThingsInScope a -> ThingsInScope a -> ThingsInScope a
emptyNameSpace :: NameSpace
mapNameSpace :: (NamesInScope -> NamesInScope) -> (ModulesInScope -> ModulesInScope) -> (InScopeSet -> InScopeSet) -> NameSpace -> NameSpace
zipNameSpace :: (NamesInScope -> NamesInScope -> NamesInScope) -> (ModulesInScope -> ModulesInScope -> ModulesInScope) -> (InScopeSet -> InScopeSet -> InScopeSet) -> NameSpace -> NameSpace -> NameSpace
mapNameSpaceM :: Applicative m => (NamesInScope -> m NamesInScope) -> (ModulesInScope -> m ModulesInScope) -> (InScopeSet -> m InScopeSet) -> NameSpace -> m NameSpace
emptyScope :: Scope
emptyScopeInfo :: ScopeInfo
mapScope :: (NameSpaceId -> NamesInScope -> NamesInScope) -> (NameSpaceId -> ModulesInScope -> ModulesInScope) -> (NameSpaceId -> InScopeSet -> InScopeSet) -> Scope -> Scope
mapScope_ :: (NamesInScope -> NamesInScope) -> (ModulesInScope -> ModulesInScope) -> (InScopeSet -> InScopeSet) -> Scope -> Scope
mapScope' :: NameSpaceId -> (NamesInScope -> NamesInScope) -> (ModulesInScope -> ModulesInScope) -> (InScopeSet -> InScopeSet) -> Scope -> Scope
mapScopeM :: Applicative m => (NameSpaceId -> NamesInScope -> m NamesInScope) -> (NameSpaceId -> ModulesInScope -> m ModulesInScope) -> (NameSpaceId -> InScopeSet -> m InScopeSet) -> Scope -> m Scope
mapScopeM_ :: Applicative m => (NamesInScope -> m NamesInScope) -> (ModulesInScope -> m ModulesInScope) -> (InScopeSet -> m InScopeSet) -> Scope -> m Scope
zipScope :: (NameSpaceId -> NamesInScope -> NamesInScope -> NamesInScope) -> (NameSpaceId -> ModulesInScope -> ModulesInScope -> ModulesInScope) -> (NameSpaceId -> InScopeSet -> InScopeSet -> InScopeSet) -> Scope -> Scope -> Scope
zipScope_ :: (NamesInScope -> NamesInScope -> NamesInScope) -> (ModulesInScope -> ModulesInScope -> ModulesInScope) -> (InScopeSet -> InScopeSet -> InScopeSet) -> Scope -> Scope -> Scope
recomputeInScopeSets :: 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
modifyNameSpace :: NameSpaceId -> (NameSpace -> NameSpace) -> Scope -> Scope
addNamesToScope :: NameSpaceId -> Name -> [AbstractName] -> Scope -> Scope
addNameToScope :: NameSpaceId -> Name -> AbstractName -> Scope -> Scope
removeNameFromScope :: NameSpaceId -> Name -> Scope -> Scope
addModuleToScope :: NameSpaceId -> Name -> AbstractModule -> Scope -> Scope
type UsingOrHiding = Either Using [ImportedName]
usingOrHiding :: ImportDirective -> UsingOrHiding
applyImportDirective :: ImportDirective -> Scope -> Scope
renameCanonicalNames :: Map QName QName -> Map ModuleName ModuleName -> Scope -> Scope
restrictPrivate :: Scope -> Scope
restrictLocalPrivate :: ModuleName -> Scope -> Scope
removeOnlyQualified :: Scope -> Scope
inScopeBecause :: (WhyInScope -> WhyInScope) -> Scope -> Scope
publicModules :: ScopeInfo -> Map ModuleName Scope
publicNames :: ScopeInfo -> Set AbstractName
everythingInScope :: ScopeInfo -> NameSpace
flattenScope :: [[Name]] -> ScopeInfo -> Map QName [AbstractName]
concreteNamesInScope :: ScopeInfo -> Set QName
scopeLookup :: InScope a => QName -> ScopeInfo -> [a]
scopeLookup' :: forall a. InScope a => QName -> ScopeInfo -> [(a, Access)]
data AllowAmbiguousNames
- = AmbiguousAnything
- | AmbiguousConProjs
- | AmbiguousNothing
isNameInScope :: QName -> ScopeInfo -> Bool
inverseScopeLookup :: Either ModuleName QName -> ScopeInfo -> [QName]
inverseScopeLookup' :: AllowAmbiguousNames -> Either ModuleName QName -> ScopeInfo -> [QName]
recomputeInverseScopeMaps :: ScopeInfo -> ScopeInfo
inverseScopeLookupName :: QName -> ScopeInfo -> [QName]
inverseScopeLookupName' :: AllowAmbiguousNames -> QName -> ScopeInfo -> [QName]
inverseScopeLookupModule :: ModuleName -> ScopeInfo -> [QName]
prettyNameSpace :: NameSpace -> [Doc]
blockOfLines :: Doc -> [Doc] -> [Doc]

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 :: ScopeNameSpaces scopeImports :: Map QName ModuleName scopeDatatypeModule :: Maybe DataOrRecord

Instances

Eq Scope #
Instance details Defined in Agda.Syntax.Scope.Base Methods (==) :: Scope -> Scope -> Bool # (/=) :: Scope -> Scope -> Bool #
Data Scope #
Instance details Defined in Agda.Syntax.Scope.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Scope -> c Scope # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Scope # toConstr :: Scope -> Constr # dataTypeOf :: Scope -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Scope) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Scope) # gmapT :: (forall b. Data b => b -> b) -> Scope -> Scope # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Scope -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Scope -> r # gmapQ :: (forall d. Data d => d -> u) -> Scope -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Scope -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Scope -> m Scope # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Scope -> m Scope # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Scope -> m Scope #
Show Scope #
Instance details Defined in Agda.Syntax.Scope.Base Methods showsPrec :: Int -> Scope -> ShowS # show :: Scope -> String # showList :: [Scope] -> ShowS #
Pretty Scope #
Instance details Defined in Agda.Syntax.Scope.Base Methods pretty :: Scope -> Doc # prettyPrec :: Int -> Scope -> Doc # prettyList :: [Scope] -> Doc #
EmbPrj Scope #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: Scope -> S Int32 # icod_ :: Scope -> S Int32 # value :: Int32 -> R Scope #
InstantiateFull Scope #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Scope -> ReduceM Scope #

data NameSpaceId #

See Access.

Constructors

PrivateNS	Things not exported by this module.
PublicNS	Things defined and exported by this module.
ImportedNS	Things from open public, exported by this module.
OnlyQualifiedNS	Visible (as qualified) from outside, but not exported when opening the module. Used for qualified constructors.

Instances

Bounded NameSpaceId #
Instance details Defined in Agda.Syntax.Scope.Base Methods minBound :: NameSpaceId # maxBound :: NameSpaceId #
Enum NameSpaceId #
Instance details Defined in Agda.Syntax.Scope.Base Methods succ :: NameSpaceId -> NameSpaceId # pred :: NameSpaceId -> NameSpaceId # toEnum :: Int -> NameSpaceId # fromEnum :: NameSpaceId -> Int # enumFrom :: NameSpaceId -> [NameSpaceId] # enumFromThen :: NameSpaceId -> NameSpaceId -> [NameSpaceId] # enumFromTo :: NameSpaceId -> NameSpaceId -> [NameSpaceId] # enumFromThenTo :: NameSpaceId -> NameSpaceId -> NameSpaceId -> [NameSpaceId] #
Eq NameSpaceId #
Instance details Defined in Agda.Syntax.Scope.Base Methods (==) :: NameSpaceId -> NameSpaceId -> Bool # (/=) :: NameSpaceId -> NameSpaceId -> Bool #
Data NameSpaceId #
Instance details Defined in Agda.Syntax.Scope.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> NameSpaceId -> c NameSpaceId # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c NameSpaceId # toConstr :: NameSpaceId -> Constr # dataTypeOf :: NameSpaceId -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c NameSpaceId) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c NameSpaceId) # gmapT :: (forall b. Data b => b -> b) -> NameSpaceId -> NameSpaceId # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> NameSpaceId -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> NameSpaceId -> r # gmapQ :: (forall d. Data d => d -> u) -> NameSpaceId -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> NameSpaceId -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> NameSpaceId -> m NameSpaceId # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> NameSpaceId -> m NameSpaceId # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> NameSpaceId -> m NameSpaceId #
Show NameSpaceId #
Instance details Defined in Agda.Syntax.Scope.Base Methods showsPrec :: Int -> NameSpaceId -> ShowS # show :: NameSpaceId -> String # showList :: [NameSpaceId] -> ShowS #
Pretty NameSpaceId #
Instance details Defined in Agda.Syntax.Scope.Base Methods pretty :: NameSpaceId -> Doc # prettyPrec :: Int -> NameSpaceId -> Doc # prettyList :: [NameSpaceId] -> Doc #
EmbPrj NameSpaceId #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: NameSpaceId -> S Int32 # icod_ :: NameSpaceId -> S Int32 # value :: Int32 -> R NameSpaceId #

type ScopeNameSpaces = [(NameSpaceId, NameSpace)] #

localNameSpace :: Access -> NameSpaceId #

nameSpaceAccess :: NameSpaceId -> Access #

scopeNameSpace :: NameSpaceId -> Scope -> NameSpace #

Get a NameSpace from Scope.

updateScopeNameSpaces :: (ScopeNameSpaces -> ScopeNameSpaces) -> Scope -> Scope #

A lens for scopeNameSpaces

updateScopeNameSpacesM :: Functor m => (ScopeNameSpaces -> m ScopeNameSpaces) -> Scope -> m Scope #

`Monadic' lens (Functor sufficient).

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 scopeVarsToBind :: LocalVars scopeLocals :: LocalVars scopePrecedence :: PrecedenceStack scopeInverseName :: Map QName [QName] scopeInverseModule :: Map ModuleName [QName] scopeInScope :: InScopeSet

Instances

Eq ScopeInfo #
Instance details Defined in Agda.Syntax.Scope.Base Methods (==) :: ScopeInfo -> ScopeInfo -> Bool # (/=) :: ScopeInfo -> ScopeInfo -> Bool #
Data ScopeInfo #
Instance details Defined in Agda.Syntax.Scope.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ScopeInfo -> c ScopeInfo # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ScopeInfo # toConstr :: ScopeInfo -> Constr # dataTypeOf :: ScopeInfo -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ScopeInfo) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ScopeInfo) # gmapT :: (forall b. Data b => b -> b) -> ScopeInfo -> ScopeInfo # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ScopeInfo -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ScopeInfo -> r # gmapQ :: (forall d. Data d => d -> u) -> ScopeInfo -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> ScopeInfo -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> ScopeInfo -> m ScopeInfo # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ScopeInfo -> m ScopeInfo # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ScopeInfo -> m ScopeInfo #
Show ScopeInfo #
Instance details Defined in Agda.Syntax.Scope.Base Methods showsPrec :: Int -> ScopeInfo -> ShowS # show :: ScopeInfo -> String # showList :: [ScopeInfo] -> ShowS #
Pretty ScopeInfo #
Instance details Defined in Agda.Syntax.Scope.Base Methods pretty :: ScopeInfo -> Doc # prettyPrec :: Int -> ScopeInfo -> Doc # prettyList :: [ScopeInfo] -> Doc #
KillRange ScopeInfo #
Instance details Defined in Agda.Syntax.Scope.Base Methods killRange :: KillRangeT ScopeInfo #
EmbPrj ScopeInfo #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: ScopeInfo -> S Int32 # icod_ :: ScopeInfo -> S Int32 # value :: Int32 -> R ScopeInfo #

type LocalVars = AssocList Name LocalVar #

Local variables.

data Binder #

For each bound variable, we want to know whether it was bound by a λ, Π, module telescope, pattern, or let.

Constructors

LambdaBound	`λ` (currently also used for `Π` and module parameters)
PatternBound	f ... =
LetBound	let ... in

Instances

Eq Binder #
Instance details Defined in Agda.Syntax.Scope.Base Methods (==) :: Binder -> Binder -> Bool # (/=) :: Binder -> Binder -> Bool #
Data Binder #
Instance details Defined in Agda.Syntax.Scope.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Binder -> c Binder # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Binder # toConstr :: Binder -> Constr # dataTypeOf :: Binder -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Binder) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Binder) # gmapT :: (forall b. Data b => b -> b) -> Binder -> Binder # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Binder -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Binder -> r # gmapQ :: (forall d. Data d => d -> u) -> Binder -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Binder -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Binder -> m Binder # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Binder -> m Binder # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Binder -> m Binder #
Show Binder #
Instance details Defined in Agda.Syntax.Scope.Base Methods showsPrec :: Int -> Binder -> ShowS # show :: Binder -> String # showList :: [Binder] -> ShowS #
EmbPrj Binder #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: Binder -> S Int32 # icod_ :: Binder -> S Int32 # value :: Int32 -> R Binder #

data LocalVar #

A local variable can be shadowed by an import. In case of reference to a shadowed variable, we want to report a scope error.

Constructors

LocalVar
Fields localVar :: Name Unique ID of local variable. localBinder :: Binder Kind of binder used to introduce the variable (`λ`, `let`, ...). localShadowedBy :: [AbstractName] If this list is not empty, the local variable is shadowed by one or more imports.

Instances

Eq LocalVar #
Instance details Defined in Agda.Syntax.Scope.Base Methods (==) :: LocalVar -> LocalVar -> Bool # (/=) :: LocalVar -> LocalVar -> Bool #
Data LocalVar #
Instance details Defined in Agda.Syntax.Scope.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LocalVar -> c LocalVar # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LocalVar # toConstr :: LocalVar -> Constr # dataTypeOf :: LocalVar -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c LocalVar) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LocalVar) # gmapT :: (forall b. Data b => b -> b) -> LocalVar -> LocalVar # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LocalVar -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LocalVar -> r # gmapQ :: (forall d. Data d => d -> u) -> LocalVar -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> LocalVar -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> LocalVar -> m LocalVar # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LocalVar -> m LocalVar # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LocalVar -> m LocalVar #
Ord LocalVar #
Instance details Defined in Agda.Syntax.Scope.Base Methods compare :: LocalVar -> LocalVar -> Ordering # (<) :: LocalVar -> LocalVar -> Bool # (<=) :: LocalVar -> LocalVar -> Bool # (>) :: LocalVar -> LocalVar -> Bool # (>=) :: LocalVar -> LocalVar -> Bool # max :: LocalVar -> LocalVar -> LocalVar # min :: LocalVar -> LocalVar -> LocalVar #
Show LocalVar #
Instance details Defined in Agda.Syntax.Scope.Base Methods showsPrec :: Int -> LocalVar -> ShowS # show :: LocalVar -> String # showList :: [LocalVar] -> ShowS #
Pretty LocalVar #	We show shadowed variables as prefixed by a ".", as not in scope.
Instance details Defined in Agda.Syntax.Scope.Base Methods pretty :: LocalVar -> Doc # prettyPrec :: Int -> LocalVar -> Doc # prettyList :: [LocalVar] -> Doc #
EmbPrj LocalVar #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: LocalVar -> S Int32 # icod_ :: LocalVar -> S Int32 # value :: Int32 -> R LocalVar #

shadowLocal :: [AbstractName] -> LocalVar -> LocalVar #

Shadow a local name by a non-empty list of imports.

notShadowedLocal :: LocalVar -> Maybe Name #

Project name of unshadowed local variable.

notShadowedLocals :: LocalVars -> AssocList Name Name #

Get all locals that are not shadowed by imports.

updateVarsToBind :: (LocalVars -> LocalVars) -> ScopeInfo -> ScopeInfo #

Lens for scopeVarsToBind.

setVarsToBind :: LocalVars -> ScopeInfo -> ScopeInfo #

updateScopeLocals :: (LocalVars -> LocalVars) -> ScopeInfo -> ScopeInfo #

Lens for scopeLocals.

setScopeLocals :: LocalVars -> ScopeInfo -> ScopeInfo #

mapScopeInfo :: (Scope -> Scope) -> ScopeInfo -> ScopeInfo #

Name spaces

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 Maps concrete names to a list of abstract names. nsModules :: ModulesInScope Maps concrete module names to a list of abstract module names. nsInScope :: InScopeSet

Instances

Eq NameSpace #
Instance details Defined in Agda.Syntax.Scope.Base Methods (==) :: NameSpace -> NameSpace -> Bool # (/=) :: NameSpace -> NameSpace -> Bool #
Data NameSpace #
Instance details Defined in Agda.Syntax.Scope.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> NameSpace -> c NameSpace # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c NameSpace # toConstr :: NameSpace -> Constr # dataTypeOf :: NameSpace -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c NameSpace) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c NameSpace) # gmapT :: (forall b. Data b => b -> b) -> NameSpace -> NameSpace # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> NameSpace -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> NameSpace -> r # gmapQ :: (forall d. Data d => d -> u) -> NameSpace -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> NameSpace -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> NameSpace -> m NameSpace # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> NameSpace -> m NameSpace # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> NameSpace -> m NameSpace #
Show NameSpace #
Instance details Defined in Agda.Syntax.Scope.Base Methods showsPrec :: Int -> NameSpace -> ShowS # show :: NameSpace -> String # showList :: [NameSpace] -> ShowS #
Pretty NameSpace #
Instance details Defined in Agda.Syntax.Scope.Base Methods pretty :: NameSpace -> Doc # prettyPrec :: Int -> NameSpace -> Doc # prettyList :: [NameSpace] -> Doc #
EmbPrj NameSpace #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: NameSpace -> S Int32 # icod_ :: NameSpace -> S Int32 # value :: Int32 -> R NameSpace #

type ThingsInScope a = Map Name [a] #

type NamesInScope = ThingsInScope AbstractName #

type ModulesInScope = ThingsInScope AbstractModule #

type InScopeSet = Set QName #

data InScopeTag a where #

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 #

Type class for some dependent-types trickery.

Minimal complete definition

inScopeTag

Methods

inScopeTag :: InScopeTag a #

Instances

InScope AbstractModule #
Instance details Defined in Agda.Syntax.Scope.Base Methods inScopeTag :: InScopeTag AbstractModule #
InScope AbstractName #
Instance details Defined in Agda.Syntax.Scope.Base Methods inScopeTag :: InScopeTag AbstractName #

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

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 #

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.
MacroName	Name of a macro
QuotableName	A name that can only be quoted.

Instances

Bounded KindOfName #
Instance details Defined in Agda.Syntax.Scope.Base Methods minBound :: KindOfName # maxBound :: KindOfName #
Enum KindOfName #
Instance details Defined in Agda.Syntax.Scope.Base Methods succ :: KindOfName -> KindOfName # pred :: KindOfName -> KindOfName # toEnum :: Int -> KindOfName # fromEnum :: KindOfName -> Int # enumFrom :: KindOfName -> [KindOfName] # enumFromThen :: KindOfName -> KindOfName -> [KindOfName] # enumFromTo :: KindOfName -> KindOfName -> [KindOfName] # enumFromThenTo :: KindOfName -> KindOfName -> KindOfName -> [KindOfName] #
Eq KindOfName #
Instance details Defined in Agda.Syntax.Scope.Base Methods (==) :: KindOfName -> KindOfName -> Bool # (/=) :: KindOfName -> KindOfName -> Bool #
Data KindOfName #
Instance details Defined in Agda.Syntax.Scope.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> KindOfName -> c KindOfName # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c KindOfName # toConstr :: KindOfName -> Constr # dataTypeOf :: KindOfName -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c KindOfName) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c KindOfName) # gmapT :: (forall b. Data b => b -> b) -> KindOfName -> KindOfName # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> KindOfName -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> KindOfName -> r # gmapQ :: (forall d. Data d => d -> u) -> KindOfName -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> KindOfName -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> KindOfName -> m KindOfName # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> KindOfName -> m KindOfName # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> KindOfName -> m KindOfName #
Show KindOfName #
Instance details Defined in Agda.Syntax.Scope.Base Methods showsPrec :: Int -> KindOfName -> ShowS # show :: KindOfName -> String # showList :: [KindOfName] -> ShowS #
EmbPrj KindOfName #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: KindOfName -> S Int32 # icod_ :: KindOfName -> S Int32 # value :: Int32 -> R KindOfName #

allKindsOfNames :: [KindOfName] #

A list containing all name kinds.

data WhyInScope #

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 WhyInScope #
Instance details Defined in Agda.Syntax.Scope.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> WhyInScope -> c WhyInScope # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c WhyInScope # toConstr :: WhyInScope -> Constr # dataTypeOf :: WhyInScope -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c WhyInScope) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c WhyInScope) # gmapT :: (forall b. Data b => b -> b) -> WhyInScope -> WhyInScope # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> WhyInScope -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> WhyInScope -> r # gmapQ :: (forall d. Data d => d -> u) -> WhyInScope -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> WhyInScope -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> WhyInScope -> m WhyInScope # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> WhyInScope -> m WhyInScope # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> WhyInScope -> m WhyInScope #
Show WhyInScope #
Instance details Defined in Agda.Syntax.Scope.Base Methods showsPrec :: Int -> WhyInScope -> ShowS # show :: WhyInScope -> String # showList :: [WhyInScope] -> ShowS #
EmbPrj WhyInScope #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: WhyInScope -> S Int32 # icod_ :: WhyInScope -> S Int32 # value :: Int32 -> R WhyInScope #

data AbstractName #

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

Eq AbstractName #
Instance details Defined in Agda.Syntax.Scope.Base Methods (==) :: AbstractName -> AbstractName -> Bool # (/=) :: AbstractName -> AbstractName -> Bool #
Data AbstractName #
Instance details Defined in Agda.Syntax.Scope.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> AbstractName -> c AbstractName # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c AbstractName # toConstr :: AbstractName -> Constr # dataTypeOf :: AbstractName -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c AbstractName) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c AbstractName) # gmapT :: (forall b. Data b => b -> b) -> AbstractName -> AbstractName # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> AbstractName -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> AbstractName -> r # gmapQ :: (forall d. Data d => d -> u) -> AbstractName -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> AbstractName -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> AbstractName -> m AbstractName # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> AbstractName -> m AbstractName # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> AbstractName -> m AbstractName #
Ord AbstractName #
Instance details Defined in Agda.Syntax.Scope.Base Methods compare :: AbstractName -> AbstractName -> Ordering # (<) :: AbstractName -> AbstractName -> Bool # (<=) :: AbstractName -> AbstractName -> Bool # (>) :: AbstractName -> AbstractName -> Bool # (>=) :: AbstractName -> AbstractName -> Bool # max :: AbstractName -> AbstractName -> AbstractName # min :: AbstractName -> AbstractName -> AbstractName #
Show AbstractName #
Instance details Defined in Agda.Syntax.Scope.Base Methods showsPrec :: Int -> AbstractName -> ShowS # show :: AbstractName -> String # showList :: [AbstractName] -> ShowS #
Pretty AbstractName #
Instance details Defined in Agda.Syntax.Scope.Base Methods pretty :: AbstractName -> Doc # prettyPrec :: Int -> AbstractName -> Doc # prettyList :: [AbstractName] -> Doc #
SetRange AbstractName #
Instance details Defined in Agda.Syntax.Scope.Base Methods setRange :: Range -> AbstractName -> AbstractName #
HasRange AbstractName #
Instance details Defined in Agda.Syntax.Scope.Base Methods getRange :: AbstractName -> Range #
InScope AbstractName #
Instance details Defined in Agda.Syntax.Scope.Base Methods inScopeTag :: InScopeTag AbstractName #
NameToExpr AbstractName #	Turn an `AbstractName` to an expression.
Instance details Defined in Agda.Syntax.Abstract Methods nameExpr :: AbstractName -> Expr #
EmbPrj AbstractName #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: AbstractName -> S Int32 # icod_ :: AbstractName -> S Int32 # value :: Int32 -> R AbstractName #
ToConcrete AbstractName QName #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: AbstractName -> AbsToCon QName # bindToConcrete :: AbstractName -> (QName -> AbsToCon b) -> AbsToCon b #

data AbstractModule #

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

Eq AbstractModule #
Instance details Defined in Agda.Syntax.Scope.Base Methods (==) :: AbstractModule -> AbstractModule -> Bool # (/=) :: AbstractModule -> AbstractModule -> Bool #
Data AbstractModule #
Instance details Defined in Agda.Syntax.Scope.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> AbstractModule -> c AbstractModule # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c AbstractModule # toConstr :: AbstractModule -> Constr # dataTypeOf :: AbstractModule -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c AbstractModule) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c AbstractModule) # gmapT :: (forall b. Data b => b -> b) -> AbstractModule -> AbstractModule # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> AbstractModule -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> AbstractModule -> r # gmapQ :: (forall d. Data d => d -> u) -> AbstractModule -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> AbstractModule -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> AbstractModule -> m AbstractModule # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> AbstractModule -> m AbstractModule # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> AbstractModule -> m AbstractModule #
Ord AbstractModule #
Instance details Defined in Agda.Syntax.Scope.Base Methods compare :: AbstractModule -> AbstractModule -> Ordering # (<) :: AbstractModule -> AbstractModule -> Bool # (<=) :: AbstractModule -> AbstractModule -> Bool # (>) :: AbstractModule -> AbstractModule -> Bool # (>=) :: AbstractModule -> AbstractModule -> Bool # max :: AbstractModule -> AbstractModule -> AbstractModule # min :: AbstractModule -> AbstractModule -> AbstractModule #
Show AbstractModule #
Instance details Defined in Agda.Syntax.Scope.Base Methods showsPrec :: Int -> AbstractModule -> ShowS # show :: AbstractModule -> String # showList :: [AbstractModule] -> ShowS #
Pretty AbstractModule #
Instance details Defined in Agda.Syntax.Scope.Base Methods pretty :: AbstractModule -> Doc # prettyPrec :: Int -> AbstractModule -> Doc # prettyList :: [AbstractModule] -> Doc #
InScope AbstractModule #
Instance details Defined in Agda.Syntax.Scope.Base Methods inScopeTag :: InScopeTag AbstractModule #
EmbPrj AbstractModule #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: AbstractModule -> S Int32 # icod_ :: AbstractModule -> S Int32 # value :: Int32 -> R AbstractModule #

lensAnameName :: Functor m => (QName -> m QName) -> AbstractName -> m AbstractName #

Van Laarhoven lens on anameName.

lensAmodName :: Functor m => (ModuleName -> m ModuleName) -> AbstractModule -> m AbstractModule #

Van Laarhoven lens on amodName.

data ResolvedName #

Constructors

VarName	Local variable bound by λ, Π, module telescope, pattern, `let`.
Fields resolvedVar :: Name resolvedBinder :: Binder What kind of binder?
DefinedName Access AbstractName	Function, data/record type, postulate.
FieldName (NonemptyList AbstractName)	Record field name. Needs to be distinguished to parse copatterns.
ConstructorName (NonemptyList AbstractName)	Data or record constructor name.
PatternSynResName (NonemptyList AbstractName)	Name of pattern synonym.
UnknownName	Unbound name.

Instances

Eq ResolvedName #
Instance details Defined in Agda.Syntax.Scope.Base Methods (==) :: ResolvedName -> ResolvedName -> Bool # (/=) :: ResolvedName -> ResolvedName -> Bool #
Data ResolvedName #
Instance details Defined in Agda.Syntax.Scope.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ResolvedName -> c ResolvedName # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ResolvedName # toConstr :: ResolvedName -> Constr # dataTypeOf :: ResolvedName -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ResolvedName) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ResolvedName) # gmapT :: (forall b. Data b => b -> b) -> ResolvedName -> ResolvedName # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ResolvedName -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ResolvedName -> r # gmapQ :: (forall d. Data d => d -> u) -> ResolvedName -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> ResolvedName -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> ResolvedName -> m ResolvedName # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ResolvedName -> m ResolvedName # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ResolvedName -> m ResolvedName #
Show ResolvedName #
Instance details Defined in Agda.Syntax.Scope.Base Methods showsPrec :: Int -> ResolvedName -> ShowS # show :: ResolvedName -> String # showList :: [ResolvedName] -> ShowS #
Pretty ResolvedName #
Instance details Defined in Agda.Syntax.Scope.Base Methods pretty :: ResolvedName -> Doc # prettyPrec :: Int -> ResolvedName -> Doc # prettyList :: [ResolvedName] -> Doc #
NameToExpr ResolvedName #	Assumes name is not `UnknownName`.
Instance details Defined in Agda.Syntax.Abstract Methods nameExpr :: ResolvedName -> Expr #
ToConcrete ResolvedName QName #	Assumes name is not `UnknownName`.
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: ResolvedName -> AbsToCon QName # bindToConcrete :: ResolvedName -> (QName -> AbsToCon b) -> AbsToCon b #

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) -> (InScopeSet -> InScopeSet) -> NameSpace -> NameSpace #

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

zipNameSpace :: (NamesInScope -> NamesInScope -> NamesInScope) -> (ModulesInScope -> ModulesInScope -> ModulesInScope) -> (InScopeSet -> InScopeSet -> InScopeSet) -> NameSpace -> NameSpace -> NameSpace #

Zip together two name spaces.

mapNameSpaceM :: Applicative m => (NamesInScope -> m NamesInScope) -> (ModulesInScope -> m ModulesInScope) -> (InScopeSet -> m InScopeSet) -> 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) -> (NameSpaceId -> InScopeSet -> InScopeSet) -> Scope -> Scope #

Map functions over the names and modules in a scope.

mapScope_ :: (NamesInScope -> NamesInScope) -> (ModulesInScope -> ModulesInScope) -> (InScopeSet -> InScopeSet) -> Scope -> Scope #

Same as mapScope but applies the same function to all name spaces.

mapScope' :: NameSpaceId -> (NamesInScope -> NamesInScope) -> (ModulesInScope -> ModulesInScope) -> (InScopeSet -> InScopeSet) -> Scope -> Scope #

Same as mapScope but applies the function only on the given name space.

mapScopeM :: Applicative m => (NameSpaceId -> NamesInScope -> m NamesInScope) -> (NameSpaceId -> ModulesInScope -> m ModulesInScope) -> (NameSpaceId -> InScopeSet -> m InScopeSet) -> Scope -> m Scope #

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

mapScopeM_ :: Applicative m => (NamesInScope -> m NamesInScope) -> (ModulesInScope -> m ModulesInScope) -> (InScopeSet -> m InScopeSet) -> 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) -> (NameSpaceId -> InScopeSet -> InScopeSet -> InScopeSet) -> 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) -> (InScopeSet -> InScopeSet -> InScopeSet) -> Scope -> Scope -> Scope #

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

recomputeInScopeSets :: Scope -> Scope #

Recompute the inScope sets of a scope.

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 #

Update a particular name space.

modifyNameSpace :: NameSpaceId -> (NameSpace -> NameSpace) -> Scope -> Scope #

Modify a particular name space.

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

Add names to a scope.

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

Add a name to a scope.

removeNameFromScope :: NameSpaceId -> Name -> Scope -> Scope #

Remove a name from a scope. Caution: does not update the nsInScope set. This is only used by rebindName and in that case we add the name right back (but with a different kind).

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

Add a module to a scope.

type UsingOrHiding = Either Using [ImportedName] #

usingOrHiding :: ImportDirective -> UsingOrHiding #

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 #

Remove private name space of a scope.

Should be a right identity for exportedNamesInScope. exportedNamesInScope . restrictPrivate == exportedNamesInScope.

restrictLocalPrivate :: ModuleName -> Scope -> Scope #

Remove private things from the given module from a scope.

removeOnlyQualified :: Scope -> Scope #

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

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

Add an explanation to why things are in scope.

publicModules :: ScopeInfo -> Map ModuleName Scope #

Get the public parts of the public modules of a scope

publicNames :: ScopeInfo -> Set AbstractName #

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.

concreteNamesInScope :: ScopeInfo -> Set QName #

Get all concrete names in scope. Includes bound variables.

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

data AllowAmbiguousNames #

Constructors

AmbiguousAnything	Used for instance arguments to check whether a name is in scope, but we do not care whether is is ambiguous
AmbiguousConProjs	Ambiguous constructors, projections, or pattern synonyms.
AmbiguousNothing

Instances

Eq AllowAmbiguousNames #
Instance details Defined in Agda.Syntax.Scope.Base Methods (==) :: AllowAmbiguousNames -> AllowAmbiguousNames -> Bool # (/=) :: AllowAmbiguousNames -> AllowAmbiguousNames -> Bool #