ModuleAgda-2.8.0.2Haskell2010

Agda.Syntax.Concrete.Name

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

Contents

Constructing simple Names.
Operations on Name and NamePart
Keeping track of which names are (not) in scope
Generating fresh names
Operations on qualified names
No name stuff
Showing names
Printing names
Range instances
NFData instances

Synopsis

data Name
type NameParts
value isOpenMixfix
data NamePart
data QName
value simpleName
value simpleBinaryOperator
value simpleHole
value lensNameParts
value nameToRawName
value nameParts
value nameStringParts
value stringNameParts
class NumHoles
value isOperator
value isHole
value isPrefix
value isPostfix
value isInfix
value isNonfix
data NameInScope
class LensInScope
data FreshNameMode
value nextRawName
value nextName
value lastIdPart
value firstNonTakenName
value nameSuffix
value nameSuffixView
value setNameSuffix
value nameRoot
value sameRoot
value lensQNameName
value qualify
value unqualify
value qnameParts
value isQualified
value isUnqualified
value noName_
value noName
class IsNoName

PackageAgda-2.8.0.2
Exports41
LanguageHaskell2010
LicenceMIT
SourceName.hs

datadata Name

Source#

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

Instances28Eq, Ord, Show, NFData, IsNoName, HasRange, …

Eq NameDefined in Agda-2.8.0.2 · 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.8.0.2 · Agda.Syntax.Concrete.Name
Show NameDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Name
NFData AsNameDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete
Ranges are not forced.
NFData NameDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Name
Ranges are not forced.
Pretty NameDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Name
IsNoName NameDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Name
HasRange AsNameDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete
HasRange NameDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Name
PrettyTCM ImportedNameDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM NameDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
ToAbstract HoleContentDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
Content of interaction hole.
ToAbstract RewriteEqnDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
SubstExpr NameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract
KillRange AsNameDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete
KillRange NameDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Name
SetRange NameDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Name
Underscore NameDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Name
LensInScope NameDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Name
NumHoles NameDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Name
ExprLike NameDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Generic
ToQName NameDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
EmbPrj NameDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan
Pretty (ThingWithFixity Name)Defined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Pretty · orphan
ToAbstract (NewName Name)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
type AbsOfCon HoleContent = HoleContentDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
type AbsOfCon RewriteEqn = RewriteEqn' () BindName Pattern ExprDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
type AbsOfCon (NewName Name) = NameDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract

typetype NameParts = List1 NamePart

valueisOpenMixfix :: Name -> Bool

Source#

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

Source#

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.8.0.2 · Agda.Syntax.Concrete.Name
Ord NamePartDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Name
Show NamePartDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Name
Generic NamePartDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Name
NFData NamePartDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Name
Pretty NamePartDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Name
NumHoles NamePartsDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Name
EmbPrj NamePartDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan
type Rep NamePart = D1 ('MetaData "NamePart" "Agda.Syntax.Concrete.Name" "Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP" 'False) (C1 ('MetaCons "Hole" 'PrefixI 'False) U1 :+: C1 ('MetaCons "Id" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RawName)))Defined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Name

datadata QName

Source#

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.8.0.2 · Agda.Syntax.Concrete.Name
Ord QNameDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Name
Show QNameDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Name
NFData QNameDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Name
Pretty QNameDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Name
IsNoName QNameDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Name
HasRange QNameDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Name
PrettyTCM QNameDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
KillRange QNameDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Name
SetRange QNameDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Name
Underscore QNameDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Name
LensInScope QNameDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Name
NumHoles QNameDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Name
ExprLike QNameDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Generic
ToQName QNameDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
EmbPrj QNameDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan

Constructing simple Names.

valuesimpleName :: RawName -> Name

Source#

Create an ordinary InScope name.

valuesimpleBinaryOperator :: RawName -> Name

Source#

Create a binary operator name in scope.

valuesimpleHole :: Name

Source#

Create an ordinary InScope name containing a single Hole.

Operations on Name and NamePart

valuelensNameParts :: Lens' Name NameParts

Source#

Don't use on 'NoName{}'.

valuenameToRawName :: Name -> RawName

valuenameParts :: Name -> NameParts

valuenameStringParts :: Name -> [RawName]

valuestringNameParts :: String -> NameParts

Source#

Parse a string to parts of a concrete name.

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

classclass NumHoles a where

Source#

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

Methods

numHoles :: a -> Int

Instances6NumHoles

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.
NumHoles NameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
NumHoles QNameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
NumHoles NameDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Name
NumHoles NamePartsDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Name
NumHoles QNameDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Name

valueisOperator :: Name -> Bool

Source#

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

datadata NameInScope

InScope NotInScope

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

Eq NameInScopeDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Name
Show NameInScopeDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Name
NFData NameInScopeDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Name
ToJSON NameInScopeDefined in Agda-2.8.0.2 · Agda.Interaction.JSONTop · orphan
EncodeTCM NameInScopeDefined in Agda-2.8.0.2 · Agda.Interaction.JSONTop · orphan
LensInScope NameInScopeDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Name
EmbPrj NameInScopeDefined in Agda-2.8.0.2 · 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.8.0.2 · Agda.Syntax.Abstract.Name
LensInScope QNameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
LensInScope NameDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Name
LensInScope NameInScopeDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Name
LensInScope QNameDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Name

Generating fresh names

datadata FreshNameMode

Source#

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

Source#

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

valuelastIdPart :: Lens' NameParts RawName

Source#

Zoom on the last non-hole in a name.

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

Source#

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

valuenameSuffix :: Lens' Name (Maybe Suffix)

Source#

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)

Source#

Split a name into a base name plus a suffix.

valuesetNameSuffix :: Maybe Suffix -> Name -> Name

Source#

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

valuenameRoot :: Name -> RawName

Source#

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

valuesameRoot :: Name -> Name -> Bool

Operations on qualified names

valuelensQNameName :: Lens' QName Name

Source#

Lens for the unqualified part of a QName

valuequalify :: QName -> Name -> QName

Source#

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

valueunqualify :: QName -> Name

Source#

unqualify A.B.x == x

The range is preserved.

valueqnameParts :: QName -> List1 Name

Source#

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

valueisQualified :: QName -> Bool

Source#

Is the name (un)qualified?

valueisUnqualified :: QName -> Maybe Name

No name stuff

valuenoName_ :: Name

Source#

noName_ = noName noRange

valuenoName :: Range -> Name

classclass IsNoName a where

Source#

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

Constructors

Constructors

Constructors

Constructing simple Names.

Operations on Name and NamePart

Methods

Keeping track of which names are (not) in scope

Methods

Generating fresh names

Constructors

Operations on qualified names

No name stuff

Methods

Showing names

Printing names

Range instances

NFData instances