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 DataOrRecord

Instances

Eq Scope

Methods

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

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

Data Scope

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

Methods

showsPrec :: Int -> Scope -> ShowS

show :: Scope -> String

showList :: [Scope] -> ShowS

Pretty Scope

Methods

pretty :: Scope -> Doc

prettyPrec :: Int -> Scope -> Doc

prettyList :: [Scope] -> Doc

InstantiateFull Scope

Methods

instantiateFull' :: Scope -> ReduceM Scope

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.

OnlyQualifiedNS

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

Instances

Bounded NameSpaceId

Methods

minBound :: NameSpaceId

maxBound :: NameSpaceId

Enum NameSpaceId

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]

Eq NameSpaceId

Methods

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

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

Data NameSpaceId

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

Methods

showsPrec :: Int -> NameSpaceId -> ShowS

show :: NameSpaceId -> String

showList :: [NameSpaceId] -> ShowS

Pretty NameSpaceId

Methods

pretty :: NameSpaceId -> Doc

prettyPrec :: Int -> NameSpaceId -> Doc

prettyList :: [NameSpaceId] -> Doc

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
• scopeLocals :: LocalVars
• scopePrecedence :: PrecedenceStack
• scopeInverseName :: Map QName [QName]
• scopeInverseModule :: Map ModuleName [QName]
• scopeInScope :: InScopeSet

Instances

Eq ScopeInfo

Methods

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

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

Data ScopeInfo

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

Methods

showsPrec :: Int -> ScopeInfo -> ShowS

show :: ScopeInfo -> String

showList :: [ScopeInfo] -> ShowS

Pretty ScopeInfo

Methods

pretty :: ScopeInfo -> Doc

prettyPrec :: Int -> ScopeInfo -> Doc

prettyList :: [ScopeInfo] -> Doc

KillRange ScopeInfo

Methods

killRange :: KillRangeT ScopeInfo

type LocalVars = AssocList Name LocalVar

Local variables.

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.

• localLetBound :: Bool

  Flag whether the variable is introduced by a let.

• localShadowedBy :: [AbstractName]

  If this list is not empty, the local variable is shadowed by one or more imports.

Instances

Eq LocalVar

Methods

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

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

Data LocalVar

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

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

Methods

showsPrec :: Int -> LocalVar -> ShowS

show :: LocalVar -> String

showList :: [LocalVar] -> ShowS

Pretty LocalVar

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

Methods

pretty :: LocalVar -> Doc

prettyPrec :: Int -> LocalVar -> Doc

prettyList :: [LocalVar] -> Doc

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

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

notShadowedLocal :: LocalVar -> Maybe Name

Project name of unshadowed local variable.

notShadowedLocals :: LocalVars -> AssocList Name Name

Get all locals that are not shadowed by imports.

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

Lens for scopeLocals.

setScopeLocals :: LocalVars -> ScopeInfo -> ScopeInfo

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

Instances

Eq NameSpace

Methods

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

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

Data NameSpace

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

Methods

showsPrec :: Int -> NameSpace -> ShowS

show :: NameSpace -> String

showList :: [NameSpace] -> ShowS

Pretty NameSpace

Methods

pretty :: NameSpace -> Doc

prettyPrec :: Int -> NameSpace -> Doc

prettyList :: [NameSpace] -> Doc

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 Eq a => InScope a where

Type class for some dependent-types trickery.

Minimal complete definition

inScopeTag

Methods

inScopeTag :: InScopeTag a

Instances

InScope AbstractModule

Methods

inScopeTag :: InScopeTag AbstractModule

InScope AbstractName

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).

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.

FldName

Record field name.

DefName

Ordinary defined name.

PatternSynName

Name of a pattern synonym.

MacroName

Name of a macro

QuotableName

A name that can only be quoted.

Instances

Bounded KindOfName

Methods

minBound :: KindOfName

maxBound :: KindOfName

Enum KindOfName

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]

Eq KindOfName

Methods

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

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

Data KindOfName

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

Methods

showsPrec :: Int -> KindOfName -> ShowS

show :: KindOfName -> String

showList :: [KindOfName] -> ShowS

allKindsOfNames :: [KindOfName]

A list containing all name kinds.

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

Data WhyInScope

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

Methods

showsPrec :: Int -> WhyInScope -> ShowS

show :: WhyInScope -> String

showList :: [WhyInScope] -> ShowS

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.

Instances

Eq AbstractName

Methods

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

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

Data AbstractName

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

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

Show AbstractName

Methods

showsPrec :: Int -> AbstractName -> ShowS

show :: AbstractName -> String

showList :: [AbstractName] -> ShowS

Pretty AbstractName

Methods

pretty :: AbstractName -> Doc

prettyPrec :: Int -> AbstractName -> Doc

prettyList :: [AbstractName] -> Doc

SetRange AbstractName

Methods

setRange :: Range -> AbstractName -> AbstractName

HasRange AbstractName

Methods

getRange :: AbstractName -> Range

InScope AbstractName

Methods

inScopeTag :: InScopeTag AbstractName

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

Eq AbstractModule

Methods

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

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

Data AbstractModule

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

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

Show AbstractModule

Methods

showsPrec :: Int -> AbstractModule -> ShowS

show :: AbstractModule -> String

showList :: [AbstractModule] -> ShowS

Pretty AbstractModule

Methods

pretty :: AbstractModule -> Doc

prettyPrec :: Int -> AbstractModule -> Doc

prettyList :: [AbstractModule] -> Doc

InScope AbstractModule

Methods

inScopeTag :: InScopeTag AbstractModule

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

Van Laarhoven lens on anameName.

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

Van Laarhoven lens on amodName.

Operations on name and module maps.

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

mapScope' :: 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.

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

Add names to a scope.

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.

type UsingOrHiding = Either Using [ImportedName]

usingOrHiding :: ImportDirective -> UsingOrHiding

applyImportDirective :: ImportDirective -> Scope -> Scope

Apply an ImportDirective to a scope.

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.

removeOnlyQualified :: Scope -> Scope

Remove names that can only be used qualified (when opening a 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

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 or projections.

AmbiguousNothing

Instances

Eq AllowAmbiguousNames

Methods

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

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

isNameInScope :: QName -> ScopeInfo -> Bool

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

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

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

recomputeInverseScopeMaps :: ScopeInfo -> ScopeInfo

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

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

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

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

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

(Debug) printing

prettyNameSpace :: NameSpace -> [Doc]

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

Add first string only if list is non-empty.

Boring instances