Agda-2.6.3.20230805: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.Syntax.Concrete.Name

Description

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

Synopsis

Documentation

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

NoName

_.

Fields

Instances

Instances details
SubstExpr Name Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

substExpr :: [(Name0, Expr)] -> Name -> Name Source #

Underscore Name Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Pretty Name Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

ExprLike Name Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

IsNoName Name Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

isNoName :: Name -> Bool Source #

LensInScope Name Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

NumHoles Name Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

numHoles :: Name -> Int Source #

HasRange AsName Source # 
Instance details

Defined in Agda.Syntax.Concrete

HasRange Name Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

getRange :: Name -> Range Source #

KillRange AsName Source # 
Instance details

Defined in Agda.Syntax.Concrete

KillRange Name Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

SetRange Name Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

setRange :: Range -> Name -> Name Source #

ToAbstract HoleContent Source #

Content of interaction hole.

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon HoleContent Source #

ToAbstract RewriteEqn Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon RewriteEqn Source #

PrettyTCM Name Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

EmbPrj Name Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Show Name Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

showsPrec :: Int -> Name -> ShowS #

show :: Name -> String #

showList :: [Name] -> ShowS #

NFData AsName Source #

Ranges are not forced.

Instance details

Defined in Agda.Syntax.Concrete

Methods

rnf :: AsName -> () #

NFData Name Source #

Ranges are not forced.

Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

rnf :: Name -> () #

Eq Name Source #

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

Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

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

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

Ord Name Source # 
Instance details

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) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

ToAbstract (NewName Name) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (NewName Name) Source #

type AbsOfCon HoleContent Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon RewriteEqn Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon (NewName Name) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

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

data NamePart Source #

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

Constructors

Hole

_ part.

Id RawName

Identifier part.

Instances

Instances details
Pretty NamePart Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

NumHoles NameParts Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

EmbPrj NamePart Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Generic NamePart Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Associated Types

type Rep NamePart :: Type -> Type #

Methods

from :: NamePart -> Rep NamePart x #

to :: Rep NamePart x -> NamePart #

Show NamePart Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

NFData NamePart Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

rnf :: NamePart -> () #

Eq NamePart Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Ord NamePart Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

type Rep NamePart Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

type Rep NamePart = D1 ('MetaData "NamePart" "Agda.Syntax.Concrete.Name" "Agda-2.6.3.20230805-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 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.

Instances

Instances details
Underscore QName Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Pretty QName Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

ExprLike QName Source # 
Instance details

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

IsNoName QName Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

isNoName :: QName -> Bool Source #

LensInScope QName Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

NumHoles QName Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

numHoles :: QName -> Int Source #

HasRange QName Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

getRange :: QName -> Range Source #

KillRange QName Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

SetRange QName Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

setRange :: Range -> QName -> QName Source #

PrettyTCM QName Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

EmbPrj QName Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Show QName Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

showsPrec :: Int -> QName -> ShowS #

show :: QName -> String #

showList :: [QName] -> ShowS #

NFData QName Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

rnf :: QName -> () #

Eq QName Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

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

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

Ord QName Source # 
Instance details

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 Source #

Create an ordinary InScope name.

simpleBinaryOperator :: RawName -> Name Source #

Create a binary operator name in scope.

simpleHole :: Name Source #

Create an ordinary InScope name containing a single Hole.

Operations on Name and NamePart

lensNameParts :: Lens' Name NameParts Source #

Don't use on 'NoName{}'.

stringNameParts :: String -> NameParts Source #

Parse a string to parts of a concrete name.

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

class NumHoles a where Source #

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

Methods

numHoles :: a -> Int Source #

Instances

Instances details
NumHoles AmbiguousQName Source #

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

Instance details

Defined in Agda.Syntax.Abstract.Name

NumHoles Name Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

numHoles :: Name -> Int Source #

NumHoles QName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

numHoles :: QName -> Int Source #

NumHoles Name Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

numHoles :: Name -> Int Source #

NumHoles NameParts Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

NumHoles QName Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

numHoles :: QName -> Int Source #

isOperator :: Name -> Bool Source #

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

Keeping track of which names are (not) in scope

data NameInScope Source #

Constructors

InScope 
NotInScope 

Instances

Instances details
EncodeTCM NameInScope Source # 
Instance details

Defined in Agda.Interaction.JSONTop

LensInScope NameInScope Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

EmbPrj NameInScope Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Show NameInScope Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

NFData NameInScope Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

rnf :: NameInScope -> () #

Eq NameInScope Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

ToJSON NameInScope Source # 
Instance details

Defined in Agda.Interaction.JSONTop

class LensInScope a where Source #

Minimal complete definition

lensInScope

Instances

Instances details
LensInScope Name Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

LensInScope QName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

LensInScope Name Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

LensInScope NameInScope Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

LensInScope QName Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Generating fresh names

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

nextName :: FreshNameMode -> Name -> Name Source #

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

lastIdPart :: Lens' NameParts RawName Source #

Zoom on the last non-hole in a name.

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

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

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

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

Split a name into a base name plus a suffix.

setNameSuffix :: Maybe Suffix -> Name -> Name Source #

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

nameRoot :: Name -> RawName Source #

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

Operations on qualified names

lensQNameName :: Lens' QName Name Source #

Lens for the unqualified part of a QName

qualify :: QName -> Name -> QName Source #

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

unqualify :: QName -> Name Source #

unqualify A.B.x == x

The range is preserved.

qnameParts :: QName -> List1 Name Source #

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

isQualified :: QName -> Bool Source #

Is the name (un)qualified?

No name stuff

class IsNoName a where Source #

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

Minimal complete definition

Nothing

Methods

isNoName :: a -> Bool Source #

default isNoName :: (Foldable t, IsNoName b, t b ~ a) => a -> Bool Source #

Instances

Instances details
IsNoName Name Source #

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

Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

isNoName :: Name -> Bool Source #

IsNoName Name Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

isNoName :: Name -> Bool Source #

IsNoName QName Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

isNoName :: QName -> Bool Source #

IsNoName RawTopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName

IsNoName ByteString Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

IsNoName String Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

isNoName :: String -> Bool Source #

IsNoName a => IsNoName (Ranged a) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

isNoName :: Ranged a -> Bool Source #

IsNoName a => IsNoName (WithOrigin a) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Showing names

Printing names

Range instances

NFData instances