Safe Haskell | None |
---|---|
Language | Haskell2010 |
Agda.Syntax.Scope.Base
Description
This module defines the notion of a scope and operations on scopes.
Synopsis
- data Scope = Scope {}
- data DataOrRecordModule
- data NameSpaceId
- 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 {}
- data NameMapEntry = NameMapEntry {}
- type NameMap = Map QName NameMapEntry
- type ModuleMap = Map ModuleName [QName]
- type LocalVars = AssocList Name LocalVar
- data BindingSource
- data LocalVar = LocalVar {}
- shadowLocal :: [AbstractName] -> LocalVar -> LocalVar
- patternToModuleBound :: LocalVar -> LocalVar
- notShadowedLocal :: LocalVar -> Maybe Name
- notShadowedLocals :: LocalVars -> AssocList Name Name
- scopeCurrent :: Lens' ModuleName ScopeInfo
- scopeModules :: Lens' (Map ModuleName Scope) ScopeInfo
- scopeVarsToBind :: Lens' LocalVars ScopeInfo
- scopeLocals :: Lens' LocalVars ScopeInfo
- scopePrecedence :: Lens' PrecedenceStack ScopeInfo
- scopeInverseName :: Lens' NameMap ScopeInfo
- scopeInverseModule :: Lens' ModuleMap ScopeInfo
- scopeInScope :: Lens' InScopeSet ScopeInfo
- scopeFixities :: Lens' Fixities ScopeInfo
- scopePolarities :: Lens' Polarities ScopeInfo
- scopeFixitiesAndPolarities :: Lens' (Fixities, Polarities) ScopeInfo
- updateVarsToBind :: (LocalVars -> LocalVars) -> ScopeInfo -> ScopeInfo
- setVarsToBind :: LocalVars -> ScopeInfo -> ScopeInfo
- updateScopeLocals :: (LocalVars -> LocalVars) -> ScopeInfo -> ScopeInfo
- setScopeLocals :: LocalVars -> ScopeInfo -> ScopeInfo
- data NameSpace = NameSpace {}
- type ThingsInScope a = Map Name [a]
- type NamesInScope = ThingsInScope AbstractName
- type ModulesInScope = ThingsInScope AbstractModule
- type InScopeSet = Set QName
- data InScopeTag a where
- class Ord a => InScope a where
- inScopeTag :: InScopeTag a
- inNameSpace :: forall a. InScope a => NameSpace -> ThingsInScope a
- data NameOrModule
- data KindOfName
- 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
- data AbstractName = AbsName {}
- data NameMetadata
- = NoMetadata
- | GeneralizedVarsMetadata (Map QName Name)
- data AbstractModule = AbsModule {}
- lensAnameName :: Lens' QName AbstractName
- lensAmodName :: Lens' ModuleName AbstractModule
- data ResolvedName
- 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)
- 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
- 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
- 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
- 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
A scope is a named collection of names partitioned into public and private names.
Constructors
Scope | |
Fields
|
Instances
Eq Scope Source # | |
Data Scope Source # | |
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 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 :: forall r r'. (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 Source # | |
Generic Scope Source # | |
NFData Scope Source # | |
Defined in Agda.Syntax.Scope.Base | |
Null Scope Source # | |
Pretty Scope Source # | |
EmbPrj Scope Source # | |
InstantiateFull Scope Source # | |
Defined in Agda.TypeChecking.Reduce | |
type Rep Scope Source # | |
Defined in Agda.Syntax.Scope.Base type Rep Scope = D1 ('MetaData "Scope" "Agda.Syntax.Scope.Base" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" '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
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
Bounded NameSpaceId Source # | |
Defined in Agda.Syntax.Scope.Base | |
Enum NameSpaceId Source # | |
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 Source # | |
Defined in Agda.Syntax.Scope.Base | |
Data NameSpaceId Source # | |
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 :: forall r r'. (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 Source # | |
Defined in Agda.Syntax.Scope.Base Methods showsPrec :: Int -> NameSpaceId -> ShowS show :: NameSpaceId -> String showList :: [NameSpaceId] -> ShowS | |
Generic NameSpaceId Source # | |
Defined in Agda.Syntax.Scope.Base Associated Types type Rep NameSpaceId :: Type -> Type | |
NFData NameSpaceId Source # | |
Defined in Agda.Syntax.Scope.Base Methods rnf :: NameSpaceId -> () | |
Pretty NameSpaceId Source # | |
Defined in Agda.Syntax.Scope.Base Methods pretty :: NameSpaceId -> Doc Source # prettyPrec :: Int -> NameSpaceId -> Doc Source # prettyList :: [NameSpaceId] -> Doc Source # | |
EmbPrj NameSpaceId Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: NameSpaceId -> S Int32 Source # icod_ :: NameSpaceId -> S Int32 Source # value :: Int32 -> R NameSpaceId Source # | |
type Rep NameSpaceId Source # | |
Defined in Agda.Syntax.Scope.Base type Rep NameSpaceId = D1 ('MetaData "NameSpaceId" "Agda.Syntax.Scope.Base" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" '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 #
updateScopeNameSpaces :: (ScopeNameSpaces -> ScopeNameSpaces) -> Scope -> Scope Source #
A lens for scopeNameSpaces
updateScopeNameSpacesM :: Functor m => (ScopeNameSpaces -> m ScopeNameSpaces) -> Scope -> m Scope Source #
`Monadic'
lens (Functor sufficient).
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
|
Instances
Eq ScopeInfo Source # | |
Data ScopeInfo Source # | |
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 :: forall r r'. (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 Source # | |
Generic ScopeInfo Source # | |
NFData ScopeInfo Source # | |
Defined in Agda.Syntax.Scope.Base | |
Null ScopeInfo Source # | |
Pretty ScopeInfo Source # | |
KillRange ScopeInfo Source # | |
Defined in Agda.Syntax.Scope.Base Methods | |
EmbPrj ScopeInfo Source # | |
type Rep ScopeInfo Source # | |
Defined in Agda.Syntax.Scope.Base type Rep ScopeInfo = D1 ('MetaData "ScopeInfo" "Agda.Syntax.Scope.Base" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" '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
|
Instances
Data NameMapEntry Source # | |
Defined in Agda.Syntax.Scope.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> NameMapEntry -> c NameMapEntry gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c NameMapEntry toConstr :: NameMapEntry -> Constr dataTypeOf :: NameMapEntry -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c NameMapEntry) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c NameMapEntry) gmapT :: (forall b. Data b => b -> b) -> NameMapEntry -> NameMapEntry gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> NameMapEntry -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> NameMapEntry -> r gmapQ :: (forall d. Data d => d -> u) -> NameMapEntry -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> NameMapEntry -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> NameMapEntry -> m NameMapEntry gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> NameMapEntry -> m NameMapEntry gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> NameMapEntry -> m NameMapEntry | |
Show NameMapEntry Source # | |
Defined in Agda.Syntax.Scope.Base Methods showsPrec :: Int -> NameMapEntry -> ShowS show :: NameMapEntry -> String showList :: [NameMapEntry] -> ShowS | |
Generic NameMapEntry Source # | |
Defined in Agda.Syntax.Scope.Base Associated Types type Rep NameMapEntry :: Type -> Type | |
Semigroup NameMapEntry Source # | Invariant: the |
Defined in Agda.Syntax.Scope.Base Methods (<>) :: NameMapEntry -> NameMapEntry -> NameMapEntry # sconcat :: NonEmpty NameMapEntry -> NameMapEntry stimes :: Integral b => b -> NameMapEntry -> NameMapEntry | |
NFData NameMapEntry Source # | |
Defined in Agda.Syntax.Scope.Base Methods rnf :: NameMapEntry -> () | |
type Rep NameMapEntry Source # | |
Defined in Agda.Syntax.Scope.Base type Rep NameMapEntry = D1 ('MetaData "NameMapEntry" "Agda.Syntax.Scope.Base" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" '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 #
data BindingSource Source #
For each bound variable, we want to know whether it was bound by a
λ, Π, module telescope, pattern, or let
.
Constructors
LambdaBound |
|
PatternBound | f ... = |
LetBound | let ... in |
WithBound | | ... in q |
Instances
Eq BindingSource Source # | |
Defined in Agda.Syntax.Scope.Base | |
Data BindingSource Source # | |
Defined in Agda.Syntax.Scope.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> BindingSource -> c BindingSource gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c BindingSource toConstr :: BindingSource -> Constr dataTypeOf :: BindingSource -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c BindingSource) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BindingSource) gmapT :: (forall b. Data b => b -> b) -> BindingSource -> BindingSource gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BindingSource -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BindingSource -> r gmapQ :: (forall d. Data d => d -> u) -> BindingSource -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> BindingSource -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> BindingSource -> m BindingSource gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BindingSource -> m BindingSource gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BindingSource -> m BindingSource | |
Show BindingSource Source # | |
Defined in Agda.Syntax.Scope.Base Methods showsPrec :: Int -> BindingSource -> ShowS show :: BindingSource -> String showList :: [BindingSource] -> ShowS | |
Generic BindingSource Source # | |
Defined in Agda.Syntax.Scope.Base Associated Types type Rep BindingSource :: Type -> Type | |
NFData BindingSource Source # | |
Defined in Agda.Syntax.Scope.Base Methods rnf :: BindingSource -> () | |
Pretty BindingSource Source # | |
Defined in Agda.Syntax.Scope.Base Methods pretty :: BindingSource -> Doc Source # prettyPrec :: Int -> BindingSource -> Doc Source # prettyList :: [BindingSource] -> Doc Source # | |
EmbPrj BindingSource Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: BindingSource -> S Int32 Source # icod_ :: BindingSource -> S Int32 Source # value :: Int32 -> R BindingSource Source # | |
type Rep BindingSource Source # | |
Defined in Agda.Syntax.Scope.Base type Rep BindingSource = D1 ('MetaData "BindingSource" "Agda.Syntax.Scope.Base" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" '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))) |
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
|
Instances
Eq LocalVar Source # | |
Data LocalVar Source # | |
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 :: forall r r'. (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 Source # | |
Defined in Agda.Syntax.Scope.Base | |
Show LocalVar Source # | |
Generic LocalVar Source # | |
NFData LocalVar Source # | |
Defined in Agda.Syntax.Scope.Base | |
Pretty LocalVar Source # | We show shadowed variables as prefixed by a ".", as not in scope. |
EmbPrj LocalVar Source # | |
type Rep LocalVar Source # | |
Defined in Agda.Syntax.Scope.Base type Rep LocalVar = D1 ('MetaData "LocalVar" "Agda.Syntax.Scope.Base" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" '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 :: [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' ModuleName ScopeInfo Source #
Lenses for ScopeInfo components
scopeModules :: Lens' (Map ModuleName Scope) ScopeInfo Source #
updateVarsToBind :: (LocalVars -> LocalVars) -> ScopeInfo -> ScopeInfo Source #
Lens for scopeVarsToBind
.
updateScopeLocals :: (LocalVars -> LocalVars) -> ScopeInfo -> ScopeInfo Source #
Lens for scopeLocals
.
Name spaces
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
|
Instances
Eq NameSpace Source # | |
Data NameSpace Source # | |
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 :: forall r r'. (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 Source # | |
Generic NameSpace Source # | |
NFData NameSpace Source # | |
Defined in Agda.Syntax.Scope.Base | |
Pretty NameSpace Source # | |
EmbPrj NameSpace Source # | |
type Rep NameSpace Source # | |
Defined in Agda.Syntax.Scope.Base type Rep NameSpace = D1 ('MetaData "NameSpace" "Agda.Syntax.Scope.Base" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" '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 [a] Source #
type NamesInScope = ThingsInScope AbstractName 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
InScope AbstractModule Source # | |
Defined in Agda.Syntax.Scope.Base Methods | |
InScope AbstractName Source # | |
Defined in Agda.Syntax.Scope.Base Methods |
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
Bounded NameOrModule Source # | |
Defined in Agda.Syntax.Scope.Base | |
Enum NameOrModule Source # | |
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] | |
Eq NameOrModule Source # | |
Defined in Agda.Syntax.Scope.Base | |
Data NameOrModule Source # | |
Defined in Agda.Syntax.Scope.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> NameOrModule -> c NameOrModule gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c NameOrModule toConstr :: NameOrModule -> Constr dataTypeOf :: NameOrModule -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c NameOrModule) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c NameOrModule) gmapT :: (forall b. Data b => b -> b) -> NameOrModule -> NameOrModule gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> NameOrModule -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> NameOrModule -> r gmapQ :: (forall d. Data d => d -> u) -> NameOrModule -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> NameOrModule -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> NameOrModule -> m NameOrModule gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> NameOrModule -> m NameOrModule gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> NameOrModule -> m NameOrModule | |
Ord NameOrModule Source # | |
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 | |
Show NameOrModule Source # | |
Defined in Agda.Syntax.Scope.Base Methods showsPrec :: Int -> NameOrModule -> ShowS show :: NameOrModule -> String showList :: [NameOrModule] -> ShowS | |
Generic NameOrModule Source # | |
Defined in Agda.Syntax.Scope.Base Associated Types type Rep NameOrModule :: Type -> Type | |
NFData NameOrModule Source # | |
Defined in Agda.Syntax.Scope.Base Methods rnf :: NameOrModule -> () | |
EmbPrj NameOrModule Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: NameOrModule -> S Int32 Source # icod_ :: NameOrModule -> S Int32 Source # value :: Int32 -> R NameOrModule Source # | |
type Rep NameOrModule Source # | |
Defined in Agda.Syntax.Scope.Base type Rep NameOrModule = D1 ('MetaData "NameOrModule" "Agda.Syntax.Scope.Base" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" '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 ( |
CoConName | Constructor name (definitely |
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 |
DataName | Name of a |
RecName | Name of a |
FunName | Name of a defined function. |
AxiomName | Name of a |
PrimName | Name of a |
OtherDefName | A |
Instances
Bounded KindOfName Source # | |
Defined in Agda.Syntax.Scope.Base | |
Enum KindOfName Source # | |
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 Source # | |
Defined in Agda.Syntax.Scope.Base | |
Data KindOfName Source # | |
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 :: forall r r'. (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 | |
Ord KindOfName Source # | |
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 | |
Show KindOfName Source # | |
Defined in Agda.Syntax.Scope.Base Methods showsPrec :: Int -> KindOfName -> ShowS show :: KindOfName -> String showList :: [KindOfName] -> ShowS | |
Generic KindOfName Source # | |
Defined in Agda.Syntax.Scope.Base Associated Types type Rep KindOfName :: Type -> Type | |
NFData KindOfName Source # | |
Defined in Agda.Syntax.Scope.Base Methods rnf :: KindOfName -> () | |
EmbPrj KindOfName Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: KindOfName -> S Int32 Source # icod_ :: KindOfName -> S Int32 Source # value :: Int32 -> R KindOfName Source # | |
type Rep KindOfName Source # | |
Defined in Agda.Syntax.Scope.Base type Rep KindOfName = D1 ('MetaData "KindOfName" "Agda.Syntax.Scope.Base" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" '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 #
approxConInduction :: Foldable t => t Induction -> Induction Source #
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 #
someKindsOfNames :: [KindOfName] -> KindsOfNames Source #
exceptKindsOfNames :: [KindOfName] -> KindsOfNames Source #
Decorate something with KindOfName
Constructors
WithKind | |
Fields
|
Instances
Functor WithKind Source # | |
Foldable WithKind Source # | |
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 elem :: Eq a => a -> WithKind a -> Bool maximum :: Ord a => WithKind a -> a minimum :: Ord a => WithKind a -> a | |
Traversable WithKind Source # | |
DeclaredNames KName Source # | |
Defined in Agda.Syntax.Abstract.Views Methods declaredNames :: Collection KName m => KName -> m Source # | |
Eq a => Eq (WithKind a) Source # | |
Data a => Data (WithKind a) Source # | |
Defined in Agda.Syntax.Scope.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> WithKind a -> c (WithKind a) gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (WithKind a) toConstr :: WithKind a -> Constr dataTypeOf :: WithKind a -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (WithKind a)) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (WithKind a)) gmapT :: (forall b. Data b => b -> b) -> WithKind a -> WithKind a gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> WithKind a -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> WithKind a -> r gmapQ :: (forall d. Data d => d -> u) -> WithKind a -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> WithKind a -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> WithKind a -> m (WithKind a) gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> WithKind a -> m (WithKind a) gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> WithKind a -> m (WithKind a) | |
Ord a => Ord (WithKind a) Source # | |
Show a => Show (WithKind a) Source # | |
data WhyInScope Source #
Where does a name come from?
This information is solely for reporting to the user,
see whyInScope
.
Constructors
Defined | Defined in this module. |
Opened QName WhyInScope | Imported from another module. |
Applied QName WhyInScope | Imported by a module application. |
Instances
Data WhyInScope Source # | |
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 :: forall r r'. (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 Source # | |
Defined in Agda.Syntax.Scope.Base Methods showsPrec :: Int -> WhyInScope -> ShowS show :: WhyInScope -> String showList :: [WhyInScope] -> ShowS | |
Generic WhyInScope Source # | |
Defined in Agda.Syntax.Scope.Base Associated Types type Rep WhyInScope :: Type -> Type | |
NFData WhyInScope Source # | |
Defined in Agda.Syntax.Scope.Base Methods rnf :: WhyInScope -> () | |
EmbPrj WhyInScope Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: WhyInScope -> S Int32 Source # icod_ :: WhyInScope -> S Int32 Source # value :: Int32 -> R WhyInScope Source # | |
type Rep WhyInScope Source # | |
Defined in Agda.Syntax.Scope.Base type Rep WhyInScope = D1 ('MetaData "WhyInScope" "Agda.Syntax.Scope.Base" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" '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
|
Instances
Eq AbstractName Source # | |
Defined in Agda.Syntax.Scope.Base | |
Data AbstractName Source # | |
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 :: forall r r'. (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 Source # | |
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 Source # | |
Defined in Agda.Syntax.Scope.Base Methods showsPrec :: Int -> AbstractName -> ShowS show :: AbstractName -> String showList :: [AbstractName] -> ShowS | |
Generic AbstractName Source # | |
Defined in Agda.Syntax.Scope.Base Associated Types type Rep AbstractName :: Type -> Type | |
NFData AbstractName Source # | |
Defined in Agda.Syntax.Scope.Base Methods rnf :: AbstractName -> () | |
Pretty AbstractName Source # | |
Defined in Agda.Syntax.Scope.Base Methods pretty :: AbstractName -> Doc Source # prettyPrec :: Int -> AbstractName -> Doc Source # prettyList :: [AbstractName] -> Doc Source # | |
SetRange AbstractName Source # | |
Defined in Agda.Syntax.Scope.Base Methods setRange :: Range -> AbstractName -> AbstractName Source # | |
HasRange AbstractName Source # | |
Defined in Agda.Syntax.Scope.Base Methods getRange :: AbstractName -> Range Source # | |
LensFixity AbstractName Source # | |
Defined in Agda.Syntax.Scope.Base Methods | |
SetBindingSite AbstractName Source # | |
Defined in Agda.Syntax.Scope.Base Methods setBindingSite :: Range -> AbstractName -> AbstractName Source # | |
InScope AbstractName Source # | |
Defined in Agda.Syntax.Scope.Base Methods | |
NameToExpr AbstractName Source # | Turn an |
Defined in Agda.Syntax.Abstract Methods nameToExpr :: AbstractName -> Expr Source # | |
EmbPrj AbstractName Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: AbstractName -> S Int32 Source # icod_ :: AbstractName -> S Int32 Source # value :: Int32 -> R AbstractName Source # | |
PrettyTCM AbstractName Source # | |
Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => AbstractName -> m Doc Source # | |
ToConcrete AbstractName Source # | |
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 # | |
type Rep AbstractName Source # | |
Defined in Agda.Syntax.Scope.Base type Rep AbstractName = D1 ('MetaData "AbstractName" "Agda.Syntax.Scope.Base" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" '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)))) | |
type ConOfAbs AbstractName Source # | |
Defined in Agda.Syntax.Translation.AbstractToConcrete |
data NameMetadata Source #
Constructors
NoMetadata | |
GeneralizedVarsMetadata (Map QName Name) |
Instances
Data NameMetadata Source # | |
Defined in Agda.Syntax.Scope.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> NameMetadata -> c NameMetadata gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c NameMetadata toConstr :: NameMetadata -> Constr dataTypeOf :: NameMetadata -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c NameMetadata) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c NameMetadata) gmapT :: (forall b. Data b => b -> b) -> NameMetadata -> NameMetadata gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> NameMetadata -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> NameMetadata -> r gmapQ :: (forall d. Data d => d -> u) -> NameMetadata -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> NameMetadata -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> NameMetadata -> m NameMetadata gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> NameMetadata -> m NameMetadata gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> NameMetadata -> m NameMetadata | |
Show NameMetadata Source # | |
Defined in Agda.Syntax.Scope.Base Methods showsPrec :: Int -> NameMetadata -> ShowS show :: NameMetadata -> String showList :: [NameMetadata] -> ShowS | |
Generic NameMetadata Source # | |
Defined in Agda.Syntax.Scope.Base Associated Types type Rep NameMetadata :: Type -> Type | |
NFData NameMetadata Source # | |
Defined in Agda.Syntax.Scope.Base Methods rnf :: NameMetadata -> () | |
EmbPrj NameMetadata Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: NameMetadata -> S Int32 Source # icod_ :: NameMetadata -> S Int32 Source # value :: Int32 -> R NameMetadata Source # | |
type Rep NameMetadata Source # | |
Defined in Agda.Syntax.Scope.Base type Rep NameMetadata = D1 ('MetaData "NameMetadata" "Agda.Syntax.Scope.Base" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" '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
|
Instances
Eq AbstractModule Source # | |
Defined in Agda.Syntax.Scope.Base Methods (==) :: AbstractModule -> AbstractModule -> Bool (/=) :: AbstractModule -> AbstractModule -> Bool | |
Data AbstractModule Source # | |
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 :: forall r r'. (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 Source # | |
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 Source # | |
Defined in Agda.Syntax.Scope.Base Methods showsPrec :: Int -> AbstractModule -> ShowS show :: AbstractModule -> String showList :: [AbstractModule] -> ShowS | |
Generic AbstractModule Source # | |
Defined in Agda.Syntax.Scope.Base Associated Types type Rep AbstractModule :: Type -> Type | |
NFData AbstractModule Source # | |
Defined in Agda.Syntax.Scope.Base Methods rnf :: AbstractModule -> () | |
Pretty AbstractModule Source # | |
Defined in Agda.Syntax.Scope.Base Methods pretty :: AbstractModule -> Doc Source # prettyPrec :: Int -> AbstractModule -> Doc Source # prettyList :: [AbstractModule] -> Doc Source # | |
SetBindingSite AbstractModule Source # | |
Defined in Agda.Syntax.Scope.Base Methods setBindingSite :: Range -> AbstractModule -> AbstractModule Source # | |
InScope AbstractModule Source # | |
Defined in Agda.Syntax.Scope.Base Methods | |
EmbPrj AbstractModule Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: AbstractModule -> S Int32 Source # icod_ :: AbstractModule -> S Int32 Source # value :: Int32 -> R AbstractModule Source # | |
type Rep AbstractModule Source # | |
Defined in Agda.Syntax.Scope.Base type Rep AbstractModule = D1 ('MetaData "AbstractModule" "Agda.Syntax.Scope.Base" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" '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' QName AbstractName Source #
Van Laarhoven lens on anameName
.
lensAmodName :: Lens' ModuleName AbstractModule Source #
Van Laarhoven lens on amodName
.
data ResolvedName Source #
Constructors
VarName | Local variable bound by λ, Π, module telescope, pattern, |
Fields
| |
DefinedName Access AbstractName Suffix | Function, data/record type, postulate. |
FieldName (List1 AbstractName) | Record field name. Needs to be distinguished to parse copatterns. |
ConstructorName (Set Induction) (List1 AbstractName) | Data or record constructor name. |
PatternSynResName (List1 AbstractName) | Name of pattern synonym. |
UnknownName | Unbound name. |
Instances
Eq ResolvedName Source # | |
Defined in Agda.Syntax.Scope.Base | |
Data ResolvedName Source # | |
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 :: forall r r'. (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 Source # | |
Defined in Agda.Syntax.Scope.Base Methods showsPrec :: Int -> ResolvedName -> ShowS show :: ResolvedName -> String showList :: [ResolvedName] -> ShowS | |
Generic ResolvedName Source # | |
Defined in Agda.Syntax.Scope.Base Associated Types type Rep ResolvedName :: Type -> Type | |
NFData ResolvedName Source # | |
Defined in Agda.Syntax.Scope.Base Methods rnf :: ResolvedName -> () | |
Pretty ResolvedName Source # | |
Defined in Agda.Syntax.Scope.Base Methods pretty :: ResolvedName -> Doc Source # prettyPrec :: Int -> ResolvedName -> Doc Source # prettyList :: [ResolvedName] -> Doc Source # | |
NameToExpr ResolvedName Source # | Turn a Assumes name is not |
Defined in Agda.Syntax.Abstract Methods nameToExpr :: ResolvedName -> Expr Source # | |
ToConcrete ResolvedName Source # | Assumes name is not |
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 # | |
type Rep ResolvedName Source # | |
Defined in Agda.Syntax.Scope.Base type Rep ResolvedName = D1 ('MetaData "ResolvedName" "Agda.Syntax.Scope.Base" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" '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)))) | |
type ConOfAbs ResolvedName Source # | |
Defined in Agda.Syntax.Translation.AbstractToConcrete |
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 #
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] |
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.
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 #
flattenScope :: [[Name]] -> ScopeInfo -> Map QName [AbstractName] Source #
Compute a flattened scope. Only include unqualified names or names qualified by modules in the first argument.
concreteNamesInScope :: ScopeInfo -> Set QName Source #
Get all concrete names in scope. Includes bound variables.
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
Eq AllowAmbiguousNames Source # | |
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 #
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
SetBindingSite ModuleName Source # | Sets the binding site of all names in the path. |
Defined in Agda.Syntax.Scope.Base Methods setBindingSite :: Range -> ModuleName -> ModuleName Source # | |
SetBindingSite QName Source # | |
Defined in Agda.Syntax.Scope.Base | |
SetBindingSite Name Source # | |
Defined in Agda.Syntax.Scope.Base | |
SetBindingSite AbstractModule Source # | |
Defined in Agda.Syntax.Scope.Base Methods setBindingSite :: Range -> AbstractModule -> AbstractModule Source # | |
SetBindingSite AbstractName Source # | |
Defined in Agda.Syntax.Scope.Base Methods setBindingSite :: Range -> AbstractName -> AbstractName Source # | |
SetBindingSite a => SetBindingSite [a] Source # | |
Defined in Agda.Syntax.Scope.Base Methods setBindingSite :: Range -> [a] -> [a] Source # |
(Debug) printing
prettyNameSpace :: NameSpace -> [Doc] Source #