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

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 :: [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 {
  - nsNames :: NamesInScope
  - nsModules :: ModulesInScope
  - nsInScope :: InScopeSet
  }
- type ThingsInScope a = Map Name [a]
- type NamesInScope = ThingsInScope AbstractName
- type ModulesInScope = ThingsInScope AbstractModule
- type InScopeSet = Set QName
- data InScopeTag a where
  - NameTag :: InScopeTag AbstractName
  - ModuleTag :: InScopeTag AbstractModule
- class 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' QName AbstractName
- lensAmodName :: Lens' ModuleName AbstractModule
- data ResolvedName
  - = VarName {
    - resolvedVar :: Name
    - resolvedBindingSource :: BindingSource
    }
  - | DefinedName Access AbstractName Suffix
  - | FieldName (List1 AbstractName)
  - | ConstructorName (Set Induction) (List1 AbstractName)
  - | PatternSynResName (List1 AbstractName)
  - | UnknownName
- 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
  - = 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
- flattenScope :: [[Name]] -> ScopeInfo -> Map QName [AbstractName]
- concreteNamesInScope :: ScopeInfo -> Set QName
- scopeLookup :: InScope a => QName -> ScopeInfo -> [a]
- scopeLookup' :: forall a. InScope a => QName -> ScopeInfo -> [(a, Access)]
- data AllowAmbiguousNames
  - = AmbiguousAnything
  - | AmbiguousConProjs
  - | AmbiguousNothing
- isNameInScope :: QName -> ScopeInfo -> Bool
- 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

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

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Scope -> c Scope Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Scope Source #

toConstr :: Scope -> Constr Source #

dataTypeOf :: Scope -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Scope) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Scope) Source #

gmapT :: (forall b. Data b => b -> b) -> Scope -> Scope Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Scope -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Scope -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Scope -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Scope -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Scope -> m Scope Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Scope -> m Scope Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Scope -> m Scope Source #

Generic Scope Source # |
Instance details Defined in Agda.Syntax.Scope.Base Associated Types type Rep Scope :: Type -> Type Source # Methods from :: Scope -> Rep Scope x Source # to :: Rep Scope x -> Scope Source #
Show Scope Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods showsPrec :: Int -> Scope -> ShowS Source # show :: Scope -> String Source # showList :: [Scope] -> ShowS Source #
NFData Scope Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods rnf :: Scope -> () Source #
Eq Scope Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods (==) :: Scope -> Scope -> Bool Source # (/=) :: Scope -> Scope -> Bool Source #
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.2.2-7KnEKyKhaJHFPwDzdI3vIK" '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 #
Data DataOrRecordModule Source # |

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DataOrRecordModule -> c DataOrRecordModule Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DataOrRecordModule Source #

toConstr :: DataOrRecordModule -> Constr Source #

dataTypeOf :: DataOrRecordModule -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DataOrRecordModule) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DataOrRecordModule) Source #

gmapT :: (forall b. Data b => b -> b) -> DataOrRecordModule -> DataOrRecordModule Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DataOrRecordModule -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DataOrRecordModule -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> DataOrRecordModule -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> DataOrRecordModule -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> DataOrRecordModule -> m DataOrRecordModule Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DataOrRecordModule -> m DataOrRecordModule Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DataOrRecordModule -> m DataOrRecordModule Source #

Bounded DataOrRecordModule Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods minBound :: DataOrRecordModule Source # maxBound :: DataOrRecordModule Source #
Enum DataOrRecordModule Source # |

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

succ :: DataOrRecordModule -> DataOrRecordModule Source #

pred :: DataOrRecordModule -> DataOrRecordModule Source #

toEnum :: Int -> DataOrRecordModule Source #

fromEnum :: DataOrRecordModule -> Int Source #

enumFrom :: DataOrRecordModule -> [DataOrRecordModule] Source #

enumFromThen :: DataOrRecordModule -> DataOrRecordModule -> [DataOrRecordModule] Source #

