Agda.Syntax.Abstract.Name

Abstract names carry unique identifiers and stuff.

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

nameId :: NameId

nameConcrete :: Name

nameBindingSite :: Range

nameFixity :: Fixity'

Instances

Eq Name

Ord Name

Show Name

Only use this show function in debugging! To convert an abstract Name into a string use prettyShow.

Hashable Name

Pretty Name

KillRange Name

SetRange Name

HasRange Name

IsNoName Name

An abstract name is empty if its concrete name is empty.

Subst Name

AddContext Name

PrettyTCM Name

EmbPrj Name

InstantiateFull Name

Typeable * Name

ToConcrete Name Name

Reify Name Name

AddContext (Dom (Name, Type))

ToAbstract (NewName Name) Name

ToAbstract (NewName BoundName) Name

(Free i, Reify i a) => Reify (Abs i) (Name, a)

AddContext ([Name], Dom Type)

AddContext (Name, Dom Type)

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

qnameModule :: ModuleName

qnameName :: Name

Instances

Eq QName

Ord QName

Show QName

Only use this show function in debugging! To convert an abstract QName into a string use prettyShow.

Hashable QName

Pretty QName

KillRange QName

KillRange Definitions

SetRange QName

HasRange QName

Sized QName

AllNames QName

TermLike QName

PrettyTCM QName

EmbPrj QName

InstantiateFull QName

Occurs QName

Unquote QName

FromTerm QName

ToTerm QName

PrimTerm QName

Typeable * QName

UniverseBi Declaration QName

ShrinkC DefName QName

ToConcrete QName QName

ToAbstract OldName QName

ToConcrete (Maybe QName) (Maybe Name)

data QNamed a

Something preceeded by a qualified name.

Constructors

QNamed

Fields

qname :: QName

qnamed :: a

Instances

Functor QNamed

Foldable QNamed

Traversable QNamed

PrettyTCM NamedClause

Reify NamedClause Clause

Show a => Show (QNamed a)

Typeable (* -> *) QNamed

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

mnameToList :: [Name]

Instances

Eq ModuleName

Ord ModuleName

Show ModuleName

Only use this show function in debugging! To convert an abstract ModuleName into a string use prettyShow.

Pretty ModuleName

KillRange ModuleName

KillRange Sections

SetRange ModuleName

HasRange ModuleName

Sized ModuleName

PrettyTCM ModuleName

EmbPrj ModuleName

InstantiateFull ModuleName

Typeable * ModuleName

UniverseBi Declaration ModuleName

ToConcrete ModuleName QName

ToAbstract OldModuleName ModuleName

ToAbstract NewModuleQName ModuleName

ToAbstract NewModuleName ModuleName

newtype AmbiguousQName

Ambiguous qualified names. Used for overloaded constructors.

Invariant: All the names in the list must have the same concrete, unqualified name. (This implies that they all have the same Range).

Constructors

AmbQ

Fields

unAmbQ :: [QName]

Instances

Eq AmbiguousQName

Show AmbiguousQName

KillRange AmbiguousQName

HasRange AmbiguousQName

The range of an AmbiguousQName is the range of any of its disambiguations (they are the same concrete name).

EmbPrj AmbiguousQName

Typeable * AmbiguousQName

UniverseBi Declaration AmbiguousQName

isAnonymousModuleName :: ModuleName -> Bool

A module is anonymous if the qualification path ends in an underscore.

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

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

mnameFromList :: [Name] -> ModuleName

noModuleName :: ModuleName

class MkName a where

Make a Name from some kind of string.

Minimal complete definition

mkName

Methods

mkName :: Range -> NameId -> a -> Name

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

mkName_ :: NameId -> a -> Name

Instances

MkName String

qnameToList :: QName -> [Name]

qnameFromList :: [Name] -> QName

qnameToMName :: QName -> ModuleName

mnameToQName :: ModuleName -> QName

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

qualify_ :: Name -> QName

Convert a Name to a QName (add no module name).

isOperator :: QName -> Bool

Is the name an operator?

isSubModuleOf :: ModuleName -> ModuleName -> Bool

isInModule :: QName -> ModuleName -> Bool

nextName :: Name -> Name

Get the next version of the concrete name. For instance, nextName "x" = "x₁". The name must not be a NoName.

Important instances: Eq, Ord, Hashable

IsNoName instances (checking for "_")

Show instances

Pretty instances

Range instances

HasRange

SetRange

KillRange

Sized instances

class IsNoName a where

Check whether a name is the empty name "_".

Methods

isNoName :: a -> Bool

Instances

IsNoName String

IsNoName ByteString

IsNoName QName

IsNoName Name

IsNoName Name

An abstract name is empty if its concrete name is empty.