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

Safe Haskell | None
Language | Haskell2010

Agda.Syntax.Scope.Base

Contents

- Scope representation
- Name spaces
- Decorated names
- Operations on name and module maps.
- Operations on name spaces
- General operations on scopes
- Specific operations on scopes
- Inverse look-up
- 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
  - _scopeRecords :: Map QName (QName, Maybe Induction)
  }
- 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 Hiding
  - | LetBound
  - | WithBound
  - | MacroBound
- data LocalVar = LocalVar {
  - localVar :: Name
  - localBindingSource :: BindingSource
  - localShadowedBy :: [AbstractName]
  }
- shadowLocal :: List1 AbstractName -> LocalVar -> LocalVar
- patternToModuleBound :: LocalVar -> LocalVar
- notShadowedLocal :: LocalVar -> Maybe Name
- notShadowedLocals :: LocalVars -> AssocList Name Name
- scopeCurrent :: Lens' ScopeInfo ModuleName
- scopeModules :: Lens' ScopeInfo (Map ModuleName Scope)
- scopeVarsToBind :: Lens' ScopeInfo LocalVars
- scopeLocals :: Lens' ScopeInfo LocalVars
- scopePrecedence :: Lens' ScopeInfo PrecedenceStack
- scopeInverseName :: Lens' ScopeInfo NameMap
- scopeInverseModule :: Lens' ScopeInfo ModuleMap
- scopeInScope :: Lens' ScopeInfo InScopeSet
- scopeFixities :: Lens' ScopeInfo Fixities
- scopePolarities :: Lens' ScopeInfo Polarities
- scopeRecords :: Lens' ScopeInfo (Map QName (QName, Maybe Induction))
- scopeFixitiesAndPolarities :: Lens' ScopeInfo (Fixities, Polarities)
- updateVarsToBind :: (LocalVars -> LocalVars) -> ScopeInfo -> ScopeInfo
- setVarsToBind :: LocalVars -> ScopeInfo -> ScopeInfo
- updateScopeLocals :: (LocalVars -> LocalVars) -> ScopeInfo -> ScopeInfo
- setScopeLocals :: LocalVars -> ScopeInfo -> ScopeInfo
- data NameSpace = NameSpace {
  - nsNames :: NamesInScope
  - nsModules :: ModulesInScope
  - nsInScope :: InScopeSet
  }
- type ThingsInScope a = Map Name (List1 a)
- type NamesInScope = ThingsInScope AbstractName
- type ModulesInScope = ThingsInScope AbstractModule
- type InScopeSet = Set QName
- data InScopeTag a where
  - NameTag :: InScopeTag AbstractName
  - ModuleTag :: InScopeTag AbstractModule
- class Ord a => InScope a where
  - inScopeTag :: InScopeTag a
- inNameSpace :: 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
- defNameKinds :: [KindOfName]
- isDefName :: KindOfName -> Bool
- conLikeNameKinds :: [KindOfName]
- isConName :: KindOfName -> Maybe Induction
- conKindOfName :: Induction -> KindOfName
- conKindOfName' :: Foldable t => t Induction -> KindOfName
- approxConInduction :: Foldable t => t Induction -> Induction
- exactConInduction :: Foldable t => t Induction -> Maybe Induction
- exactConName :: Foldable t => t Induction -> Maybe KindOfName
- data KindsOfNames
  - = AllKindsOfNames
  - | SomeKindsOfNames (Set KindOfName)
  - | ExceptKindsOfNames (Set KindOfName)
- elemKindsOfNames :: KindOfName -> KindsOfNames -> Bool
- allKindsOfNames :: KindsOfNames
- someKindsOfNames :: [KindOfName] -> KindsOfNames
- exceptKindsOfNames :: [KindOfName] -> KindsOfNames
- data WithKind a = WithKind {
  - theKind :: KindOfName
  - kindedThing :: a
  }
- data WhyInScope
  - = Defined
  - | Opened QName WhyInScope
  - | Applied QName WhyInScope
- data AbstractName = AbsName {
  - anameName :: QName
  - anameKind :: KindOfName
  - anameLineage :: WhyInScope
  - anameMetadata :: NameMetadata
  }
- data NameMetadata
  - = NoMetadata
  - | GeneralizedVarsMetadata (Map QName Name)
- data AbstractModule = AbsModule {
  - amodName :: ModuleName
  - amodLineage :: WhyInScope
  }
- lensAnameName :: Lens' AbstractName QName
- lensAmodName :: Lens' AbstractModule ModuleName
- data ResolvedName
  - = VarName {
    - resolvedVar :: Name
    - resolvedBindingSource :: BindingSource
    }
  - | DefinedName Access AbstractName Suffix
  - | FieldName (List1 AbstractName)
  - | ConstructorName (Set1 Induction) (List1 AbstractName)
  - | PatternSynResName (List1 AbstractName)
  - | UnknownName
- data AmbiguousNameReason
  - = AmbiguousLocalVar LocalVar (List1 AbstractName)
  - | AmbiguousDeclName (List2 AbstractName)
