ModuleAgda-2.7.0.1Haskell2010

Agda.Syntax.Concrete.Name

Names in the concrete syntax are just strings (or lists of strings for qualified names).

6 types
3 classes
32 values

PackageAgda-2.7.0.1
Exports41
LanguageHaskell2010
LicenceMIT
SourceName.hs

datadata Name

A name is a non-empty list of alternating Ids and Holes. A normal name is represented by a singleton list, and operators are represented by a list with Holes where the arguments should go. For instance: [Hole,Id "+",Hole] is infix addition.

Equality and ordering on Names are defined to ignore range so same names in different locations are equal.

Constructors

Name
A (mixfix) identifier.
- nameRange :: Range
- nameInScope :: NameInScope
- nameNameParts :: NameParts
NoName
_.
- nameRange :: Range
- nameId :: NameId

Instances27Eq, Ord, Show, NFData, IsNoName, HasRange, …

Eq NameDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Name
Define equality on Name to ignore range so same names in different locations are equal.
Is there a reason not to do this? -Jeff
No. But there are tons of reasons to do it. For instance, when using names as keys in maps you really don't want to have to get the range right to be able to do a lookup. -Ulf
Ord NameDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Name
Show NameDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Name
NFData AsNameDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete
Ranges are not forced.
NFData NameDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Name
Ranges are not forced.
Pretty NameDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Name
IsNoName NameDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Name
HasRange AsNameDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete
HasRange NameDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Name
PrettyTCM NameDefined in Agda-2.7.0.1 · Agda.TypeChecking.Pretty
SubstExpr NameDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract
KillRange AsNameDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete
KillRange NameDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Name
SetRange NameDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Name
Underscore NameDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Name
LensInScope NameDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Name
NumHoles NameDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Name
ExprLike NameDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Generic
ToAbstract HoleContentDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
Content of interaction hole.
ToAbstract RewriteEqnDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
ToQName NameDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
EmbPrj NameDefined in Agda-2.7.0.1 · Agda.TypeChecking.Serialise.Instances.Common · orphan
Pretty (ThingWithFixity Name)Defined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Pretty · orphan
ToAbstract (NewName Name)Defined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
type AbsOfCon HoleContent = HoleContentDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
type AbsOfCon RewriteEqn = RewriteEqn' () BindName Pattern ExprDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
type AbsOfCon (NewName Name) = NameDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract

typetype NameParts = List1 NamePart

valueisOpenMixfix :: Name -> Bool

An open mixfix identifier is either prefix, infix, or suffix. That is to say: at least one of its extremities is a Hole

datadata NamePart

Mixfix identifiers are composed of words and holes, e.g. _+_ or if_then_else_ or [_/_].

Constructors

Hole
_ part.
Id RawName
Identifier part.

Instances9Eq, Ord, Show, Generic, NFData, Pretty, …

Eq NamePartDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Name
Ord NamePartDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Name
Show NamePartDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Name
Generic NamePartDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Name
NFData NamePartDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Name
Pretty NamePartDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Name
NumHoles NamePartsDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Name
EmbPrj NamePartDefined in Agda-2.7.0.1 · Agda.TypeChecking.Serialise.Instances.Common · orphan
type Rep NamePart = D1 ('MetaData "NamePart" "Agda.Syntax.Concrete.Name" "Agda-2.7.0.1-DbbZpETDDF1KkwuzEZvfn8" 'False) (C1 ('MetaCons "Hole" 'PrefixI 'False) U1 :+: C1 ('MetaCons "Id" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RawName)))Defined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Name

datadata QName

QName is a list of namespaces and the name of the constant. For the moment assumes namespaces are just Names and not explicitly applied modules. Also assumes namespaces are generative by just using derived equality. We will have to define an equality instance to non-generative namespaces (as well as having some sort of lookup table for namespace names).

Constructors

Qual Name QName
A.rest.
QName Name
x.

Instances16Eq, Ord, Show, NFData, Pretty, IsNoName, …

Eq QNameDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Name
Ord QNameDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Name
Show QNameDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Name
NFData QNameDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Name
Pretty QNameDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Name
IsNoName QNameDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Name
HasRange QNameDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Name
PrettyTCM QNameDefined in Agda-2.7.0.1 · Agda.TypeChecking.Pretty
KillRange QNameDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Name
SetRange QNameDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Name
Underscore QNameDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Name
LensInScope QNameDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Name
NumHoles QNameDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Name
ExprLike QNameDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Generic
ToQName QNameDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
EmbPrj QNameDefined in Agda-2.7.0.1 · Agda.TypeChecking.Serialise.Instances.Common · orphan

