Agda-2.5.2: 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 #

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

Instances

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.

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.

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

Unique ID of local variable.

Fields

ShadowedVar

This local variable is shadowed by one or more imports. (List not empty).

Instances

Eq LocalVar # 
Ord LocalVar # 
Show LocalVar #

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

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.

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

type ThingsInScope a = Map Name [a] #

data InScopeTag a where #

Set of types consisting of exactly AbstractName and AbstractModule.

A GADT just for some dependent-types trickery.

class Eq a => InScope a where #

Type class for some dependent-types trickery.

Minimal complete definition

inScopeTag

Methods

inScopeTag :: InScopeTag a #

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.

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.

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.

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.

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.

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

Returns the scope's non-private names.

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.

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

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 

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

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

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

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

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

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

(Debug) printing

blockOfLines :: String -> [String] -> [String] #

Add first string only if list is non-empty.

Boring instances