Agda-2.6.0.1: 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
- (Debug) printing
- Boring 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 DataOrRecord
  }
- data NameSpaceId
  - = PrivateNS
  - | PublicNS
  - | ImportedNS
  - | OnlyQualifiedNS
- 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
  }
- type NameMap = Map QName (NonemptyList QName)
- type ModuleMap = Map ModuleName [QName]
- type LocalVars = AssocList Name LocalVar
- data Binder
  - = LambdaBound
  - | PatternBound
  - | LetBound
- data LocalVar = LocalVar {
  - localVar :: Name
  - localBinder :: Binder
  - localShadowedBy :: [AbstractName]
  }
- shadowLocal :: [AbstractName] -> LocalVar -> LocalVar
- patternToModuleBound :: LocalVar -> LocalVar
- notShadowedLocal :: LocalVar -> Maybe Name
- notShadowedLocals :: LocalVars -> AssocList Name Name
- updateVarsToBind :: (LocalVars -> LocalVars) -> ScopeInfo -> ScopeInfo
- setVarsToBind :: LocalVars -> ScopeInfo -> ScopeInfo
- updateScopeLocals :: (LocalVars -> LocalVars) -> ScopeInfo -> ScopeInfo
- setScopeLocals :: LocalVars -> ScopeInfo -> ScopeInfo
- mapScopeInfo :: (Scope -> Scope) -> ScopeInfo -> ScopeInfo
- data NameSpace = NameSpace {
  - nsNames :: NamesInScope
  - nsModules :: ModulesInScope
  - nsInScope :: InScopeSet
  }
- type ThingsInScope a = Map Name [a]
- type NamesInScope = ThingsInScope AbstractName
- type ModulesInScope = ThingsInScope AbstractModule
- type InScopeSet = Set QName
- data InScopeTag a where
  - NameTag :: InScopeTag AbstractName
  - ModuleTag :: InScopeTag AbstractModule
- class Eq a => InScope a where
  - inScopeTag :: InScopeTag a
- inNameSpace :: forall a. InScope a => NameSpace -> ThingsInScope a
- data KindOfName
  - = ConName
  - | FldName
  - | DefName
  - | PatternSynName
  - | GeneralizeName
  - | DisallowedGeneralizeName
  - | MacroName
  - | QuotableName
- allKindsOfNames :: [KindOfName]
- 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 :: Functor m => (QName -> m QName) -> AbstractName -> m AbstractName
- lensAmodName :: Functor m => (ModuleName -> m ModuleName) -> AbstractModule -> m AbstractModule
- data ResolvedName
  - = VarName {
    - resolvedVar :: Name
    - resolvedBinder :: Binder
    }
  - | DefinedName Access AbstractName
  - | FieldName (NonemptyList AbstractName)
  - | ConstructorName (NonemptyList AbstractName)
  - | PatternSynResName (NonemptyList AbstractName)
  - | UnknownName