enumFromTo :: DataOrRecordModule -> DataOrRecordModule -> [DataOrRecordModule] Source #

enumFromThenTo :: DataOrRecordModule -> DataOrRecordModule -> DataOrRecordModule -> [DataOrRecordModule] Source #

Generic DataOrRecordModule Source # |
Instance details Defined in Agda.Syntax.Scope.Base Associated Types type Rep DataOrRecordModule :: Type -> Type Source # Methods from :: DataOrRecordModule -> Rep DataOrRecordModule x Source # to :: Rep DataOrRecordModule x -> DataOrRecordModule Source #
Show DataOrRecordModule Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods showsPrec :: Int -> DataOrRecordModule -> ShowS Source # show :: DataOrRecordModule -> String Source # showList :: [DataOrRecordModule] -> ShowS Source #
NFData DataOrRecordModule Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods rnf :: DataOrRecordModule -> () Source #
Eq DataOrRecordModule Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods (==) :: DataOrRecordModule -> DataOrRecordModule -> Bool Source # (/=) :: DataOrRecordModule -> DataOrRecordModule -> Bool Source #
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.2.2-7KnEKyKhaJHFPwDzdI3vIK" '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

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

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> NameSpaceId -> c NameSpaceId Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c NameSpaceId Source #

toConstr :: NameSpaceId -> Constr Source #

dataTypeOf :: NameSpaceId -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c NameSpaceId) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c NameSpaceId) Source #

gmapT :: (forall b. Data b => b -> b) -> NameSpaceId -> NameSpaceId Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> NameSpaceId -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> NameSpaceId -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> NameSpaceId -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> NameSpaceId -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> NameSpaceId -> m NameSpaceId Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> NameSpaceId -> m NameSpaceId Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> NameSpaceId -> m NameSpaceId Source #

Bounded NameSpaceId Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods minBound :: NameSpaceId Source # maxBound :: NameSpaceId Source #
Enum NameSpaceId Source # |

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

succ :: NameSpaceId -> NameSpaceId Source #

pred :: NameSpaceId -> NameSpaceId Source #

toEnum :: Int -> NameSpaceId Source #

fromEnum :: NameSpaceId -> Int Source #

enumFrom :: NameSpaceId -> [NameSpaceId] Source #

enumFromThen :: NameSpaceId -> NameSpaceId -> [NameSpaceId] Source #

enumFromTo :: NameSpaceId -> NameSpaceId -> [NameSpaceId] Source #

enumFromThenTo :: NameSpaceId -> NameSpaceId -> NameSpaceId -> [NameSpaceId] Source #

Generic NameSpaceId Source # |
Instance details Defined in Agda.Syntax.Scope.Base Associated Types type Rep NameSpaceId :: Type -> Type Source # Methods from :: NameSpaceId -> Rep NameSpaceId x Source # to :: Rep NameSpaceId x -> NameSpaceId Source #
Show NameSpaceId Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods showsPrec :: Int -> NameSpaceId -> ShowS Source # show :: NameSpaceId -> String Source # showList :: [NameSpaceId] -> ShowS Source #
NFData NameSpaceId Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods rnf :: NameSpaceId -> () Source #
Eq NameSpaceId Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods (==) :: NameSpaceId -> NameSpaceId -> Bool Source # (/=) :: NameSpaceId -> NameSpaceId -> Bool Source #
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.2.2-7KnEKyKhaJHFPwDzdI3vIK" '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

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

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ScopeInfo -> c ScopeInfo Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ScopeInfo Source #

toConstr :: ScopeInfo -> Constr Source #

dataTypeOf :: ScopeInfo -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ScopeInfo) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ScopeInfo) Source #

gmapT :: (forall b. Data b => b -> b) -> ScopeInfo -> ScopeInfo Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ScopeInfo -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ScopeInfo -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> ScopeInfo -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> ScopeInfo -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ScopeInfo -> m ScopeInfo Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ScopeInfo -> m ScopeInfo Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ScopeInfo -> m ScopeInfo Source #

