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 Range [NamePart]

A (mixfix) identifier.

NoName Range NameId

_.

Instances

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

Data Name

Defined in Agda.Syntax.Concrete.Name

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Name -> c Name

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Name

toConstr :: Name -> Constr

dataTypeOf :: Name -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Name)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Name)

gmapT :: (forall b. Data b => b -> b) -> Name -> Name

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Name -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Name -> r

gmapQ :: (forall d. Data d => d -> u) -> Name -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Name -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Name -> m Name

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Name -> m Name

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Name -> m Name

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

Show Name

Defined in Agda.Syntax.Concrete.Name

Methods

showsPrec :: Int -> Name -> ShowS

show :: Name -> String

showList :: [Name] -> ShowS

NFData Name

Ranges are not forced.

Defined in Agda.Syntax.Concrete.Name

Methods

rnf :: Name -> ()

Pretty Name

Defined in Agda.Syntax.Concrete.Name

Methods

pretty :: Name -> Doc

prettyPrec :: Int -> Name -> Doc

prettyList :: [Name] -> Doc

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

HasRange Name

Defined in Agda.Syntax.Concrete.Name

Methods

getRange :: Name -> Range

Underscore Name

Defined in Agda.Syntax.Concrete.Name

Methods

underscore :: Name

isUnderscore :: Name -> Bool

IsNoName Name

Defined in Agda.Syntax.Concrete.Name

Methods

isNoName :: Name -> Bool

NumHoles Name

Defined in Agda.Syntax.Concrete.Name

Methods

numHoles :: Name -> Int

ExprLike Name

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

SubstExpr Name

Defined in Agda.Syntax.Abstract

Methods

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

EmbPrj Name

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Name -> S Int32

icod_ :: Name -> S Int32

value :: Int32 -> R Name

PrettyTCM Name

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Name -> TCM Doc

ToConcrete Name Name

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

toConcrete :: Name -> AbsToCon Name0

bindToConcrete :: Name -> (Name0 -> AbsToCon b) -> AbsToCon b

ToConcrete BindName Name

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

toConcrete :: BindName -> AbsToCon Name

bindToConcrete :: BindName -> (Name -> AbsToCon b) -> AbsToCon b

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) Name

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Methods

toAbstract :: NewName Name0 -> ScopeM Name

ToConcrete (Maybe QName) (Maybe Name)

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

toConcrete :: Maybe QName -> AbsToCon (Maybe Name)

bindToConcrete :: Maybe QName -> (Maybe Name -> AbsToCon b) -> AbsToCon b

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

Eq NamePart

Defined in Agda.Syntax.Concrete.Name

Methods

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

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

Data NamePart

Defined in Agda.Syntax.Concrete.Name

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> NamePart -> c NamePart

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c NamePart

toConstr :: NamePart -> Constr

dataTypeOf :: NamePart -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c NamePart)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c NamePart)

gmapT :: (forall b. Data b => b -> b) -> NamePart -> NamePart

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> NamePart -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> NamePart -> r

gmapQ :: (forall d. Data d => d -> u) -> NamePart -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> NamePart -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> NamePart -> m NamePart

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> NamePart -> m NamePart

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> NamePart -> m NamePart

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

Show NamePart

Defined in Agda.Syntax.Concrete.Name

Methods

showsPrec :: Int -> NamePart -> ShowS

show :: NamePart -> String

showList :: [NamePart] -> ShowS

Generic NamePart

Defined in Agda.Syntax.Concrete.Name

Associated Types

type Rep NamePart :: * -> *

Methods

from :: NamePart -> Rep NamePart x

to :: Rep NamePart x -> NamePart

NFData NamePart

Defined in Agda.Syntax.Concrete.Name

Methods

rnf :: NamePart -> ()

Pretty NamePart

Defined in Agda.Syntax.Concrete.Name

Methods

pretty :: NamePart -> Doc

prettyPrec :: Int -> NamePart -> Doc

prettyList :: [NamePart] -> Doc

EmbPrj NamePart

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: NamePart -> S Int32

icod_ :: NamePart -> S Int32

value :: Int32 -> R NamePart

NumHoles [NamePart]

Defined in Agda.Syntax.Concrete.Name

Methods

numHoles :: [NamePart] -> Int