Constructing simple Names.

3 declarations

valuesimpleName :: RawName -> Name

Create an ordinary InScope name.

valuesimpleBinaryOperator :: RawName -> Name

Create a binary operator name in scope.

valuesimpleHole :: Name

Create an ordinary InScope name containing a single Hole.

Operations on Name and NamePart

12 declarations

valuelensNameParts :: Lens' Name NameParts

Don't use on 'NoName{}'.

valuenameToRawName :: Name -> RawName

valuenameParts :: Name -> NameParts

valuenameStringParts :: Name -> [RawName]

valuestringNameParts :: String -> NameParts

Parse a string to parts of a concrete name.

Note: stringNameParts "_" == [Id "_"] == nameParts NoName{}

classclass NumHoles a where

Number of holes in a Name (i.e., arity of a mixfix-operator).

Methods

numHoles :: a -> Int

Instances6NumHoles

NumHoles AmbiguousQNameDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Name
We can have an instance for ambiguous names as all share a common concrete name.
NumHoles NameDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Name
NumHoles QNameDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Name
NumHoles NameDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Name
NumHoles NamePartsDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Name
NumHoles QNameDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Name

valueisOperator :: Name -> Bool

Is the name an operator? Needs at least 2 NameParts.

valueisHole :: NamePart -> Bool

valueisPrefix :: Name -> Bool

valueisPostfix :: Name -> Bool

valueisInfix :: Name -> Bool

valueisNonfix :: Name -> Bool

Keeping track of which names are (not) in scope

2 declarations

datadata NameInScope

InScope NotInScope

Instances7Eq, Show, NFData, ToJSON, EncodeTCM, LensInScope, …

Eq NameInScopeDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Name
Show NameInScopeDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Name
NFData NameInScopeDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Name
ToJSON NameInScopeDefined in Agda-2.7.0.1 · Agda.Interaction.JSONTop · orphan
EncodeTCM NameInScopeDefined in Agda-2.7.0.1 · Agda.Interaction.JSONTop · orphan
LensInScope NameInScopeDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Name
EmbPrj NameInScopeDefined in Agda-2.7.0.1 · Agda.TypeChecking.Serialise.Instances.Common · orphan

classclass LensInScope a where

Methods

lensInScope :: Lens' a NameInScope
isInScope :: a -> NameInScope
mapInScope :: (NameInScope -> NameInScope) -> a -> a
setInScope :: a -> a
setNotInScope :: a -> a

Instances5LensInScope

LensInScope NameDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Name
LensInScope QNameDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Name
LensInScope NameDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Name
LensInScope NameInScopeDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Name
LensInScope QNameDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Name

Generating fresh names

10 declarations

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, …

valuenextRawName :: FreshNameMode -> RawName -> RawName

valuenextName :: FreshNameMode -> Name -> Name

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

valuelastIdPart :: Lens' NameParts RawName

Zoom on the last non-hole in a name.

valuefirstNonTakenName :: FreshNameMode -> (Name -> Bool) -> Name -> Name

Get the first version of the concrete name that does not satisfy the given predicate.

valuenameSuffix :: Lens' Name (Maybe Suffix)

Lens for accessing and modifying the suffix of a name. The suffix of a NoName is always Nothing, and should not be changed.

valuenameSuffixView :: Name -> (Maybe Suffix, Name)

Split a name into a base name plus a suffix.

valuesetNameSuffix :: Maybe Suffix -> Name -> Name

Replaces the suffix of a name. Unless the suffix is Nothing, the name should not be NoName.

valuenameRoot :: Name -> RawName

Get a raw version of the name with all suffixes removed. For instance, nameRoot "x₁₂₃" = "x".

valuesameRoot :: Name -> Name -> Bool

Operations on qualified names

6 declarations

valuelensQNameName :: Lens' QName Name

Lens for the unqualified part of a QName

valuequalify :: QName -> Name -> QName

qualify A.B x == A.B.x

valueunqualify :: QName -> Name

unqualify A.B.x == x

The range is preserved.

valueqnameParts :: QName -> List1 Name

qnameParts A.B.x = [A, B, x]

valueisQualified :: QName -> Bool

Is the name (un)qualified?

valueisUnqualified :: QName -> Maybe Name

No name stuff

3 declarations

valuenoName_ :: Name

noName_ = noName noRange

valuenoName :: Range -> Name

classclass IsNoName a where

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

Methods

isNoName :: a -> Bool

Instances8IsNoName, …

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

Showing names

0 declarations

Printing names

0 declarations

Range instances

0 declarations

NFData instances

0 declarations