Agda-2.6.20240714: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.Syntax.Scope.Base

Description

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

Synopsis

Scope representation

data Scope Source #

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

Instances

Instances details
Pretty Scope Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

InstantiateFull Scope Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

EmbPrj Scope Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: Scope -> S Int32 Source #

icod_ :: Scope -> S Int32 Source #

value :: Int32 -> R Scope Source #

Null Scope Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

empty :: Scope Source #

null :: Scope -> Bool Source #

NFData Scope Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

rnf :: Scope -> ()

Generic Scope Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Associated Types

type Rep Scope 
Instance details

Defined in Agda.Syntax.Scope.Base

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

Methods

from :: Scope -> Rep Scope x

to :: Rep Scope x -> Scope

Show Scope Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

showsPrec :: Int -> Scope -> ShowS

show :: Scope -> String

showList :: [Scope] -> ShowS

Eq Scope Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

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

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

type Rep Scope Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

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

data DataOrRecordModule Source #

Instances

Instances details
EmbPrj DataOrRecordModule Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

NFData DataOrRecordModule Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

rnf :: DataOrRecordModule -> ()

Bounded DataOrRecordModule Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Enum DataOrRecordModule Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Generic DataOrRecordModule Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Associated Types

type Rep DataOrRecordModule 
Instance details

Defined in Agda.Syntax.Scope.Base

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

Defined in Agda.Syntax.Scope.Base

Methods

showsPrec :: Int -> DataOrRecordModule -> ShowS

show :: DataOrRecordModule -> String

showList :: [DataOrRecordModule] -> ShowS

Eq DataOrRecordModule Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

type Rep DataOrRecordModule Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

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

data NameSpaceId Source #

See Access.

Constructors

PrivateNS

Things not exported by this module.

PublicNS

Things defined and exported by this module.

ImportedNS

Things from open public, exported by this module.

Instances

Instances details
Pretty NameSpaceId Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

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 #

NFData NameSpaceId Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

rnf :: NameSpaceId -> ()

Bounded NameSpaceId Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Enum NameSpaceId Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Generic NameSpaceId Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Associated Types

type Rep NameSpaceId 
Instance details

Defined in Agda.Syntax.Scope.Base

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

Methods

from :: NameSpaceId -> Rep NameSpaceId x

to :: Rep NameSpaceId x -> NameSpaceId

Show NameSpaceId Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

showsPrec :: Int -> NameSpaceId -> ShowS

show :: NameSpaceId -> String

showList :: [NameSpaceId] -> ShowS

Eq NameSpaceId Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

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

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

type Rep NameSpaceId Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

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

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

Instances

Instances details
Pretty ScopeInfo Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

KillRange ScopeInfo Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

EmbPrj ScopeInfo Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: ScopeInfo -> S Int32 Source #

icod_ :: ScopeInfo -> S Int32 Source #

value :: Int32 -> R ScopeInfo Source #

Null ScopeInfo Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

NFData ScopeInfo Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

rnf :: ScopeInfo -> ()

Generic ScopeInfo Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Associated Types

type Rep ScopeInfo 
Instance details

Defined in Agda.Syntax.Scope.Base

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

Methods

from :: ScopeInfo -> Rep ScopeInfo x

to :: Rep ScopeInfo x -> ScopeInfo

Show ScopeInfo Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

showsPrec :: Int -> ScopeInfo -> ShowS

show :: ScopeInfo -> String

showList :: [ScopeInfo] -> ShowS

Eq ScopeInfo Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

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

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

type Rep ScopeInfo Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

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

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

Constructors

NameMapEntry 

Fields

Instances

Instances details
NFData NameMapEntry Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

rnf :: NameMapEntry -> ()

Semigroup NameMapEntry Source #

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

Instance details

Defined in Agda.Syntax.Scope.Base

Generic NameMapEntry Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Associated Types

type Rep NameMapEntry 
Instance details

Defined in Agda.Syntax.Scope.Base

