ModuleAgda-2.8.0.2Haskell2010

Agda.Syntax.Abstract.Name

Abstract names carry unique identifiers and stuff.

7 types
3 classes
37 values

PackageAgda-2.8.0.2
Exports47
LanguageHaskell2010
LicenceMIT
SourceName.hs

valuecommonParentModule :: ModuleName -> ModuleName -> ModuleName

valuegetUnambiguous :: AmbiguousQName -> Maybe QName

Get the name if unambiguous.

valueheadAmbQ :: AmbiguousQName -> QName

Get the first of the ambiguous names.

valueisAmbiguous :: AmbiguousQName -> Bool

Is a name ambiguous.

valueisAnonymousModuleName :: ModuleName -> Bool

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

valueisInModule :: QName -> ModuleName -> Bool

valueisLeChildModuleOf :: ModuleName -> ModuleName -> Bool

Is the first module a weak child of the second?

valueisLeParentModuleOf :: ModuleName -> ModuleName -> Bool

Is the first module a weak parent of the second?

valueisLtChildModuleOf :: ModuleName -> ModuleName -> Bool

Is the first module a proper child of the second?

valueisLtParentModuleOf :: ModuleName -> ModuleName -> Bool

Is the first module a proper parent of the second?

valueisOperator :: QName -> Bool

Is the name an operator?

valuelensQNameName :: Lens' QName Name

valuemakeName :: NameId -> Name -> Range -> Fixity' -> Bool -> Name

valuemnameFromList :: [Name] -> ModuleName

valuemnameFromList1 :: List1 Name -> ModuleName

valuemnameToConcrete :: ModuleName -> QName

valuemnameToList1 :: ModuleName -> List1 Name

valuemnameToQName :: ModuleName -> QName

valuenameToArgName :: Name -> ArgName

valuenamedArgName :: NamedArg Name -> ArgName

valuenextName :: FreshNameMode -> Name -> Name

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

valuenoModuleName :: ModuleName

valueqnameFromList :: List1 Name -> QName

valueqnameToConcrete :: 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.

valueqnameToList :: QName -> List1 Name

valueqnameToList0 :: QName -> [Name]

valueqnameToMName :: QName -> ModuleName

valuequalify :: ModuleName -> Name -> QName

valuequalifyM :: ModuleName -> ModuleName -> ModuleName

valuequalifyQ :: ModuleName -> QName -> QName

valuequalify_ :: Name -> QName

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

valuesameRoot :: Name -> Name -> Bool

valueshowQNameId :: QName -> String

valueuglyShowName :: Name -> String

Useful for debugging scoping problems

valueunambiguous :: QName -> AmbiguousQName

A singleton "ambiguous" name.

valuewithRangesOf :: ModuleName -> List1 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.

valuewithRangesOfQ :: ModuleName -> QName -> ModuleName

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

newtypenewtype 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
- unAmbQ :: List1 QName

Instances11Eq, Ord, Show, NFData, Pretty, HasRange, …

Eq AmbiguousQNameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
Ord AmbiguousQNameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
Show AmbiguousQNameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
NFData AmbiguousQNameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
Pretty AmbiguousQNameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
HasRange AmbiguousQNameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
The range of an AmbiguousQName is the range of any of its disambiguations (they are the same concrete name).
Hilite AmbiguousQNameDefined in Agda-2.8.0.2 · Agda.Interaction.Highlighting.FromAbstract
KillRange AmbiguousQNameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
NumHoles AmbiguousQNameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
We can have an instance for ambiguous names as all share a common concrete name.
NamesIn AmbiguousQNameDefined in Agda-2.8.0.2 · Agda.Syntax.Internal.Names
EmbPrj AmbiguousQNameDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan

classclass IsProjP a where

Check whether we are a projection pattern.

Methods

isProjP :: a -> Maybe (ProjOrigin, AmbiguousQName)

Instances6IsProjP

