Agda.Syntax.Scope.Base

This module defines the notion of a scope and operations on scopes.

Scope representation

data Scope

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

InstantiateFull Scope

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Scope -> ReduceM Scope

EmbPrj Scope

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: Scope -> S Int32

icod_ :: Scope -> S Int32

value :: Int32 -> R Scope

Null Scope

Defined in Agda.Syntax.Scope.Base

Methods

empty :: Scope

null :: Scope -> Bool

Pretty Scope

Defined in Agda.Syntax.Scope.Base

Methods

pretty :: Scope -> Doc

prettyPrec :: Int -> Scope -> Doc

prettyList :: [Scope] -> Doc

Data Scope

Defined in Agda.Syntax.Scope.Base

Methods

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

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

toConstr :: Scope -> Constr

dataTypeOf :: Scope -> DataType

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

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

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

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

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

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

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

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

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

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

Generic Scope

Defined in Agda.Syntax.Scope.Base

Associated Types

type Rep Scope :: Type -> Type

Methods

from :: Scope -> Rep Scope x

to :: Rep Scope x -> Scope

Show Scope

Defined in Agda.Syntax.Scope.Base

Methods

showsPrec :: Int -> Scope -> ShowS

show :: Scope -> String

showList :: [Scope] -> ShowS

NFData Scope

Defined in Agda.Syntax.Scope.Base

Methods

rnf :: Scope -> ()

Eq Scope

Defined in Agda.Syntax.Scope.Base

Methods

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

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

type Rep Scope

Defined in Agda.Syntax.Scope.Base

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

Constructors

IsDataModule

IsRecordModule

Instances

EmbPrj DataOrRecordModule

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: DataOrRecordModule -> S Int32

icod_ :: DataOrRecordModule -> S Int32

value :: Int32 -> R DataOrRecordModule

Data DataOrRecordModule

Defined in Agda.Syntax.Scope.Base

Methods

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

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

toConstr :: DataOrRecordModule -> Constr

dataTypeOf :: DataOrRecordModule -> DataType

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

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

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

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

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

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

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

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

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

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

Bounded DataOrRecordModule

Defined in Agda.Syntax.Scope.Base

Methods

minBound :: DataOrRecordModule

maxBound :: DataOrRecordModule

Enum DataOrRecordModule

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

Defined in Agda.Syntax.Scope.Base

Associated Types

type Rep DataOrRecordModule :: Type -> Type

Methods

from :: DataOrRecordModule -> Rep DataOrRecordModule x

to :: Rep DataOrRecordModule x -> DataOrRecordModule

Show DataOrRecordModule

Defined in Agda.Syntax.Scope.Base

Methods

showsPrec :: Int -> DataOrRecordModule -> ShowS

show :: DataOrRecordModule -> String

showList :: [DataOrRecordModule] -> ShowS

NFData DataOrRecordModule

Defined in Agda.Syntax.Scope.Base

Methods

rnf :: DataOrRecordModule -> ()

Eq DataOrRecordModule

Defined in Agda.Syntax.Scope.Base

Methods

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

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

type Rep DataOrRecordModule

Defined in Agda.Syntax.Scope.Base

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

data NameSpaceId

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

EmbPrj NameSpaceId

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: NameSpaceId -> S Int32

icod_ :: NameSpaceId -> S Int32

value :: Int32 -> R NameSpaceId

Pretty NameSpaceId

Defined in Agda.Syntax.Scope.Base

Methods

pretty :: NameSpaceId -> Doc

prettyPrec :: Int -> NameSpaceId -> Doc

prettyList :: [NameSpaceId] -> Doc

Data NameSpaceId

Defined in Agda.Syntax.Scope.Base

Methods

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

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

toConstr :: NameSpaceId -> Constr

dataTypeOf :: NameSpaceId -> DataType

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

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

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

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

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

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

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

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

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

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

Bounded NameSpaceId

Defined in Agda.Syntax.Scope.Base

Methods

minBound :: NameSpaceId

maxBound :: NameSpaceId

Enum NameSpaceId

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

Defined in Agda.Syntax.Scope.Base

Associated Types

type Rep NameSpaceId :: Type -> Type

Methods