- data NameResolutionError
  - = IllegalAmbiguity AmbiguousNameReason
  - | ConstrOfNonRecord QName ResolvedName
- ambiguousNamesInReason :: AmbiguousNameReason -> List2 QName
- data WhyInScopeData = WhyInScopeData QName FilePath (Maybe LocalVar) [AbstractName] [AbstractModule]
- whyInScopeDataFromAmbiguousNameReason :: QName -> AmbiguousNameReason -> WhyInScopeData
- mergeNames :: Eq a => ThingsInScope a -> ThingsInScope a -> ThingsInScope a
- mergeNamesMany :: Eq a => [ThingsInScope a] -> ThingsInScope a
- emptyNameSpace :: NameSpace
- mapNameSpace :: (NamesInScope -> NamesInScope) -> (ModulesInScope -> ModulesInScope) -> (InScopeSet -> InScopeSet) -> NameSpace -> NameSpace
- zipNameSpace :: (NamesInScope -> NamesInScope -> NamesInScope) -> (ModulesInScope -> ModulesInScope -> ModulesInScope) -> (InScopeSet -> InScopeSet -> InScopeSet) -> NameSpace -> NameSpace -> NameSpace
- mapNameSpaceM :: Applicative m => (NamesInScope -> m NamesInScope) -> (ModulesInScope -> m ModulesInScope) -> (InScopeSet -> m InScopeSet) -> NameSpace -> m NameSpace
- emptyScope :: Scope
- emptyScopeInfo :: ScopeInfo
- mapScope :: (NameSpaceId -> NamesInScope -> NamesInScope) -> (NameSpaceId -> ModulesInScope -> ModulesInScope) -> (NameSpaceId -> InScopeSet -> InScopeSet) -> Scope -> Scope
- mapScope_ :: (NamesInScope -> NamesInScope) -> (ModulesInScope -> ModulesInScope) -> (InScopeSet -> InScopeSet) -> Scope -> Scope
- mapScopeNS :: NameSpaceId -> (NamesInScope -> NamesInScope) -> (ModulesInScope -> ModulesInScope) -> (InScopeSet -> InScopeSet) -> Scope -> Scope
- mapScopeM :: Applicative m => (NameSpaceId -> NamesInScope -> m NamesInScope) -> (NameSpaceId -> ModulesInScope -> m ModulesInScope) -> (NameSpaceId -> InScopeSet -> m InScopeSet) -> Scope -> m Scope
- mapScopeM_ :: Applicative m => (NamesInScope -> m NamesInScope) -> (ModulesInScope -> m ModulesInScope) -> (InScopeSet -> m InScopeSet) -> Scope -> m Scope
- zipScope :: (NameSpaceId -> NamesInScope -> NamesInScope -> NamesInScope) -> (NameSpaceId -> ModulesInScope -> ModulesInScope -> ModulesInScope) -> (NameSpaceId -> InScopeSet -> InScopeSet -> InScopeSet) -> Scope -> Scope -> Scope
- zipScope_ :: (NamesInScope -> NamesInScope -> NamesInScope) -> (ModulesInScope -> ModulesInScope -> ModulesInScope) -> (InScopeSet -> InScopeSet -> InScopeSet) -> Scope -> Scope -> Scope
- recomputeInScopeSets :: Scope -> Scope
- filterScope :: (Name -> Bool) -> (Name -> Bool) -> Scope -> Scope
- allNamesInScope :: InScope a => Scope -> ThingsInScope a
- allNamesInScope' :: InScope a => Scope -> ThingsInScope (a, Access)
- findNameInScope :: InScope a => Name -> Scope -> [(a, Access)]
- exportedNamesInScope :: InScope a => Scope -> ThingsInScope a
- namesInScope :: InScope a => [NameSpaceId] -> Scope -> ThingsInScope a
- allThingsInScope :: Scope -> NameSpace
- thingsInScope :: [NameSpaceId] -> Scope -> NameSpace
- mergeScope :: Scope -> Scope -> Scope
- mergeScopes :: [Scope] -> Scope
- setScopeAccess :: NameSpaceId -> Scope -> Scope
- setNameSpace :: NameSpaceId -> NameSpace -> Scope -> Scope
- modifyNameSpace :: NameSpaceId -> (NameSpace -> NameSpace) -> Scope -> Scope
- addNameToScope :: NameSpaceId -> Name -> AbstractName -> Scope -> Scope
- removeNameFromScope :: NameSpaceId -> Name -> Scope -> Scope
- addModuleToScope :: NameSpaceId -> Name -> AbstractModule -> Scope -> Scope
- data UsingOrHiding
  - = UsingOnly [ImportedName]
  - | HidingOnly [ImportedName]
