Safe Haskell	Safe-Inferred
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
Update binding site
(Debug) printing
Boring instances
Orphan 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 DataOrRecordModule
}
data DataOrRecordModule
- = IsDataModule
- | IsRecordModule
data NameSpaceId
- = PrivateNS
- | PublicNS
- | ImportedNS
allNameSpaces :: [NameSpaceId]
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 :: NameMap
- _scopeInverseModule :: ModuleMap
- _scopeInScope :: InScopeSet
- _scopeFixities :: Fixities
- _scopePolarities :: Polarities
}
data NameMapEntry = NameMapEntry {
- qnameKind :: KindOfName
- qnameConcrete :: List1 QName
}
type NameMap = Map QName NameMapEntry
type ModuleMap = Map ModuleName [QName]
type LocalVars = AssocList Name LocalVar
data BindingSource
- = LambdaBound
- | PatternBound
- | LetBound
- | WithBound
data LocalVar = LocalVar {
- localVar :: Name
- localBindingSource :: BindingSource
- localShadowedBy :: [AbstractName]
}
shadowLocal :: List1 AbstractName -> LocalVar -> LocalVar
patternToModuleBound :: LocalVar -> LocalVar
notShadowedLocal :: LocalVar -> Maybe Name
notShadowedLocals :: LocalVars -> AssocList Name Name
scopeCurrent :: Lens' ScopeInfo ModuleName
scopeModules :: Lens' ScopeInfo (Map ModuleName Scope)
scopeVarsToBind :: Lens' ScopeInfo LocalVars
scopeLocals :: Lens' ScopeInfo LocalVars
scopePrecedence :: Lens' ScopeInfo PrecedenceStack
scopeInverseName :: Lens' ScopeInfo NameMap
scopeInverseModule :: Lens' ScopeInfo ModuleMap
scopeInScope :: Lens' ScopeInfo InScopeSet
scopeFixities :: Lens' ScopeInfo Fixities
scopePolarities :: Lens' ScopeInfo Polarities
scopeFixitiesAndPolarities :: Lens' ScopeInfo (Fixities, Polarities)
updateVarsToBind :: (LocalVars -> LocalVars) -> ScopeInfo -> ScopeInfo
setVarsToBind :: LocalVars -> ScopeInfo -> ScopeInfo
updateScopeLocals :: (LocalVars -> LocalVars) -> ScopeInfo -> ScopeInfo
setScopeLocals :: LocalVars -> ScopeInfo -> ScopeInfo
data NameSpace = NameSpace {
- nsNames :: NamesInScope
- nsModules :: ModulesInScope
- nsInScope :: InScopeSet
}
type ThingsInScope a = Map Name (List1 a)
type NamesInScope = ThingsInScope AbstractName
type ModulesInScope = ThingsInScope AbstractModule
type InScopeSet = Set QName
data InScopeTag a where
- NameTag :: InScopeTag AbstractName
- ModuleTag :: InScopeTag AbstractModule
class Ord a => InScope a where
- inScopeTag :: InScopeTag a
inNameSpace :: forall a. InScope a => NameSpace -> ThingsInScope a
data NameOrModule
- = NameNotModule
- | ModuleNotName
data KindOfName
- = ConName
- | CoConName
- | FldName
- | PatternSynName
- | GeneralizeName
- | DisallowedGeneralizeName
- | MacroName
- | QuotableName
- | DataName
- | RecName
- | FunName
- | AxiomName
- | PrimName
- | OtherDefName
isDefName :: KindOfName -> Bool
isConName :: KindOfName -> Maybe Induction
conKindOfName :: Induction -> KindOfName
conKindOfName' :: Foldable t => t Induction -> KindOfName
approxConInduction :: Foldable t => t Induction -> Induction
exactConInduction :: Foldable t => t Induction -> Maybe Induction
exactConName :: Foldable t => t Induction -> Maybe KindOfName
data KindsOfNames
- = AllKindsOfNames
- | SomeKindsOfNames (Set KindOfName)
- | ExceptKindsOfNames (Set KindOfName)
elemKindsOfNames :: KindOfName -> KindsOfNames -> Bool
allKindsOfNames :: KindsOfNames
someKindsOfNames :: [KindOfName] -> KindsOfNames
exceptKindsOfNames :: [KindOfName] -> KindsOfNames
data WithKind a = WithKind {
- theKind :: KindOfName
- kindedThing :: a
}
data WhyInScope
- = Defined
- | Opened QName WhyInScope
- | Applied QName WhyInScope
data AbstractName = AbsName {
- anameName :: QName
- anameKind :: KindOfName
- anameLineage :: WhyInScope
- anameMetadata :: NameMetadata
}
data NameMetadata
- = NoMetadata
- | GeneralizedVarsMetadata (Map QName Name)
data AbstractModule = AbsModule {
- amodName :: ModuleName
- amodLineage :: WhyInScope
}
lensAnameName :: Lens' AbstractName QName
lensAmodName :: Lens' AbstractModule ModuleName
data ResolvedName
- = VarName {
  - resolvedVar :: Name
  - resolvedBindingSource :: BindingSource
  }
