Agda.Syntax.Concrete.Name

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

Documentation

data 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.

Fields

• nameRange :: Range
• nameInScope :: NameInScope
• nameNameParts :: NameParts

NoName

_.

Fields

• nameRange :: Range
• nameId :: NameId

Instances

SubstExpr Name

Defined in Agda.Syntax.Abstract

Methods

substExpr :: [(Name, Expr)] -> Name -> Name

Underscore Name

Defined in Agda.Syntax.Concrete.Name

Methods

underscore :: Name

isUnderscore :: Name -> Bool

Pretty Name

Defined in Agda.Syntax.Concrete.Name

Methods

pretty :: Name -> Doc

prettyPrec :: Int -> Name -> Doc

prettyList :: [Name] -> Doc

ExprLike Name

Defined in Agda.Syntax.Concrete.Generic

Methods

mapExpr :: (Expr -> Expr) -> Name -> Name

foldExpr :: Monoid m => (Expr -> m) -> Name -> m

traverseExpr :: Monad m => (Expr -> m Expr) -> Name -> m Name

IsNoName Name

Defined in Agda.Syntax.Concrete.Name

Methods

isNoName :: Name -> Bool

LensInScope Name

Defined in Agda.Syntax.Concrete.Name

Methods

lensInScope :: Lens' Name NameInScope

isInScope :: Name -> NameInScope

mapInScope :: (NameInScope -> NameInScope) -> Name -> Name

setInScope :: Name -> Name

setNotInScope :: Name -> Name

NumHoles Name

Defined in Agda.Syntax.Concrete.Name

Methods

numHoles :: Name -> Int

HasRange AsName

Defined in Agda.Syntax.Concrete

Methods

getRange :: AsName -> Range

HasRange Name

Defined in Agda.Syntax.Concrete.Name

Methods

getRange :: Name -> Range

KillRange AsName

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT AsName

KillRange Name

Defined in Agda.Syntax.Concrete.Name

Methods

killRange :: KillRangeT Name

SetRange Name

Defined in Agda.Syntax.Concrete.Name

Methods

setRange :: Range -> Name -> Name

ToAbstract HoleContent

Content of interaction hole.

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon HoleContent

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon HoleContent = HoleContent

Methods

toAbstract :: HoleContent -> ScopeM (AbsOfCon HoleContent)

ToAbstract RewriteEqn

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon RewriteEqn

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon RewriteEqn = RewriteEqn' () BindName Pattern Expr

Methods

toAbstract :: RewriteEqn -> ScopeM (AbsOfCon RewriteEqn)

PrettyTCM Name

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Name -> m Doc

EmbPrj Name

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Name -> S Int32

icod_ :: Name -> S Int32

value :: Int32 -> R Name

Show Name

Defined in Agda.Syntax.Concrete.Name

Methods

showsPrec :: Int -> Name -> ShowS

show :: Name -> String

showList :: [Name] -> ShowS

NFData AsName

Ranges are not forced.

Defined in Agda.Syntax.Concrete

Methods

rnf :: AsName -> ()

NFData Name

Ranges are not forced.

Defined in Agda.Syntax.Concrete.Name

Methods

rnf :: Name -> ()

Eq 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

Defined in Agda.Syntax.Concrete.Name

Methods

(==) :: Name -> Name -> Bool

(/=) :: Name -> Name -> Bool

Ord Name

Defined in Agda.Syntax.Concrete.Name

Methods

compare :: Name -> Name -> Ordering

(<) :: Name -> Name -> Bool

(<=) :: Name -> Name -> Bool

(>) :: Name -> Name -> Bool

(>=) :: Name -> Name -> Bool

max :: Name -> Name -> Name

min :: Name -> Name -> Name

Pretty (ThingWithFixity Name)

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: ThingWithFixity Name -> Doc

prettyPrec :: Int -> ThingWithFixity Name -> Doc

prettyList :: [ThingWithFixity Name] -> Doc

ToAbstract (NewName Name)

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (NewName Name)

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon (NewName Name) = Name

Methods

toAbstract :: NewName Name -> ScopeM (AbsOfCon (NewName Name))

type AbsOfCon HoleContent

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon HoleContent = HoleContent

type AbsOfCon RewriteEqn

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon RewriteEqn = RewriteEqn' () BindName Pattern Expr