from :: NameSpaceId -> Rep NameSpaceId x

to :: Rep NameSpaceId x -> NameSpaceId

Show NameSpaceId

Defined in Agda.Syntax.Scope.Base

Methods

showsPrec :: Int -> NameSpaceId -> ShowS

show :: NameSpaceId -> String

showList :: [NameSpaceId] -> ShowS

NFData NameSpaceId

Defined in Agda.Syntax.Scope.Base

Methods

rnf :: NameSpaceId -> ()

Eq NameSpaceId

Defined in Agda.Syntax.Scope.Base

Methods

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

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

type Rep NameSpaceId

Defined in Agda.Syntax.Scope.Base

type Rep NameSpaceId = D1 ('MetaData "NameSpaceId" "Agda.Syntax.Scope.Base" "Agda-2.6.2.1.20220320-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]

type ScopeNameSpaces = [(NameSpaceId, NameSpace)]

localNameSpace :: Access -> NameSpaceId

nameSpaceAccess :: NameSpaceId -> Access

scopeNameSpace :: NameSpaceId -> Scope -> NameSpace

Get a NameSpace from Scope.

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

A lens for scopeNameSpaces

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

`Monadic' lens (Functor sufficient).

data ScopeInfo

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

KillRange ScopeInfo

Defined in Agda.Syntax.Scope.Base

Methods

killRange :: KillRangeT ScopeInfo

EmbPrj ScopeInfo

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: ScopeInfo -> S Int32

icod_ :: ScopeInfo -> S Int32

value :: Int32 -> R ScopeInfo

Null ScopeInfo

Defined in Agda.Syntax.Scope.Base

Methods

empty :: ScopeInfo

null :: ScopeInfo -> Bool

Pretty ScopeInfo

Defined in Agda.Syntax.Scope.Base

Methods

pretty :: ScopeInfo -> Doc

prettyPrec :: Int -> ScopeInfo -> Doc

prettyList :: [ScopeInfo] -> Doc

Data ScopeInfo

Defined in Agda.Syntax.Scope.Base

Methods

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

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

toConstr :: ScopeInfo -> Constr

dataTypeOf :: ScopeInfo -> DataType

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

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

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

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

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

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

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

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

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

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

Generic ScopeInfo

Defined in Agda.Syntax.Scope.Base

Associated Types

type Rep ScopeInfo :: Type -> Type

Methods

from :: ScopeInfo -> Rep ScopeInfo x

to :: Rep ScopeInfo x -> ScopeInfo

Show ScopeInfo

Defined in Agda.Syntax.Scope.Base

Methods

showsPrec :: Int -> ScopeInfo -> ShowS

show :: ScopeInfo -> String

showList :: [ScopeInfo] -> ShowS

NFData ScopeInfo

Defined in Agda.Syntax.Scope.Base

Methods

rnf :: ScopeInfo -> ()

Eq ScopeInfo

Defined in Agda.Syntax.Scope.Base

Methods

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

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

type Rep ScopeInfo

Defined in Agda.Syntax.Scope.Base

type Rep ScopeInfo = D1 ('MetaData "ScopeInfo" "Agda.Syntax.Scope.Base" "Agda-2.6.2.1.20220320-inplace" 'False) (C1 ('MetaCons "ScopeInfo" 'PrefixI 'True) (((S1 ('MetaSel ('Just "_scopeCurrent") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName) :*: S1 ('MetaSel ('Just "_scopeModules") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map ModuleName Scope))) :*: (S1 ('MetaSel ('Just "_scopeVarsToBind") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LocalVars) :*: (S1 ('MetaSel ('Just "_scopeLocals") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LocalVars) :*: S1 ('MetaSel ('Just "_scopePrecedence") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 PrecedenceStack)))) :*: ((S1 ('MetaSel ('Just "_scopeInverseName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NameMap) :*: S1 ('MetaSel ('Just "_scopeInverseModule") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleMap)) :*: (S1 ('MetaSel ('Just "_scopeInScope") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 InScopeSet) :*: (S1 ('MetaSel ('Just "_scopeFixities") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Fixities) :*: S1 ('MetaSel ('Just "_scopePolarities") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Polarities))))))

data NameMapEntry

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

Data NameMapEntry

Defined in Agda.Syntax.Scope.Base

Methods

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

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

toConstr :: NameMapEntry -> Constr

dataTypeOf :: NameMapEntry -> DataType

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

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

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

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

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

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

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

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

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

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

Semigroup NameMapEntry

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

Defined in Agda.Syntax.Scope.Base

Methods

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

sconcat :: NonEmpty NameMapEntry -> NameMapEntry

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

Generic NameMapEntry

Defined in Agda.Syntax.Scope.Base

Associated Types

type Rep NameMapEntry :: Type -> Type

Methods

from :: NameMapEntry -> Rep NameMapEntry x

to :: Rep NameMapEntry x -> NameMapEntry

Show NameMapEntry

Defined in Agda.Syntax.Scope.Base

Methods

showsPrec :: Int -> NameMapEntry -> ShowS

show :: NameMapEntry -> String

showList :: [NameMapEntry] -> ShowS

NFData NameMapEntry

Defined in Agda.Syntax.Scope.Base

Methods

rnf :: NameMapEntry -> ()

type Rep NameMapEntry

Defined in Agda.Syntax.Scope.Base

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

type ModuleMap = Map ModuleName [QName]

type LocalVars = AssocList Name LocalVar

Local variables.

data BindingSource

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

EmbPrj BindingSource

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: BindingSource -> S Int32

icod_ :: BindingSource -> S Int32

value :: Int32 -> R BindingSource

Pretty BindingSource

Defined in Agda.Syntax.Scope.Base

Methods

pretty :: BindingSource -> Doc

prettyPrec :: Int -> BindingSource -> Doc

prettyList :: [BindingSource] -> Doc

Data BindingSource

Defined in Agda.Syntax.Scope.Base

Methods

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

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

toConstr :: BindingSource -> Constr

dataTypeOf :: BindingSource -> DataType

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

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

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

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

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

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

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

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

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

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

Generic BindingSource

Defined in Agda.Syntax.Scope.Base

Associated Types

type Rep BindingSource :: Type -> Type

Methods

from :: BindingSource -> Rep BindingSource x

to :: Rep BindingSource x -> BindingSource

Show BindingSource

Defined in Agda.Syntax.Scope.Base

Methods

showsPrec :: Int -> BindingSource -> ShowS

show :: BindingSource -> String

showList :: [BindingSource] -> ShowS

NFData BindingSource

Defined in Agda.Syntax.Scope.Base

Methods

rnf :: BindingSource -> ()

Eq BindingSource

Defined in Agda.Syntax.Scope.Base

Methods

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

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

type Rep BindingSource

Defined in Agda.Syntax.Scope.Base

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

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

EmbPrj LocalVar

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: LocalVar -> S Int32

icod_ :: LocalVar -> S Int32

value :: Int32 -> R LocalVar

Pretty LocalVar

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

Defined in Agda.Syntax.Scope.Base

Methods

pretty :: LocalVar -> Doc

prettyPrec :: Int -> LocalVar -> Doc

prettyList :: [LocalVar] -> Doc

Data LocalVar

Defined in Agda.Syntax.Scope.Base

Methods

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

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

toConstr :: LocalVar -> Constr

dataTypeOf :: LocalVar -> DataType

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

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

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

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

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

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

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

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

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

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

Generic LocalVar

Defined in Agda.Syntax.Scope.Base

Associated Types

type Rep LocalVar :: Type -> Type

Methods

from :: LocalVar -> Rep LocalVar x

to :: Rep LocalVar x -> LocalVar

Show LocalVar

Defined in Agda.Syntax.Scope.Base

Methods

showsPrec :: Int -> LocalVar -> ShowS

show :: LocalVar -> String

showList :: [LocalVar] -> ShowS

NFData LocalVar

Defined in Agda.Syntax.Scope.Base

Methods

rnf :: LocalVar -> ()

Eq LocalVar

Defined in Agda.Syntax.Scope.Base

Methods

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

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

Ord LocalVar

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

Defined in Agda.Syntax.Scope.Base

type Rep LocalVar = D1 ('MetaData "LocalVar" "Agda.Syntax.Scope.Base" "Agda-2.6.2.1.20220320-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 :: [AbstractName] -> LocalVar -> LocalVar

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

patternToModuleBound :: LocalVar -> LocalVar

Treat patternBound variable as a module parameter

notShadowedLocal :: LocalVar -> Maybe Name

Project name of unshadowed local variable.

notShadowedLocals :: LocalVars -> AssocList Name Name

Get all locals that are not shadowed by imports.

scopeCurrent :: Lens' ModuleName ScopeInfo

Lenses for ScopeInfo components

scopeModules :: Lens' (Map ModuleName Scope) ScopeInfo

scopeVarsToBind :: Lens' LocalVars ScopeInfo

scopeLocals :: Lens' LocalVars ScopeInfo

scopePrecedence :: Lens' PrecedenceStack ScopeInfo

scopeInverseName :: Lens' NameMap ScopeInfo

scopeInverseModule :: Lens' ModuleMap ScopeInfo

scopeInScope :: Lens' InScopeSet ScopeInfo

scopeFixities :: Lens' Fixities ScopeInfo

scopePolarities :: Lens' Polarities ScopeInfo

scopeFixitiesAndPolarities :: Lens' (Fixities, Polarities) ScopeInfo

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

Lens for scopeVarsToBind.

setVarsToBind :: LocalVars -> ScopeInfo -> ScopeInfo

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

Lens for scopeLocals.

setScopeLocals :: LocalVars -> ScopeInfo -> ScopeInfo

Name spaces

data NameSpace

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

EmbPrj NameSpace

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: NameSpace -> S Int32

icod_ :: NameSpace -> S Int32

value :: Int32 -> R NameSpace

Pretty NameSpace

Defined in Agda.Syntax.Scope.Base

Methods

pretty :: NameSpace -> Doc

prettyPrec :: Int -> NameSpace -> Doc

prettyList :: [NameSpace] -> Doc

Data NameSpace

Defined in Agda.Syntax.Scope.Base

Methods

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

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

toConstr :: NameSpace -> Constr

dataTypeOf :: NameSpace -> DataType

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

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

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

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

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

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

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

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

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

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

Generic NameSpace

Defined in Agda.Syntax.Scope.Base

Associated Types

type Rep NameSpace :: Type -> Type

Methods

from :: NameSpace -> Rep NameSpace x

to :: Rep NameSpace x -> NameSpace

Show NameSpace

Defined in Agda.Syntax.Scope.Base

Methods

showsPrec :: Int -> NameSpace -> ShowS

show :: NameSpace -> String

showList :: [NameSpace] -> ShowS

NFData NameSpace

Defined in Agda.Syntax.Scope.Base

Methods

rnf :: NameSpace -> ()

Eq NameSpace

Defined in Agda.Syntax.Scope.Base

Methods

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

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

type Rep NameSpace

Defined in Agda.Syntax.Scope.Base

type Rep NameSpace = D1 ('MetaData "NameSpace" "Agda.Syntax.Scope.Base" "Agda-2.6.2.1.20220320-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 [a]

type NamesInScope = ThingsInScope AbstractName

type ModulesInScope = ThingsInScope AbstractModule

type InScopeSet = Set QName

data InScopeTag a where

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

Type class for some dependent-types trickery.

Methods

inScopeTag :: InScopeTag a

Instances

InScope AbstractModule

Defined in Agda.Syntax.Scope.Base

Methods

inScopeTag :: InScopeTag AbstractModule

InScope AbstractName

Defined in Agda.Syntax.Scope.Base

Methods

inScopeTag :: InScopeTag AbstractName

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

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

Non-dependent tag for name or module.

Constructors

NameNotModule

ModuleNotName

Instances

EmbPrj NameOrModule

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: NameOrModule -> S Int32

icod_ :: NameOrModule -> S Int32

value :: Int32 -> R NameOrModule

Data NameOrModule

Defined in Agda.Syntax.Scope.Base

Methods

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

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

toConstr :: NameOrModule -> Constr

dataTypeOf :: NameOrModule -> DataType

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

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

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

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

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

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

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

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

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

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

Bounded NameOrModule

Defined in Agda.Syntax.Scope.Base

Methods

minBound :: NameOrModule

maxBound :: NameOrModule

Enum NameOrModule

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

Defined in Agda.Syntax.Scope.Base

Associated Types

type Rep NameOrModule :: Type -> Type

Methods

from :: NameOrModule -> Rep NameOrModule x

to :: Rep NameOrModule x -> NameOrModule

Show NameOrModule

Defined in Agda.Syntax.Scope.Base

Methods

showsPrec :: Int -> NameOrModule -> ShowS

show :: NameOrModule -> String

showList :: [NameOrModule] -> ShowS

NFData NameOrModule

Defined in Agda.Syntax.Scope.Base

Methods

rnf :: NameOrModule -> ()

Eq NameOrModule

Defined in Agda.Syntax.Scope.Base

Methods

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

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

Ord NameOrModule

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

Defined in Agda.Syntax.Scope.Base

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

Decorated names

data KindOfName

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

EmbPrj KindOfName

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: KindOfName -> S Int32

icod_ :: KindOfName -> S Int32

value :: Int32 -> R KindOfName

Data KindOfName

Defined in Agda.Syntax.Scope.Base

Methods

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

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

toConstr :: KindOfName -> Constr

dataTypeOf :: KindOfName -> DataType

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

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

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

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

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

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

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

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

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

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

Bounded KindOfName

Defined in Agda.Syntax.Scope.Base

Methods

minBound :: KindOfName

maxBound :: KindOfName

Enum KindOfName

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

Defined in Agda.Syntax.Scope.Base

Associated Types

type Rep KindOfName :: Type -> Type

Methods

from :: KindOfName -> Rep KindOfName x

to :: Rep KindOfName x -> KindOfName

Show KindOfName

Defined in Agda.Syntax.Scope.Base

Methods

showsPrec :: Int -> KindOfName -> ShowS

show :: KindOfName -> String

showList :: [KindOfName] -> ShowS

NFData KindOfName

Defined in Agda.Syntax.Scope.Base

Methods

rnf :: KindOfName -> ()

Eq KindOfName

Defined in Agda.Syntax.Scope.Base

Methods

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

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

Ord KindOfName

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

Defined in Agda.Syntax.Scope.Base

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

isConName :: KindOfName -> Maybe Induction

conKindOfName :: Induction -> KindOfName

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

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

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

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

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

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

Only return [Co]ConName if no ambiguity.

data KindsOfNames

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

allKindsOfNames :: KindsOfNames

someKindsOfNames :: [KindOfName] -> KindsOfNames

exceptKindsOfNames :: [KindOfName] -> KindsOfNames

data WithKind a

Decorate something with KindOfName

Constructors

WithKind

Fields

• theKind :: KindOfName
• kindedThing :: a

Instances

DeclaredNames KName

Defined in Agda.Syntax.Abstract.Views

Methods

declaredNames :: Collection KName m => KName -> m

Foldable WithKind

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

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

Defined in Agda.Syntax.Scope.Base

Methods

fmap :: (a -> b) -> WithKind a -> WithKind b

(<$) :: a -> WithKind b -> WithKind a

Data a => Data (WithKind a)

Defined in Agda.Syntax.Scope.Base

Methods

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

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

toConstr :: WithKind a -> Constr

dataTypeOf :: WithKind a -> DataType

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

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

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

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

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

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

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

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

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

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

Show a => Show (WithKind a)

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)

Defined in Agda.Syntax.Scope.Base

Methods

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

(/=) :: WithKind a -> WithKind a -> Bool

Ord a => Ord (WithKind a)

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

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

EmbPrj WhyInScope

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: WhyInScope -> S Int32

icod_ :: WhyInScope -> S Int32

value :: Int32 -> R WhyInScope

Data WhyInScope

Defined in Agda.Syntax.Scope.Base

Methods

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

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

toConstr :: WhyInScope -> Constr

dataTypeOf :: WhyInScope -> DataType

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

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

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

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

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

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

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

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

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

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

Generic WhyInScope

Defined in Agda.Syntax.Scope.Base

Associated Types

type Rep WhyInScope :: Type -> Type

Methods

from :: WhyInScope -> Rep WhyInScope x

to :: Rep WhyInScope x -> WhyInScope

Show WhyInScope

Defined in Agda.Syntax.Scope.Base

Methods

showsPrec :: Int -> WhyInScope -> ShowS

show :: WhyInScope -> String

showList :: [WhyInScope] -> ShowS

NFData WhyInScope

Defined in Agda.Syntax.Scope.Base

Methods

rnf :: WhyInScope -> ()

type Rep WhyInScope

Defined in Agda.Syntax.Scope.Base

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

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

NameToExpr AbstractName

Turn an AbstractName into an expression.

Defined in Agda.Syntax.Abstract

Methods

nameToExpr :: AbstractName -> Expr

LensFixity AbstractName

Defined in Agda.Syntax.Scope.Base

Methods

lensFixity :: Lens' Fixity AbstractName

HasRange AbstractName

Defined in Agda.Syntax.Scope.Base

Methods

getRange :: AbstractName -> Range

SetRange AbstractName

Defined in Agda.Syntax.Scope.Base

Methods

setRange :: Range -> AbstractName -> AbstractName

InScope AbstractName

Defined in Agda.Syntax.Scope.Base

Methods

inScopeTag :: InScopeTag AbstractName

SetBindingSite AbstractName

Defined in Agda.Syntax.Scope.Base

Methods

setBindingSite :: Range -> AbstractName -> AbstractName

ToConcrete AbstractName

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs AbstractName

Methods

toConcrete :: AbstractName -> AbsToCon (ConOfAbs AbstractName)

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

PrettyTCM AbstractName

Defined in Agda.TypeChecking.Pretty

Methods

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

EmbPrj AbstractName

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: AbstractName -> S Int32

icod_ :: AbstractName -> S Int32

value :: Int32 -> R AbstractName

Pretty AbstractName

Defined in Agda.Syntax.Scope.Base

Methods

pretty :: AbstractName -> Doc

prettyPrec :: Int -> AbstractName -> Doc

prettyList :: [AbstractName] -> Doc

Data AbstractName

Defined in Agda.Syntax.Scope.Base

Methods

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

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

toConstr :: AbstractName -> Constr

dataTypeOf :: AbstractName -> DataType

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

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

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

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

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

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

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

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

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

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

Generic AbstractName

Defined in Agda.Syntax.Scope.Base

Associated Types

type Rep AbstractName :: Type -> Type

Methods

from :: AbstractName -> Rep AbstractName x

to :: Rep AbstractName x -> AbstractName

Show AbstractName

Defined in Agda.Syntax.Scope.Base

Methods

showsPrec :: Int -> AbstractName -> ShowS

show :: AbstractName -> String

showList :: [AbstractName] -> ShowS

NFData AbstractName

Defined in Agda.Syntax.Scope.Base

Methods

rnf :: AbstractName -> ()

Eq AbstractName

Defined in Agda.Syntax.Scope.Base

Methods

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

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

Ord AbstractName

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

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs AbstractName = QName

type Rep AbstractName

Defined in Agda.Syntax.Scope.Base

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

Constructors

NoMetadata

GeneralizedVarsMetadata (Map QName Name)

Instances

EmbPrj NameMetadata

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: NameMetadata -> S Int32

icod_ :: NameMetadata -> S Int32

value :: Int32 -> R NameMetadata

Data NameMetadata

Defined in Agda.Syntax.Scope.Base

Methods

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

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

toConstr :: NameMetadata -> Constr

dataTypeOf :: NameMetadata -> DataType

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

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

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

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

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

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

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

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

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

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

Generic NameMetadata

Defined in Agda.Syntax.Scope.Base

Associated Types

type Rep NameMetadata :: Type -> Type

Methods

from :: NameMetadata -> Rep NameMetadata x

to :: Rep NameMetadata x -> NameMetadata

Show NameMetadata

Defined in Agda.Syntax.Scope.Base

Methods

showsPrec :: Int -> NameMetadata -> ShowS

show :: NameMetadata -> String

showList :: [NameMetadata] -> ShowS

NFData NameMetadata

Defined in Agda.Syntax.Scope.Base

Methods

rnf :: NameMetadata -> ()

type Rep NameMetadata

Defined in Agda.Syntax.Scope.Base

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

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

InScope AbstractModule

Defined in Agda.Syntax.Scope.Base

Methods

inScopeTag :: InScopeTag AbstractModule

SetBindingSite AbstractModule

Defined in Agda.Syntax.Scope.Base

Methods

setBindingSite :: Range -> AbstractModule -> AbstractModule

EmbPrj AbstractModule

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: AbstractModule -> S Int32

icod_ :: AbstractModule -> S Int32

value :: Int32 -> R AbstractModule

Pretty AbstractModule

Defined in Agda.Syntax.Scope.Base

Methods

pretty :: AbstractModule -> Doc

prettyPrec :: Int -> AbstractModule -> Doc

prettyList :: [AbstractModule] -> Doc

Data AbstractModule

Defined in Agda.Syntax.Scope.Base

Methods

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

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

toConstr :: AbstractModule -> Constr

dataTypeOf :: AbstractModule -> DataType

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

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

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

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

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

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

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

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

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

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

Generic AbstractModule

Defined in Agda.Syntax.Scope.Base

Associated Types

type Rep AbstractModule :: Type -> Type

Methods

from :: AbstractModule -> Rep AbstractModule x

to :: Rep AbstractModule x -> AbstractModule

Show AbstractModule

Defined in Agda.Syntax.Scope.Base

Methods

showsPrec :: Int -> AbstractModule -> ShowS

show :: AbstractModule -> String

showList :: [AbstractModule] -> ShowS

NFData AbstractModule

Defined in Agda.Syntax.Scope.Base

Methods

rnf :: AbstractModule -> ()

Eq AbstractModule

Defined in Agda.Syntax.Scope.Base

Methods

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

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

Ord AbstractModule

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

Defined in Agda.Syntax.Scope.Base

type Rep AbstractModule = D1 ('MetaData "AbstractModule" "Agda.Syntax.Scope.Base" "Agda-2.6.2.1.20220320-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' QName AbstractName

Van Laarhoven lens on anameName.

lensAmodName :: Lens' ModuleName AbstractModule

Van Laarhoven lens on amodName.

data ResolvedName

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

NameToExpr ResolvedName

Turn a ResolvedName into an expression.

Assumes name is not UnknownName.

Defined in Agda.Syntax.Abstract

Methods

nameToExpr :: ResolvedName -> Expr

ToConcrete ResolvedName

Assumes name is not UnknownName.

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs ResolvedName

Methods

toConcrete :: ResolvedName -> AbsToCon (ConOfAbs ResolvedName)

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

Pretty ResolvedName

Defined in Agda.Syntax.Scope.Base

Methods

pretty :: ResolvedName -> Doc

prettyPrec :: Int -> ResolvedName -> Doc

prettyList :: [ResolvedName] -> Doc

Data ResolvedName

Defined in Agda.Syntax.Scope.Base

Methods

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

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

toConstr :: ResolvedName -> Constr

dataTypeOf :: ResolvedName -> DataType

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

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

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

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

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

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

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

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

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

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

Generic ResolvedName

Defined in Agda.Syntax.Scope.Base

Associated Types

type Rep ResolvedName :: Type -> Type

Methods

from :: ResolvedName -> Rep ResolvedName x

to :: Rep ResolvedName x -> ResolvedName

Show ResolvedName

Defined in Agda.Syntax.Scope.Base

Methods

showsPrec :: Int -> ResolvedName -> ShowS

show :: ResolvedName -> String

showList :: [ResolvedName] -> ShowS

NFData ResolvedName

Defined in Agda.Syntax.Scope.Base

Methods

rnf :: ResolvedName -> ()

Eq ResolvedName

Defined in Agda.Syntax.Scope.Base

Methods

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

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

type ConOfAbs ResolvedName

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs ResolvedName = QName

type Rep ResolvedName

Defined in Agda.Syntax.Scope.Base

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

Operations on name and module maps.

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

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

Operations on name spaces

emptyNameSpace :: NameSpace

The empty name space.

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

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

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

Zip together two name spaces.

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

Map monadic function over a namespace.

General operations on scopes

emptyScope :: Scope

The empty scope.

emptyScopeInfo :: ScopeInfo

The empty scope info.

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

Map functions over the names and modules in a scope.

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

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

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

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

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

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

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

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

recomputeInScopeSets :: Scope -> Scope

Recompute the inScope sets of a scope.

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

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

Return all names in a scope.

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

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

Returns the scope's non-private names.

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

allThingsInScope :: Scope -> NameSpace

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

mergeScope :: Scope -> Scope -> Scope

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

mergeScopes :: [Scope] -> Scope

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

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

setNameSpace :: NameSpaceId -> NameSpace -> Scope -> Scope

Update a particular name space.

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

Modify a particular name space.

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

Add a name to a scope.

removeNameFromScope :: NameSpaceId -> Name -> Scope -> Scope

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

Add a module to a scope.

data UsingOrHiding

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

Constructors

UsingOnly [ImportedName]

HidingOnly [ImportedName]

usingOrHiding :: ImportDirective -> UsingOrHiding

applyImportDirective :: ImportDirective -> Scope -> Scope

Apply an ImportDirective to a scope:

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

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

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

applyImportDirective_

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

Rename the abstract names in a scope.

restrictPrivate :: Scope -> Scope

Remove private name space of a scope.

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

restrictLocalPrivate :: ModuleName -> Scope -> Scope

Remove private things from the given module from a scope.

withoutPrivates :: ScopeInfo -> ScopeInfo

Filter privates out of a ScopeInfo

disallowGeneralizedVars :: Scope -> Scope

Disallow using generalized variables from the scope

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

Add an explanation to why things are in scope.

publicModules :: ScopeInfo -> Map ModuleName Scope

Get the public parts of the public modules of a scope

publicNames :: ScopeInfo -> Set AbstractName

everythingInScope :: ScopeInfo -> NameSpace

everythingInScopeQualified :: ScopeInfo -> NameSpace

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

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

concreteNamesInScope :: ScopeInfo -> Set QName

Get all concrete names in scope. Includes bound variables.

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

Look up a name in the scope

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

Inverse look-up

data AllowAmbiguousNames

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

Defined in Agda.Syntax.Scope.Base

Methods

(==) :: AllowAmbiguousNames -> AllowAmbiguousNames -> Bool

(/=) :: AllowAmbiguousNames -> AllowAmbiguousNames -> Bool

isNameInScope :: QName -> ScopeInfo -> Bool

isNameInScopeUnqualified :: QName -> ScopeInfo -> Bool

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

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]

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

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

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

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

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

recomputeInverseScopeMaps :: ScopeInfo -> ScopeInfo

Update binding site

class SetBindingSite a where

Set the nameBindingSite in an abstract name.

Minimal complete definition

Nothing

Methods

setBindingSite :: Range -> a -> a

default setBindingSite :: (SetBindingSite b, Functor t, t b ~ a) => Range -> a -> a

Instances

SetBindingSite ModuleName

Sets the binding site of all names in the path.

Defined in Agda.Syntax.Scope.Base

Methods

setBindingSite :: Range -> ModuleName -> ModuleName

SetBindingSite Name

Defined in Agda.Syntax.Scope.Base

Methods

setBindingSite :: Range -> Name -> Name

SetBindingSite QName

Defined in Agda.Syntax.Scope.Base

Methods

setBindingSite :: Range -> QName -> QName

SetBindingSite AbstractModule

Defined in Agda.Syntax.Scope.Base

Methods

setBindingSite :: Range -> AbstractModule -> AbstractModule

SetBindingSite AbstractName

Defined in Agda.Syntax.Scope.Base

Methods

setBindingSite :: Range -> AbstractName -> AbstractName

SetBindingSite a => SetBindingSite [a]

Defined in Agda.Syntax.Scope.Base

Methods

setBindingSite :: Range -> [a] -> [a]

(Debug) printing

prettyNameSpace :: NameSpace -> [Doc]

blockOfLines :: Doc -> [Doc] -> [Doc]

Add first string only if list is non-empty.

Boring instances

Orphan instances

Pretty Suffix

Methods

pretty :: Suffix -> Doc

prettyPrec :: Int -> Suffix -> Doc

prettyList :: [Suffix] -> Doc