type Rep NamePart

Defined in Agda.Syntax.Concrete.Name

type Rep NamePart = D1 (MetaData "NamePart" "Agda.Syntax.Concrete.Name" "Agda-2.5.4-KW6aUUUGirkK5xqjcQ2M8W" False) (C1 (MetaCons "Hole" PrefixI False) (U1 :: * -> *) :+: 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

Eq QName

Defined in Agda.Syntax.Concrete.Name

Methods

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

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

Data QName

Defined in Agda.Syntax.Concrete.Name

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> QName -> c QName

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c QName

toConstr :: QName -> Constr

dataTypeOf :: QName -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c QName)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c QName)

gmapT :: (forall b. Data b => b -> b) -> QName -> QName

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> QName -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> QName -> r

gmapQ :: (forall d. Data d => d -> u) -> QName -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> QName -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> QName -> m QName

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> QName -> m QName

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> QName -> m QName

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

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 -> ()

Pretty QName

Defined in Agda.Syntax.Concrete.Name

Methods

pretty :: QName -> Doc

prettyPrec :: Int -> QName -> Doc

prettyList :: [QName] -> Doc

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

HasRange QName

Defined in Agda.Syntax.Concrete.Name

Methods

getRange :: QName -> Range

Underscore QName

Defined in Agda.Syntax.Concrete.Name

Methods

underscore :: QName

isUnderscore :: QName -> Bool

IsNoName QName

Defined in Agda.Syntax.Concrete.Name

Methods

isNoName :: QName -> Bool

NumHoles QName

Defined in Agda.Syntax.Concrete.Name

Methods

numHoles :: QName -> Int

ExprLike QName

Defined in Agda.Syntax.Concrete.Generic

Methods

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

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

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

EmbPrj QName

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: QName -> S Int32

icod_ :: QName -> S Int32

value :: Int32 -> R QName

PrettyTCM QName

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: QName -> TCM Doc

ToConcrete ModuleName QName

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

toConcrete :: ModuleName -> AbsToCon QName

bindToConcrete :: ModuleName -> (QName -> AbsToCon b) -> AbsToCon b

ToConcrete QName QName

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

toConcrete :: QName -> AbsToCon QName0

bindToConcrete :: QName -> (QName0 -> AbsToCon b) -> AbsToCon b

ToConcrete ResolvedName QName

Assumes name is not UnknownName.

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

toConcrete :: ResolvedName -> AbsToCon QName

bindToConcrete :: ResolvedName -> (QName -> AbsToCon b) -> AbsToCon b

ToConcrete AbstractName QName

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

toConcrete :: AbstractName -> AbsToCon QName

bindToConcrete :: AbstractName -> (QName -> AbsToCon b) -> AbsToCon b

data TopLevelModuleName

Top-level module names. Used in connection with the file system.

Invariant: The list must not be empty.

Constructors

TopLevelModuleName

Fields

• moduleNameRange :: Range
• moduleNameParts :: [String]

Instances

Eq TopLevelModuleName

Defined in Agda.Syntax.Concrete.Name

Methods

(==) :: TopLevelModuleName -> TopLevelModuleName -> Bool

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

Data TopLevelModuleName

Defined in Agda.Syntax.Concrete.Name

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TopLevelModuleName -> c TopLevelModuleName

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TopLevelModuleName

toConstr :: TopLevelModuleName -> Constr

dataTypeOf :: TopLevelModuleName -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c TopLevelModuleName)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TopLevelModuleName)

gmapT :: (forall b. Data b => b -> b) -> TopLevelModuleName -> TopLevelModuleName

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TopLevelModuleName -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TopLevelModuleName -> r

gmapQ :: (forall d. Data d => d -> u) -> TopLevelModuleName -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> TopLevelModuleName -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> TopLevelModuleName -> m TopLevelModuleName

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TopLevelModuleName -> m TopLevelModuleName

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TopLevelModuleName -> m TopLevelModuleName

Ord TopLevelModuleName

Defined in Agda.Syntax.Concrete.Name

Methods

compare :: TopLevelModuleName -> TopLevelModuleName -> Ordering

(<) :: TopLevelModuleName -> TopLevelModuleName -> Bool

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