Generic ScopeInfo Source # |
Instance details Defined in Agda.Syntax.Scope.Base Associated Types type Rep ScopeInfo :: Type -> Type Source # Methods from :: ScopeInfo -> Rep ScopeInfo x Source # to :: Rep ScopeInfo x -> ScopeInfo Source #
Show ScopeInfo Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods showsPrec :: Int -> ScopeInfo -> ShowS Source # show :: ScopeInfo -> String Source # showList :: [ScopeInfo] -> ShowS Source #
NFData ScopeInfo Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods rnf :: ScopeInfo -> () Source #
Eq ScopeInfo Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods (==) :: ScopeInfo -> ScopeInfo -> Bool Source # (/=) :: ScopeInfo -> ScopeInfo -> Bool Source #
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.2.2-7KnEKyKhaJHFPwDzdI3vIK" '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

Data NameMapEntry Source # |

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> NameMapEntry -> c NameMapEntry Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c NameMapEntry Source #

toConstr :: NameMapEntry -> Constr Source #

dataTypeOf :: NameMapEntry -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c NameMapEntry) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c NameMapEntry) Source #

gmapT :: (forall b. Data b => b -> b) -> NameMapEntry -> NameMapEntry Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> NameMapEntry -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> NameMapEntry -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> NameMapEntry -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> NameMapEntry -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> NameMapEntry -> m NameMapEntry Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> NameMapEntry -> m NameMapEntry Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> NameMapEntry -> m NameMapEntry Source #

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 Source # sconcat :: NonEmpty NameMapEntry -> NameMapEntry Source # stimes :: Integral b => b -> NameMapEntry -> NameMapEntry Source #
Generic NameMapEntry Source # |
Instance details Defined in Agda.Syntax.Scope.Base Associated Types type Rep NameMapEntry :: Type -> Type Source # Methods from :: NameMapEntry -> Rep NameMapEntry x Source # to :: Rep NameMapEntry x -> NameMapEntry Source #
Show NameMapEntry Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods showsPrec :: Int -> NameMapEntry -> ShowS Source # show :: NameMapEntry -> String Source # showList :: [NameMapEntry] -> ShowS Source #
NFData NameMapEntry Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods rnf :: NameMapEntry -> () Source #
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.2.2-7KnEKyKhaJHFPwDzdI3vIK" '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

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

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> BindingSource -> c BindingSource Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c BindingSource Source #

toConstr :: BindingSource -> Constr Source #

dataTypeOf :: BindingSource -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c BindingSource) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BindingSource) Source #

gmapT :: (forall b. Data b => b -> b) -> BindingSource -> BindingSource Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BindingSource -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BindingSource -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> BindingSource -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> BindingSource -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> BindingSource -> m BindingSource Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BindingSource -> m BindingSource Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BindingSource -> m BindingSource Source #

Generic BindingSource Source # |
Instance details Defined in Agda.Syntax.Scope.Base Associated Types type Rep BindingSource :: Type -> Type Source # Methods from :: BindingSource -> Rep BindingSource x Source # to :: Rep BindingSource x -> BindingSource Source #
Show BindingSource Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods showsPrec :: Int -> BindingSource -> ShowS Source # show :: BindingSource -> String Source # showList :: [BindingSource] -> ShowS Source #
NFData BindingSource Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods rnf :: BindingSource -> () Source #
Eq BindingSource Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods (==) :: BindingSource -> BindingSource -> Bool Source # (/=) :: BindingSource -> BindingSource -> Bool Source #
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.2.2-7KnEKyKhaJHFPwDzdI3vIK" '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

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

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LocalVar -> c LocalVar Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LocalVar Source #

toConstr :: LocalVar -> Constr Source #

dataTypeOf :: LocalVar -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c LocalVar) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LocalVar) Source #