IsProjP ExprDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract
IsProjP VoidDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
IsProjP (Pattern' e)Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract
IsProjP (Pattern' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal
IsProjP a => IsProjP (Arg a)Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
IsProjP a => IsProjP (Named n a)Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name

classclass MkName a where

Make a Name from some kind of string.

Methods

mkName :: Range -> NameId -> a -> Name
The Range sets the definition site of the name, not the use site.
mkName_ :: NameId -> a -> Name

Instances1MkName

MkName StringDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name

newtypenewtype 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
- mnameToList :: [Name]

Instances24Eq, Ord, Show, NFData, Pretty, IsNoName, …

Eq ModuleNameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
Ord ModuleNameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
Show ModuleNameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
NFData ModuleNameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
Pretty ModuleNameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
IsNoName ModuleNameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
Null ModuleNameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
Sized ModuleNameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
HasRange ModuleNameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
PrettyTCM ModuleNameDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
ToConcrete ModuleNameDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
Hilite ModuleNameDefined in Agda-2.8.0.2 · Agda.Interaction.Highlighting.FromAbstract
BlankVars ModuleNameDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.InternalToAbstract
SubstExpr ModuleNameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract
KillRange ModuleNameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
KillRange SectionsDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
SetRange ModuleNameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
BoundAndUsed ModuleNameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.UsedNames
ExprLike ModuleNameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Views
SetBindingSite ModuleNameDefined in Agda-2.8.0.2 · Agda.Syntax.Scope.Base
Sets the binding site of all names in the path.
InstantiateFull ModuleNameDefined in Agda-2.8.0.2 · Agda.TypeChecking.Reduce
EmbPrj ModuleNameDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan
Hilite (RenamingTo ModuleName)Defined in Agda-2.8.0.2 · Agda.Interaction.Highlighting.FromAbstract
type ConOfAbs ModuleName = QNameDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete

datadata 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
- nameId :: !NameId
- nameConcrete :: Name
  The concrete name used for this instance
- nameCanonical :: Name
  The concrete name in the original definition (needed by primShowQName, see #4735)
- nameBindingSite :: Range
- nameFixity :: Fixity'
- nameIsRecordName :: Bool
  Is this the name of the invisible record variable self? Should not be printed or displayed in the context, see issue #3584.

Instances39Eq, Ord, Show, NFData, Hashable, Pretty, …

Eq NameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
Ord NameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
Show NameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
Use prettyShow to print names to the user.
NFData NameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
The range is not forced.
Hashable NameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
Pretty NameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
IsNoName NameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
An abstract name is empty if its concrete name is empty.
FreshName NameDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
AddContext NameDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Context
HasRange NameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
Subst NameDefined in Agda-2.8.0.2 · Agda.TypeChecking.Substitute · orphan
PrettyTCM NameDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
Reify NameDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.InternalToAbstract
ToConcrete NameDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
KillRange NameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
SetRange NameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
LensFixity' NameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
LensFixity NameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
LensInScope NameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
NumHoles NameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
Suggest NameDefined in Agda-2.8.0.2 · Agda.Syntax.Internal
SetBindingSite NameDefined in Agda-2.8.0.2 · Agda.Syntax.Scope.Base
InstantiateFull NameDefined in Agda-2.8.0.2 · Agda.TypeChecking.Reduce
EmbPrj NameDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan
AddContext (Dom (Name, Type))Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Context
AddContext (Name, Dom Type)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Context
AddContext (List1 Name, Dom Type)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Context
AddContext (List1 (Arg Name), Type)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Context
AddContext (List1 (NamedArg Name), Type)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Context
AddContext (List1 (WithHiding Name), Dom Type)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Context
AddContext ([Name], Dom Type)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Context
AddContext ([Arg Name], Type)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Context
AddContext ([NamedArg Name], Type)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Context
AddContext ([WithHiding Name], Dom Type)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Context
(ToAbstract r, AbsOfRef r ~ Expr) => ToAbstract (Dom r, Name)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.ReflectedToAbstract
type SubstArg Name = TermDefined in Agda-2.8.0.2 · Agda.TypeChecking.Substitute · orphan
type ConOfAbs Name = NameDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
type ReifiesTo Name = NameDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.InternalToAbstract
type AbsOfRef (Dom r, Name) = TypedBindingDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.ReflectedToAbstract

datadata 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
- qnameModule :: ModuleName
- qnameName :: Name

Instances40Eq, Ord, Show, NFData, Hashable, Pretty, …

Eq QNameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
Ord QNameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
Show QNameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
NFData QNameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
Hashable QNameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
Pretty QNameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
ChaseDisplayForms QNameDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Signature
Sized QNameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
HasRange QNameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
Subst QNameDefined in Agda-2.8.0.2 · Agda.TypeChecking.Substitute.Class
PrettyTCM QNameDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
ToConcrete QNameDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
Hilite QNameDefined in Agda-2.8.0.2 · Agda.Interaction.Highlighting.FromAbstract
DeclaredNames KNameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Views
KillRange QNameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
KillRange DefinitionsDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
KillRange RewriteRuleMapDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
SetRange QNameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
LensFixity' QNameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
LensFixity QNameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
LensInScope QNameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
NumHoles QNameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
ExprLike QNameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Views
TermLike QNameDefined in Agda-2.8.0.2 · Agda.Syntax.Internal.Generic
NamesIn QNameDefined in Agda-2.8.0.2 · Agda.Syntax.Internal.Names
SetBindingSite QNameDefined in Agda-2.8.0.2 · Agda.Syntax.Scope.Base
LivesInCurrentModule QNameDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
InstantiateFull QNameDefined in Agda-2.8.0.2 · Agda.TypeChecking.Reduce
Occurs QNameDefined in Agda-2.8.0.2 · Agda.TypeChecking.MetaVars.Occurs
FromTerm QNameDefined in Agda-2.8.0.2 · Agda.TypeChecking.Primitive
PrimTerm QNameDefined in Agda-2.8.0.2 · Agda.TypeChecking.Primitive
PrimType QNameDefined in Agda-2.8.0.2 · Agda.TypeChecking.Primitive
ToTerm QNameDefined in Agda-2.8.0.2 · Agda.TypeChecking.Primitive
EmbPrj QNameDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan
Unquote QNameDefined in Agda-2.8.0.2 · Agda.TypeChecking.Unquote
Singleton KName NameKindBuilderDefined in Agda-2.8.0.2 · Agda.Interaction.Highlighting.Generate
Collection KName NameKindBuilderDefined in Agda-2.8.0.2 · Agda.Interaction.Highlighting.Generate
Hilite (RenamingTo QName)Defined in Agda-2.8.0.2 · Agda.Interaction.Highlighting.FromAbstract
type SubstArg QName = TermDefined in Agda-2.8.0.2 · Agda.TypeChecking.Substitute.Class
type ConOfAbs QName = QNameDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete

datadata QNamed a

Something preceeded by a qualified name.

Constructors

QNamed
- qname :: QName
- qnamed :: a

Instances16Functor, Foldable, Traversable, Show, Pretty, PrettyTCM, …

Functor QNamedDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
Foldable QNamedDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
Traversable QNamedDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
Show a => Show (QNamed a)Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
Pretty a => Pretty (QNamed a)Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
PrettyTCM (QNamed Clause)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
Reify (QNamed Clause)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.InternalToAbstract
Reify (QNamed System)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.InternalToAbstract
ToAbstract (QNamed Clause)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.ReflectedToAbstract
ToAbstract (List1 (QNamed Clause))Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.ReflectedToAbstract
ToAbstract [QNamed Clause]Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.ReflectedToAbstract
type ReifiesTo (QNamed Clause) = ClauseDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.InternalToAbstract
type ReifiesTo (QNamed System) = [Clause]Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.InternalToAbstract
type AbsOfRef (QNamed Clause) = ClauseDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.ReflectedToAbstract
type AbsOfRef (List1 (QNamed Clause)) = List1 ClauseDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.ReflectedToAbstract
type AbsOfRef [QNamed Clause] = [Clause]Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.ReflectedToAbstract

datadata Suffix

A name suffix

Constructors

NoSuffix
Suffix !Integer

Instances8Eq, Ord, Show, NFData, Pretty, Null, …

Eq SuffixDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
Ord SuffixDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
Show SuffixDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
NFData SuffixDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
Pretty SuffixDefined in Agda-2.8.0.2 · Agda.Syntax.Scope.Base · orphan
Null SuffixDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
KillRange SuffixDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract · orphan
EmbPrj SuffixDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Abstract · orphan

classclass IsNoName a where

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

Methods

isNoName :: a -> Bool

Instances9IsNoName, …

IsNoName ModuleNameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
IsNoName NameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
An abstract name is empty if its concrete name is empty.
IsNoName NameDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Name
IsNoName QNameDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Name
IsNoName RawTopLevelModuleNameDefined in Agda-2.8.0.2 · Agda.Syntax.TopLevelModuleName
IsNoName ByteStringDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Name
IsNoName StringDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Name
IsNoName a => IsNoName (Ranged a)Defined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Name
IsNoName a => IsNoName (WithOrigin a)Defined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Name

datadata FreshNameMode

Method by which to generate fresh unshadowed names.

Constructors

UnicodeSubscript
Append an integer Unicode subscript: x, x₁, x₂, …
AsciiCounter
Append an integer ASCII counter: x, x1, x2, …