(>) :: TopLevelModuleName -> TopLevelModuleName -> Bool

(>=) :: TopLevelModuleName -> TopLevelModuleName -> Bool

max :: TopLevelModuleName -> TopLevelModuleName -> TopLevelModuleName

min :: TopLevelModuleName -> TopLevelModuleName -> TopLevelModuleName

Show TopLevelModuleName

Defined in Agda.Syntax.Concrete.Name

Methods

showsPrec :: Int -> TopLevelModuleName -> ShowS

show :: TopLevelModuleName -> String

showList :: [TopLevelModuleName] -> ShowS

Pretty TopLevelModuleName

Defined in Agda.Syntax.Concrete.Name

Methods

pretty :: TopLevelModuleName -> Doc

prettyPrec :: Int -> TopLevelModuleName -> Doc

prettyList :: [TopLevelModuleName] -> Doc

Sized TopLevelModuleName

Defined in Agda.Syntax.Concrete.Name

Methods

size :: TopLevelModuleName -> Int

KillRange TopLevelModuleName

Defined in Agda.Syntax.Concrete.Name

Methods

killRange :: KillRangeT TopLevelModuleName

SetRange TopLevelModuleName

Defined in Agda.Syntax.Concrete.Name

Methods

setRange :: Range -> TopLevelModuleName -> TopLevelModuleName

HasRange TopLevelModuleName

Defined in Agda.Syntax.Concrete.Name

Methods

getRange :: TopLevelModuleName -> Range

EmbPrj TopLevelModuleName

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: TopLevelModuleName -> S Int32

icod_ :: TopLevelModuleName -> S Int32

value :: Int32 -> R TopLevelModuleName

Operations on Name and NamePart

nameToRawName :: Name -> RawName

nameParts :: Name -> [NamePart]

nameStringParts :: Name -> [RawName]

stringNameParts :: String -> [NamePart]

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

Minimal complete definition

numHoles

Methods

numHoles :: a -> Int

Instances

NumHoles QName

Defined in Agda.Syntax.Concrete.Name

Methods

numHoles :: QName -> Int

NumHoles Name

Defined in Agda.Syntax.Concrete.Name

Methods

numHoles :: Name -> Int

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 QName

Defined in Agda.Syntax.Abstract.Name

Methods

numHoles :: QName -> Int

NumHoles Name

Defined in Agda.Syntax.Abstract.Name

Methods

numHoles :: Name -> Int

NumHoles [NamePart]

Defined in Agda.Syntax.Concrete.Name

Methods

numHoles :: [NamePart] -> Int

isOperator :: Name -> Bool

Is the name an operator?

isHole :: NamePart -> Bool

isPrefix :: Name -> Bool

isPostfix :: Name -> Bool

isInfix :: Name -> Bool

isNonfix :: Name -> Bool

Operations on qualified names

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 -> [Name]

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

isQualified :: QName -> Bool

Is the name qualified?

Operations on TopLevelModuleName

toTopLevelModuleName :: QName -> TopLevelModuleName

Turns a qualified name into a TopLevelModuleName. The qualified name is assumed to represent a top-level module name.

moduleNameToFileName :: TopLevelModuleName -> String -> FilePath

Turns a top-level module name into a file name with the given suffix.

projectRoot :: AbsolutePath -> TopLevelModuleName -> AbsolutePath

Finds the current project's "root" directory, given a project file and the corresponding top-level module name.

Example: If the module "A.B.C" is located in the file "fooABC.agda", then the root is "foo".

Precondition: The module name must be well-formed.

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

isNoName

Methods

isNoName :: a -> Bool

Instances

IsNoName String

Defined in Agda.Syntax.Concrete.Name

Methods

isNoName :: String -> Bool

IsNoName ByteString

Defined in Agda.Syntax.Concrete.Name

Methods

isNoName :: ByteString -> Bool

IsNoName QName

Defined in Agda.Syntax.Concrete.Name

Methods

isNoName :: QName -> Bool

IsNoName Name

Defined in Agda.Syntax.Concrete.Name

Methods

isNoName :: Name -> Bool

IsNoName Name

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

Defined in Agda.Syntax.Abstract.Name

Methods

isNoName :: Name -> Bool

Showing names

Printing names

Range instances

NFData instances