- usingOrHiding :: ImportDirective -> UsingOrHiding
- applyImportDirective :: ImportDirective -> Scope -> Scope
- applyImportDirective_ :: ImportDirective -> Scope -> (Scope, (Set Name, Set Name))
- renameCanonicalNames :: Map QName QName -> Map ModuleName ModuleName -> Scope -> Scope
- restrictPrivate :: Scope -> Scope
- restrictLocalPrivate :: ModuleName -> Scope -> Scope
- withoutPrivates :: ScopeInfo -> ScopeInfo
- disallowGeneralizedVars :: Scope -> Scope
- inScopeBecause :: (WhyInScope -> WhyInScope) -> Scope -> Scope
- publicModules :: ScopeInfo -> Map ModuleName Scope
- publicNames :: ScopeInfo -> Set AbstractName
- publicNamesOfModules :: Map ModuleName Scope -> [AbstractName]
- everythingInScope :: ScopeInfo -> NameSpace
- everythingInScopeQualified :: ScopeInfo -> NameSpace
- concreteNamesInScope :: ScopeInfo -> Set QName
- scopeLookup :: InScope a => QName -> ScopeInfo -> [a]
- scopeLookup' :: InScope a => QName -> ScopeInfo -> [(a, Access)]
- data AllowAmbiguousNames
  - = AmbiguousAnything
  - | AmbiguousConProjs
  - | AmbiguousNothing
- isNameInScope :: QName -> ScopeInfo -> Bool
- isNameInScopeUnqualified :: QName -> ScopeInfo -> Bool
- inverseScopeLookupName :: QName -> ScopeInfo -> [QName]
- inverseScopeLookupName' :: AllowAmbiguousNames -> QName -> ScopeInfo -> [QName]
- inverseScopeLookupName'' :: AllowAmbiguousNames -> QName -> ScopeInfo -> Maybe NameMapEntry
- inverseScopeLookupModule :: ModuleName -> ScopeInfo -> [QName]
- inverseScopeLookupModule' :: AllowAmbiguousNames -> ModuleName -> ScopeInfo -> [QName]
- recomputeInverseScopeMaps :: ScopeInfo -> ScopeInfo
- class SetBindingSite a where
  - setBindingSite :: Range -> a -> a
- prettyNameSpace :: NameSpace -> [Doc]
- blockOfLines :: Doc -> [Doc] -> [Doc]

# Scope representation

data Scope Source #

A scope is a named collection of names partitioned into public and private names.

Constructors

Scope |

Fields

- scopeName :: ModuleName
- scopeParents :: [ModuleName]
- scopeNameSpaces :: ScopeNameSpaces
- scopeImports :: Map QName ModuleName
- scopeDatatypeModule :: Maybe DataOrRecordModule

#### Instances

Instances details

Pretty Scope Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods pretty :: Scope -> Doc Source # prettyPrec :: Int -> Scope -> Doc Source # prettyList :: [Scope] -> Doc Source #
InstantiateFull Scope Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Scope -> ReduceM Scope Source #
EmbPrj Scope Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: Scope -> S Word32 Source # icod_ :: Scope -> S Word32 Source # value :: Word32 -> R Scope Source #
Null Scope Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods empty :: Scope Source # null :: Scope -> Bool Source #
NFData Scope Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods rnf :: Scope -> () Source #
Generic Scope Source # |

Instance details

Defined in Agda.Syntax.Scope.Base

Associated Types

type Rep Scope |

Instance details

Defined in Agda.Syntax.Scope.Base

type Rep Scope = D1 ('MetaData "Scope" "Agda.Syntax.Scope.Base" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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))))))

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 #
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.8.0-DJrTbcOFazJDzri4fKrI2F" '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 Word32 Source # icod_ :: DataOrRecordModule -> S Word32 Source # value :: Word32 -> R DataOrRecordModule Source #
NFData DataOrRecordModule Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods rnf :: 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 |
Instance details Defined in Agda.Syntax.Scope.Base type Rep DataOrRecordModule = D1 ('MetaData "DataOrRecordModule" "Agda.Syntax.Scope.Base" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "IsDataModule" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "IsRecordModule" 'PrefixI 'False) (U1 :: Type -> Type))

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 #
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.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "IsDataModule" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "IsRecordModule" 'PrefixI 'False) (U1 :: Type -> Type))

data NameSpaceId Source #

See `Access`.

Constructors

PrivateNS | Things not exported by this module.
PublicNS | Things defined and exported by this module.
ImportedNS | Things from open public, exported by this module.

#### Instances

Instances details