gmapT :: (forall b. Data b => b -> b) -> LocalVar -> LocalVar Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LocalVar -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LocalVar -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> LocalVar -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> LocalVar -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> LocalVar -> m LocalVar Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LocalVar -> m LocalVar Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LocalVar -> m LocalVar Source #

Generic LocalVar Source # |
Instance details Defined in Agda.Syntax.Scope.Base Associated Types type Rep LocalVar :: Type -> Type Source # Methods from :: LocalVar -> Rep LocalVar x Source # to :: Rep LocalVar x -> LocalVar Source #
Show LocalVar Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods showsPrec :: Int -> LocalVar -> ShowS Source # show :: LocalVar -> String Source # showList :: [LocalVar] -> ShowS Source #
NFData LocalVar Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods rnf :: LocalVar -> () Source #
Eq LocalVar Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods (==) :: LocalVar -> LocalVar -> Bool Source # (/=) :: LocalVar -> LocalVar -> Bool Source #
Ord LocalVar Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods compare :: LocalVar -> LocalVar -> Ordering Source # (<) :: LocalVar -> LocalVar -> Bool Source # (<=) :: LocalVar -> LocalVar -> Bool Source # (>) :: LocalVar -> LocalVar -> Bool Source # (>=) :: LocalVar -> LocalVar -> Bool Source # max :: LocalVar -> LocalVar -> LocalVar Source # min :: LocalVar -> LocalVar -> LocalVar Source #
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.2.2-7KnEKyKhaJHFPwDzdI3vIK" '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 #

scopeVarsToBind :: Lens' LocalVars ScopeInfo Source #

scopeLocals :: Lens' LocalVars ScopeInfo Source #

scopePrecedence :: Lens' PrecedenceStack ScopeInfo Source #

scopeInverseName :: Lens' NameMap ScopeInfo Source #

scopeInverseModule :: Lens' ModuleMap ScopeInfo Source #

scopeInScope :: Lens' InScopeSet ScopeInfo Source #

scopeFixities :: Lens' Fixities ScopeInfo Source #

scopePolarities :: Lens' Polarities ScopeInfo Source #

scopeFixitiesAndPolarities :: Lens' (Fixities, Polarities) ScopeInfo 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

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

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> NameSpace -> c NameSpace Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c NameSpace Source #

toConstr :: NameSpace -> Constr Source #

dataTypeOf :: NameSpace -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c NameSpace) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c NameSpace) Source #

gmapT :: (forall b. Data b => b -> b) -> NameSpace -> NameSpace Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> NameSpace -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> NameSpace -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> NameSpace -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> NameSpace -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> NameSpace -> m NameSpace Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> NameSpace -> m NameSpace Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> NameSpace -> m NameSpace Source #

Generic NameSpace Source # |
Instance details Defined in Agda.Syntax.Scope.Base Associated Types type Rep NameSpace :: Type -> Type Source # Methods from :: NameSpace -> Rep NameSpace x Source # to :: Rep NameSpace x -> NameSpace Source #
Show NameSpace Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods showsPrec :: Int -> NameSpace -> ShowS Source # show :: NameSpace -> String Source # showList :: [NameSpace] -> ShowS Source #
NFData NameSpace Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods rnf :: NameSpace -> () Source #
Eq NameSpace Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods (==) :: NameSpace -> NameSpace -> Bool Source # (/=) :: NameSpace -> NameSpace -> Bool Source #
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.2.2-7KnEKyKhaJHFPwDzdI3vIK" '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 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 #
Data NameOrModule Source # |

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> NameOrModule -> c NameOrModule Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c NameOrModule Source #

toConstr :: NameOrModule -> Constr Source #

dataTypeOf :: NameOrModule -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c NameOrModule) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c NameOrModule) Source #