- | DefinedName Access AbstractName Suffix
- | FieldName (List1 AbstractName)
- | ConstructorName (Set Induction) (List1 AbstractName)
- | PatternSynResName (List1 AbstractName)
- | UnknownName
data AmbiguousNameReason
- = AmbiguousLocalVar LocalVar (List1 AbstractName)
- | AmbiguousDeclName (List2 AbstractName)
ambiguousNamesInReason :: AmbiguousNameReason -> List2 QName
data WhyInScopeData = WhyInScopeData QName FilePath (Maybe LocalVar) [AbstractName] [AbstractModule]
whyInScopeDataFromAmbiguousNameReason :: QName -> AmbiguousNameReason -> WhyInScopeData
mergeNames :: Eq a => ThingsInScope a -> ThingsInScope a -> ThingsInScope a
mergeNamesMany :: Eq 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
mapScopeNS :: 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)
findNameInScope :: InScope a => Name -> Scope -> [(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
addNameToScope :: NameSpaceId -> Name -> AbstractName -> Scope -> Scope
removeNameFromScope :: NameSpaceId -> Name -> Scope -> Scope
addModuleToScope :: NameSpaceId -> Name -> AbstractModule -> Scope -> Scope
data UsingOrHiding
- = UsingOnly [ImportedName]
- | HidingOnly [ImportedName]
usingOrHiding :: ImportDirective -> UsingOrHiding
applyImportDirective :: ImportDirective -> Scope -> Scope
applyImportDirective_ :: ImportDirective -> Scope -> (Scope, (Set Name, Set Name))
renameCanonicalNames :: Map QName QName -> Map ModuleName ModuleName -> Scope -> Scope
restrictPrivate :: Scope -> Scope
restrictLocalPrivate :: ModuleName -> Scope -> Scope
withoutPrivates :: ScopeInfo -> ScopeInfo
disallowGeneralizedVars :: Scope -> Scope
inScopeBecause :: (WhyInScope -> WhyInScope) -> Scope -> Scope
publicModules :: ScopeInfo -> Map ModuleName Scope
publicNames :: ScopeInfo -> Set AbstractName
everythingInScope :: ScopeInfo -> NameSpace
everythingInScopeQualified :: ScopeInfo -> NameSpace
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
isNameInScopeUnqualified :: QName -> ScopeInfo -> Bool
inverseScopeLookupName :: QName -> ScopeInfo -> [QName]
inverseScopeLookupName' :: AllowAmbiguousNames -> QName -> ScopeInfo -> [QName]
inverseScopeLookupName'' :: AllowAmbiguousNames -> QName -> ScopeInfo -> Maybe NameMapEntry
inverseScopeLookupModule :: ModuleName -> ScopeInfo -> [QName]
inverseScopeLookupModule' :: AllowAmbiguousNames -> ModuleName -> ScopeInfo -> [QName]
recomputeInverseScopeMaps :: ScopeInfo -> ScopeInfo
class SetBindingSite a where
- setBindingSite :: Range -> a -> a
prettyNameSpace :: NameSpace -> [Doc]
blockOfLines :: Doc -> [Doc] -> [Doc]

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

Instances

Instances details

Pretty Scope Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods pretty :: Scope -> Doc Source # prettyPrec :: Int -> Scope -> Doc Source # prettyList :: [Scope] -> Doc Source #
InstantiateFull Scope Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Scope -> ReduceM Scope Source #
EmbPrj Scope Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: Scope -> S Int32 Source # icod_ :: Scope -> S Int32 Source # value :: Int32 -> R Scope Source #
Null Scope Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods empty :: Scope Source # null :: Scope -> Bool Source #
Generic Scope Source #
Instance details Defined in Agda.Syntax.Scope.Base Associated Types type Rep Scope :: Type -> Type Methods from :: Scope -> Rep Scope x to :: Rep Scope x -> Scope
Show Scope Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods showsPrec :: Int -> Scope -> ShowS show :: Scope -> String showList :: [Scope] -> ShowS
NFData Scope Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods rnf :: Scope -> ()
Eq Scope Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods (==) :: Scope -> Scope -> Bool (/=) :: Scope -> Scope -> Bool
type Rep Scope Source #
Instance details Defined in Agda.Syntax.Scope.Base type Rep Scope = D1 ('MetaData "Scope" "Agda.Syntax.Scope.Base" "Agda-2.6.3.20230930-inplace" 'False) (C1 ('MetaCons "Scope" 'PrefixI 'True) ((S1 ('MetaSel ('Just "scopeName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName) :: S1 ('MetaSel ('Just "scopeParents") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [ModuleName])) :: (S1 ('MetaSel ('Just "scopeNameSpaces") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ScopeNameSpaces) :: (S1 ('MetaSel ('Just "scopeImports") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map QName ModuleName)) :: S1 ('MetaSel ('Just "scopeDatatypeModule") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe DataOrRecordModule))))))

data DataOrRecordModule Source #

Constructors

IsDataModule
IsRecordModule

Instances

Instances details

EmbPrj DataOrRecordModule Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: DataOrRecordModule -> S Int32 Source # icod_ :: DataOrRecordModule -> S Int32 Source # value :: Int32 -> R DataOrRecordModule Source #
Bounded DataOrRecordModule Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods minBound :: DataOrRecordModule maxBound :: DataOrRecordModule
Enum DataOrRecordModule Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods succ :: DataOrRecordModule -> DataOrRecordModule pred :: DataOrRecordModule -> DataOrRecordModule toEnum :: Int -> DataOrRecordModule fromEnum :: DataOrRecordModule -> Int enumFrom :: DataOrRecordModule -> [DataOrRecordModule] enumFromThen :: DataOrRecordModule -> DataOrRecordModule -> [DataOrRecordModule] enumFromTo :: DataOrRecordModule -> DataOrRecordModule -> [DataOrRecordModule] enumFromThenTo :: DataOrRecordModule -> DataOrRecordModule -> DataOrRecordModule -> [DataOrRecordModule]
Generic DataOrRecordModule Source #
Instance details Defined in Agda.Syntax.Scope.Base Associated Types type Rep DataOrRecordModule :: Type -> Type Methods from :: DataOrRecordModule -> Rep DataOrRecordModule x to :: Rep DataOrRecordModule x -> DataOrRecordModule
Show DataOrRecordModule Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods showsPrec :: Int -> DataOrRecordModule -> ShowS show :: DataOrRecordModule -> String showList :: [DataOrRecordModule] -> ShowS
NFData DataOrRecordModule Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods rnf :: DataOrRecordModule -> ()
Eq DataOrRecordModule Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods (==) :: DataOrRecordModule -> DataOrRecordModule -> Bool (/=) :: DataOrRecordModule -> DataOrRecordModule -> Bool
type Rep DataOrRecordModule Source #
Instance details Defined in Agda.Syntax.Scope.Base type Rep DataOrRecordModule = D1 ('MetaData "DataOrRecordModule" "Agda.Syntax.Scope.Base" "Agda-2.6.3.20230930-inplace" 'False) (C1 ('MetaCons "IsDataModule" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "IsRecordModule" 'PrefixI 'False) (U1 :: Type -> Type))

data NameSpaceId Source #

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.

Instances

Instances details

Pretty NameSpaceId Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods pretty :: NameSpaceId -> Doc Source # prettyPrec :: Int -> NameSpaceId -> Doc Source # prettyList :: [NameSpaceId] -> Doc Source #
EmbPrj NameSpaceId Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: NameSpaceId -> S Int32 Source # icod_ :: NameSpaceId -> S Int32 Source # value :: Int32 -> R NameSpaceId Source #
Bounded NameSpaceId Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods minBound :: NameSpaceId maxBound :: NameSpaceId
Enum NameSpaceId Source #
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]
Generic NameSpaceId Source #
Instance details Defined in Agda.Syntax.Scope.Base Associated Types type Rep NameSpaceId :: Type -> Type Methods from :: NameSpaceId -> Rep NameSpaceId x to :: Rep NameSpaceId x -> NameSpaceId
Show NameSpaceId Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods showsPrec :: Int -> NameSpaceId -> ShowS show :: NameSpaceId -> String showList :: [NameSpaceId] -> ShowS
NFData NameSpaceId Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods rnf :: NameSpaceId -> ()
Eq NameSpaceId Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods (==) :: NameSpaceId -> NameSpaceId -> Bool (/=) :: NameSpaceId -> NameSpaceId -> Bool
type Rep NameSpaceId Source #
Instance details Defined in Agda.Syntax.Scope.Base type Rep NameSpaceId = D1 ('MetaData "NameSpaceId" "Agda.Syntax.Scope.Base" "Agda-2.6.3.20230930-inplace" 'False) (C1 ('MetaCons "PrivateNS" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "PublicNS" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ImportedNS" 'PrefixI 'False) (U1 :: Type -> Type)))

allNameSpaces :: [NameSpaceId] Source #

type ScopeNameSpaces = [(NameSpaceId, NameSpace)] Source #

localNameSpace :: Access -> NameSpaceId Source #

nameSpaceAccess :: NameSpaceId -> Access Source #

scopeNameSpace :: NameSpaceId -> Scope -> NameSpace Source #

Get a NameSpace from Scope.

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

A lens for scopeNameSpaces

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

`Monadic' lens (Functor sufficient).

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
_scopeVarsToBind :: LocalVars
The variables that will be bound at the end of the current block of variables (i.e. clause). We collect them here instead of binding them immediately so we can avoid shadowing between variables in the same variable block.
_scopeLocals :: LocalVars
_scopePrecedence :: !PrecedenceStack
_scopeInverseName :: NameMap
_scopeInverseModule :: ModuleMap
_scopeInScope :: InScopeSet
_scopeFixities :: Fixities
Maps concrete names C.Name to fixities
_scopePolarities :: Polarities
Maps concrete names C.Name to polarities

Instances

Instances details

Pretty ScopeInfo Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods pretty :: ScopeInfo -> Doc Source # prettyPrec :: Int -> ScopeInfo -> Doc Source # prettyList :: [ScopeInfo] -> Doc Source #
KillRange ScopeInfo Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods killRange :: KillRangeT ScopeInfo Source #
EmbPrj ScopeInfo Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: ScopeInfo -> S Int32 Source # icod_ :: ScopeInfo -> S Int32 Source # value :: Int32 -> R ScopeInfo Source #
Null ScopeInfo Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods empty :: ScopeInfo Source # null :: ScopeInfo -> Bool Source #
Generic ScopeInfo Source #
Instance details Defined in Agda.Syntax.Scope.Base Associated Types type Rep ScopeInfo :: Type -> Type Methods from :: ScopeInfo -> Rep ScopeInfo x to :: Rep ScopeInfo x -> ScopeInfo
Show ScopeInfo Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods showsPrec :: Int -> ScopeInfo -> ShowS show :: ScopeInfo -> String showList :: [ScopeInfo] -> ShowS
NFData ScopeInfo Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods rnf :: ScopeInfo -> ()
Eq ScopeInfo Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods (==) :: ScopeInfo -> ScopeInfo -> Bool (/=) :: ScopeInfo -> ScopeInfo -> Bool
type Rep ScopeInfo Source #
Instance details Defined in Agda.Syntax.Scope.Base type Rep ScopeInfo = D1 ('MetaData "ScopeInfo" "Agda.Syntax.Scope.Base" "Agda-2.6.3.20230930-inplace" 'False) (C1 ('MetaCons "ScopeInfo" 'PrefixI 'True) (((S1 ('MetaSel ('Just "_scopeCurrent") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName) :: S1 ('MetaSel ('Just "_scopeModules") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map ModuleName Scope))) :: (S1 ('MetaSel ('Just "_scopeVarsToBind") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LocalVars) :: (S1 ('MetaSel ('Just "_scopeLocals") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LocalVars) :: S1 ('MetaSel ('Just "_scopePrecedence") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 PrecedenceStack)))) :: ((S1 ('MetaSel ('Just "_scopeInverseName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NameMap) :: S1 ('MetaSel ('Just "_scopeInverseModule") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleMap)) :: (S1 ('MetaSel ('Just "_scopeInScope") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 InScopeSet) :: (S1 ('MetaSel ('Just "_scopeFixities") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Fixities) :*: S1 ('MetaSel ('Just "_scopePolarities") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Polarities))))))

data NameMapEntry Source #

For the sake of highlighting, the _scopeInverseName map also stores the KindOfName of an A.QName.

Constructors

NameMapEntry
Fields qnameKind :: KindOfName The `anameKind`. qnameConcrete :: List1 QName Possible renderings of the abstract name.

Instances

Instances details

Semigroup NameMapEntry Source #	Invariant: the `KindOfName` components should be equal whenever we have to concrete renderings of an abstract name.
Instance details Defined in Agda.Syntax.Scope.Base Methods (<>) :: NameMapEntry -> NameMapEntry -> NameMapEntry # sconcat :: NonEmpty NameMapEntry -> NameMapEntry stimes :: Integral b => b -> NameMapEntry -> NameMapEntry
Generic NameMapEntry Source #
Instance details Defined in Agda.Syntax.Scope.Base Associated Types type Rep NameMapEntry :: Type -> Type Methods from :: NameMapEntry -> Rep NameMapEntry x to :: Rep NameMapEntry x -> NameMapEntry
Show NameMapEntry Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods showsPrec :: Int -> NameMapEntry -> ShowS show :: NameMapEntry -> String showList :: [NameMapEntry] -> ShowS
NFData NameMapEntry Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods rnf :: NameMapEntry -> ()
type Rep NameMapEntry Source #
Instance details Defined in Agda.Syntax.Scope.Base type Rep NameMapEntry = D1 ('MetaData "NameMapEntry" "Agda.Syntax.Scope.Base" "Agda-2.6.3.20230930-inplace" 'False) (C1 ('MetaCons "NameMapEntry" 'PrefixI 'True) (S1 ('MetaSel ('Just "qnameKind") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KindOfName) :*: S1 ('MetaSel ('Just "qnameConcrete") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 QName))))

type NameMap = Map QName NameMapEntry Source #

type ModuleMap = Map ModuleName [QName] Source #

type LocalVars = AssocList Name LocalVar Source #

Local variables.

data BindingSource Source #

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
WithBound	\| ... in q

Instances

Instances details

Pretty BindingSource Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods pretty :: BindingSource -> Doc Source # prettyPrec :: Int -> BindingSource -> Doc Source # prettyList :: [BindingSource] -> Doc Source #
EmbPrj BindingSource Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: BindingSource -> S Int32 Source # icod_ :: BindingSource -> S Int32 Source # value :: Int32 -> R BindingSource Source #
Generic BindingSource Source #
Instance details Defined in Agda.Syntax.Scope.Base Associated Types type Rep BindingSource :: Type -> Type Methods from :: BindingSource -> Rep BindingSource x to :: Rep BindingSource x -> BindingSource
Show BindingSource Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods showsPrec :: Int -> BindingSource -> ShowS show :: BindingSource -> String showList :: [BindingSource] -> ShowS
NFData BindingSource Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods rnf :: BindingSource -> ()
Eq BindingSource Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods (==) :: BindingSource -> BindingSource -> Bool (/=) :: BindingSource -> BindingSource -> Bool
type Rep BindingSource Source #
Instance details Defined in Agda.Syntax.Scope.Base type Rep BindingSource = D1 ('MetaData "BindingSource" "Agda.Syntax.Scope.Base" "Agda-2.6.3.20230930-inplace" 'False) ((C1 ('MetaCons "LambdaBound" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PatternBound" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "LetBound" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "WithBound" 'PrefixI 'False) (U1 :: Type -> Type)))

data LocalVar Source #

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. localBindingSource :: BindingSource 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

Instances details

Pretty LocalVar Source #	We show shadowed variables as prefixed by a ".", as not in scope.
Instance details Defined in Agda.Syntax.Scope.Base Methods pretty :: LocalVar -> Doc Source # prettyPrec :: Int -> LocalVar -> Doc Source # prettyList :: [LocalVar] -> Doc Source #
EmbPrj LocalVar Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: LocalVar -> S Int32 Source # icod_ :: LocalVar -> S Int32 Source # value :: Int32 -> R LocalVar Source #
Generic LocalVar Source #
Instance details Defined in Agda.Syntax.Scope.Base Associated Types type Rep LocalVar :: Type -> Type Methods from :: LocalVar -> Rep LocalVar x to :: Rep LocalVar x -> LocalVar
Show LocalVar Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods showsPrec :: Int -> LocalVar -> ShowS show :: LocalVar -> String showList :: [LocalVar] -> ShowS
NFData LocalVar Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods rnf :: LocalVar -> ()
Eq LocalVar Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods (==) :: LocalVar -> LocalVar -> Bool (/=) :: LocalVar -> LocalVar -> Bool
Ord LocalVar Source #
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
type Rep LocalVar Source #
Instance details Defined in Agda.Syntax.Scope.Base type Rep LocalVar = D1 ('MetaData "LocalVar" "Agda.Syntax.Scope.Base" "Agda-2.6.3.20230930-inplace" 'False) (C1 ('MetaCons "LocalVar" 'PrefixI 'True) (S1 ('MetaSel ('Just "localVar") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :: (S1 ('MetaSel ('Just "localBindingSource") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 BindingSource) :: S1 ('MetaSel ('Just "localShadowedBy") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [AbstractName]))))

shadowLocal :: List1 AbstractName -> LocalVar -> LocalVar Source #

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

patternToModuleBound :: LocalVar -> LocalVar Source #

Treat patternBound variable as a module parameter

notShadowedLocal :: LocalVar -> Maybe Name Source #

Project name of unshadowed local variable.

notShadowedLocals :: LocalVars -> AssocList Name Name Source #

Get all locals that are not shadowed by imports.

scopeCurrent :: Lens' ScopeInfo ModuleName Source #

Lenses for ScopeInfo components

scopeModules :: Lens' ScopeInfo (Map ModuleName Scope) Source #

scopeVarsToBind :: Lens' ScopeInfo LocalVars Source #

scopeLocals :: Lens' ScopeInfo LocalVars Source #

scopePrecedence :: Lens' ScopeInfo PrecedenceStack Source #

scopeInverseName :: Lens' ScopeInfo NameMap Source #

scopeInverseModule :: Lens' ScopeInfo ModuleMap Source #

scopeInScope :: Lens' ScopeInfo InScopeSet Source #

scopeFixities :: Lens' ScopeInfo Fixities Source #

scopePolarities :: Lens' ScopeInfo Polarities Source #

scopeFixitiesAndPolarities :: Lens' ScopeInfo (Fixities, Polarities) Source #

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

Lens for scopeVarsToBind.

setVarsToBind :: LocalVars -> ScopeInfo -> ScopeInfo Source #

updateScopeLocals :: (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. nsInScope :: InScopeSet All abstract names targeted by a concrete name in scope. Computed by `recomputeInScopeSets`.

Instances

Instances details

Pretty NameSpace Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods pretty :: NameSpace -> Doc Source # prettyPrec :: Int -> NameSpace -> Doc Source # prettyList :: [NameSpace] -> Doc Source #
EmbPrj NameSpace Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: NameSpace -> S Int32 Source # icod_ :: NameSpace -> S Int32 Source # value :: Int32 -> R NameSpace Source #
Generic NameSpace Source #
Instance details Defined in Agda.Syntax.Scope.Base Associated Types type Rep NameSpace :: Type -> Type Methods from :: NameSpace -> Rep NameSpace x to :: Rep NameSpace x -> NameSpace
Show NameSpace Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods showsPrec :: Int -> NameSpace -> ShowS show :: NameSpace -> String showList :: [NameSpace] -> ShowS
NFData NameSpace Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods rnf :: NameSpace -> ()
Eq NameSpace Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods (==) :: NameSpace -> NameSpace -> Bool (/=) :: NameSpace -> NameSpace -> Bool
type Rep NameSpace Source #
Instance details Defined in Agda.Syntax.Scope.Base type Rep NameSpace = D1 ('MetaData "NameSpace" "Agda.Syntax.Scope.Base" "Agda-2.6.3.20230930-inplace" 'False) (C1 ('MetaCons "NameSpace" 'PrefixI 'True) (S1 ('MetaSel ('Just "nsNames") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NamesInScope) :: (S1 ('MetaSel ('Just "nsModules") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModulesInScope) :: S1 ('MetaSel ('Just "nsInScope") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 InScopeSet))))

type ThingsInScope a = Map Name (List1 a) Source #

type NamesInScope = ThingsInScope AbstractName Source #

type ModulesInScope = ThingsInScope AbstractModule Source #

type InScopeSet = Set QName 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 Ord a => InScope a where Source #

Type class for some dependent-types trickery.

Methods

inScopeTag :: InScopeTag a Source #

Instances

Instances details

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

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

data NameOrModule Source #

Non-dependent tag for name or module.

Constructors

NameNotModule
ModuleNotName

Instances

Instances details

EmbPrj NameOrModule Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: NameOrModule -> S Int32 Source # icod_ :: NameOrModule -> S Int32 Source # value :: Int32 -> R NameOrModule Source #
Bounded NameOrModule Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods minBound :: NameOrModule maxBound :: NameOrModule
Enum NameOrModule Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods succ :: NameOrModule -> NameOrModule pred :: NameOrModule -> NameOrModule toEnum :: Int -> NameOrModule fromEnum :: NameOrModule -> Int enumFrom :: NameOrModule -> [NameOrModule] enumFromThen :: NameOrModule -> NameOrModule -> [NameOrModule] enumFromTo :: NameOrModule -> NameOrModule -> [NameOrModule] enumFromThenTo :: NameOrModule -> NameOrModule -> NameOrModule -> [NameOrModule]
Generic NameOrModule Source #
Instance details Defined in Agda.Syntax.Scope.Base Associated Types type Rep NameOrModule :: Type -> Type Methods from :: NameOrModule -> Rep NameOrModule x to :: Rep NameOrModule x -> NameOrModule
Show NameOrModule Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods showsPrec :: Int -> NameOrModule -> ShowS show :: NameOrModule -> String showList :: [NameOrModule] -> ShowS
NFData NameOrModule Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods rnf :: NameOrModule -> ()
Eq NameOrModule Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods (==) :: NameOrModule -> NameOrModule -> Bool (/=) :: NameOrModule -> NameOrModule -> Bool
Ord NameOrModule Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods compare :: NameOrModule -> NameOrModule -> Ordering (<) :: NameOrModule -> NameOrModule -> Bool (<=) :: NameOrModule -> NameOrModule -> Bool (>) :: NameOrModule -> NameOrModule -> Bool (>=) :: NameOrModule -> NameOrModule -> Bool max :: NameOrModule -> NameOrModule -> NameOrModule min :: NameOrModule -> NameOrModule -> NameOrModule
type Rep NameOrModule Source #
Instance details Defined in Agda.Syntax.Scope.Base type Rep NameOrModule = D1 ('MetaData "NameOrModule" "Agda.Syntax.Scope.Base" "Agda-2.6.3.20230930-inplace" 'False) (C1 ('MetaCons "NameNotModule" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ModuleNotName" 'PrefixI 'False) (U1 :: Type -> Type))

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 (`Inductive` or don't know).
CoConName	Constructor name (definitely `CoInductive`).
FldName	Record field name.
PatternSynName	Name of a pattern synonym.
GeneralizeName	Name to be generalized
DisallowedGeneralizeName	Generalizable variable from a let open
MacroName	Name of a macro
QuotableName	A name that can only be quoted. Previous category `DefName`: (Refined in a flat manner as Enum and Bounded are not hereditary.)
DataName	Name of a `data`.
RecName	Name of a `record`.
FunName	Name of a defined function.
AxiomName	Name of a `postulate`.
PrimName	Name of a `primitive`.
OtherDefName	A `DefName`, but either other kind or don't know which kind. End `DefName`. Keep these together in sequence, for sake of `isDefName`!

Instances

Instances details

EmbPrj KindOfName Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: KindOfName -> S Int32 Source # icod_ :: KindOfName -> S Int32 Source # value :: Int32 -> R KindOfName Source #
Bounded KindOfName Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods minBound :: KindOfName maxBound :: KindOfName
Enum KindOfName Source #
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]
Generic KindOfName Source #
Instance details Defined in Agda.Syntax.Scope.Base Associated Types type Rep KindOfName :: Type -> Type Methods from :: KindOfName -> Rep KindOfName x to :: Rep KindOfName x -> KindOfName
Show KindOfName Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods showsPrec :: Int -> KindOfName -> ShowS show :: KindOfName -> String showList :: [KindOfName] -> ShowS
NFData KindOfName Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods rnf :: KindOfName -> ()
Eq KindOfName Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods (==) :: KindOfName -> KindOfName -> Bool (/=) :: KindOfName -> KindOfName -> Bool
Ord KindOfName Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods compare :: KindOfName -> KindOfName -> Ordering (<) :: KindOfName -> KindOfName -> Bool (<=) :: KindOfName -> KindOfName -> Bool (>) :: KindOfName -> KindOfName -> Bool (>=) :: KindOfName -> KindOfName -> Bool max :: KindOfName -> KindOfName -> KindOfName min :: KindOfName -> KindOfName -> KindOfName
type Rep KindOfName Source #
Instance details Defined in Agda.Syntax.Scope.Base type Rep KindOfName = D1 ('MetaData "KindOfName" "Agda.Syntax.Scope.Base" "Agda-2.6.3.20230930-inplace" 'False) (((C1 ('MetaCons "ConName" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "CoConName" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FldName" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "PatternSynName" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "GeneralizeName" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "DisallowedGeneralizeName" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "MacroName" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "QuotableName" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "DataName" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RecName" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "FunName" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "AxiomName" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "PrimName" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "OtherDefName" 'PrefixI 'False) (U1 :: Type -> Type)))))

isDefName :: KindOfName -> Bool Source #

isConName :: KindOfName -> Maybe Induction Source #

conKindOfName :: Induction -> KindOfName Source #

conKindOfName' :: Foldable t => t Induction -> KindOfName Source #

For ambiguous constructors, we might have both alternatives of Induction. In this case, we default to ConName.

approxConInduction :: Foldable t => t Induction -> Induction Source #

For ambiguous constructors, we might have both alternatives of Induction. In this case, we default to Inductive.

exactConInduction :: Foldable t => t Induction -> Maybe Induction Source #

exactConName :: Foldable t => t Induction -> Maybe KindOfName Source #

Only return [Co]ConName if no ambiguity.

data KindsOfNames Source #

A set of KindOfName, for the sake of elemKindsOfNames.

Constructors

AllKindsOfNames
SomeKindsOfNames (Set KindOfName)	Only these kinds.
ExceptKindsOfNames (Set KindOfName)	All but these Kinds.

elemKindsOfNames :: KindOfName -> KindsOfNames -> Bool Source #

allKindsOfNames :: KindsOfNames Source #

someKindsOfNames :: [KindOfName] -> KindsOfNames Source #

exceptKindsOfNames :: [KindOfName] -> KindsOfNames Source #

data WithKind a Source #

Decorate something with KindOfName

Constructors

WithKind
Fields theKind :: KindOfName kindedThing :: a

Instances

Instances details

DeclaredNames KName Source #
Instance details Defined in Agda.Syntax.Abstract.Views Methods declaredNames :: Collection KName m => KName -> m Source #
Foldable WithKind Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods fold :: Monoid m => WithKind m -> m foldMap :: Monoid m => (a -> m) -> WithKind a -> m foldMap' :: Monoid m => (a -> m) -> WithKind a -> m foldr :: (a -> b -> b) -> b -> WithKind a -> b foldr' :: (a -> b -> b) -> b -> WithKind a -> b foldl :: (b -> a -> b) -> b -> WithKind a -> b foldl' :: (b -> a -> b) -> b -> WithKind a -> b foldr1 :: (a -> a -> a) -> WithKind a -> a foldl1 :: (a -> a -> a) -> WithKind a -> a toList :: WithKind a -> [a] null :: WithKind a -> Bool length :: WithKind a -> Int elem :: Eq a => a -> WithKind a -> Bool maximum :: Ord a => WithKind a -> a minimum :: Ord a => WithKind a -> a sum :: Num a => WithKind a -> a product :: Num a => WithKind a -> a
Traversable WithKind Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods traverse :: Applicative f => (a -> f b) -> WithKind a -> f (WithKind b) sequenceA :: Applicative f => WithKind (f a) -> f (WithKind a) mapM :: Monad m => (a -> m b) -> WithKind a -> m (WithKind b) sequence :: Monad m => WithKind (m a) -> m (WithKind a)
Functor WithKind Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods fmap :: (a -> b) -> WithKind a -> WithKind b (<$) :: a -> WithKind b -> WithKind a #
Show a => Show (WithKind a) Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods showsPrec :: Int -> WithKind a -> ShowS show :: WithKind a -> String showList :: [WithKind a] -> ShowS
Eq a => Eq (WithKind a) Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods (==) :: WithKind a -> WithKind a -> Bool (/=) :: WithKind a -> WithKind a -> Bool
Ord a => Ord (WithKind a) Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods compare :: WithKind a -> WithKind a -> Ordering (<) :: WithKind a -> WithKind a -> Bool (<=) :: WithKind a -> WithKind a -> Bool (>) :: WithKind a -> WithKind a -> Bool (>=) :: WithKind a -> WithKind a -> Bool max :: WithKind a -> WithKind a -> WithKind a min :: WithKind a -> WithKind a -> WithKind a

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

Instances details

EmbPrj WhyInScope Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: WhyInScope -> S Int32 Source # icod_ :: WhyInScope -> S Int32 Source # value :: Int32 -> R WhyInScope Source #
Generic WhyInScope Source #
Instance details Defined in Agda.Syntax.Scope.Base Associated Types type Rep WhyInScope :: Type -> Type Methods from :: WhyInScope -> Rep WhyInScope x to :: Rep WhyInScope x -> WhyInScope
Show WhyInScope Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods showsPrec :: Int -> WhyInScope -> ShowS show :: WhyInScope -> String showList :: [WhyInScope] -> ShowS
NFData WhyInScope Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods rnf :: WhyInScope -> ()
type Rep WhyInScope Source #
Instance details Defined in Agda.Syntax.Scope.Base type Rep WhyInScope = D1 ('MetaData "WhyInScope" "Agda.Syntax.Scope.Base" "Agda-2.6.3.20230930-inplace" 'False) (C1 ('MetaCons "Defined" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Opened" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 WhyInScope)) :+: C1 ('MetaCons "Applied" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 WhyInScope))))

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. anameMetadata :: NameMetadata Additional information needed during scope checking. Currently used for generalized data/record params.

Instances

Instances details

NameToExpr AbstractName Source #	Turn an `AbstractName` into an expression.
Instance details Defined in Agda.Syntax.Abstract Methods nameToExpr :: AbstractName -> Expr Source #
LensFixity AbstractName Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods lensFixity :: Lens' AbstractName Fixity Source #
Pretty AbstractName Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods pretty :: AbstractName -> Doc Source # prettyPrec :: Int -> AbstractName -> Doc Source # prettyList :: [AbstractName] -> Doc Source #
HasRange AbstractName Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods getRange :: AbstractName -> Range Source #
SetRange AbstractName Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods setRange :: Range -> AbstractName -> AbstractName Source #
InScope AbstractName Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods inScopeTag :: InScopeTag AbstractName Source #
SetBindingSite AbstractName Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods setBindingSite :: Range -> AbstractName -> AbstractName Source #
ToConcrete AbstractName Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs AbstractName Source # Methods toConcrete :: AbstractName -> AbsToCon (ConOfAbs AbstractName) Source # bindToConcrete :: AbstractName -> (ConOfAbs AbstractName -> AbsToCon b) -> AbsToCon b Source #
PrettyTCM AbstractName Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => AbstractName -> m Doc Source #
EmbPrj AbstractName Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: AbstractName -> S Int32 Source # icod_ :: AbstractName -> S Int32 Source # value :: Int32 -> R AbstractName Source #
Generic AbstractName Source #
Instance details Defined in Agda.Syntax.Scope.Base Associated Types type Rep AbstractName :: Type -> Type Methods from :: AbstractName -> Rep AbstractName x to :: Rep AbstractName x -> AbstractName
Show AbstractName Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods showsPrec :: Int -> AbstractName -> ShowS show :: AbstractName -> String showList :: [AbstractName] -> ShowS
NFData AbstractName Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods rnf :: AbstractName -> ()
Eq AbstractName Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods (==) :: AbstractName -> AbstractName -> Bool (/=) :: AbstractName -> AbstractName -> Bool
Ord AbstractName Source #
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
type ConOfAbs AbstractName Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs AbstractName = QName
type Rep AbstractName Source #
Instance details Defined in Agda.Syntax.Scope.Base type Rep AbstractName = D1 ('MetaData "AbstractName" "Agda.Syntax.Scope.Base" "Agda-2.6.3.20230930-inplace" 'False) (C1 ('MetaCons "AbsName" 'PrefixI 'True) ((S1 ('MetaSel ('Just "anameName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :: S1 ('MetaSel ('Just "anameKind") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KindOfName)) :: (S1 ('MetaSel ('Just "anameLineage") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 WhyInScope) :*: S1 ('MetaSel ('Just "anameMetadata") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NameMetadata))))

data NameMetadata Source #

Constructors

NoMetadata
GeneralizedVarsMetadata (Map QName Name)

Instances

Instances details

EmbPrj NameMetadata Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: NameMetadata -> S Int32 Source # icod_ :: NameMetadata -> S Int32 Source # value :: Int32 -> R NameMetadata Source #
Generic NameMetadata Source #
Instance details Defined in Agda.Syntax.Scope.Base Associated Types type Rep NameMetadata :: Type -> Type Methods from :: NameMetadata -> Rep NameMetadata x to :: Rep NameMetadata x -> NameMetadata
Show NameMetadata Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods showsPrec :: Int -> NameMetadata -> ShowS show :: NameMetadata -> String showList :: [NameMetadata] -> ShowS
NFData NameMetadata Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods rnf :: NameMetadata -> ()
type Rep NameMetadata Source #
Instance details Defined in Agda.Syntax.Scope.Base type Rep NameMetadata = D1 ('MetaData "NameMetadata" "Agda.Syntax.Scope.Base" "Agda-2.6.3.20230930-inplace" 'False) (C1 ('MetaCons "NoMetadata" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "GeneralizedVarsMetadata" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map QName Name))))

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

Instances details

Pretty AbstractModule Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods pretty :: AbstractModule -> Doc Source # prettyPrec :: Int -> AbstractModule -> Doc Source # prettyList :: [AbstractModule] -> Doc Source #
InScope AbstractModule Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods inScopeTag :: InScopeTag AbstractModule Source #
SetBindingSite AbstractModule Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods setBindingSite :: Range -> AbstractModule -> AbstractModule Source #
EmbPrj AbstractModule Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: AbstractModule -> S Int32 Source # icod_ :: AbstractModule -> S Int32 Source # value :: Int32 -> R AbstractModule Source #
Generic AbstractModule Source #
Instance details Defined in Agda.Syntax.Scope.Base Associated Types type Rep AbstractModule :: Type -> Type Methods from :: AbstractModule -> Rep AbstractModule x to :: Rep AbstractModule x -> AbstractModule
Show AbstractModule Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods showsPrec :: Int -> AbstractModule -> ShowS show :: AbstractModule -> String showList :: [AbstractModule] -> ShowS
NFData AbstractModule Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods rnf :: AbstractModule -> ()
Eq AbstractModule Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods (==) :: AbstractModule -> AbstractModule -> Bool (/=) :: AbstractModule -> AbstractModule -> Bool
Ord AbstractModule Source #
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
type Rep AbstractModule Source #
Instance details Defined in Agda.Syntax.Scope.Base type Rep AbstractModule = D1 ('MetaData "AbstractModule" "Agda.Syntax.Scope.Base" "Agda-2.6.3.20230930-inplace" 'False) (C1 ('MetaCons "AbsModule" 'PrefixI 'True) (S1 ('MetaSel ('Just "amodName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName) :*: S1 ('MetaSel ('Just "amodLineage") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 WhyInScope)))

lensAnameName :: Lens' AbstractName QName Source #

Van Laarhoven lens on anameName.

lensAmodName :: Lens' AbstractModule ModuleName Source #

Van Laarhoven lens on amodName.

data ResolvedName Source #

Constructors

VarName	Local variable bound by λ, Π, module telescope, pattern, `let`.
Fields resolvedVar :: Name resolvedBindingSource :: BindingSource What kind of binder?
DefinedName	Function, data/record type, postulate.
Fields Access AbstractName Suffix `anameKind` can be `DefName`, `MacroName`, `QuotableName`.
FieldName	Record field name. Needs to be distinguished to parse copatterns.
Fields (List1 AbstractName) `(FldName ==) . anameKind` for all names.
ConstructorName	Data or record constructor name.
Fields (Set Induction) (List1 AbstractName) `isJust . isConName . anameKind` for all names.
PatternSynResName	Name of pattern synonym.
Fields (List1 AbstractName) `(PatternSynName ==) . anameKind` for all names.
UnknownName	Unbound name.

Instances

Instances details

NameToExpr ResolvedName Source #	Turn a `ResolvedName` into an expression. Assumes name is not `UnknownName`.
Instance details Defined in Agda.Syntax.Abstract Methods nameToExpr :: ResolvedName -> Expr Source #
Pretty ResolvedName Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods pretty :: ResolvedName -> Doc Source # prettyPrec :: Int -> ResolvedName -> Doc Source # prettyList :: [ResolvedName] -> Doc Source #
ToConcrete ResolvedName Source #	Assumes name is not `UnknownName`.
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs ResolvedName Source # Methods toConcrete :: ResolvedName -> AbsToCon (ConOfAbs ResolvedName) Source # bindToConcrete :: ResolvedName -> (ConOfAbs ResolvedName -> AbsToCon b) -> AbsToCon b Source #
Generic ResolvedName Source #
Instance details Defined in Agda.Syntax.Scope.Base Associated Types type Rep ResolvedName :: Type -> Type Methods from :: ResolvedName -> Rep ResolvedName x to :: Rep ResolvedName x -> ResolvedName
Show ResolvedName Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods showsPrec :: Int -> ResolvedName -> ShowS show :: ResolvedName -> String showList :: [ResolvedName] -> ShowS
NFData ResolvedName Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods rnf :: ResolvedName -> ()
Eq ResolvedName Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods (==) :: ResolvedName -> ResolvedName -> Bool (/=) :: ResolvedName -> ResolvedName -> Bool
type ConOfAbs ResolvedName Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs ResolvedName = QName
type Rep ResolvedName Source #
Instance details Defined in Agda.Syntax.Scope.Base type Rep ResolvedName = D1 ('MetaData "ResolvedName" "Agda.Syntax.Scope.Base" "Agda-2.6.3.20230930-inplace" 'False) ((C1 ('MetaCons "VarName" 'PrefixI 'True) (S1 ('MetaSel ('Just "resolvedVar") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :: S1 ('MetaSel ('Just "resolvedBindingSource") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 BindingSource)) :+: (C1 ('MetaCons "DefinedName" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Access) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AbstractName) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Suffix))) :+: C1 ('MetaCons "FieldName" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 AbstractName))))) :+: (C1 ('MetaCons "ConstructorName" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set Induction)) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 AbstractName))) :+: (C1 ('MetaCons "PatternSynResName" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 AbstractName))) :+: C1 ('MetaCons "UnknownName" 'PrefixI 'False) (U1 :: Type -> Type))))

data AmbiguousNameReason Source #

Why is a resolved name ambiguous? What did it resolve to?

Invariant (statically enforced): At least two resolvents in total.

Constructors

AmbiguousLocalVar LocalVar (List1 AbstractName)	The name resolves both to a local variable and some declared names.
AmbiguousDeclName (List2 AbstractName)	The name resolves to at least 2 declared names.

Instances

Instances details

Generic AmbiguousNameReason Source #
Instance details Defined in Agda.Syntax.Scope.Base Associated Types type Rep AmbiguousNameReason :: Type -> Type Methods from :: AmbiguousNameReason -> Rep AmbiguousNameReason x to :: Rep AmbiguousNameReason x -> AmbiguousNameReason
Show AmbiguousNameReason Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods showsPrec :: Int -> AmbiguousNameReason -> ShowS show :: AmbiguousNameReason -> String showList :: [AmbiguousNameReason] -> ShowS
NFData AmbiguousNameReason Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods rnf :: AmbiguousNameReason -> ()
type Rep AmbiguousNameReason Source #
Instance details Defined in Agda.Syntax.Scope.Base type Rep AmbiguousNameReason = D1 ('MetaData "AmbiguousNameReason" "Agda.Syntax.Scope.Base" "Agda-2.6.3.20230930-inplace" 'False) (C1 ('MetaCons "AmbiguousLocalVar" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LocalVar) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 AbstractName))) :+: C1 ('MetaCons "AmbiguousDeclName" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List2 AbstractName))))

ambiguousNamesInReason :: AmbiguousNameReason -> List2 QName Source #

The flat list of ambiguous names in AmbiguousNameReason.

data WhyInScopeData Source #

Constructors

WhyInScopeData
Fields QName The name `x` this explanation is about. FilePath The directory in which the current module resides. (Maybe LocalVar) The local variable that `x` could denote, if any. [AbstractName] The defined names that `x` could denote. [AbstractModule] The modules that `x` could denote.

whyInScopeDataFromAmbiguousNameReason :: QName -> AmbiguousNameReason -> WhyInScopeData Source #

Operations on name and module maps.

mergeNames :: Eq a => ThingsInScope a -> ThingsInScope a -> ThingsInScope a Source #

mergeNamesMany :: Eq a => [ThingsInScope a] -> ThingsInScope a Source #

Operations on name spaces

emptyNameSpace :: NameSpace Source #

The empty name space.

mapNameSpace :: (NamesInScope -> NamesInScope) -> (ModulesInScope -> ModulesInScope) -> (InScopeSet -> InScopeSet) -> NameSpace -> NameSpace Source #

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

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

Zip together two name spaces.

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

Map functions over the names and modules in a scope.

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

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

mapScopeNS :: NameSpaceId -> (NamesInScope -> NamesInScope) -> (ModulesInScope -> ModulesInScope) -> (InScopeSet -> InScopeSet) -> Scope -> Scope Source #

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

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 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) -> (NameSpaceId -> InScopeSet -> InScopeSet -> InScopeSet) -> 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) -> (InScopeSet -> InScopeSet -> InScopeSet) -> Scope -> Scope -> Scope Source #

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

recomputeInScopeSets :: Scope -> Scope Source #

Recompute the inScope sets of a scope.

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 #

findNameInScope :: InScope a => Name -> Scope -> [(a, Access)] Source #

Look up a single name in the current scope.

This is equivalent to Map.lookup n . allNamesInScope', but more efficient when only a single name needs to be looked up.

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 #

Update a particular name space.

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

Modify a particular name space.

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

Add a name to a scope.

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

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

Add a module to a scope.

data UsingOrHiding Source #

When we get here we cannot have both using and hiding.

Constructors

UsingOnly [ImportedName]
HidingOnly [ImportedName]

usingOrHiding :: ImportDirective -> UsingOrHiding Source #

applyImportDirective :: ImportDirective -> Scope -> Scope Source #

Apply an ImportDirective to a scope:

rename keys (C.Name) according to renaming;
for untouched keys, either of

a) remove keys according to hiding, or b) filter keys according to using.

Both steps could be done in one pass, by first preparing key-filtering functions C.Name -> Maybe C.Name for defined names and module names. However, the penalty of doing it in two passes should not be too high. (Doubling the run time.)

applyImportDirective_ Source #

Arguments

:: ImportDirective
-> Scope
-> (Scope, (Set Name, Set Name))	Merged scope, clashing names, clashing module names.

Version of applyImportDirective that also returns sets of name and module name clashes introduced by renaming to identifiers that are already imported by using or lack of hiding.

renameCanonicalNames :: Map QName QName -> Map ModuleName ModuleName -> Scope -> Scope Source #

Rename the abstract names in a scope.

restrictPrivate :: Scope -> Scope Source #

Remove private name space of a scope.

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

restrictLocalPrivate :: ModuleName -> Scope -> Scope Source #

Remove private things from the given module from a scope.

withoutPrivates :: ScopeInfo -> ScopeInfo Source #

Filter privates out of a ScopeInfo

disallowGeneralizedVars :: Scope -> Scope Source #

Disallow using generalized variables from the 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

publicNames :: ScopeInfo -> Set AbstractName Source #

everythingInScope :: ScopeInfo -> NameSpace Source #

everythingInScopeQualified :: ScopeInfo -> NameSpace Source #

concreteNamesInScope :: ScopeInfo -> Set QName Source #

Get all concrete names in scope. Includes bound variables.

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

data AllowAmbiguousNames Source #

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

Instances details

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

isNameInScope :: QName -> ScopeInfo -> Bool Source #

isNameInScopeUnqualified :: QName -> ScopeInfo -> Bool Source #

inverseScopeLookupName :: QName -> ScopeInfo -> [QName] Source #

Find the concrete names that map (uniquely) to a given abstract qualified name. Sort by number of modules in the qualified name, unqualified names first.

inverseScopeLookupName' :: AllowAmbiguousNames -> QName -> ScopeInfo -> [QName] Source #

inverseScopeLookupName'' :: AllowAmbiguousNames -> QName -> ScopeInfo -> Maybe NameMapEntry Source #

A version of inverseScopeLookupName that also delivers the KindOfName. Used in highlighting.

inverseScopeLookupModule :: ModuleName -> ScopeInfo -> [QName] Source #

Find the concrete names that map (uniquely) to a given abstract module name. Sort by length, shortest first.

inverseScopeLookupModule' :: AllowAmbiguousNames -> ModuleName -> ScopeInfo -> [QName] Source #

recomputeInverseScopeMaps :: ScopeInfo -> ScopeInfo Source #

Update binding site

class SetBindingSite a where Source #

Set the nameBindingSite in an abstract name.

Minimal complete definition

Nothing

Methods

setBindingSite :: Range -> a -> a Source #

default setBindingSite :: (SetBindingSite b, Functor t, t b ~ a) => Range -> a -> a Source #

Instances

Instances details

SetBindingSite ModuleName Source #	Sets the binding site of all names in the path.
Instance details Defined in Agda.Syntax.Scope.Base Methods setBindingSite :: Range -> ModuleName -> ModuleName Source #
SetBindingSite Name Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods setBindingSite :: Range -> Name -> Name Source #
SetBindingSite QName Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods setBindingSite :: Range -> QName -> QName Source #
SetBindingSite AbstractModule Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods setBindingSite :: Range -> AbstractModule -> AbstractModule Source #
SetBindingSite AbstractName Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods setBindingSite :: Range -> AbstractName -> AbstractName Source #
SetBindingSite a => SetBindingSite (List1 a) Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods setBindingSite :: Range -> List1 a -> List1 a Source #
SetBindingSite a => SetBindingSite [a] Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods setBindingSite :: Range -> [a] -> [a] Source #

(Debug) printing

prettyNameSpace :: NameSpace -> [Doc] Source #

blockOfLines :: Doc -> [Doc] -> [Doc] Source #

Add first string only if list is non-empty.

Boring instances

Orphan instances

Pretty Suffix Source #
Instance details Methods pretty :: Suffix -> Doc Source # prettyPrec :: Int -> Suffix -> Doc Source # prettyList :: [Suffix] -> Doc Source #