- mergeNames :: Eq a => ThingsInScope 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
- mapScope' :: NameSpaceId -> (NamesInScope -> NamesInScope) -> (ModulesInScope -> ModulesInScope) -> (InScopeSet -> InScopeSet) -> Scope -> Scope
- mapScopeM :: Applicative m => (NameSpaceId -> NamesInScope -> m NamesInScope) -> (NameSpaceId -> ModulesInScope -> m ModulesInScope) -> (NameSpaceId -> InScopeSet -> m InScopeSet) -> Scope -> m Scope
- mapScopeM_ :: Applicative m => (NamesInScope -> m NamesInScope) -> (ModulesInScope -> m ModulesInScope) -> (InScopeSet -> m InScopeSet) -> Scope -> m Scope
- zipScope :: (NameSpaceId -> NamesInScope -> NamesInScope -> NamesInScope) -> (NameSpaceId -> ModulesInScope -> ModulesInScope -> ModulesInScope) -> (NameSpaceId -> InScopeSet -> InScopeSet -> InScopeSet) -> Scope -> Scope -> Scope
- zipScope_ :: (NamesInScope -> NamesInScope -> NamesInScope) -> (ModulesInScope -> ModulesInScope -> ModulesInScope) -> (InScopeSet -> InScopeSet -> InScopeSet) -> Scope -> Scope -> Scope
- recomputeInScopeSets :: Scope -> Scope
- filterScope :: (Name -> Bool) -> (Name -> Bool) -> Scope -> Scope
- allNamesInScope :: InScope a => Scope -> ThingsInScope a
- allNamesInScope' :: InScope a => Scope -> ThingsInScope (a, Access)
- exportedNamesInScope :: InScope a => Scope -> ThingsInScope a
- namesInScope :: InScope a => [NameSpaceId] -> Scope -> ThingsInScope a
- allThingsInScope :: Scope -> NameSpace
- thingsInScope :: [NameSpaceId] -> Scope -> NameSpace
- mergeScope :: Scope -> Scope -> Scope
- mergeScopes :: [Scope] -> Scope
- setScopeAccess :: NameSpaceId -> Scope -> Scope
- setNameSpace :: NameSpaceId -> NameSpace -> Scope -> Scope
- modifyNameSpace :: NameSpaceId -> (NameSpace -> NameSpace) -> Scope -> Scope
- addNamesToScope :: NameSpaceId -> Name -> [AbstractName] -> Scope -> Scope
- addNameToScope :: NameSpaceId -> Name -> AbstractName -> Scope -> Scope
- removeNameFromScope :: NameSpaceId -> Name -> Scope -> Scope
- addModuleToScope :: NameSpaceId -> Name -> AbstractModule -> Scope -> Scope
- type UsingOrHiding = Either Using [ImportedName]
- usingOrHiding :: ImportDirective -> UsingOrHiding
- applyImportDirective :: ImportDirective -> Scope -> Scope
- renameCanonicalNames :: Map QName QName -> Map ModuleName ModuleName -> Scope -> Scope
- restrictPrivate :: Scope -> Scope
- restrictLocalPrivate :: ModuleName -> Scope -> Scope
- removeOnlyQualified :: Scope -> Scope
- disallowGeneralizedVars :: Scope -> Scope
- inScopeBecause :: (WhyInScope -> WhyInScope) -> Scope -> Scope
- publicModules :: ScopeInfo -> Map ModuleName Scope
- publicNames :: ScopeInfo -> Set AbstractName
- everythingInScope :: ScopeInfo -> NameSpace
- everythingInScopeQualified :: ScopeInfo -> NameSpace
- flattenScope :: [[Name]] -> ScopeInfo -> Map QName [AbstractName]
- concreteNamesInScope :: ScopeInfo -> Set QName
- scopeLookup :: InScope a => QName -> ScopeInfo -> [a]
- scopeLookup' :: forall a. InScope a => QName -> ScopeInfo -> [(a, Access)]
- data AllowAmbiguousNames
  - = AmbiguousAnything
  - | AmbiguousConProjs
  - | AmbiguousNothing
- isNameInScope :: QName -> ScopeInfo -> Bool
- inverseScopeLookup :: Either ModuleName QName -> ScopeInfo -> [QName]
- inverseScopeLookup' :: AllowAmbiguousNames -> Either ModuleName QName -> ScopeInfo -> [QName]
- recomputeInverseScopeMaps :: ScopeInfo -> ScopeInfo
- inverseScopeLookupName :: QName -> ScopeInfo -> [QName]
- inverseScopeLookupName' :: AllowAmbiguousNames -> QName -> ScopeInfo -> [QName]
- inverseScopeLookupModule :: ModuleName -> ScopeInfo -> [QName]
- 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 DataOrRecord

Instances

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

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

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

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

toConstr :: Scope -> Constr Source #

dataTypeOf :: Scope -> DataType Source #

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

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

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

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

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

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

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

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

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

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

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 #
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 #
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 #
InstantiateFull Scope Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Scope -> ReduceM Scope Source #

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.
OnlyQualifiedNS | Visible (as qualified) from outside, but not exported when opening the module. Used for qualified constructors.

Instances

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 #

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

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

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

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

toConstr :: NameSpaceId -> Constr Source #

dataTypeOf :: NameSpaceId -> DataType Source #

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

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

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

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

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

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

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

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

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

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

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

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
- scopeLocals :: LocalVars
- scopePrecedence :: PrecedenceStack
- scopeInverseName :: NameMap
- scopeInverseModule :: ModuleMap
- scopeInScope :: InScopeSet
- scopeFixities :: Fixities

  Maps concrete names to fixities