gmapT :: (forall b. Data b => b -> b) -> NameOrModule -> NameOrModule Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> NameOrModule -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> NameOrModule -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> NameOrModule -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> NameOrModule -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> NameOrModule -> m NameOrModule Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> NameOrModule -> m NameOrModule Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> NameOrModule -> m NameOrModule Source #

Bounded NameOrModule Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods minBound :: NameOrModule Source # maxBound :: NameOrModule Source #
Enum NameOrModule Source # |

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

succ :: NameOrModule -> NameOrModule Source #

pred :: NameOrModule -> NameOrModule Source #

toEnum :: Int -> NameOrModule Source #

fromEnum :: NameOrModule -> Int Source #

enumFrom :: NameOrModule -> [NameOrModule] Source #

enumFromThen :: NameOrModule -> NameOrModule -> [NameOrModule] Source #

enumFromTo :: NameOrModule -> NameOrModule -> [NameOrModule] Source #

enumFromThenTo :: NameOrModule -> NameOrModule -> NameOrModule -> [NameOrModule] Source #

Generic NameOrModule Source # |
Instance details Defined in Agda.Syntax.Scope.Base Associated Types type Rep NameOrModule :: Type -> Type Source # Methods from :: NameOrModule -> Rep NameOrModule x Source # to :: Rep NameOrModule x -> NameOrModule Source #
Show NameOrModule Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods showsPrec :: Int -> NameOrModule -> ShowS Source # show :: NameOrModule -> String Source # showList :: [NameOrModule] -> ShowS Source #
NFData NameOrModule Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods rnf :: NameOrModule -> () Source #
Eq NameOrModule Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods (==) :: NameOrModule -> NameOrModule -> Bool Source # (/=) :: NameOrModule -> NameOrModule -> Bool Source #
Ord NameOrModule Source # |

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

compare :: NameOrModule -> NameOrModule -> Ordering Source #

(<) :: NameOrModule -> NameOrModule -> Bool Source #

(<=) :: NameOrModule -> NameOrModule -> Bool Source #

(>) :: NameOrModule -> NameOrModule -> Bool Source #

(>=) :: NameOrModule -> NameOrModule -> Bool Source #

max :: NameOrModule -> NameOrModule -> NameOrModule Source #

min :: NameOrModule -> NameOrModule -> NameOrModule Source #

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.2.2-7KnEKyKhaJHFPwDzdI3vIK" '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 #
Data KindOfName Source # |

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> KindOfName -> c KindOfName Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c KindOfName Source #

toConstr :: KindOfName -> Constr Source #

dataTypeOf :: KindOfName -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c KindOfName) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c KindOfName) Source #

gmapT :: (forall b. Data b => b -> b) -> KindOfName -> KindOfName Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> KindOfName -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> KindOfName -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> KindOfName -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> KindOfName -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> KindOfName -> m KindOfName Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> KindOfName -> m KindOfName Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> KindOfName -> m KindOfName Source #

Bounded KindOfName Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods minBound :: KindOfName Source # maxBound :: KindOfName Source #
Enum KindOfName Source # |

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

succ :: KindOfName -> KindOfName Source #

pred :: KindOfName -> KindOfName Source #

toEnum :: Int -> KindOfName Source #

fromEnum :: KindOfName -> Int Source #

enumFrom :: KindOfName -> [KindOfName] Source #

enumFromThen :: KindOfName -> KindOfName -> [KindOfName] Source #

enumFromTo :: KindOfName -> KindOfName -> [KindOfName] Source #

enumFromThenTo :: KindOfName -> KindOfName -> KindOfName -> [KindOfName] Source #

Generic KindOfName Source # |
Instance details Defined in Agda.Syntax.Scope.Base Associated Types type Rep KindOfName :: Type -> Type Source # Methods from :: KindOfName -> Rep KindOfName x Source # to :: Rep KindOfName x -> KindOfName Source #
Show KindOfName Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods showsPrec :: Int -> KindOfName -> ShowS Source # show :: KindOfName -> String Source # showList :: [KindOfName] -> ShowS Source #
NFData KindOfName Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods rnf :: KindOfName -> () Source #
Eq KindOfName Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods (==) :: KindOfName -> KindOfName -> Bool Source # (/=) :: KindOfName -> KindOfName -> Bool Source #
Ord KindOfName Source # |

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

