Agda-2.2.6: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.Syntax.Abstract.Name
Description
Abstract names should carry unique identifiers and stuff. Not right now though.
Synopsis
data Name = Name {
nameId :: NameId
nameConcrete :: Name
nameBindingSite :: Range
nameFixity :: Fixity
}
data QName = QName {
qnameModule :: ModuleName
qnameName :: Name
}
newtype ModuleName = MName {
mnameToList :: [Name]
}
newtype AmbiguousQName = AmbQ {
unAmbQ :: [QName]
}
withRangesOf :: ModuleName -> [Name] -> ModuleName
withRangesOfQ :: ModuleName -> QName -> ModuleName
mnameFromList :: [Name] -> ModuleName
noModuleName :: ModuleName
mkName :: Range -> NameId -> String -> Name
mkName_ :: NameId -> String -> Name
qnameToList :: QName -> [Name]
qnameFromList :: [Name] -> QName
qnameToConcrete :: QName -> QName
mnameToConcrete :: ModuleName -> QName
toTopLevelModuleName :: ModuleName -> TopLevelModuleName
qualifyM :: ModuleName -> ModuleName -> ModuleName
qualifyQ :: ModuleName -> QName -> QName
qualify :: ModuleName -> Name -> QName
isOperator :: QName -> Bool
isSubModuleOf :: ModuleName -> ModuleName -> Bool
isInModule :: QName -> ModuleName -> Bool
freshName :: (MonadState s m, HasFresh NameId s) => Range -> String -> m Name
freshName_ :: (MonadState s m, HasFresh NameId s) => String -> m Name
freshNoName :: (MonadState s m, HasFresh NameId s) => Range -> m Name
freshNoName_ :: (MonadState s m, HasFresh NameId s) => m Name
nextName :: Name -> Name
Documentation
data Name Source
A name is a unique identifier and a suggestion for a concrete name. The concrete name contains the source location (if any) of the name. The source location of the binding site is also recorded.
Constructors
Name
nameId :: NameId
nameConcrete :: Name
nameBindingSite :: Range
nameFixity :: Fixity
show/hide Instances
data QName Source

Qualified names are non-empty lists of names. Equality on qualified names are just equality on the last name, i.e. the module part is just for show.

The SetRange instance for qualified names sets all individual ranges (including those of the module prefix) to the given one.

Constructors
QName
qnameModule :: ModuleName
qnameName :: Name
show/hide Instances
newtype ModuleName Source

A module name is just a qualified name.

The SetRange instance for module names sets all individual ranges to the given one.

Constructors
MName
mnameToList :: [Name]
show/hide Instances
newtype AmbiguousQName Source

Ambiguous qualified names. Used for overloaded constructors.

Invariant: All the names in the list must have the same concrete, unqualified name.

Constructors
AmbQ
unAmbQ :: [QName]
show/hide Instances
withRangesOf :: ModuleName -> [Name] -> ModuleNameSource

Sets the ranges of the individual names in the module name to match those of the corresponding concrete names. If the concrete names are fewer than the number of module name name parts, then the initial name parts get the range noRange.

C.D.E withRangesOf [A, B] returns C.D.E but with ranges set as follows:

  • C: noRange.
  • D: the range of A.
  • E: the range of B.

Precondition: The number of module name name parts has to be at least as large as the length of the list.

withRangesOfQ :: ModuleName -> QName -> ModuleNameSource
Like withRangesOf, but uses the name parts (qualifier + name) of the qualified name as the list of concrete names.
mnameFromList :: [Name] -> ModuleNameSource
noModuleName :: ModuleNameSource
mkName :: Range -> NameId -> String -> NameSource
The Range sets the definition site of the name, not the use site.
mkName_ :: NameId -> String -> NameSource
qnameToList :: QName -> [Name]Source
qnameFromList :: [Name] -> QNameSource
qnameToConcrete :: QName -> QNameSource
Turn a qualified name into a concrete name. This should only be used as a fallback when looking up the right concrete name in the scope fails.
mnameToConcrete :: ModuleName -> QNameSource
toTopLevelModuleName :: ModuleName -> TopLevelModuleNameSource

Computes the TopLevelModuleName corresponding to the given module name, which is assumed to represent a top-level module name.

Precondition: The module name must be well-formed.

qualifyM :: ModuleName -> ModuleName -> ModuleNameSource
qualifyQ :: ModuleName -> QName -> QNameSource
qualify :: ModuleName -> Name -> QNameSource
isOperator :: QName -> BoolSource
Is the name an operator?
isSubModuleOf :: ModuleName -> ModuleName -> BoolSource
isInModule :: QName -> ModuleName -> BoolSource
freshName :: (MonadState s m, HasFresh NameId s) => Range -> String -> m NameSource
freshName_ :: (MonadState s m, HasFresh NameId s) => String -> m NameSource
freshNoName :: (MonadState s m, HasFresh NameId s) => Range -> m NameSource
freshNoName_ :: (MonadState s m, HasFresh NameId s) => m NameSource
nextName :: Name -> NameSource
Get the next version of the concrete name. For instance, nextName x = x'. The name must not be a NoName.
Produced by Haddock version 2.4.2