Agda.Syntax.Abstract.Name
Description
Abstract names should carry unique identifiers and stuff. Not right now though.
- data Name = Name {}
- data QName = QName {}
- newtype ModuleName = MName {
- mnameToList :: [Name]
- newtype AmbiguousQName = AmbQ {}
- 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
- qnameToMName :: QName -> ModuleName
- showQNameId :: QName -> String
- 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
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 | |
Fields
|
data QName
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 | |
Fields
|
newtype ModuleName
A module name is just a qualified name.
The SetRange
instance for module names sets all individual ranges
to the given one.
Constructors
MName | |
Fields
|
Instances
newtype AmbiguousQName
Ambiguous qualified names. Used for overloaded constructors.
Invariant: All the names in the list must have the same concrete, unqualified name.
withRangesOf :: ModuleName -> [Name] -> ModuleName
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
returns withRangesOf
[A, B]C.D.E
but with ranges set
as follows:
-
C
:noRange
. -
D
: the range ofA
. -
E
: the range ofB
.
Precondition: The number of module name name parts has to be at least as large as the length of the list.
withRangesOfQ :: ModuleName -> QName -> ModuleName
Like withRangesOf
, but uses the name parts (qualifier + name)
of the qualified name as the list of concrete names.
mnameFromList :: [Name] -> ModuleName
mkName :: Range -> NameId -> String -> Name
The Range
sets the definition site of the name, not the use
site.
qnameToList :: QName -> [Name]
qnameFromList :: [Name] -> QName
qnameToMName :: QName -> ModuleName
showQNameId :: QName -> String
qnameToConcrete :: QName -> QName
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 -> QName
toTopLevelModuleName :: ModuleName -> TopLevelModuleName
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 -> ModuleName
qualifyQ :: ModuleName -> QName -> QName
qualify :: ModuleName -> Name -> QName
isOperator :: QName -> Bool
Is the name an operator?
isSubModuleOf :: ModuleName -> ModuleName -> Bool
isInModule :: QName -> ModuleName -> Bool
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