- scopePolarities :: Polarities

  Maps concrete names to polarities

Instances

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

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

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

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

toConstr :: ScopeInfo -> Constr Source #

dataTypeOf :: ScopeInfo -> DataType Source #

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

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

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

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

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

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

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

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

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

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

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

type NameMap = Map QName (NonemptyList QName) Source #

type ModuleMap = Map ModuleName [QName] Source #

type LocalVars = AssocList Name LocalVar Source #

Local variables.

data Binder 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

Instances

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

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

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

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

toConstr :: Binder -> Constr Source #

dataTypeOf :: Binder -> DataType Source #

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

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

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

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

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

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

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

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

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

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

Show Binder Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods showsPrec :: Int -> Binder -> ShowS Source # show :: Binder -> String Source # showList :: [Binder] -> ShowS Source #
EmbPrj Binder Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: Binder -> S Int32 Source # icod_ :: Binder -> S Int32 Source # value :: Int32 -> R Binder Source #

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.

- localBinder :: Binder

  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

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

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

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

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

toConstr :: LocalVar -> Constr Source #

dataTypeOf :: LocalVar -> DataType Source #

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

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

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

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

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

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

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

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

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

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

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

shadowLocal :: [AbstractName] -> LocalVar -> LocalVar Source #

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

patternToModuleBound :: LocalVar -> LocalVar Source #

Treat patternBound variable as a module parameter

notShadowedLocal :: LocalVar -> Maybe Name Source #

Project name of unshadowed local variable.

notShadowedLocals :: LocalVars -> AssocList Name Name Source #

Get all locals that are not shadowed by imports.

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 #

mapScopeInfo :: (Scope -> Scope) -> 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

Instances

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

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

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

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

toConstr :: NameSpace -> Constr Source #

dataTypeOf :: NameSpace -> DataType Source #

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

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

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

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

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

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

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

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

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

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

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

type ThingsInScope a = Map Name [a] Source #

type NamesInScope = ThingsInScope AbstractName Source #

type ModulesInScope = ThingsInScope AbstractModule Source #

type InScopeSet = Set QName Source #

data InScopeTag a where Source #

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

A GADT just for some dependent-types trickery.

Constructors

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

class Eq a => InScope a where Source #

Type class for some dependent-types trickery.

Methods

inScopeTag :: InScopeTag a Source #

Instances

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

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

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

# 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.
FldName | Record field name.
DefName | Ordinary defined 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.

Instances

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 #

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

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

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

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

toConstr :: KindOfName -> Constr Source #

dataTypeOf :: KindOfName -> DataType Source #

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

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

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

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

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

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

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

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

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

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

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

allKindsOfNames :: [KindOfName] Source #

A list containing all name kinds.

data WhyInScope Source #

Where does a name come from?

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

Constructors

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

Instances

Data WhyInScope Source # |

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

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

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

toConstr :: WhyInScope -> Constr Source #

dataTypeOf :: WhyInScope -> DataType Source #

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

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

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

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

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

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

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

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

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

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

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 #
EmbPrj WhyInScope Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: WhyInScope -> S Int32 Source # icod_ :: WhyInScope -> S Int32 Source # value :: Int32 -> R WhyInScope Source #

data 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

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

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

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

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

toConstr :: AbstractName -> Constr Source #

dataTypeOf :: AbstractName -> DataType Source #

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

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

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

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

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

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

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

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

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

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

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 #

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 #
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 #
SetRange AbstractName Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods setRange :: Range -> AbstractName -> AbstractName Source #
HasRange AbstractName Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods getRange :: AbstractName -> Range Source #
InScope AbstractName Source # |
Instance details Defined in Agda.Syntax.Scope.Base Methods inScopeTag :: InScopeTag AbstractName Source #
NameToExpr AbstractName Source # | Turn an `AbstractName` to an expression.
Instance details Defined in Agda.Syntax.Abstract Methods nameExpr :: AbstractName -> Expr 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 #
ToConcrete AbstractName QName Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: AbstractName -> AbsToCon QName Source # bindToConcrete :: AbstractName -> (QName -> AbsToCon b) -> AbsToCon b Source #

data NameMetadata Source #

Constructors

NoMetadata |
GeneralizedVarsMetadata (Map QName Name) |

Instances

Data NameMetadata Source # |

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

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

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