type Rep NameMapEntry = D1 ('MetaData "NameMapEntry" "Agda.Syntax.Scope.Base" "Agda-2.6.20240714-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))))
Show NameMapEntry Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

showsPrec :: Int -> NameMapEntry -> ShowS

show :: NameMapEntry -> String

showList :: [NameMapEntry] -> ShowS

type Rep NameMapEntry Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

type Rep NameMapEntry = D1 ('MetaData "NameMapEntry" "Agda.Syntax.Scope.Base" "Agda-2.6.20240714-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 LocalVars = AssocList Name LocalVar Source #

Local variables.

data BindingSource Source #

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

Constructors

LambdaBound

λ (currently also used for Π and module parameters)

PatternBound Hiding

f ... =. Remember Hiding for pattern variables {x} and {{x}}. This information is only used for checking pattern synonyms. It is not serialized.

LetBound
let ... in
WithBound
| ... in q

Instances

Instances details
Pretty BindingSource Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

EmbPrj BindingSource Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: BindingSource -> S Int32 Source #

icod_ :: BindingSource -> S Int32 Source #

value :: Int32 -> R BindingSource Source #

NFData BindingSource Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

rnf :: BindingSource -> ()

Generic BindingSource Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Associated Types

type Rep BindingSource 
Instance details

Defined in Agda.Syntax.Scope.Base

type Rep BindingSource = D1 ('MetaData "BindingSource" "Agda.Syntax.Scope.Base" "Agda-2.6.20240714-inplace" 'False) ((C1 ('MetaCons "LambdaBound" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PatternBound" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Hiding))) :+: (C1 ('MetaCons "LetBound" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "WithBound" 'PrefixI 'False) (U1 :: Type -> Type)))
Show BindingSource Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

showsPrec :: Int -> BindingSource -> ShowS

show :: BindingSource -> String

showList :: [BindingSource] -> ShowS

Eq BindingSource Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

type Rep BindingSource Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

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

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

Instances

Instances details
Pretty LocalVar Source #

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

Instance details

Defined in Agda.Syntax.Scope.Base

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 #

NFData LocalVar Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

rnf :: LocalVar -> ()

Generic LocalVar Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Associated Types

type Rep LocalVar 
Instance details

Defined in Agda.Syntax.Scope.Base

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

Methods

from :: LocalVar -> Rep LocalVar x

to :: Rep LocalVar x -> LocalVar

Show LocalVar Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

showsPrec :: Int -> LocalVar -> ShowS

show :: LocalVar -> String

showList :: [LocalVar] -> ShowS

Eq LocalVar Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

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

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

Ord LocalVar Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

compare :: LocalVar -> LocalVar -> Ordering

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

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

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

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

max :: LocalVar -> LocalVar -> LocalVar

min :: LocalVar -> LocalVar -> LocalVar

type Rep LocalVar Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

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

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

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

patternToModuleBound :: LocalVar -> LocalVar Source #

Treat patternBound variable as a module parameter

notShadowedLocal :: LocalVar -> Maybe Name Source #

Project name of unshadowed local variable.

notShadowedLocals :: LocalVars -> AssocList Name Name Source #

Get all locals that are not shadowed by imports.

scopeCurrent :: Lens' ScopeInfo ModuleName Source #

Lenses for ScopeInfo components

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

Instances

Instances details
Pretty NameSpace Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

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 #

NFData NameSpace Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

rnf :: NameSpace -> ()

Generic NameSpace Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Associated Types

type Rep NameSpace 
Instance details

Defined in Agda.Syntax.Scope.Base

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

Methods

from :: NameSpace -> Rep NameSpace x

to :: Rep NameSpace x -> NameSpace

Show NameSpace Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

showsPrec :: Int -> NameSpace -> ShowS

show :: NameSpace -> String

showList :: [NameSpace] -> ShowS

Eq NameSpace Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

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

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

type Rep NameSpace Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

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

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

data InScopeTag a where Source #

Set of types consisting of exactly AbstractName and AbstractModule.

A GADT just for some dependent-types trickery.

class Ord a => InScope a where Source #

Type class for some dependent-types trickery.

Instances

Instances details
InScope AbstractModule Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

InScope AbstractName Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

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

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

data NameOrModule Source #

Non-dependent tag for name or module.

Instances

Instances details
EmbPrj NameOrModule Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: NameOrModule -> S Int32 Source #

icod_ :: NameOrModule -> S Int32 Source #

value :: Int32 -> R NameOrModule Source #

NFData NameOrModule Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

rnf :: NameOrModule -> ()

Bounded NameOrModule Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Enum NameOrModule Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Generic NameOrModule Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Associated Types

type Rep NameOrModule 
Instance details

Defined in Agda.Syntax.Scope.Base

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

Defined in Agda.Syntax.Scope.Base

Methods

showsPrec :: Int -> NameOrModule -> ShowS

show :: NameOrModule -> String

showList :: [NameOrModule] -> ShowS

Eq NameOrModule Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

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

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

Ord NameOrModule Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

type Rep NameOrModule Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

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

Decorated names

data KindOfName Source #

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

Constructors

ConName

Constructor name (Inductive or don't know).

CoConName

Constructor name (definitely CoInductive).

FldName

Record field name.

PatternSynName

Name of a pattern synonym.

GeneralizeName

Name to be generalized

DisallowedGeneralizeName

Generalizable variable from a let open

MacroName

Name of a macro

QuotableName

A name that can only be quoted. Previous category DefName: (Refined in a flat manner as Enum and Bounded are not hereditary.)

DataName

Name of a data.

RecName

Name of a record.

FunName

Name of a defined function.

AxiomName

Name of a postulate.

PrimName

Name of a primitive.

OtherDefName

A DefName, but either other kind or don't know which kind. End DefName. Keep these together in sequence, for sake of isDefName!

Instances

Instances details
EmbPrj KindOfName Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: KindOfName -> S Int32 Source #

icod_ :: KindOfName -> S Int32 Source #

value :: Int32 -> R KindOfName Source #

NFData KindOfName Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

rnf :: KindOfName -> ()

Bounded KindOfName Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Enum KindOfName Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Generic KindOfName Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Associated Types

type Rep KindOfName 
Instance details

Defined in Agda.Syntax.Scope.Base

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

Methods

from :: KindOfName -> Rep KindOfName x

to :: Rep KindOfName x -> KindOfName

Show KindOfName Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

showsPrec :: Int -> KindOfName -> ShowS

show :: KindOfName -> String

showList :: [KindOfName] -> ShowS

Eq KindOfName Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

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

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

Ord KindOfName Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

type Rep KindOfName Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

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

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

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

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

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

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

Only return [Co]ConName if no ambiguity.

data KindsOfNames Source #

A set of KindOfName, for the sake of elemKindsOfNames.

Constructors

AllKindsOfNames 
SomeKindsOfNames (Set KindOfName)

Only these kinds.

ExceptKindsOfNames (Set KindOfName)

All but these Kinds.

data WithKind a Source #

Decorate something with KindOfName

Constructors

WithKind 

Fields

Instances

Instances details
DeclaredNames KName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

Functor WithKind Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

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

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

Foldable WithKind Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

fold :: Monoid m => WithKind m -> m

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

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

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

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

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

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

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

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

toList :: WithKind a -> [a]

null :: WithKind a -> Bool

length :: WithKind a -> Int

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

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

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

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

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

Traversable WithKind Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

traverse :: Applicative f => (a -> f b) -> WithKind a -> f (WithKind b)

sequenceA :: Applicative f => WithKind (f a) -> f (WithKind a)

mapM :: Monad m => (a -> m b) -> WithKind a -> m (WithKind b)

sequence :: Monad m => WithKind (m a) -> m (WithKind a)

Show a => Show (WithKind a) Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

showsPrec :: Int -> WithKind a -> ShowS

show :: WithKind a -> String

showList :: [WithKind a] -> ShowS

Eq a => Eq (WithKind a) Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

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

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

Ord a => Ord (WithKind a) Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

compare :: WithKind a -> WithKind a -> Ordering

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

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

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

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

max :: WithKind a -> WithKind a -> WithKind a

min :: WithKind a -> WithKind a -> WithKind a

data WhyInScope Source #

Where does a name come from?

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

Constructors

Defined

Defined in this module.

Opened QName WhyInScope

Imported from another module.

Applied QName WhyInScope

Imported by a module application.

Instances

Instances details
EmbPrj WhyInScope Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: WhyInScope -> S Int32 Source #

icod_ :: WhyInScope -> S Int32 Source #

value :: Int32 -> R WhyInScope Source #

NFData WhyInScope Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

rnf :: WhyInScope -> ()

Generic WhyInScope Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Associated Types

type Rep WhyInScope 
Instance details

Defined in Agda.Syntax.Scope.Base

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

Methods

from :: WhyInScope -> Rep WhyInScope x

to :: Rep WhyInScope x -> WhyInScope

Show WhyInScope Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

showsPrec :: Int -> WhyInScope -> ShowS

show :: WhyInScope -> String

showList :: [WhyInScope] -> ShowS

type Rep WhyInScope Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

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

data AbstractName Source #

A decoration of QName.

Constructors

AbsName 

Fields

Instances

Instances details
NameToExpr AbstractName Source #

Turn an AbstractName into an expression.

Instance details

Defined in Agda.Syntax.Abstract

LensFixity AbstractName Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Pretty AbstractName Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

HasRange AbstractName Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

SetRange AbstractName Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

InScope AbstractName Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

SetBindingSite AbstractName Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

ToConcrete AbstractName Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs AbstractName 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

PrettyTCM AbstractName Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

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 #

NFData AbstractName Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

rnf :: AbstractName -> ()

Generic AbstractName Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Associated Types

type Rep AbstractName 
Instance details

Defined in Agda.Syntax.Scope.Base

type Rep AbstractName = D1 ('MetaData "AbstractName" "Agda.Syntax.Scope.Base" "Agda-2.6.20240714-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))))
Show AbstractName Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

showsPrec :: Int -> AbstractName -> ShowS

show :: AbstractName -> String

showList :: [AbstractName] -> ShowS

Eq AbstractName Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

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

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

Ord AbstractName Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

type ConOfAbs AbstractName Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type Rep AbstractName Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

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

data NameMetadata Source #

Instances

Instances details
EmbPrj NameMetadata Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: NameMetadata -> S Int32 Source #

icod_ :: NameMetadata -> S Int32 Source #

value :: Int32 -> R NameMetadata Source #

NFData NameMetadata Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

rnf :: NameMetadata -> ()

Generic NameMetadata Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Associated Types

type Rep NameMetadata 
Instance details

Defined in Agda.Syntax.Scope.Base

type Rep NameMetadata = D1 ('MetaData "NameMetadata" "Agda.Syntax.Scope.Base" "Agda-2.6.20240714-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))))
Show NameMetadata Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

showsPrec :: Int -> NameMetadata -> ShowS

show :: NameMetadata -> String

showList :: [NameMetadata] -> ShowS

type Rep NameMetadata Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

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

data AbstractModule Source #

A decoration of abstract syntax module names.

Constructors

AbsModule 

Fields

Instances

Instances details
Pretty AbstractModule Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

InScope AbstractModule Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

SetBindingSite AbstractModule Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

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 #

NFData AbstractModule Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

rnf :: AbstractModule -> ()

Generic AbstractModule Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Associated Types

type Rep AbstractModule 
Instance details

Defined in Agda.Syntax.Scope.Base

type Rep AbstractModule = D1 ('MetaData "AbstractModule" "Agda.Syntax.Scope.Base" "Agda-2.6.20240714-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)))
Show AbstractModule Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

showsPrec :: Int -> AbstractModule -> ShowS

show :: AbstractModule -> String

showList :: [AbstractModule] -> ShowS

Eq AbstractModule Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Ord AbstractModule Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

type Rep AbstractModule Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

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

data ResolvedName Source #

Constructors

VarName

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

Fields

DefinedName

Function, data/record type, postulate.

FieldName

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

Fields

ConstructorName

Data or record constructor name.

Fields

PatternSynResName

Name of pattern synonym.

Fields

UnknownName

Unbound name.

Instances

Instances details
NameToExpr ResolvedName Source #

Turn a ResolvedName into an expression.

Assumes name is not UnknownName.

Instance details

Defined in Agda.Syntax.Abstract

Pretty ResolvedName Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

ToConcrete ResolvedName Source #

Assumes name is not UnknownName.

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs ResolvedName 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

NFData ResolvedName Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

rnf :: ResolvedName -> ()

Generic ResolvedName Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Associated Types

type Rep ResolvedName 
Instance details

Defined in Agda.Syntax.Scope.Base

type Rep ResolvedName = D1 ('MetaData "ResolvedName" "Agda.Syntax.Scope.Base" "Agda-2.6.20240714-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))))
Show ResolvedName Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

showsPrec :: Int -> ResolvedName -> ShowS

show :: ResolvedName -> String

showList :: [ResolvedName] -> ShowS

Eq ResolvedName Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

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

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

type ConOfAbs ResolvedName Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type Rep ResolvedName Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

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

data AmbiguousNameReason Source #

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

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

Constructors

AmbiguousLocalVar LocalVar (List1 AbstractName)

The name resolves both to a local variable and some declared names.

AmbiguousDeclName (List2 AbstractName)

The name resolves to at least 2 declared names.

Instances

Instances details
NFData AmbiguousNameReason Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

rnf :: AmbiguousNameReason -> ()

Generic AmbiguousNameReason Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Associated Types

type Rep AmbiguousNameReason 
Instance details

Defined in Agda.Syntax.Scope.Base

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

Defined in Agda.Syntax.Scope.Base

Methods

showsPrec :: Int -> AmbiguousNameReason -> ShowS

show :: AmbiguousNameReason -> String

showList :: [AmbiguousNameReason] -> ShowS

type Rep AmbiguousNameReason Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

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

data WhyInScopeData Source #

Constructors

WhyInScopeData 

Fields

  • QName

    The name x this explanation is about.

  • FilePath

    The directory in which the current module resides.

  • (Maybe LocalVar)

    The local variable that x could denote, if any.

  • [AbstractName]

    The defined names that x could denote.

  • [AbstractModule]

    The modules that x could denote.

Operations on name and module maps.

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.

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

Map monadic function over a namespace.

General operations on scopes

emptyScope :: Scope Source #

The empty scope.

emptyScopeInfo :: ScopeInfo Source #

The empty scope info.

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

Map functions over the names and modules in a scope.

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

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

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

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

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

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

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

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

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

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

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

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

recomputeInScopeSets :: Scope -> Scope Source #

Recompute the inScope sets of a scope.

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

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

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

Return all names in a scope.

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

Look up a single name in the current scope.

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

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

Returns the scope's non-private names.

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

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

mergeScopes :: [Scope] -> Scope Source #

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

Specific operations on scopes

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

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

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

Update a particular name space.

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

Modify a particular name space.

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

Add a name to a scope.

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

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

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

Add a module to a scope.

data UsingOrHiding Source #

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

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

Apply an ImportDirective to a scope:

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

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

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

applyImportDirective_ Source #

Arguments

:: ImportDirective 
-> Scope 
-> (Scope, (Set Name, Set Name))

Merged scope, clashing names, clashing module names.

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

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

Rename the abstract names in a scope.

restrictPrivate :: Scope -> Scope Source #

Remove private name space of a scope.

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

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

Remove private things from the given module from a scope.

withoutPrivates :: ScopeInfo -> ScopeInfo Source #

Filter privates out of a ScopeInfo

disallowGeneralizedVars :: Scope -> Scope Source #

Disallow using generalized variables from the scope

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

Add an explanation to why things are in scope.

publicModules :: ScopeInfo -> Map ModuleName Scope Source #

Get the public parts of the public modules of a scope

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

Inverse look-up

data AllowAmbiguousNames Source #

Constructors

AmbiguousAnything

Used for instance arguments to check whether a name is in scope, but we do not care whether is is ambiguous

AmbiguousConProjs

Ambiguous constructors, projections, or pattern synonyms.

AmbiguousNothing 

Instances

Instances details
Eq AllowAmbiguousNames Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

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

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

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

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

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

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

Update binding site

class SetBindingSite a where Source #

Set the nameBindingSite in an abstract name.

Minimal complete definition

Nothing

Methods

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

default setBindingSite :: forall b (t :: Type -> Type). (SetBindingSite b, Functor t, t b ~ a) => Range -> a -> a Source #

Instances

Instances details
SetBindingSite ModuleName Source #

Sets the binding site of all names in the path.

Instance details

Defined in Agda.Syntax.Scope.Base

SetBindingSite Name Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

SetBindingSite QName Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

SetBindingSite AbstractModule Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

SetBindingSite AbstractName Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

SetBindingSite a => SetBindingSite (List1 a) Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

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

SetBindingSite a => SetBindingSite [a] Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

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

(Debug) printing

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

Add first string only if list is non-empty.

Boring instances

Orphan instances

Pretty Suffix Source # 
Instance details