Pretty NameSpaceId Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods pretty :: NameSpaceId -> Doc Source # prettyPrec :: Int -> NameSpaceId -> Doc Source # prettyList :: [NameSpaceId] -> Doc Source #
EmbPrj NameSpaceId Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: NameSpaceId -> S Word32 Source # icod_ :: NameSpaceId -> S Word32 Source # value :: Word32 -> R NameSpaceId Source #
NFData NameSpaceId Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods rnf :: 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 |
Instance details Defined in Agda.Syntax.Scope.Base type Rep NameSpaceId = D1 ('MetaData "NameSpaceId" "Agda.Syntax.Scope.Base" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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)))

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 #
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.8.0-DJrTbcOFazJDzri4fKrI2F" '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

- _scopeRecords :: Map QName (QName, Maybe Induction)

  Maps the name of a record to the name of its (co)constructor.

#### Instances

Instances details

Pretty ScopeInfo Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods pretty :: ScopeInfo -> Doc Source # prettyPrec :: Int -> ScopeInfo -> Doc Source # prettyList :: [ScopeInfo] -> Doc Source #
KillRange ScopeInfo Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods killRange :: KillRangeT ScopeInfo Source #
EmbPrj ScopeInfo Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: ScopeInfo -> S Word32 Source # icod_ :: ScopeInfo -> S Word32 Source # value :: Word32 -> R ScopeInfo Source #
Null ScopeInfo Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods empty :: ScopeInfo Source # null :: ScopeInfo -> Bool Source #
NFData ScopeInfo Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods rnf :: ScopeInfo -> () Source #
Generic ScopeInfo Source # |

Instance details

Defined in Agda.Syntax.Scope.Base

Associated Types

type Rep ScopeInfo |

Instance details

Defined in Agda.Syntax.Scope.Base

type Rep ScopeInfo = D1 ('MetaData "ScopeInfo" "Agda.Syntax.Scope.Base" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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) :*: S1 ('MetaSel ('Just "_scopeRecords") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map QName (QName, Maybe Induction))))))))

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 #
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.8.0-DJrTbcOFazJDzri4fKrI2F" '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) :*: S1 ('MetaSel ('Just "_scopeRecords") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map QName (QName, Maybe Induction))))))))

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

NFData NameMapEntry Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods rnf :: 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 |

Instance details

Defined in Agda.Syntax.Scope.Base

type Rep NameMapEntry = D1 ('MetaData "NameMapEntry" "Agda.Syntax.Scope.Base" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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))))

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 #
type Rep NameMapEntry Source # |

Instance details

Defined in Agda.Syntax.Scope.Base

type Rep NameMapEntry = D1 ('MetaData "NameMapEntry" "Agda.Syntax.Scope.Base" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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 Hiding | `f ... =`. Remember `Hiding` for pattern variables `{x}` and `{{x}}`. This information is only used for checking pattern synonyms. It is not serialized.

LetBound

    let ... in

WithBound

    | ... in q

MacroBound | Binding added to scope by one of context-manipulating reflection primitives

#### Instances

Instances details

Pretty BindingSource Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods pretty :: BindingSource -> Doc Source # prettyPrec :: Int -> BindingSource -> Doc Source # prettyList :: [BindingSource] -> Doc Source #
EmbPrj BindingSource Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: BindingSource -> S Word32 Source # icod_ :: BindingSource -> S Word32 Source # value :: Word32 -> R BindingSource Source #
NFData BindingSource Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods rnf :: BindingSource -> () Source #
Generic BindingSource Source # |

Instance details

Defined in Agda.Syntax.Scope.Base

Associated Types

type Rep BindingSource |

Instance details

Defined in Agda.Syntax.Scope.Base

type Rep BindingSource = D1 ('MetaData "BindingSource" "Agda.Syntax.Scope.Base" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) ((C1 ('MetaCons "LambdaBound" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PatternBound" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Hiding))) :+: (C1 ('MetaCons "LetBound" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "WithBound" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "MacroBound" 'PrefixI 'False) (U1 :: Type -> Type))))

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 #
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.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) ((C1 ('MetaCons "LambdaBound" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PatternBound" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Hiding))) :+: (C1 ('MetaCons "LetBound" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "WithBound" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "MacroBound" 'PrefixI 'False) (U1 :: Type -> Type))))

data LocalVar Source #

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

Constructors

LocalVar |

Fields

- localVar :: Name

  Unique ID of local variable.

- localBindingSource :: BindingSource

  Kind of binder used to introduce the variable (`λ`, `let`, ...).

- localShadowedBy :: [AbstractName]

  If this list is not empty, the local variable is shadowed by one or more imports.

#### Instances

Instances details

Pretty LocalVar Source # | We show shadowed variables as prefixed by a ".", as not in scope.
Instance details Defined in Agda.Syntax.Scope.Base Methods pretty :: LocalVar -> Doc Source # prettyPrec :: Int -> LocalVar -> Doc Source # prettyList :: [LocalVar] -> Doc Source #
EmbPrj LocalVar Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: LocalVar -> S Word32 Source # icod_ :: LocalVar -> S Word32 Source # value :: Word32 -> R LocalVar Source #
NFData LocalVar Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods rnf :: LocalVar -> () Source #
Generic LocalVar Source # |

Instance details

Defined in Agda.Syntax.Scope.Base

Associated Types

type Rep LocalVar |

Instance details

Defined in Agda.Syntax.Scope.Base

type Rep LocalVar = D1 ('MetaData "LocalVar" "Agda.Syntax.Scope.Base" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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]))))

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 #
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.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "LocalVar" 'PrefixI 'True) (S1 ('MetaSel ('Just "localVar") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: (S1 ('MetaSel ('Just "localBindingSource") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 BindingSource) :*: S1 ('MetaSel ('Just "localShadowedBy") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [AbstractName]))))

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

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

patternToModuleBound :: LocalVar -> LocalVar Source #

Treat patternBound variable as a module parameter

notShadowedLocal :: LocalVar -> Maybe Name Source #

Project name of unshadowed local variable.

notShadowedLocals :: LocalVars -> AssocList Name Name Source #

Get all locals that are not shadowed by imports.

scopeCurrent :: Lens' ScopeInfo ModuleName Source #

Lenses for ScopeInfo components

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

scopeVarsToBind :: Lens' ScopeInfo LocalVars Source #

scopeLocals :: Lens' ScopeInfo LocalVars Source #

scopePrecedence :: Lens' ScopeInfo PrecedenceStack Source #

scopeInverseName :: Lens' ScopeInfo NameMap Source #

scopeInverseModule :: Lens' ScopeInfo ModuleMap Source #

scopeInScope :: Lens' ScopeInfo InScopeSet Source #

scopeFixities :: Lens' ScopeInfo Fixities Source #

scopePolarities :: Lens' ScopeInfo Polarities Source #

scopeRecords :: Lens' ScopeInfo (Map QName (QName, Maybe Induction)) Source #

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

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

Lens for `scopeVarsToBind`.

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

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

Lens for `scopeLocals`.

setScopeLocals :: LocalVars -> ScopeInfo -> ScopeInfo Source #

# Name spaces

data NameSpace Source #

A `NameSpace` contains the mappings from concrete names that the user can write to the abstract fully qualified names that the type checker wants to read.

Constructors

NameSpace |

Fields

- nsNames :: NamesInScope

  Maps concrete names to a list of abstract names.

- nsModules :: ModulesInScope

  Maps concrete module names to a list of abstract module names.

- nsInScope :: InScopeSet

  All abstract names targeted by a concrete name in scope. Computed by `recomputeInScopeSets`.

#### Instances

Instances details

Pretty NameSpace Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods pretty :: NameSpace -> Doc Source # prettyPrec :: Int -> NameSpace -> Doc Source # prettyList :: [NameSpace] -> Doc Source #
EmbPrj NameSpace Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: NameSpace -> S Word32 Source # icod_ :: NameSpace -> S Word32 Source # value :: Word32 -> R NameSpace Source #
NFData NameSpace Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods rnf :: NameSpace -> () Source #
Generic NameSpace Source # |

Instance details

Defined in Agda.Syntax.Scope.Base

Associated Types

type Rep NameSpace |

Instance details

Defined in Agda.Syntax.Scope.Base

type Rep NameSpace = D1 ('MetaData "NameSpace" "Agda.Syntax.Scope.Base" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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))))

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 #
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.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "NameSpace" 'PrefixI 'True) (S1 ('MetaSel ('Just "nsNames") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NamesInScope) :*: (S1 ('MetaSel ('Just "nsModules") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModulesInScope) :*: S1 ('MetaSel ('Just "nsInScope") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 InScopeSet))))

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