toConstr :: NameMetadata -> Constr Source #

dataTypeOf :: NameMetadata -> DataType Source #

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

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

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

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

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

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

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

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

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

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

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 #
EmbPrj NameMetadata Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: NameMetadata -> S Int32 Source # icod_ :: NameMetadata -> S Int32 Source # value :: Int32 -> R NameMetadata Source #

data 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

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

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

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

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

toConstr :: AbstractModule -> Constr Source #

dataTypeOf :: AbstractModule -> DataType Source #

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

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

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

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

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

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

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

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

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

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

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 #

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

lensAnameName :: Functor m => (QName -> m QName) -> AbstractName -> m AbstractName Source #

Van Laarhoven lens on `anameName`.

lensAmodName :: Functor m => (ModuleName -> m ModuleName) -> AbstractModule -> m AbstractModule Source #

Van Laarhoven lens on `amodName`.

data ResolvedName Source #

Constructors

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

Fields

- resolvedVar :: Name
- resolvedBinder :: Binder

  What kind of binder?

DefinedName Access AbstractName | Function, data/record type, postulate.
FieldName (NonemptyList AbstractName) | Record field name. Needs to be distinguished to parse copatterns.
ConstructorName (NonemptyList AbstractName) | Data or record constructor name.
PatternSynResName (NonemptyList AbstractName) | Name of pattern synonym.
UnknownName | Unbound name.

Instances

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

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

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

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

toConstr :: ResolvedName -> Constr Source #

dataTypeOf :: ResolvedName -> DataType Source #

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

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

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

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

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

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

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

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

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

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

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 #
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 #
NameToExpr ResolvedName Source # | Assumes name is not `UnknownName`.
Instance details Defined in Agda.Syntax.Abstract Methods nameExpr :: ResolvedName -> Expr Source #
ToConcrete ResolvedName QName Source # | Assumes name is not `UnknownName`.
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: ResolvedName -> AbsToCon QName Source # bindToConcrete :: ResolvedName -> (QName -> AbsToCon b) -> AbsToCon b Source #

# Operations on name and module maps.

mergeNames :: Eq a => ThingsInScope 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.

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

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

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

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

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

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

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

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

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

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

recomputeInScopeSets :: Scope -> Scope Source #

Recompute the inScope sets of a scope.

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

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

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

Return all names in a scope.

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

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

Returns the scope's non-private names.

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

allThingsInScope :: Scope -> NameSpace Source #

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

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

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

mergeScopes :: [Scope] -> Scope Source #

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

# Specific operations on scopes

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

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

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

Update a particular name space.

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

Modify a particular name space.

addNamesToScope :: NameSpaceId -> Name -> [AbstractName] -> Scope -> Scope Source #

Add names to a scope.

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.

type UsingOrHiding = Either Using [ImportedName] Source #

usingOrHiding :: ImportDirective -> UsingOrHiding Source #

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

Apply an `ImportDirective` to a scope.

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.

removeOnlyQualified :: Scope -> Scope Source #

Remove names that can only be used qualified (when opening a scope)

disallowGeneralizedVars :: Scope -> Scope Source #

Disallow using generalized variables from the scope

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

Add an explanation to why things are in scope.

publicModules :: ScopeInfo -> Map ModuleName Scope Source #

Get the public parts of the public modules of a scope

publicNames :: ScopeInfo -> Set AbstractName Source #

everythingInScope :: ScopeInfo -> NameSpace Source #

everythingInScopeQualified :: ScopeInfo -> NameSpace Source #

flattenScope :: [[Name]] -> ScopeInfo -> Map QName [AbstractName] Source #

Compute a flattened scope. Only include unqualified names or names qualified by modules in the first argument.

concreteNamesInScope :: ScopeInfo -> Set QName Source #

Get all concrete names in scope. Includes bound variables.

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

Look up a name in the scope

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

# Inverse look-up

data AllowAmbiguousNames Source #

Constructors

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

Instances

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 #

inverseScopeLookup :: Either ModuleName QName -> ScopeInfo -> [QName] Source #

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

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

recomputeInverseScopeMaps :: ScopeInfo -> ScopeInfo Source #

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

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

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

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

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

# (Debug) printing

prettyNameSpace :: NameSpace -> [Doc] Source #

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

Add first string only if list is non-empty.

# Boring instances