Agda-2.3.2: A dependently typed functional programming language and proof assistant

Safe Haskell | None

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
  }
- data QNamed a = QNamed {
  - qname :: QName
  - qnamed :: a
  }
- newtype ModuleName = MName {
  - mnameToList :: [Name]
  }
- newtype AmbiguousQName = AmbQ {
  - unAmbQ :: [QName]
  }
- isAnonymousModuleName :: ModuleName -> Bool
- 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
- mnameToQName :: ModuleName -> QName
- 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 nameId :: NameId nameConcrete :: Name nameBindingSite :: Range nameFixity :: Fixity'

Instances

Eq Name |
Ord Name |
Show Name |
Typeable Name |
Hashable Name |
KillRange Name |
SetRange Name |
HasRange Name |
Alpha Name |
PrettyTCM Name |
InstantiateFull Name |
EmbPrj Name |
ToConcrete Name Name |
ToAbstract (NewName Name) Name |
ToAbstract (NewName BoundName) Name |
(Free i, Reify i a) => Reify (Abs i) (Name, a) |

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 |
Typeable QName |
Hashable QName |
Sized QName |
KillRange QName |
SetRange QName |
HasRange QName |
PrettyTCM QName |
InstantiateFull QName |
EmbPrj QName |
Occurs QName |
Unquote QName |
FromTerm QName |
ToTerm QName |
PrimTerm QName |
UniverseBi Declaration QName |
ToConcrete QName QName |
ToAbstract OldName QName |
ShrinkC ConName QName |
ShrinkC DefName 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 |
Typeable1 QNamed |
Foldable QNamed |
Traversable QNamed |
PrettyTCM NamedClause |
Reify NamedClause Clause |
Show a => Show (QNamed a) |

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 |
Typeable ModuleName |
Sized ModuleName |
KillRange ModuleName |
SetRange ModuleName |
HasRange ModuleName |
PrettyTCM ModuleName |
InstantiateFull ModuleName |
EmbPrj 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.

Constructors

AmbQ |
Fields unAmbQ :: [QName]

Instances

Eq AmbiguousQName |
Show AmbiguousQName |
Typeable AmbiguousQName |
KillRange AmbiguousQName |
HasRange AmbiguousQName |
EmbPrj 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

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

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

mkName_ :: NameId -> String -> Name

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

isOperator :: QName -> Bool

Is the name an operator?

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

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