| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

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 |

Instances

Eq Name
Data Name
Ord Name
Show Name
Typeable Name
KillRange Name
SetRange Name
HasRange Name
EmbPrj Name
InstantiateFull Name
PrettyTCM Name
ShowAsOptimizedTerm Name
ShowAsUntypedTerm Name
ToConcrete Name Name
ToAbstract (NewName Name) Name
ToAbstract (NewName BoundName) Name

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 |

Instances

Eq QName
Data QName
Ord QName
Show QName
Typeable QName
Sized QName
KillRange QName
SetRange QName
HasRange QName
EmbPrj QName
PrettyTCM QName
ShowAsOptimizedTerm QName
ShowAsOptimizedType QName
ShowAsUntypedTerm QName
ToConcrete QName QName
ToAbstract OldName QName
ShrinkC ConName QName
ShrinkC DefName QName

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] |

Instances

Eq ModuleName
Data ModuleName
Ord ModuleName
Show ModuleName
Typeable ModuleName
Sized ModuleName
KillRange ModuleName
SetRange ModuleName
HasRange ModuleName
EmbPrj ModuleName
InstantiateFull ModuleName
PrettyTCM ModuleName
ToConcrete ModuleName QName
ToAbstract OldModuleName ModuleName
ToAbstract NewModuleQName ModuleName
ToAbstract NewModuleName ModuleName

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] |

Instances

Data AmbiguousQName
Show AmbiguousQName
Typeable AmbiguousQName
KillRange AmbiguousQName
HasRange AmbiguousQName

withRangesOf :: ModuleName -> [Name] -> ModuleName | Source

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 -> ModuleName | Source

Like `withRangesOf`, but uses the name parts (qualifier + name) of the qualified name as the list of concrete names.

mnameFromList :: [Name] -> ModuleName | Source

noModuleName :: ModuleName | Source

mkName :: Range -> NameId -> String -> Name | Source

The `Range` sets the definition site of the name, not the use site.

mkName_ :: NameId -> String -> Name | Source

qnameToList :: QName -> [Name] | Source

qnameFromList :: [Name] -> QName | Source

qnameToConcrete :: QName -> QName | Source

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 | Source

toTopLevelModuleName :: ModuleName -> TopLevelModuleName | Source

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 | Source

qualifyQ :: ModuleName -> QName -> QName | Source

qualify :: ModuleName -> Name -> QName | Source

isOperator :: QName -> Bool | Source

Is the name an operator?

isSubModuleOf :: ModuleName -> ModuleName -> Bool | Source

isInModule :: QName -> ModuleName -> Bool | Source

freshName :: (MonadState s m, HasFresh NameId s) => Range -> String -> m Name | Source

freshName_ :: (MonadState s m, HasFresh NameId s) => String -> m Name | Source

freshNoName :: (MonadState s m, HasFresh NameId s) => Range -> m Name | Source

freshNoName_ :: (MonadState s m, HasFresh NameId s) => m Name | Source

nextName :: Name -> Name | Source

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