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

Scope representation

data Scope Source #

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

Constructors

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

Instances

Instances details

Pretty Scope Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

pretty :: Scope -> Doc Source #

prettyPrec :: Int -> Scope -> Doc Source #

prettyList :: [Scope] -> Doc Source #

InstantiateFull Scope Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Scope -> ReduceM Scope Source #

EmbPrj Scope Source #

Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: Scope -> S Int32 Source #

icod_ :: Scope -> S Int32 Source #

value :: Int32 -> R Scope Source #

Null Scope Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

empty :: Scope Source #

null :: Scope -> Bool Source #

Generic Scope Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Associated Types

type Rep Scope

Instance details

Defined in Agda.Syntax.Scope.Base

type Rep Scope = D1 ('MetaData "Scope" "Agda.Syntax.Scope.Base" "Agda-2.6.4.2-inplace" 'False) (C1 ('MetaCons "Scope" 'PrefixI 'True) ((S1 ('MetaSel ('Just "scopeName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName) :*: S1 ('MetaSel ('Just "scopeParents") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [ModuleName])) :*: (S1 ('MetaSel ('Just "scopeNameSpaces") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ScopeNameSpaces) :*: (S1 ('MetaSel ('Just "scopeImports") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map QName ModuleName)) :*: S1 ('MetaSel ('Just "scopeDatatypeModule") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe DataOrRecordModule))))))

Methods

from :: Scope -> Rep Scope x #

to :: Rep Scope x -> Scope #

Show Scope Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

showsPrec :: Int -> Scope -> ShowS #

show :: Scope -> String #

showList :: [Scope] -> ShowS #

NFData Scope Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

rnf :: Scope -> () #

Eq Scope Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

(==) :: Scope -> Scope -> Bool #

(/=) :: Scope -> Scope -> Bool #

type Rep Scope Source #

Instance details

Defined in Agda.Syntax.Scope.Base

type Rep Scope = D1 ('MetaData "Scope" "Agda.Syntax.Scope.Base" "Agda-2.6.4.2-inplace" 'False) (C1 ('MetaCons "Scope" 'PrefixI 'True) ((S1 ('MetaSel ('Just "scopeName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName) :*: S1 ('MetaSel ('Just "scopeParents") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [ModuleName])) :*: (S1 ('MetaSel ('Just "scopeNameSpaces") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ScopeNameSpaces) :*: (S1 ('MetaSel ('Just "scopeImports") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map QName ModuleName)) :*: S1 ('MetaSel ('Just "scopeDatatypeModule") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe DataOrRecordModule))))))

data DataOrRecordModule Source #

Constructors

IsDataModule
IsRecordModule

Instances

Instances details

EmbPrj DataOrRecordModule Source #

Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: DataOrRecordModule -> S Int32 Source #

icod_ :: DataOrRecordModule -> S Int32 Source #

value :: Int32 -> R DataOrRecordModule Source #

Bounded DataOrRecordModule Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

minBound :: DataOrRecordModule #

maxBound :: DataOrRecordModule #

Enum DataOrRecordModule Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

succ :: DataOrRecordModule -> DataOrRecordModule #

pred :: DataOrRecordModule -> DataOrRecordModule #

toEnum :: Int -> DataOrRecordModule #

fromEnum :: DataOrRecordModule -> Int #

enumFrom :: DataOrRecordModule -> [DataOrRecordModule] #

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

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

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

Generic DataOrRecordModule Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Associated Types

type Rep DataOrRecordModule
Instance details Defined in Agda.Syntax.Scope.Base type Rep DataOrRecordModule = D1 ('MetaData "DataOrRecordModule" "Agda.Syntax.Scope.Base" "Agda-2.6.4.2-inplace" 'False) (C1 ('MetaCons "IsDataModule" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "IsRecordModule" 'PrefixI 'False) (U1 :: Type -> Type))

Methods

from :: DataOrRecordModule -> Rep DataOrRecordModule x #

to :: Rep DataOrRecordModule x -> DataOrRecordModule #

Show DataOrRecordModule Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

showsPrec :: Int -> DataOrRecordModule -> ShowS #

show :: DataOrRecordModule -> String #

showList :: [DataOrRecordModule] -> ShowS #

NFData DataOrRecordModule Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

rnf :: DataOrRecordModule -> () #

Eq DataOrRecordModule Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

(==) :: DataOrRecordModule -> DataOrRecordModule -> Bool #

(/=) :: DataOrRecordModule -> DataOrRecordModule -> Bool #

type Rep DataOrRecordModule Source #

Instance details

Defined in Agda.Syntax.Scope.Base

type Rep DataOrRecordModule = D1 ('MetaData "DataOrRecordModule" "Agda.Syntax.Scope.Base" "Agda-2.6.4.2-inplace" 'False) (C1 ('MetaCons "IsDataModule" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "IsRecordModule" 'PrefixI 'False) (U1 :: Type -> Type))

data NameSpaceId Source #

See Access.

Constructors

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

Instances

Instances details

Pretty NameSpaceId Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

pretty :: NameSpaceId -> Doc Source #

prettyPrec :: Int -> NameSpaceId -> Doc Source #

prettyList :: [NameSpaceId] -> Doc Source #

EmbPrj NameSpaceId Source #

Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: NameSpaceId -> S Int32 Source #

icod_ :: NameSpaceId -> S Int32 Source #

value :: Int32 -> R NameSpaceId Source #

Bounded NameSpaceId Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

minBound :: NameSpaceId #

maxBound :: NameSpaceId #

Enum NameSpaceId Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

succ :: NameSpaceId -> NameSpaceId #

pred :: NameSpaceId -> NameSpaceId #

toEnum :: Int -> NameSpaceId #

fromEnum :: NameSpaceId -> Int #

enumFrom :: NameSpaceId -> [NameSpaceId] #

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

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

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

Generic NameSpaceId Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Associated Types

type Rep NameSpaceId
Instance details Defined in Agda.Syntax.Scope.Base type Rep NameSpaceId = D1 ('MetaData "NameSpaceId" "Agda.Syntax.Scope.Base" "Agda-2.6.4.2-inplace" 'False) (C1 ('MetaCons "PrivateNS" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "PublicNS" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ImportedNS" 'PrefixI 'False) (U1 :: Type -> Type)))

Methods

from :: NameSpaceId -> Rep NameSpaceId x #

to :: Rep NameSpaceId x -> NameSpaceId #

Show NameSpaceId Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

showsPrec :: Int -> NameSpaceId -> ShowS #

show :: NameSpaceId -> String #

showList :: [NameSpaceId] -> ShowS #

NFData NameSpaceId Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

rnf :: NameSpaceId -> () #

Eq NameSpaceId Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

(==) :: NameSpaceId -> NameSpaceId -> Bool #

(/=) :: NameSpaceId -> NameSpaceId -> Bool #

type Rep NameSpaceId Source #

Instance details

Defined in Agda.Syntax.Scope.Base

type Rep NameSpaceId = D1 ('MetaData "NameSpaceId" "Agda.Syntax.Scope.Base" "Agda-2.6.4.2-inplace" 'False) (C1 ('MetaCons "PrivateNS" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "PublicNS" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ImportedNS" 'PrefixI 'False) (U1 :: Type -> Type)))

allNameSpaces :: [NameSpaceId] Source #

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

localNameSpace :: Access -> NameSpaceId Source #

nameSpaceAccess :: NameSpaceId -> Access Source #

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

Get a NameSpace from Scope.

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

A lens for scopeNameSpaces

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

`Monadic' lens (Functor sufficient).

data ScopeInfo Source #

The complete information about the scope at a particular program point includes the scope stack, the local variables, and the context precedence.

Constructors

ScopeInfo

Fields

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

Instances

Instances details

Pretty ScopeInfo Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

pretty :: ScopeInfo -> Doc Source #

prettyPrec :: Int -> ScopeInfo -> Doc Source #

prettyList :: [ScopeInfo] -> Doc Source #

KillRange ScopeInfo Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

killRange :: KillRangeT ScopeInfo Source #

EmbPrj ScopeInfo Source #

Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: ScopeInfo -> S Int32 Source #

icod_ :: ScopeInfo -> S Int32 Source #

value :: Int32 -> R ScopeInfo Source #

Null ScopeInfo Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

empty :: ScopeInfo Source #

null :: ScopeInfo -> Bool Source #

Generic ScopeInfo Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Associated Types

type Rep ScopeInfo

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

from :: ScopeInfo -> Rep ScopeInfo x #

to :: Rep ScopeInfo x -> ScopeInfo #

Show ScopeInfo Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

showsPrec :: Int -> ScopeInfo -> ShowS #

show :: ScopeInfo -> String #

showList :: [ScopeInfo] -> ShowS #

NFData ScopeInfo Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

rnf :: ScopeInfo -> () #

Eq ScopeInfo Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

(==) :: ScopeInfo -> ScopeInfo -> Bool #

(/=) :: ScopeInfo -> ScopeInfo -> Bool #

type Rep ScopeInfo Source #

Instance details

Defined in Agda.Syntax.Scope.Base

data NameMapEntry Source #

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

Constructors

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

Instances

Instances details

Semigroup NameMapEntry Source #

Invariant: the KindOfName components should be equal whenever we have to concrete renderings of an abstract name.

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

(<>) :: NameMapEntry -> NameMapEntry -> NameMapEntry #

sconcat :: NonEmpty NameMapEntry -> NameMapEntry #

stimes :: Integral b => b -> NameMapEntry -> NameMapEntry #

Generic NameMapEntry Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Associated Types

type Rep NameMapEntry

Instance details

Defined in Agda.Syntax.Scope.Base

type Rep NameMapEntry = D1 ('MetaData "NameMapEntry" "Agda.Syntax.Scope.Base" "Agda-2.6.4.2-inplace" 'False) (C1 ('MetaCons "NameMapEntry" 'PrefixI 'True) (S1 ('MetaSel ('Just "qnameKind") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KindOfName) :*: S1 ('MetaSel ('Just "qnameConcrete") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 QName))))

Methods

from :: NameMapEntry -> Rep NameMapEntry x #

to :: Rep NameMapEntry x -> NameMapEntry #

Show NameMapEntry Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

showsPrec :: Int -> NameMapEntry -> ShowS #

show :: NameMapEntry -> String #

showList :: [NameMapEntry] -> ShowS #

NFData NameMapEntry Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

rnf :: NameMapEntry -> () #

type Rep NameMapEntry Source #

Instance details

Defined in Agda.Syntax.Scope.Base

type Rep NameMapEntry = D1 ('MetaData "NameMapEntry" "Agda.Syntax.Scope.Base" "Agda-2.6.4.2-inplace" 'False) (C1 ('MetaCons "NameMapEntry" 'PrefixI 'True) (S1 ('MetaSel ('Just "qnameKind") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KindOfName) :*: S1 ('MetaSel ('Just "qnameConcrete") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 QName))))

type NameMap = Map QName NameMapEntry Source #

type ModuleMap = Map ModuleName [QName] Source #

type LocalVars = AssocList Name LocalVar Source #

Local variables.

data BindingSource Source #

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

Constructors

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

Instances

Instances details

Pretty BindingSource Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

pretty :: BindingSource -> Doc Source #

prettyPrec :: Int -> BindingSource -> Doc Source #

prettyList :: [BindingSource] -> Doc Source #

EmbPrj BindingSource Source #

Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: BindingSource -> S Int32 Source #

icod_ :: BindingSource -> S Int32 Source #

value :: Int32 -> R BindingSource Source #

Generic BindingSource Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Associated Types

type Rep BindingSource

Instance details

Defined in Agda.Syntax.Scope.Base

type Rep BindingSource = D1 ('MetaData "BindingSource" "Agda.Syntax.Scope.Base" "Agda-2.6.4.2-inplace" 'False) ((C1 ('MetaCons "LambdaBound" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PatternBound" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "LetBound" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "WithBound" 'PrefixI 'False) (U1 :: Type -> Type)))

Methods

from :: BindingSource -> Rep BindingSource x #

to :: Rep BindingSource x -> BindingSource #

Show BindingSource Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

showsPrec :: Int -> BindingSource -> ShowS #

show :: BindingSource -> String #

showList :: [BindingSource] -> ShowS #

NFData BindingSource Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

rnf :: BindingSource -> () #

Eq BindingSource Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

(==) :: BindingSource -> BindingSource -> Bool #

(/=) :: BindingSource -> BindingSource -> Bool #

type Rep BindingSource Source #

Instance details

Defined in Agda.Syntax.Scope.Base

type Rep BindingSource = D1 ('MetaData "BindingSource" "Agda.Syntax.Scope.Base" "Agda-2.6.4.2-inplace" 'False) ((C1 ('MetaCons "LambdaBound" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PatternBound" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "LetBound" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "WithBound" 'PrefixI 'False) (U1 :: Type -> Type)))

data LocalVar Source #

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

Constructors

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

Instances

Instances details

Pretty LocalVar Source #

We show shadowed variables as prefixed by a ".", as not in scope.

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

pretty :: LocalVar -> Doc Source #

prettyPrec :: Int -> LocalVar -> Doc Source #

prettyList :: [LocalVar] -> Doc Source #

EmbPrj LocalVar Source #

Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: LocalVar -> S Int32 Source #

icod_ :: LocalVar -> S Int32 Source #

value :: Int32 -> R LocalVar Source #

Generic LocalVar Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Associated Types

type Rep LocalVar

Instance details

Defined in Agda.Syntax.Scope.Base

type Rep LocalVar = D1 ('MetaData "LocalVar" "Agda.Syntax.Scope.Base" "Agda-2.6.4.2-inplace" 'False) (C1 ('MetaCons "LocalVar" 'PrefixI 'True) (S1 ('MetaSel ('Just "localVar") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: (S1 ('MetaSel ('Just "localBindingSource") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 BindingSource) :*: S1 ('MetaSel ('Just "localShadowedBy") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [AbstractName]))))

Methods

from :: LocalVar -> Rep LocalVar x #

to :: Rep LocalVar x -> LocalVar #

Show LocalVar Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

showsPrec :: Int -> LocalVar -> ShowS #

show :: LocalVar -> String #

showList :: [LocalVar] -> ShowS #

NFData LocalVar Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

rnf :: LocalVar -> () #

Eq LocalVar Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

(==) :: LocalVar -> LocalVar -> Bool #

(/=) :: LocalVar -> LocalVar -> Bool #

Ord LocalVar Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

compare :: LocalVar -> LocalVar -> Ordering #

(<) :: LocalVar -> LocalVar -> Bool #

(<=) :: LocalVar -> LocalVar -> Bool #

(>) :: LocalVar -> LocalVar -> Bool #

(>=) :: LocalVar -> LocalVar -> Bool #

max :: LocalVar -> LocalVar -> LocalVar #

min :: LocalVar -> LocalVar -> LocalVar #

type Rep LocalVar Source #

Instance details

Defined in Agda.Syntax.Scope.Base

type Rep LocalVar = D1 ('MetaData "LocalVar" "Agda.Syntax.Scope.Base" "Agda-2.6.4.2-inplace" 'False) (C1 ('MetaCons "LocalVar" 'PrefixI 'True) (S1 ('MetaSel ('Just "localVar") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: (S1 ('MetaSel ('Just "localBindingSource") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 BindingSource) :*: S1 ('MetaSel ('Just "localShadowedBy") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [AbstractName]))))

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

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

patternToModuleBound :: LocalVar -> LocalVar Source #

Treat patternBound variable as a module parameter

notShadowedLocal :: LocalVar -> Maybe Name Source #

Project name of unshadowed local variable.

notShadowedLocals :: LocalVars -> AssocList Name Name Source #

Get all locals that are not shadowed by imports.

scopeCurrent :: Lens' ScopeInfo ModuleName Source #

Lenses for ScopeInfo components

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

scopeVarsToBind :: Lens' ScopeInfo LocalVars Source #

scopeLocals :: Lens' ScopeInfo LocalVars Source #

scopePrecedence :: Lens' ScopeInfo PrecedenceStack Source #

scopeInverseName :: Lens' ScopeInfo NameMap Source #

scopeInverseModule :: Lens' ScopeInfo ModuleMap Source #

scopeInScope :: Lens' ScopeInfo InScopeSet Source #

scopeFixities :: Lens' ScopeInfo Fixities Source #

scopePolarities :: Lens' ScopeInfo Polarities Source #

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

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

Lens for scopeVarsToBind.

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

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

Lens for scopeLocals.

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

Name spaces

data NameSpace Source #

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

Constructors

NameSpace
Fields nsNames :: NamesInScope Maps concrete names to a list of abstract names. nsModules :: ModulesInScope Maps concrete module names to a list of abstract module names. nsInScope :: InScopeSet All abstract names targeted by a concrete name in scope. Computed by `recomputeInScopeSets`.

Instances

Instances details

Pretty NameSpace Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

pretty :: NameSpace -> Doc Source #

prettyPrec :: Int -> NameSpace -> Doc Source #

prettyList :: [NameSpace] -> Doc Source #

EmbPrj NameSpace Source #

Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: NameSpace -> S Int32 Source #

icod_ :: NameSpace -> S Int32 Source #

value :: Int32 -> R NameSpace Source #

Generic NameSpace Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Associated Types

type Rep NameSpace

Instance details

Defined in Agda.Syntax.Scope.Base

type Rep NameSpace = D1 ('MetaData "NameSpace" "Agda.Syntax.Scope.Base" "Agda-2.6.4.2-inplace" 'False) (C1 ('MetaCons "NameSpace" 'PrefixI 'True) (S1 ('MetaSel ('Just "nsNames") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NamesInScope) :*: (S1 ('MetaSel ('Just "nsModules") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModulesInScope) :*: S1 ('MetaSel ('Just "nsInScope") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 InScopeSet))))

Methods

from :: NameSpace -> Rep NameSpace x #

to :: Rep NameSpace x -> NameSpace #

Show NameSpace Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

showsPrec :: Int -> NameSpace -> ShowS #

show :: NameSpace -> String #

showList :: [NameSpace] -> ShowS #

NFData NameSpace Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

rnf :: NameSpace -> () #

Eq NameSpace Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

(==) :: NameSpace -> NameSpace -> Bool #

(/=) :: NameSpace -> NameSpace -> Bool #

type Rep NameSpace Source #

Instance details

Defined in Agda.Syntax.Scope.Base

type Rep NameSpace = D1 ('MetaData "NameSpace" "Agda.Syntax.Scope.Base" "Agda-2.6.4.2-inplace" 'False) (C1 ('MetaCons "NameSpace" 'PrefixI 'True) (S1 ('MetaSel ('Just "nsNames") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NamesInScope) :*: (S1 ('MetaSel ('Just "nsModules") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModulesInScope) :*: S1 ('MetaSel ('Just "nsInScope") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 InScopeSet))))

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

type NamesInScope = ThingsInScope AbstractName Source #

type ModulesInScope = ThingsInScope AbstractModule Source #

type InScopeSet = Set QName Source #

data InScopeTag a where Source #

Set of types consisting of exactly AbstractName and AbstractModule.

A GADT just for some dependent-types trickery.

Constructors

NameTag :: InScopeTag AbstractName
ModuleTag :: InScopeTag AbstractModule

class Ord a => InScope a where Source #

Type class for some dependent-types trickery.

Methods

inScopeTag :: InScopeTag a Source #

Instances

Instances details

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

inNameSpace :: InScope a => NameSpace -> ThingsInScope a Source #

inNameSpace selects either the name map or the module name map from a NameSpace. What is selected is determined by result type (using the dependent-type trickery).

data NameOrModule Source #

Non-dependent tag for name or module.

Constructors

NameNotModule
ModuleNotName

Instances

Instances details

EmbPrj NameOrModule Source #

Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: NameOrModule -> S Int32 Source #

icod_ :: NameOrModule -> S Int32 Source #

value :: Int32 -> R NameOrModule Source #

Bounded NameOrModule Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

minBound :: NameOrModule #

maxBound :: NameOrModule #

Enum NameOrModule Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

succ :: NameOrModule -> NameOrModule #

pred :: NameOrModule -> NameOrModule #

toEnum :: Int -> NameOrModule #

fromEnum :: NameOrModule -> Int #

enumFrom :: NameOrModule -> [NameOrModule] #

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

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

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

Generic NameOrModule Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Associated Types

type Rep NameOrModule
Instance details Defined in Agda.Syntax.Scope.Base type Rep NameOrModule = D1 ('MetaData "NameOrModule" "Agda.Syntax.Scope.Base" "Agda-2.6.4.2-inplace" 'False) (C1 ('MetaCons "NameNotModule" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ModuleNotName" 'PrefixI 'False) (U1 :: Type -> Type))

Methods

from :: NameOrModule -> Rep NameOrModule x #

to :: Rep NameOrModule x -> NameOrModule #

Show NameOrModule Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

showsPrec :: Int -> NameOrModule -> ShowS #

show :: NameOrModule -> String #

showList :: [NameOrModule] -> ShowS #

NFData NameOrModule Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

rnf :: NameOrModule -> () #

Eq NameOrModule Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

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

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

Ord NameOrModule Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

compare :: NameOrModule -> NameOrModule -> Ordering #

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

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

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

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

max :: NameOrModule -> NameOrModule -> NameOrModule #

min :: NameOrModule -> NameOrModule -> NameOrModule #

type Rep NameOrModule Source #

Instance details

Defined in Agda.Syntax.Scope.Base

type Rep NameOrModule = D1 ('MetaData "NameOrModule" "Agda.Syntax.Scope.Base" "Agda-2.6.4.2-inplace" 'False) (C1 ('MetaCons "NameNotModule" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ModuleNotName" 'PrefixI 'False) (U1 :: Type -> Type))

Decorated names

data KindOfName Source #

For the sake of parsing left-hand sides, we distinguish constructor and record field names from defined names.

Constructors

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

Instances

Instances details

EmbPrj KindOfName Source #

Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: KindOfName -> S Int32 Source #

icod_ :: KindOfName -> S Int32 Source #

value :: Int32 -> R KindOfName Source #

Bounded KindOfName Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

minBound :: KindOfName #

maxBound :: KindOfName #

Enum KindOfName Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

succ :: KindOfName -> KindOfName #

pred :: KindOfName -> KindOfName #

toEnum :: Int -> KindOfName #

fromEnum :: KindOfName -> Int #

enumFrom :: KindOfName -> [KindOfName] #

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

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

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

Generic KindOfName Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Associated Types

type Rep KindOfName

Instance details

Defined in Agda.Syntax.Scope.Base

type Rep KindOfName = D1 ('MetaData "KindOfName" "Agda.Syntax.Scope.Base" "Agda-2.6.4.2-inplace" 'False) (((C1 ('MetaCons "ConName" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "CoConName" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FldName" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "PatternSynName" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "GeneralizeName" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "DisallowedGeneralizeName" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "MacroName" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "QuotableName" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "DataName" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RecName" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "FunName" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "AxiomName" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "PrimName" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "OtherDefName" 'PrefixI 'False) (U1 :: Type -> Type)))))

Methods

from :: KindOfName -> Rep KindOfName x #

to :: Rep KindOfName x -> KindOfName #

Show KindOfName Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

showsPrec :: Int -> KindOfName -> ShowS #

show :: KindOfName -> String #

showList :: [KindOfName] -> ShowS #

NFData KindOfName Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

rnf :: KindOfName -> () #

Eq KindOfName Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

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

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

Ord KindOfName Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

compare :: KindOfName -> KindOfName -> Ordering #

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

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

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

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

max :: KindOfName -> KindOfName -> KindOfName #

min :: KindOfName -> KindOfName -> KindOfName #

type Rep KindOfName Source #

Instance details

Defined in Agda.Syntax.Scope.Base

type Rep KindOfName = D1 ('MetaData "KindOfName" "Agda.Syntax.Scope.Base" "Agda-2.6.4.2-inplace" 'False) (((C1 ('MetaCons "ConName" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "CoConName" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FldName" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "PatternSynName" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "GeneralizeName" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "DisallowedGeneralizeName" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "MacroName" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "QuotableName" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "DataName" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RecName" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "FunName" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "AxiomName" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "PrimName" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "OtherDefName" 'PrefixI 'False) (U1 :: Type -> Type)))))

isDefName :: KindOfName -> Bool Source #

isConName :: KindOfName -> Maybe Induction Source #

conKindOfName :: Induction -> KindOfName Source #

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

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

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

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

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

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

Only return [Co]ConName if no ambiguity.

data KindsOfNames Source #

A set of KindOfName, for the sake of elemKindsOfNames.

Constructors

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

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

allKindsOfNames :: KindsOfNames Source #

someKindsOfNames :: [KindOfName] -> KindsOfNames Source #

exceptKindsOfNames :: [KindOfName] -> KindsOfNames Source #

data WithKind a Source #

Decorate something with KindOfName

Constructors

WithKind
Fields theKind :: KindOfName kindedThing :: a

Instances

Instances details

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

data WhyInScope Source #

Where does a name come from?

This information is solely for reporting to the user, see whyInScope.

Constructors

Defined	Defined in this module.
Opened QName WhyInScope	Imported from another module.
Applied QName WhyInScope	Imported by a module application.

Instances

Instances details

EmbPrj WhyInScope Source #

Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: WhyInScope -> S Int32 Source #

icod_ :: WhyInScope -> S Int32 Source #

value :: Int32 -> R WhyInScope Source #

Generic WhyInScope Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Associated Types

type Rep WhyInScope

Instance details

Defined in Agda.Syntax.Scope.Base

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

Methods

from :: WhyInScope -> Rep WhyInScope x #

to :: Rep WhyInScope x -> WhyInScope #

Show WhyInScope Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

showsPrec :: Int -> WhyInScope -> ShowS #

show :: WhyInScope -> String #

showList :: [WhyInScope] -> ShowS #

NFData WhyInScope Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

rnf :: WhyInScope -> () #

type Rep WhyInScope Source #

Instance details

Defined in Agda.Syntax.Scope.Base

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

data AbstractName Source #

A decoration of QName.

Constructors

AbsName
Fields anameName :: QName The resolved qualified name. anameKind :: KindOfName The kind (definition, constructor, record field etc.). anameLineage :: WhyInScope Explanation where this name came from. anameMetadata :: NameMetadata Additional information needed during scope checking. Currently used for generalized data/record params.

Instances

Instances details

NameToExpr AbstractName Source #

Turn an AbstractName into an expression.

Instance details

Defined in Agda.Syntax.Abstract

Methods

nameToExpr :: AbstractName -> Expr Source #

LensFixity AbstractName Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

lensFixity :: Lens' AbstractName Fixity Source #

Pretty AbstractName Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

pretty :: AbstractName -> Doc Source #

prettyPrec :: Int -> AbstractName -> Doc Source #

prettyList :: [AbstractName] -> Doc Source #

HasRange AbstractName Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

getRange :: AbstractName -> Range Source #

SetRange AbstractName Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

setRange :: Range -> AbstractName -> AbstractName Source #

InScope AbstractName Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

inScopeTag :: InScopeTag AbstractName Source #

SetBindingSite AbstractName Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

setBindingSite :: Range -> AbstractName -> AbstractName Source #

ToConcrete AbstractName Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

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

Methods

toConcrete :: AbstractName -> AbsToCon (ConOfAbs AbstractName) Source #

bindToConcrete :: AbstractName -> (ConOfAbs AbstractName -> AbsToCon b) -> AbsToCon b Source #

PrettyTCM AbstractName Source #

Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => AbstractName -> m Doc Source #

EmbPrj AbstractName Source #

Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: AbstractName -> S Int32 Source #

icod_ :: AbstractName -> S Int32 Source #

value :: Int32 -> R AbstractName Source #

Generic AbstractName Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Associated Types

type Rep AbstractName

Instance details

Defined in Agda.Syntax.Scope.Base

type Rep AbstractName = D1 ('MetaData "AbstractName" "Agda.Syntax.Scope.Base" "Agda-2.6.4.2-inplace" 'False) (C1 ('MetaCons "AbsName" 'PrefixI 'True) ((S1 ('MetaSel ('Just "anameName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Just "anameKind") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KindOfName)) :*: (S1 ('MetaSel ('Just "anameLineage") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 WhyInScope) :*: S1 ('MetaSel ('Just "anameMetadata") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NameMetadata))))

Methods

from :: AbstractName -> Rep AbstractName x #

to :: Rep AbstractName x -> AbstractName #

Show AbstractName Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

showsPrec :: Int -> AbstractName -> ShowS #

show :: AbstractName -> String #

showList :: [AbstractName] -> ShowS #

NFData AbstractName Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

rnf :: AbstractName -> () #

Eq AbstractName Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

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

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

Ord AbstractName Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

compare :: AbstractName -> AbstractName -> Ordering #

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

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

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

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

max :: AbstractName -> AbstractName -> AbstractName #

min :: AbstractName -> AbstractName -> AbstractName #

type ConOfAbs AbstractName Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs AbstractName = QName

type Rep AbstractName Source #

Instance details

Defined in Agda.Syntax.Scope.Base

type Rep AbstractName = D1 ('MetaData "AbstractName" "Agda.Syntax.Scope.Base" "Agda-2.6.4.2-inplace" 'False) (C1 ('MetaCons "AbsName" 'PrefixI 'True) ((S1 ('MetaSel ('Just "anameName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Just "anameKind") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KindOfName)) :*: (S1 ('MetaSel ('Just "anameLineage") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 WhyInScope) :*: S1 ('MetaSel ('Just "anameMetadata") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NameMetadata))))

data NameMetadata Source #

Constructors

NoMetadata
GeneralizedVarsMetadata (Map QName Name)

Instances

Instances details

EmbPrj NameMetadata Source #

Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: NameMetadata -> S Int32 Source #

icod_ :: NameMetadata -> S Int32 Source #

value :: Int32 -> R NameMetadata Source #

Generic NameMetadata Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Associated Types

type Rep NameMetadata

Instance details

Defined in Agda.Syntax.Scope.Base

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

Methods

from :: NameMetadata -> Rep NameMetadata x #

to :: Rep NameMetadata x -> NameMetadata #

Show NameMetadata Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

showsPrec :: Int -> NameMetadata -> ShowS #

show :: NameMetadata -> String #

showList :: [NameMetadata] -> ShowS #

NFData NameMetadata Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

rnf :: NameMetadata -> () #

type Rep NameMetadata Source #

Instance details

Defined in Agda.Syntax.Scope.Base

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

data AbstractModule Source #

A decoration of abstract syntax module names.

Constructors

AbsModule
Fields amodName :: ModuleName The resolved module name. amodLineage :: WhyInScope Explanation where this name came from.

Instances

Instances details

Pretty AbstractModule Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

pretty :: AbstractModule -> Doc Source #

prettyPrec :: Int -> AbstractModule -> Doc Source #

prettyList :: [AbstractModule] -> Doc Source #

InScope AbstractModule Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

inScopeTag :: InScopeTag AbstractModule Source #

SetBindingSite AbstractModule Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

setBindingSite :: Range -> AbstractModule -> AbstractModule Source #

EmbPrj AbstractModule Source #

Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: AbstractModule -> S Int32 Source #

icod_ :: AbstractModule -> S Int32 Source #

value :: Int32 -> R AbstractModule Source #

Generic AbstractModule Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Associated Types

type Rep AbstractModule

Instance details

Defined in Agda.Syntax.Scope.Base

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

Methods

from :: AbstractModule -> Rep AbstractModule x #

to :: Rep AbstractModule x -> AbstractModule #

Show AbstractModule Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

showsPrec :: Int -> AbstractModule -> ShowS #

show :: AbstractModule -> String #

showList :: [AbstractModule] -> ShowS #

NFData AbstractModule Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

rnf :: AbstractModule -> () #

Eq AbstractModule Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

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

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

Ord AbstractModule Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

compare :: AbstractModule -> AbstractModule -> Ordering #

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

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

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

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

max :: AbstractModule -> AbstractModule -> AbstractModule #

min :: AbstractModule -> AbstractModule -> AbstractModule #

type Rep AbstractModule Source #

Instance details

Defined in Agda.Syntax.Scope.Base

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

lensAnameName :: Lens' AbstractName QName Source #

Van Laarhoven lens on anameName.

lensAmodName :: Lens' AbstractModule ModuleName Source #

Van Laarhoven lens on amodName.

data ResolvedName Source #

Constructors

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

Instances

Instances details

NameToExpr ResolvedName Source #

Turn a ResolvedName into an expression.

Assumes name is not UnknownName.

Instance details

Defined in Agda.Syntax.Abstract

Methods

nameToExpr :: ResolvedName -> Expr Source #

Pretty ResolvedName Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

pretty :: ResolvedName -> Doc Source #

prettyPrec :: Int -> ResolvedName -> Doc Source #

prettyList :: [ResolvedName] -> Doc Source #

ToConcrete ResolvedName Source #

Assumes name is not UnknownName.

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

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

Methods

toConcrete :: ResolvedName -> AbsToCon (ConOfAbs ResolvedName) Source #

bindToConcrete :: ResolvedName -> (ConOfAbs ResolvedName -> AbsToCon b) -> AbsToCon b Source #

Generic ResolvedName Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Associated Types

type Rep ResolvedName

Instance details

Defined in Agda.Syntax.Scope.Base

type Rep ResolvedName = D1 ('MetaData "ResolvedName" "Agda.Syntax.Scope.Base" "Agda-2.6.4.2-inplace" 'False) ((C1 ('MetaCons "VarName" 'PrefixI 'True) (S1 ('MetaSel ('Just "resolvedVar") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Just "resolvedBindingSource") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 BindingSource)) :+: (C1 ('MetaCons "DefinedName" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Access) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AbstractName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Suffix))) :+: C1 ('MetaCons "FieldName" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 AbstractName))))) :+: (C1 ('MetaCons "ConstructorName" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set Induction)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 AbstractName))) :+: (C1 ('MetaCons "PatternSynResName" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 AbstractName))) :+: C1 ('MetaCons "UnknownName" 'PrefixI 'False) (U1 :: Type -> Type))))

Methods

from :: ResolvedName -> Rep ResolvedName x #

to :: Rep ResolvedName x -> ResolvedName #

Show ResolvedName Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

showsPrec :: Int -> ResolvedName -> ShowS #

show :: ResolvedName -> String #

showList :: [ResolvedName] -> ShowS #

NFData ResolvedName Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

rnf :: ResolvedName -> () #

Eq ResolvedName Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

(==) :: ResolvedName -> ResolvedName -> Bool #

(/=) :: ResolvedName -> ResolvedName -> Bool #

type ConOfAbs ResolvedName Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs ResolvedName = QName

type Rep ResolvedName Source #

Instance details

Defined in Agda.Syntax.Scope.Base

type Rep ResolvedName = D1 ('MetaData "ResolvedName" "Agda.Syntax.Scope.Base" "Agda-2.6.4.2-inplace" 'False) ((C1 ('MetaCons "VarName" 'PrefixI 'True) (S1 ('MetaSel ('Just "resolvedVar") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Just "resolvedBindingSource") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 BindingSource)) :+: (C1 ('MetaCons "DefinedName" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Access) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AbstractName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Suffix))) :+: C1 ('MetaCons "FieldName" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 AbstractName))))) :+: (C1 ('MetaCons "ConstructorName" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set Induction)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 AbstractName))) :+: (C1 ('MetaCons "PatternSynResName" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 AbstractName))) :+: C1 ('MetaCons "UnknownName" 'PrefixI 'False) (U1 :: Type -> Type))))

data AmbiguousNameReason Source #

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

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

Constructors

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

Instances

Instances details

Generic AmbiguousNameReason Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Associated Types

type Rep AmbiguousNameReason

Instance details

Defined in Agda.Syntax.Scope.Base

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

Methods

from :: AmbiguousNameReason -> Rep AmbiguousNameReason x #

to :: Rep AmbiguousNameReason x -> AmbiguousNameReason #

Show AmbiguousNameReason Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

showsPrec :: Int -> AmbiguousNameReason -> ShowS #

show :: AmbiguousNameReason -> String #

showList :: [AmbiguousNameReason] -> ShowS #

NFData AmbiguousNameReason Source #

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

rnf :: AmbiguousNameReason -> () #

type Rep AmbiguousNameReason Source #

Instance details

Defined in Agda.Syntax.Scope.Base

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

ambiguousNamesInReason :: AmbiguousNameReason -> List2 QName Source #

The flat list of ambiguous names in AmbiguousNameReason.

data WhyInScopeData Source #

Constructors

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

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

Operations on name and module maps.

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

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

Operations on name spaces

emptyNameSpace :: NameSpace Source #

The empty name space.

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

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

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

Zip together two name spaces.

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

Map monadic function over a namespace.

General operations on scopes

emptyScope :: Scope Source #

The empty scope.

emptyScopeInfo :: ScopeInfo Source #

The empty scope info.

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

Map functions over the names and modules in a scope.

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

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

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

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

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

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

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

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

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

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

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

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

recomputeInScopeSets :: Scope -> Scope Source #

Recompute the inScope sets of a scope.

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

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

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

Return all names in a scope.

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

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

Look up a single name in the current scope.

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

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

Returns the scope's non-private names.

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

allThingsInScope :: Scope -> NameSpace Source #

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

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

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

mergeScopes :: [Scope] -> Scope Source #

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

Specific operations on scopes

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

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

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

Update a particular name space.

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

Modify a particular name space.

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

Add a name to a scope.

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

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

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

Add a module to a scope.

data UsingOrHiding Source #

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

Constructors

UsingOnly [ImportedName]
HidingOnly [ImportedName]

usingOrHiding :: ImportDirective -> UsingOrHiding Source #

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

Apply an ImportDirective to a scope:

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

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

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

applyImportDirective_ Source #

Arguments

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

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

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

Rename the abstract names in a scope.

restrictPrivate :: Scope -> Scope Source #

Remove private name space of a scope.

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

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

Remove private things from the given module from a scope.

withoutPrivates :: ScopeInfo -> ScopeInfo Source #

Filter privates out of a ScopeInfo

disallowGeneralizedVars :: Scope -> Scope Source #

Disallow using generalized variables from the scope

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

Add an explanation to why things are in scope.

publicModules :: ScopeInfo -> Map ModuleName Scope Source #

Get the public parts of the public modules of a scope

publicNames :: ScopeInfo -> Set AbstractName Source #

everythingInScope :: ScopeInfo -> NameSpace Source #

everythingInScopeQualified :: ScopeInfo -> NameSpace Source #

concreteNamesInScope :: ScopeInfo -> Set QName Source #

Get all concrete names in scope. Includes bound variables.

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

Look up a name in the scope

scopeLookup' :: InScope a => QName -> ScopeInfo -> [(a, Access)] Source #

Inverse look-up

data AllowAmbiguousNames Source #

Constructors

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

Instances

Instances details

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

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

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

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

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

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

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

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

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

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

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

recomputeInverseScopeMaps :: ScopeInfo -> ScopeInfo Source #

Update binding site

class SetBindingSite a where Source #

Set the nameBindingSite in an abstract name.

Minimal complete definition

Nothing

Methods

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

default setBindingSite :: 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 #