compare :: KindOfName -> KindOfName -> Ordering Source #

(<) :: KindOfName -> KindOfName -> Bool Source #

(<=) :: KindOfName -> KindOfName -> Bool Source #

(>) :: KindOfName -> KindOfName -> Bool Source #

(>=) :: KindOfName -> KindOfName -> Bool Source #

max :: KindOfName -> KindOfName -> KindOfName Source #

min :: KindOfName -> KindOfName -> KindOfName Source #

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.2.2-7KnEKyKhaJHFPwDzdI3vIK" '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 Source #

foldMap :: Monoid m => (a -> m) -> WithKind a -> m Source #

foldMap' :: Monoid m => (a -> m) -> WithKind a -> m Source #

foldr :: (a -> b -> b) -> b -> WithKind a -> b Source #

foldr' :: (a -> b -> b) -> b -> WithKind a -> b Source #

foldl :: (b -> a -> b) -> b -> WithKind a -> b Source #

foldl' :: (b -> a -> b) -> b -> WithKind a -> b Source #

foldr1 :: (a -> a -> a) -> WithKind a -> a Source #

foldl1 :: (a -> a -> a) -> WithKind a -> a Source #

toList :: WithKind a -> [a] Source #

null :: WithKind a -> Bool Source #

length :: WithKind a -> Int Source #

elem :: Eq a => a -> WithKind a -> Bool Source #

maximum :: Ord a => WithKind a -> a Source #

minimum :: Ord a => WithKind a -> a Source #

sum :: Num a => WithKind a -> a Source #

product :: Num a => WithKind a -> a Source #

Traversable WithKind Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods traverse :: Applicative f => (a -> f b) -> WithKind a -> f (WithKind b) Source # sequenceA :: Applicative f => WithKind (f a) -> f (WithKind a) Source # mapM :: Monad m => (a -> m b) -> WithKind a -> m (WithKind b) Source # sequence :: Monad m => WithKind (m a) -> m (WithKind a) Source #
Functor WithKind Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods fmap :: (a -> b) -> WithKind a -> WithKind b Source # (<$) :: a -> WithKind b -> WithKind a Source #
Data a => Data (WithKind a) Source # |

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> WithKind a -> c (WithKind a) Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (WithKind a) Source #

toConstr :: WithKind a -> Constr Source #

dataTypeOf :: WithKind a -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (WithKind a)) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (WithKind a)) Source #

gmapT :: (forall b. Data b => b -> b) -> WithKind a -> WithKind a Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> WithKind a -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> WithKind a -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> WithKind a -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> WithKind a -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> WithKind a -> m (WithKind a) Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> WithKind a -> m (WithKind a) Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> WithKind a -> m (WithKind a) Source #

Show a => Show (WithKind a) Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods showsPrec :: Int -> WithKind a -> ShowS Source # show :: WithKind a -> String Source # showList :: [WithKind a] -> ShowS Source #
Eq a => Eq (WithKind a) Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods (==) :: WithKind a -> WithKind a -> Bool Source # (/=) :: WithKind a -> WithKind a -> Bool Source #
Ord a => Ord (WithKind a) Source # |

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

compare :: WithKind a -> WithKind a -> Ordering Source #

(<) :: WithKind a -> WithKind a -> Bool Source #

(<=) :: WithKind a -> WithKind a -> Bool Source #

(>) :: WithKind a -> WithKind a -> Bool Source #

(>=) :: WithKind a -> WithKind a -> Bool Source #

max :: WithKind a -> WithKind a -> WithKind a Source #

min :: WithKind a -> WithKind a -> 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

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

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> WhyInScope -> c WhyInScope Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c WhyInScope Source #