type AbsOfCon (NewName Name)

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon (NewName Name) = Name

type NameParts = List1 NamePart

isOpenMixfix :: 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

data NamePart

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

Constructors

Hole

_ part.

Id RawName

Identifier part.

Instances

Pretty NamePart

Defined in Agda.Syntax.Concrete.Name

Methods

pretty :: NamePart -> Doc

prettyPrec :: Int -> NamePart -> Doc

prettyList :: [NamePart] -> Doc

NumHoles NameParts

Defined in Agda.Syntax.Concrete.Name

Methods

numHoles :: NameParts -> Int

EmbPrj NamePart

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: NamePart -> S Int32

icod_ :: NamePart -> S Int32

value :: Int32 -> R NamePart

Generic NamePart

Defined in Agda.Syntax.Concrete.Name

Associated Types

type Rep NamePart

Defined in Agda.Syntax.Concrete.Name

type Rep NamePart = D1 ('MetaData "NamePart" "Agda.Syntax.Concrete.Name" "Agda-2.6.4.2-inplace" 'False) (C1 ('MetaCons "Hole" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Id" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RawName)))

Methods

from :: NamePart -> Rep NamePart x

to :: Rep NamePart x -> NamePart

Show NamePart

Defined in Agda.Syntax.Concrete.Name

Methods

showsPrec :: Int -> NamePart -> ShowS

show :: NamePart -> String

showList :: [NamePart] -> ShowS

NFData NamePart

Defined in Agda.Syntax.Concrete.Name

Methods

rnf :: NamePart -> ()

Eq NamePart

Defined in Agda.Syntax.Concrete.Name

Methods

(==) :: NamePart -> NamePart -> Bool

(/=) :: NamePart -> NamePart -> Bool

Ord NamePart

Defined in Agda.Syntax.Concrete.Name

Methods

compare :: NamePart -> NamePart -> Ordering

(<) :: NamePart -> NamePart -> Bool

(<=) :: NamePart -> NamePart -> Bool

(>) :: NamePart -> NamePart -> Bool

(>=) :: NamePart -> NamePart -> Bool

max :: NamePart -> NamePart -> NamePart

min :: NamePart -> NamePart -> NamePart

type Rep NamePart

Defined in Agda.Syntax.Concrete.Name

type Rep NamePart = D1 ('MetaData "NamePart" "Agda.Syntax.Concrete.Name" "Agda-2.6.4.2-inplace" 'False) (C1 ('MetaCons "Hole" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Id" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RawName)))

data 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.

Instances

Underscore QName

Defined in Agda.Syntax.Concrete.Name

Methods

underscore :: QName

isUnderscore :: QName -> Bool

Pretty QName

Defined in Agda.Syntax.Concrete.Name

Methods

pretty :: QName -> Doc

prettyPrec :: Int -> QName -> Doc

prettyList :: [QName] -> Doc

ExprLike QName

Defined in Agda.Syntax.Concrete.Generic

Methods

mapExpr :: (Expr -> Expr) -> QName -> QName

foldExpr :: Monoid m => (Expr -> m) -> QName -> m

traverseExpr :: Monad m => (Expr -> m Expr) -> QName -> m QName

IsNoName QName

Defined in Agda.Syntax.Concrete.Name

Methods

isNoName :: QName -> Bool

LensInScope QName

Defined in Agda.Syntax.Concrete.Name

Methods

lensInScope :: Lens' QName NameInScope

isInScope :: QName -> NameInScope

mapInScope :: (NameInScope -> NameInScope) -> QName -> QName

setInScope :: QName -> QName

setNotInScope :: QName -> QName

NumHoles QName

Defined in Agda.Syntax.Concrete.Name

Methods

numHoles :: QName -> Int

HasRange QName

Defined in Agda.Syntax.Concrete.Name

Methods

getRange :: QName -> Range

KillRange QName

Defined in Agda.Syntax.Concrete.Name

Methods

killRange :: KillRangeT QName

SetRange QName

Defined in Agda.Syntax.Concrete.Name

Methods

setRange :: Range -> QName -> QName

PrettyTCM QName

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => QName -> m Doc

EmbPrj QName

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: QName -> S Int32

icod_ :: QName -> S Int32

value :: Int32 -> R QName

Show QName

Defined in Agda.Syntax.Concrete.Name

Methods

showsPrec :: Int -> QName -> ShowS

show :: QName -> String

showList :: [QName] -> ShowS

NFData QName

Defined in Agda.Syntax.Concrete.Name

Methods

rnf :: QName -> ()

Eq QName

Defined in Agda.Syntax.Concrete.Name

Methods

(==) :: QName -> QName -> Bool

(/=) :: QName -> QName -> Bool

Ord QName

Defined in Agda.Syntax.Concrete.Name

Methods

compare :: QName -> QName -> Ordering

(<) :: QName -> QName -> Bool

(<=) :: QName -> QName -> Bool

(>) :: QName -> QName -> Bool

(>=) :: QName -> QName -> Bool

max :: QName -> QName -> QName

min :: QName -> QName -> QName

Constructing simple Names.

simpleName :: RawName -> Name

Create an ordinary InScope name.

simpleBinaryOperator :: RawName -> Name

Create a binary operator name in scope.

simpleHole :: Name

Create an ordinary InScope name containing a single Hole.

Operations on Name and NamePart

lensNameParts :: Lens' Name NameParts

Don't use on 'NoName{}'.

nameToRawName :: Name -> RawName

nameParts :: Name -> NameParts

nameStringParts :: Name -> [RawName]

stringNameParts :: String -> NameParts

Parse a string to parts of a concrete name.

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

class NumHoles a where

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

Methods

numHoles :: a -> Int

Instances

NumHoles AmbiguousQName

We can have an instance for ambiguous names as all share a common concrete name.

Defined in Agda.Syntax.Abstract.Name

Methods

numHoles :: AmbiguousQName -> Int

NumHoles Name

Defined in Agda.Syntax.Abstract.Name

Methods

numHoles :: Name -> Int

NumHoles QName

Defined in Agda.Syntax.Abstract.Name

Methods

numHoles :: QName -> Int

NumHoles Name

Defined in Agda.Syntax.Concrete.Name

Methods

numHoles :: Name -> Int

NumHoles NameParts

Defined in Agda.Syntax.Concrete.Name

Methods

numHoles :: NameParts -> Int

NumHoles QName

Defined in Agda.Syntax.Concrete.Name

Methods

numHoles :: QName -> Int

isOperator :: Name -> Bool

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

isHole :: NamePart -> Bool

isPrefix :: Name -> Bool

isPostfix :: Name -> Bool

isInfix :: Name -> Bool

isNonfix :: Name -> Bool

Keeping track of which names are (not) in scope

data NameInScope

Constructors

InScope

NotInScope

Instances

EncodeTCM NameInScope

Defined in Agda.Interaction.JSONTop

Methods

encodeTCM :: NameInScope -> TCM Value

LensInScope NameInScope

Defined in Agda.Syntax.Concrete.Name

Methods

lensInScope :: Lens' NameInScope NameInScope

isInScope :: NameInScope -> NameInScope

mapInScope :: (NameInScope -> NameInScope) -> NameInScope -> NameInScope

setInScope :: NameInScope -> NameInScope

setNotInScope :: NameInScope -> NameInScope

EmbPrj NameInScope

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: NameInScope -> S Int32

icod_ :: NameInScope -> S Int32

value :: Int32 -> R NameInScope

Show NameInScope

Defined in Agda.Syntax.Concrete.Name

Methods

showsPrec :: Int -> NameInScope -> ShowS

show :: NameInScope -> String

showList :: [NameInScope] -> ShowS

NFData NameInScope

Defined in Agda.Syntax.Concrete.Name

Methods

rnf :: NameInScope -> ()

Eq NameInScope

Defined in Agda.Syntax.Concrete.Name

Methods

(==) :: NameInScope -> NameInScope -> Bool

(/=) :: NameInScope -> NameInScope -> Bool

ToJSON NameInScope

Defined in Agda.Interaction.JSONTop

Methods

toJSON :: NameInScope -> Value

toEncoding :: NameInScope -> Encoding

toJSONList :: [NameInScope] -> Value

toEncodingList :: [NameInScope] -> Encoding

omitField :: NameInScope -> Bool

class LensInScope a where

Minimal complete definition

lensInScope

Methods

lensInScope :: Lens' a NameInScope

isInScope :: a -> NameInScope

mapInScope :: (NameInScope -> NameInScope) -> a -> a

setInScope :: a -> a

setNotInScope :: a -> a

Instances

LensInScope Name

Defined in Agda.Syntax.Abstract.Name

Methods

lensInScope :: Lens' Name NameInScope

isInScope :: Name -> NameInScope

mapInScope :: (NameInScope -> NameInScope) -> Name -> Name

setInScope :: Name -> Name

setNotInScope :: Name -> Name

LensInScope QName

Defined in Agda.Syntax.Abstract.Name

Methods

lensInScope :: Lens' QName NameInScope

isInScope :: QName -> NameInScope

mapInScope :: (NameInScope -> NameInScope) -> QName -> QName

setInScope :: QName -> QName

setNotInScope :: QName -> QName

LensInScope Name

Defined in Agda.Syntax.Concrete.Name

Methods

lensInScope :: Lens' Name NameInScope

isInScope :: Name -> NameInScope

mapInScope :: (NameInScope -> NameInScope) -> Name -> Name

setInScope :: Name -> Name

setNotInScope :: Name -> Name

LensInScope NameInScope

Defined in Agda.Syntax.Concrete.Name

Methods

lensInScope :: Lens' NameInScope NameInScope

isInScope :: NameInScope -> NameInScope

mapInScope :: (NameInScope -> NameInScope) -> NameInScope -> NameInScope

setInScope :: NameInScope -> NameInScope

setNotInScope :: NameInScope -> NameInScope

LensInScope QName

Defined in Agda.Syntax.Concrete.Name

Methods

lensInScope :: Lens' QName NameInScope

isInScope :: QName -> NameInScope

mapInScope :: (NameInScope -> NameInScope) -> QName -> QName

setInScope :: QName -> QName

setNotInScope :: QName -> QName

Generating fresh names

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

nextRawName :: FreshNameMode -> RawName -> RawName

nextName :: FreshNameMode -> Name -> Name

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

lastIdPart :: Lens' NameParts RawName

Zoom on the last non-hole in a name.

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

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

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

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

Split a name into a base name plus a suffix.

setNameSuffix :: Maybe Suffix -> Name -> Name

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

nameRoot :: Name -> RawName

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

sameRoot :: Name -> Name -> Bool

Operations on qualified names

lensQNameName :: Lens' QName Name

Lens for the unqualified part of a QName

qualify :: QName -> Name -> QName

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

unqualify :: QName -> Name

unqualify A.B.x == x

The range is preserved.

qnameParts :: QName -> List1 Name

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

isQualified :: QName -> Bool

Is the name (un)qualified?

isUnqualified :: QName -> Maybe Name

No name stuff

noName_ :: Name

noName_ = noName noRange

noName :: Range -> Name

class IsNoName a where

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

Minimal complete definition

Nothing

Methods

isNoName :: a -> Bool

default isNoName :: forall (t :: Type -> Type) b. (Foldable t, IsNoName b, t b ~ a) => a -> Bool

Instances

IsNoName Name

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

Defined in Agda.Syntax.Abstract.Name

Methods

isNoName :: Name -> Bool

IsNoName Name

Defined in Agda.Syntax.Concrete.Name

Methods

isNoName :: Name -> Bool

IsNoName QName

Defined in Agda.Syntax.Concrete.Name

Methods

isNoName :: QName -> Bool

IsNoName RawTopLevelModuleName

Defined in Agda.Syntax.TopLevelModuleName

Methods

isNoName :: RawTopLevelModuleName -> Bool

IsNoName ByteString

Defined in Agda.Syntax.Concrete.Name

Methods

isNoName :: ByteString -> Bool

IsNoName String

Defined in Agda.Syntax.Concrete.Name

Methods

isNoName :: String -> Bool

IsNoName a => IsNoName (Ranged a)

Defined in Agda.Syntax.Concrete.Name

Methods

isNoName :: Ranged a -> Bool

IsNoName a => IsNoName (WithOrigin a)

Defined in Agda.Syntax.Concrete.Name

Methods

isNoName :: WithOrigin a -> Bool

Showing names

Printing names

Range instances

NFData instances