type NamesInScope = ThingsInScope AbstractName Source #

type ModulesInScope = ThingsInScope AbstractModule Source #

type InScopeSet = Set QName Source #

data InScopeTag a where Source #

Set of types consisting of exactly `AbstractName` and `AbstractModule`.

A GADT just for some dependent-types trickery.

Constructors

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

class Ord a => InScope a where Source #

Type class for some dependent-types trickery.

Methods

inScopeTag :: InScopeTag a Source #

#### Instances

Instances details

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

inNameSpace :: 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 Word32 Source # icod_ :: NameOrModule -> S Word32 Source # value :: Word32 -> R NameOrModule Source #
NFData NameOrModule Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods rnf :: 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 |
Instance details Defined in Agda.Syntax.Scope.Base type Rep NameOrModule = D1 ('MetaData "NameOrModule" "Agda.Syntax.Scope.Base" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "NameNotModule" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ModuleNotName" 'PrefixI 'False) (U1 :: Type -> Type))

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 #
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.8.0-DJrTbcOFazJDzri4fKrI2F" '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 Word32 Source # icod_ :: KindOfName -> S Word32 Source # value :: Word32 -> R KindOfName Source #
NFData KindOfName Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods rnf :: 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 |

Instance details

Defined in Agda.Syntax.Scope.Base

type Rep KindOfName = D1 ('MetaData "KindOfName" "Agda.Syntax.Scope.Base" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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)))))

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 #
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.8.0-DJrTbcOFazJDzri4fKrI2F" '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)))))

defNameKinds :: [KindOfName] Source #

All kinds of regular definitions.

isDefName :: KindOfName -> Bool Source #

conLikeNameKinds :: [KindOfName] Source #

Constructor and pattern synonyms.

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 #
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 #
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 #
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 Word32 Source # icod_ :: WhyInScope -> S Word32 Source # value :: Word32 -> R WhyInScope Source #
NFData WhyInScope Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods rnf :: WhyInScope -> () Source #
Generic WhyInScope Source # |

Instance details

Defined in Agda.Syntax.Scope.Base

Associated Types

type Rep WhyInScope |

Instance details

Defined in Agda.Syntax.Scope.Base

type Rep WhyInScope = D1 ('MetaData "WhyInScope" "Agda.Syntax.Scope.Base" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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))))

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 #
type Rep WhyInScope Source # |

Instance details

Defined in Agda.Syntax.Scope.Base

type Rep WhyInScope = D1 ('MetaData "WhyInScope" "Agda.Syntax.Scope.Base" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "Defined" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Opened" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 WhyInScope)) :+: C1 ('MetaCons "Applied" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 WhyInScope))))