toConstr :: WhyInScope -> Constr Source #

dataTypeOf :: WhyInScope -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c WhyInScope) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c WhyInScope) Source #

gmapT :: (forall b. Data b => b -> b) -> WhyInScope -> WhyInScope Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> WhyInScope -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> WhyInScope -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> WhyInScope -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> WhyInScope -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> WhyInScope -> m WhyInScope Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> WhyInScope -> m WhyInScope Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> WhyInScope -> m WhyInScope Source #

Generic WhyInScope Source # |
Instance details Defined in Agda.Syntax.Scope.Base Associated Types type Rep WhyInScope :: Type -> Type Source # Methods from :: WhyInScope -> Rep WhyInScope x Source # to :: Rep WhyInScope x -> WhyInScope Source #
Show WhyInScope Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods showsPrec :: Int -> WhyInScope -> ShowS Source # show :: WhyInScope -> String Source # showList :: [WhyInScope] -> ShowS Source #
NFData WhyInScope Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods rnf :: WhyInScope -> () Source #
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.2.2-7KnEKyKhaJHFPwDzdI3vIK" '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' Fixity AbstractName 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 #
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 #
Data AbstractName Source # |

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> AbstractName -> c AbstractName Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c AbstractName Source #

toConstr :: AbstractName -> Constr Source #

dataTypeOf :: AbstractName -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c AbstractName) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c AbstractName) Source #

gmapT :: (forall b. Data b => b -> b) -> AbstractName -> AbstractName Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> AbstractName -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> AbstractName -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> AbstractName -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> AbstractName -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> AbstractName -> m AbstractName Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> AbstractName -> m AbstractName Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> AbstractName -> m AbstractName Source #

Generic AbstractName Source # |
Instance details Defined in Agda.Syntax.Scope.Base Associated Types type Rep AbstractName :: Type -> Type Source # Methods from :: AbstractName -> Rep AbstractName x Source # to :: Rep AbstractName x -> AbstractName Source #
Show AbstractName Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods showsPrec :: Int -> AbstractName -> ShowS Source # show :: AbstractName -> String Source # showList :: [AbstractName] -> ShowS Source #
NFData AbstractName Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods rnf :: AbstractName -> () Source #
Eq AbstractName Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods (==) :: AbstractName -> AbstractName -> Bool Source # (/=) :: AbstractName -> AbstractName -> Bool Source #
Ord AbstractName Source # |

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

compare :: AbstractName -> AbstractName -> Ordering Source #

(<) :: AbstractName -> AbstractName -> Bool Source #

(<=) :: AbstractName -> AbstractName -> Bool Source #

(>) :: AbstractName -> AbstractName -> Bool Source #

(>=) :: AbstractName -> AbstractName -> Bool Source #

max :: AbstractName -> AbstractName -> AbstractName Source #

min :: AbstractName -> AbstractName -> AbstractName Source #

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.2.2-7KnEKyKhaJHFPwDzdI3vIK" '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 #
Data NameMetadata Source # |

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> NameMetadata -> c NameMetadata Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c NameMetadata Source #

toConstr :: NameMetadata -> Constr Source #

dataTypeOf :: NameMetadata -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c NameMetadata) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c NameMetadata) Source #

gmapT :: (forall b. Data b => b -> b) -> NameMetadata -> NameMetadata Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> NameMetadata -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> NameMetadata -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> NameMetadata -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> NameMetadata -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> NameMetadata -> m NameMetadata Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> NameMetadata -> m NameMetadata Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> NameMetadata -> m NameMetadata Source #

