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

Safe HaskellNone
LanguageHaskell2010

Agda.Syntax.Scope.Base

Contents

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
Eq Scope Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

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

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

Data Scope Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

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

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 :: (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

Show Scope Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

showsPrec :: Int -> Scope -> ShowS

show :: Scope -> String

showList :: [Scope] -> ShowS

Pretty Scope Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

EmbPrj Scope Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: Scope -> S Int32 Source #

icod_ :: Scope -> S Int32 Source #

value :: Int32 -> R Scope Source #

InstantiateFull Scope Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

data NameSpaceId Source #

See Access.

Constructors

PrivateNS

Things not exported by this module.

PublicNS

Things defined and exported by this module.

ImportedNS

Things from open public, exported by this module.

OnlyQualifiedNS

Visible (as qualified) from outside, but not exported when opening the module. Used for qualified constructors.

Instances
Bounded NameSpaceId Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Enum NameSpaceId Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Eq NameSpaceId Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

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

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

Data NameSpaceId Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

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

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 :: (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

Show NameSpaceId Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

showsPrec :: Int -> NameSpaceId -> ShowS

show :: NameSpaceId -> String

showList :: [NameSpaceId] -> ShowS

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 #

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.

Instances
Eq ScopeInfo Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

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

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

Data ScopeInfo Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

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

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 :: (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

Show ScopeInfo Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

showsPrec :: Int -> ScopeInfo -> ShowS

show :: ScopeInfo -> String

showList :: [ScopeInfo] -> ShowS

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 #

type LocalVars = AssocList Name LocalVar Source #

Local variables.

data Binder Source #

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

Constructors

LambdaBound

λ (currently also used for Π and module parameters)

PatternBound
f ... =
LetBound
let ... in
Instances
Eq Binder Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

(==) :: Binder -> Binder -> Bool

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

Data Binder Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

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

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

toConstr :: Binder -> Constr

dataTypeOf :: Binder -> DataType

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

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

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

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

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

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

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

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

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

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

Show Binder Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

showsPrec :: Int -> Binder -> ShowS

show :: Binder -> String

showList :: [Binder] -> ShowS

EmbPrj Binder Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: Binder -> S Int32 Source #

icod_ :: Binder -> S Int32 Source #

value :: Int32 -> R Binder Source #

data LocalVar Source #

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

Constructors

LocalVar 

Fields

Instances
Eq LocalVar Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

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

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

Data LocalVar Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

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

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 :: (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

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

Show LocalVar Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

showsPrec :: Int -> LocalVar -> ShowS

show :: LocalVar -> String

showList :: [LocalVar] -> ShowS

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 #

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

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

patternToModuleBound :: LocalVar -> LocalVar Source #

Treat patternBound variable as a module parameter

notShadowedLocal :: LocalVar -> Maybe Name Source #

Project name of unshadowed local variable.

notShadowedLocals :: LocalVars -> AssocList Name Name Source #

Get all locals that are not shadowed by imports.

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
Eq NameSpace Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

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

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

Data NameSpace Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

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

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 :: (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

Show NameSpace Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

showsPrec :: Int -> NameSpace -> ShowS

show :: NameSpace -> String

showList :: [NameSpace] -> ShowS

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 #

type ThingsInScope a = Map Name [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 Eq a => InScope a where Source #

Type class for some dependent-types trickery.

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

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

Decorated names

data KindOfName Source #

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

Constructors

ConName

Constructor name.

FldName

Record field name.

DefName

Ordinary defined name.

PatternSynName

Name of a pattern synonym.

GeneralizeName

Name to be generalized

DisallowedGeneralizeName

Generalizable variable from a let open

MacroName

Name of a macro

QuotableName

A name that can only be quoted.

Instances
Bounded KindOfName Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Enum KindOfName Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Eq KindOfName Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

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

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

Data KindOfName Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

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

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 :: (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

Show KindOfName Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

showsPrec :: Int -> KindOfName -> ShowS

show :: KindOfName -> String

showList :: [KindOfName] -> ShowS

EmbPrj KindOfName Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: KindOfName -> S Int32 Source #

icod_ :: KindOfName -> S Int32 Source #

value :: Int32 -> R KindOfName Source #

allKindsOfNames :: [KindOfName] Source #

A list containing all name kinds.

data WhyInScope Source #

Where does a name come from?

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

Constructors

Defined

Defined in this module.

Opened QName WhyInScope

Imported from another module.

Applied QName WhyInScope

Imported by a module application.

Instances
Data WhyInScope Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

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

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 :: (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

Show WhyInScope Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

showsPrec :: Int -> WhyInScope -> ShowS

show :: WhyInScope -> String

showList :: [WhyInScope] -> ShowS

EmbPrj WhyInScope Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: WhyInScope -> S Int32 Source #

icod_ :: WhyInScope -> S Int32 Source #

value :: Int32 -> R WhyInScope Source #

data AbstractName Source #

A decoration of QName.

Constructors

AbsName 

Fields

Instances
Eq AbstractName Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

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

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

Data AbstractName Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

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

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 :: (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

Ord AbstractName Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Show AbstractName Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

showsPrec :: Int -> AbstractName -> ShowS

show :: AbstractName -> String

showList :: [AbstractName] -> ShowS

Pretty AbstractName Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

SetRange AbstractName Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

HasRange AbstractName Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

InScope AbstractName Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

NameToExpr AbstractName Source #

Turn an AbstractName to an expression.

Instance details

Defined in Agda.Syntax.Abstract

EmbPrj AbstractName Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: AbstractName -> S Int32 Source #

icod_ :: AbstractName -> S Int32 Source #

value :: Int32 -> R AbstractName Source #

ToConcrete AbstractName QName Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

data NameMetadata Source #

Instances
Data NameMetadata Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

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

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 :: (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

Show NameMetadata Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

showsPrec :: Int -> NameMetadata -> ShowS

show :: NameMetadata -> String

showList :: [NameMetadata] -> ShowS

EmbPrj NameMetadata Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: NameMetadata -> S Int32 Source #

icod_ :: NameMetadata -> S Int32 Source #

value :: Int32 -> R NameMetadata Source #

data AbstractModule Source #

A decoration of abstract syntax module names.

Constructors

AbsModule 

Fields

Instances
Eq AbstractModule Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Data AbstractModule Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

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

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 :: (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

Ord AbstractModule Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Show AbstractModule Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

showsPrec :: Int -> AbstractModule -> ShowS

show :: AbstractModule -> String

showList :: [AbstractModule] -> ShowS

Pretty AbstractModule Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

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

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

Van Laarhoven lens on anameName.

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

Van Laarhoven lens on amodName.

data ResolvedName Source #

Constructors

VarName

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

Fields

DefinedName Access AbstractName

Function, data/record type, postulate.

FieldName (NonemptyList AbstractName)

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

ConstructorName (NonemptyList AbstractName)

Data or record constructor name.

PatternSynResName (NonemptyList AbstractName)

Name of pattern synonym.

UnknownName

Unbound name.

Instances
Eq ResolvedName Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

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

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

Data ResolvedName Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

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

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 :: (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

Show ResolvedName Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

showsPrec :: Int -> ResolvedName -> ShowS

show :: ResolvedName -> String

showList :: [ResolvedName] -> ShowS

Pretty ResolvedName Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

NameToExpr ResolvedName Source #

Assumes name is not UnknownName.

Instance details

Defined in Agda.Syntax.Abstract

ToConcrete ResolvedName QName Source #

Assumes name is not UnknownName.

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

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.

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

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

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

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

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

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

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

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

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

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

recomputeInScopeSets :: Scope -> Scope Source #

Recompute the inScope sets of a scope.

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

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

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

Return all names in a scope.

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.

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

Add names to a scope.

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

Add a name to a scope.

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

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

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

Add a module to a scope.

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

Rename the abstract names in a scope.

restrictPrivate :: Scope -> Scope Source #

Remove private name space of a scope.

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

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

Remove private things from the given module from a scope.

removeOnlyQualified :: Scope -> Scope Source #

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

disallowGeneralizedVars :: Scope -> Scope Source #

Disallow using generalized variables from the scope

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

Add an explanation to why things are in scope.

publicModules :: ScopeInfo -> Map ModuleName Scope Source #

Get the public parts of the public modules of a scope

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

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

concreteNamesInScope :: ScopeInfo -> Set QName Source #

Get all concrete names in scope. Includes bound variables.

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

Look up a name in the scope

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

Inverse look-up

data AllowAmbiguousNames Source #

Constructors

AmbiguousAnything

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

AmbiguousConProjs

Ambiguous constructors, projections, or pattern synonyms.

AmbiguousNothing 

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

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

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

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

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

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

(Debug) printing

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

Add first string only if list is non-empty.

Boring instances