data AbstractName Source #

A decoration of `QName`.

Constructors

AbsName |

Fields

- anameName :: QName

  The resolved qualified name.

- anameKind :: KindOfName

  The kind (definition, constructor, record field etc.).

- anameLineage :: WhyInScope

  Explanation where this name came from.

- anameMetadata :: NameMetadata

  Additional information needed during scope checking. Currently used for generalized data/record params.

#### Instances

Instances details

NameToExpr AbstractName Source # | Turn an `AbstractName` into an expression.
Instance details Defined in Agda.Syntax.Abstract Methods nameToExpr :: AbstractName -> Expr Source #
LensFixity AbstractName Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods lensFixity :: Lens' AbstractName Fixity Source #
Pretty AbstractName Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods pretty :: AbstractName -> Doc Source # prettyPrec :: Int -> AbstractName -> Doc Source # prettyList :: [AbstractName] -> Doc Source #
HasRange AbstractName Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods getRange :: AbstractName -> Range Source #
SetRange AbstractName Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods setRange :: Range -> AbstractName -> AbstractName Source #
InScope AbstractName Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods inScopeTag :: InScopeTag AbstractName Source #
SetBindingSite AbstractName Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods setBindingSite :: Range -> AbstractName -> AbstractName Source #
ToConcrete AbstractName Source # |

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs AbstractName |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs AbstractName = QName

Methods

toConcrete :: MonadToConcrete m => AbstractName -> m (ConOfAbs AbstractName) Source #

bindToConcrete :: MonadToConcrete m => AbstractName -> (ConOfAbs AbstractName -> m b) -> m 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 Word32 Source # icod_ :: AbstractName -> S Word32 Source # value :: Word32 -> R AbstractName Source #
NFData AbstractName Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods rnf :: AbstractName -> () Source #
Generic AbstractName Source # |

Instance details

Defined in Agda.Syntax.Scope.Base

Associated Types

type Rep AbstractName |

Instance details

Defined in Agda.Syntax.Scope.Base