Generic NameMetadata Source # |
Instance details Defined in Agda.Syntax.Scope.Base Associated Types type Rep NameMetadata :: Type -> Type Source # Methods from :: NameMetadata -> Rep NameMetadata x Source # to :: Rep NameMetadata x -> NameMetadata Source #
Show NameMetadata Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods showsPrec :: Int -> NameMetadata -> ShowS Source # show :: NameMetadata -> String Source # showList :: [NameMetadata] -> ShowS Source #
NFData NameMetadata Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods rnf :: NameMetadata -> () Source #
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.2.2-7KnEKyKhaJHFPwDzdI3vIK" '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

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

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> AbstractModule -> c AbstractModule Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c AbstractModule Source #

toConstr :: AbstractModule -> Constr Source #

dataTypeOf :: AbstractModule -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c AbstractModule) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c AbstractModule) Source #

gmapT :: (forall b. Data b => b -> b) -> AbstractModule -> AbstractModule Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> AbstractModule -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> AbstractModule -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> AbstractModule -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> AbstractModule -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> AbstractModule -> m AbstractModule Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> AbstractModule -> m AbstractModule Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> AbstractModule -> m AbstractModule Source #

Generic AbstractModule Source # |
Instance details Defined in Agda.Syntax.Scope.Base Associated Types type Rep AbstractModule :: Type -> Type Source # Methods from :: AbstractModule -> Rep AbstractModule x Source # to :: Rep AbstractModule x -> AbstractModule Source #
Show AbstractModule Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods showsPrec :: Int -> AbstractModule -> ShowS Source # show :: AbstractModule -> String Source # showList :: [AbstractModule] -> ShowS Source #
NFData AbstractModule Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods rnf :: AbstractModule -> () Source #
Eq AbstractModule Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods (==) :: AbstractModule -> AbstractModule -> Bool Source # (/=) :: AbstractModule -> AbstractModule -> Bool Source #
Ord AbstractModule Source # |

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

compare :: AbstractModule -> AbstractModule -> Ordering Source #

(<) :: AbstractModule -> AbstractModule -> Bool Source #

(<=) :: AbstractModule -> AbstractModule -> Bool Source #

(>) :: AbstractModule -> AbstractModule -> Bool Source #

(>=) :: AbstractModule -> AbstractModule -> Bool Source #

max :: AbstractModule -> AbstractModule -> AbstractModule Source #

min :: AbstractModule -> AbstractModule -> AbstractModule Source #

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.2.2-7KnEKyKhaJHFPwDzdI3vIK" '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, `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 #
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 #
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 #
Data ResolvedName Source # |

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ResolvedName -> c ResolvedName Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ResolvedName Source #

toConstr :: ResolvedName -> Constr Source #

dataTypeOf :: ResolvedName -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ResolvedName) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ResolvedName) Source #

gmapT :: (forall b. Data b => b -> b) -> ResolvedName -> ResolvedName Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ResolvedName -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ResolvedName -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> ResolvedName -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> ResolvedName -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ResolvedName -> m ResolvedName Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ResolvedName -> m ResolvedName Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ResolvedName -> m ResolvedName Source #

Generic ResolvedName Source # |
Instance details Defined in Agda.Syntax.Scope.Base Associated Types type Rep ResolvedName :: Type -> Type Source # Methods from :: ResolvedName -> Rep ResolvedName x Source # to :: Rep ResolvedName x -> ResolvedName Source #
Show ResolvedName Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods showsPrec :: Int -> ResolvedName -> ShowS Source # show :: ResolvedName -> String Source # showList :: [ResolvedName] -> ShowS Source #
NFData ResolvedName Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods rnf :: ResolvedName -> () Source #
Eq ResolvedName Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods (==) :: ResolvedName -> ResolvedName -> Bool Source # (/=) :: ResolvedName -> ResolvedName -> Bool Source #
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.2.2-7KnEKyKhaJHFPwDzdI3vIK" '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))))

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

usingOrHiding :: ImportDirective -> UsingOrHiding Source #

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

Apply an `ImportDirective` to a scope:

1. rename keys (C.Name) according to `renaming`;
2. 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 #

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.

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 Source # (/=) :: AllowAmbiguousNames -> AllowAmbiguousNames -> Bool Source #

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