type Rep AbstractName = D1 ('MetaData "AbstractName" "Agda.Syntax.Scope.Base" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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))))

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 #
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.8.0-DJrTbcOFazJDzri4fKrI2F" '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 Word32 Source # icod_ :: NameMetadata -> S Word32 Source # value :: Word32 -> R NameMetadata Source #
NFData NameMetadata Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods rnf :: NameMetadata -> () Source #
Generic NameMetadata Source # |

Instance details

Defined in Agda.Syntax.Scope.Base

Associated Types

type Rep NameMetadata |

Instance details

Defined in Agda.Syntax.Scope.Base

type Rep NameMetadata = D1 ('MetaData "NameMetadata" "Agda.Syntax.Scope.Base" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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))))

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 #
type Rep NameMetadata Source # |

Instance details

Defined in Agda.Syntax.Scope.Base

type Rep NameMetadata = D1 ('MetaData "NameMetadata" "Agda.Syntax.Scope.Base" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "NoMetadata" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "GeneralizedVarsMetadata" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map QName Name))))

data AbstractModule Source #

A decoration of abstract syntax module names.

Constructors

AbsModule |

Fields

- amodName :: ModuleName

  The resolved module name.

- amodLineage :: WhyInScope

  Explanation where this name came from.

#### Instances

Instances details

Pretty AbstractModule Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods pretty :: AbstractModule -> Doc Source # prettyPrec :: Int -> AbstractModule -> Doc Source # prettyList :: [AbstractModule] -> Doc Source #
InScope AbstractModule Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods inScopeTag :: InScopeTag AbstractModule Source #
SetBindingSite AbstractModule Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods setBindingSite :: Range -> AbstractModule -> AbstractModule Source #
EmbPrj AbstractModule Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: AbstractModule -> S Word32 Source # icod_ :: AbstractModule -> S Word32 Source # value :: Word32 -> R AbstractModule Source #
NFData AbstractModule Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods rnf :: AbstractModule -> () Source #
Generic AbstractModule Source # |

Instance details

Defined in Agda.Syntax.Scope.Base

Associated Types

type Rep AbstractModule |

Instance details

Defined in Agda.Syntax.Scope.Base

type Rep AbstractModule = D1 ('MetaData "AbstractModule" "Agda.Syntax.Scope.Base" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "AbsModule" 'PrefixI 'True) (S1 ('MetaSel ('Just "amodName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName) :*: S1 ('MetaSel ('Just "amodLineage") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 WhyInScope)))

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 #
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.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "AbsModule" 'PrefixI 'True) (S1 ('MetaSel ('Just "amodName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName) :*: S1 ('MetaSel ('Just "amodLineage") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 WhyInScope)))

lensAnameName :: Lens' AbstractName QName Source #

Van Laarhoven lens on `anameName`.

lensAmodName :: Lens' AbstractModule ModuleName Source #

Van Laarhoven lens on `amodName`.

data ResolvedName Source #

Constructors

VarName | Local variable bound by λ, Π, module telescope, pattern, `let`.

Fields

- resolvedVar :: Name
- resolvedBindingSource :: BindingSource

  What kind of binder?

DefinedName | Function, data/record type, postulate.

Fields

- Access
- AbstractName
- Suffix

  `anameKind` can be `DefName`, `MacroName`, `QuotableName`.

FieldName | Record field name. Needs to be distinguished to parse copatterns.

Fields

- (List1 AbstractName)

  `(`FldName` ==) . `anameKind`` for all names.

ConstructorName | Data or record constructor name.

Fields

- (Set1 Induction)

  `Inductive` or `CoInductive` or both.

- (List1 AbstractName)

  `isJust . `isConName` . `anameKind`` for all names.

PatternSynResName | Name of pattern synonym.

Fields

- (List1 AbstractName)

  `(`PatternSynName` ==) . `anameKind`` for all names.

UnknownName | Unbound name.

#### Instances

Instances details

NameToExpr ResolvedName Source # | Turn a `ResolvedName` into an expression. Assumes name is not `UnknownName`.
Instance details Defined in Agda.Syntax.Abstract Methods nameToExpr :: ResolvedName -> Expr Source #
Pretty ResolvedName Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods pretty :: ResolvedName -> Doc Source # prettyPrec :: Int -> ResolvedName -> Doc Source # prettyList :: [ResolvedName] -> Doc Source #
ToConcrete ResolvedName Source # | Assumes name is not `UnknownName`.

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs ResolvedName |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs ResolvedName = QName

Methods

toConcrete :: MonadToConcrete m => ResolvedName -> m (ConOfAbs ResolvedName) Source #

bindToConcrete :: MonadToConcrete m => ResolvedName -> (ConOfAbs ResolvedName -> m b) -> m b Source #

NFData ResolvedName Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods rnf :: ResolvedName -> () Source #
Generic ResolvedName Source # |

Instance details

Defined in Agda.Syntax.Scope.Base

Associated Types

type Rep ResolvedName |

Instance details

Defined in Agda.Syntax.Scope.Base

type Rep ResolvedName = D1 ('MetaData "ResolvedName" "Agda.Syntax.Scope.Base" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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 (Set1 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))))

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 #
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.8.0-DJrTbcOFazJDzri4fKrI2F" '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 (Set1 Induction)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 AbstractName))) :+: (C1 ('MetaCons "PatternSynResName" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 AbstractName))) :+: C1 ('MetaCons "UnknownName" 'PrefixI 'False) (U1 :: Type -> Type))))

data AmbiguousNameReason Source #

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

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

Constructors

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

#### Instances

Instances details

NFData AmbiguousNameReason Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods rnf :: AmbiguousNameReason -> () Source #
Generic AmbiguousNameReason Source # |

Instance details

Defined in Agda.Syntax.Scope.Base

Associated Types

type Rep AmbiguousNameReason |

Instance details

Defined in Agda.Syntax.Scope.Base

type Rep AmbiguousNameReason = D1 ('MetaData "AmbiguousNameReason" "Agda.Syntax.Scope.Base" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "AmbiguousLocalVar" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LocalVar) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 AbstractName))) :+: C1 ('MetaCons "AmbiguousDeclName" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List2 AbstractName))))

Methods

from :: AmbiguousNameReason -> Rep AmbiguousNameReason x Source #

to :: Rep AmbiguousNameReason x -> AmbiguousNameReason Source #

Show AmbiguousNameReason Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods showsPrec :: Int -> AmbiguousNameReason -> ShowS Source # show :: AmbiguousNameReason -> String Source # showList :: [AmbiguousNameReason] -> ShowS Source #
type Rep AmbiguousNameReason Source # |

Instance details

Defined in Agda.Syntax.Scope.Base

type Rep AmbiguousNameReason = D1 ('MetaData "AmbiguousNameReason" "Agda.Syntax.Scope.Base" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "AmbiguousLocalVar" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LocalVar) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 AbstractName))) :+: C1 ('MetaCons "AmbiguousDeclName" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List2 AbstractName))))

data NameResolutionError Source #

A failure in name resolution, indicating the reason that a name which is in scope could not be returned from `tryResolveName`.

Constructors

IllegalAmbiguity AmbiguousNameReason | Ambiguous names are not supported in this situation.
ConstrOfNonRecord QName ResolvedName | The name was `Foo.constructor`, and `Foo` is in scope, but it is not a record.

#### Instances

Instances details

Generic NameResolutionError Source # |

Instance details

Defined in Agda.Syntax.Scope.Base

Associated Types

type Rep NameResolutionError |

Instance details

Defined in Agda.Syntax.Scope.Base

type Rep NameResolutionError = D1 ('MetaData "NameResolutionError" "Agda.Syntax.Scope.Base" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "IllegalAmbiguity" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AmbiguousNameReason)) :+: C1 ('MetaCons "ConstrOfNonRecord" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ResolvedName)))

Methods

from :: NameResolutionError -> Rep NameResolutionError x Source #

to :: Rep NameResolutionError x -> NameResolutionError Source #

Show NameResolutionError Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods showsPrec :: Int -> NameResolutionError -> ShowS Source # show :: NameResolutionError -> String Source # showList :: [NameResolutionError] -> ShowS Source #
type Rep NameResolutionError Source # |

Instance details

Defined in Agda.Syntax.Scope.Base

type Rep NameResolutionError = D1 ('MetaData "NameResolutionError" "Agda.Syntax.Scope.Base" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "IllegalAmbiguity" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AmbiguousNameReason)) :+: C1 ('MetaCons "ConstrOfNonRecord" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ResolvedName)))

ambiguousNamesInReason :: AmbiguousNameReason -> List2 QName Source #

The flat list of ambiguous names in `AmbiguousNameReason`.

data WhyInScopeData Source #

Constructors

WhyInScopeData |

Fields

- QName

  The name `x` this explanation is about.

- FilePath

  The directory in which the current module resides.

- (Maybe LocalVar)

  The local variable that `x` could denote, if any.

- [AbstractName]

  The defined names that `x` could denote.

- [AbstractModule]

  The modules that `x` could denote.

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

# Operations on name and module maps.

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

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

# Operations on name spaces

emptyNameSpace :: NameSpace Source #

The empty name space.

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

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

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

Zip together two name spaces.

mapNameSpaceM :: Applicative m => (NamesInScope -> m NamesInScope) -> (ModulesInScope -> m ModulesInScope) -> (InScopeSet -> m InScopeSet) -> NameSpace -> m NameSpace Source #

Map monadic function over a namespace.

# General operations on scopes

emptyScope :: Scope Source #

The empty scope.

emptyScopeInfo :: ScopeInfo Source #

The empty scope info.

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

Map functions over the names and modules in a scope.

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

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

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

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

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

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

mapScopeM_ :: Applicative m => (NamesInScope -> m NamesInScope) -> (ModulesInScope -> m ModulesInScope) -> (InScopeSet -> m InScopeSet) -> Scope -> m Scope Source #

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

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

Zip together two scopes. The resulting scope has the same name as the first scope.

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

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

recomputeInScopeSets :: Scope -> Scope Source #

Recompute the inScope sets of a scope.

filterScope :: (Name -> Bool) -> (Name -> Bool) -> Scope -> Scope Source #

Filter a scope keeping only concrete names matching the predicates. The first predicate is applied to the names and the second to the modules.

allNamesInScope :: InScope a => Scope -> ThingsInScope a Source #

Return all names in a scope.

allNamesInScope' :: InScope a => Scope -> ThingsInScope (a, Access) Source #

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

Look up a single name in the current scope.

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

exportedNamesInScope :: InScope a => Scope -> ThingsInScope a Source #

Returns the scope's non-private names.

namesInScope :: InScope a => [NameSpaceId] -> Scope -> ThingsInScope a Source #

allThingsInScope :: Scope -> NameSpace Source #

thingsInScope :: [NameSpaceId] -> Scope -> NameSpace Source #

mergeScope :: Scope -> Scope -> Scope Source #

Merge two scopes. The result has the name of the first scope.

mergeScopes :: [Scope] -> Scope Source #

Merge a non-empty list of scopes. The result has the name of the first scope in the list.

# Specific operations on scopes

setScopeAccess :: NameSpaceId -> Scope -> Scope Source #

Move all names in a scope to the given name space (except never move from Imported to Public).

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

Update a particular name space.

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

Modify a particular name space.

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

Add a name to a scope.

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

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

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

Add a module to a scope.

data UsingOrHiding Source #

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

Constructors

UsingOnly [ImportedName] |
HidingOnly [ImportedName] |

usingOrHiding :: ImportDirective -> UsingOrHiding Source #

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

Apply an `ImportDirective` to a scope:

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 #

publicNamesOfModules :: Map ModuleName Scope -> [AbstractName] Source #

everythingInScope :: ScopeInfo -> NameSpace Source #

everythingInScopeQualified :: ScopeInfo -> NameSpace Source #

concreteNamesInScope :: ScopeInfo -> Set QName Source #

Get all concrete names in scope. Includes bound variables.

scopeLookup :: InScope a => QName -> ScopeInfo -> [a] Source #

Look up a name in the scope

scopeLookup' :: 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 :: forall b (t :: Type -> Type). (SetBindingSite b, Functor t, t b ~ a) => Range -> a -> a Source #

#### Instances

Instances details

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

# (Debug) printing

prettyNameSpace :: NameSpace -> [Doc] Source #

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

Add first string only if list is non-empty.

# Boring instances

# Orphan instances

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