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]

NoName !Range NameId

Instances

Eq Name

Data Name

Ord Name

Show Name

Typeable Name

Pretty Name

KillRange Name

SetRange Name

HasRange Name

EmbPrj Name

ToConcrete Name Name

ToAbstract (NewName Name) Name

data NamePart

Constructors

Hole

Id String

Instances

Eq NamePart

Data NamePart

Ord NamePart

Show NamePart

Typeable NamePart

EmbPrj NamePart

noName_ :: Name

noName_ = noName noRange

noName :: Range -> Name

noName r = Name r [Hole]

isNoName :: Name -> Bool

isOperator :: Name -> Bool

Is the name an operator?

nameParts :: Name -> [NamePart]

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]

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

QName Name

Instances

Eq QName

Data QName

Ord QName

Show QName

Typeable QName

Pretty QName

KillRange QName

HasRange QName

EmbPrj QName

ToConcrete ModuleName QName

ToConcrete QName QName

newtype TopLevelModuleName

Top-level module names.

Invariant: The list must not be empty.

Constructors

TopLevelModuleName

Fields

moduleNameParts :: [String]

Instances

Eq TopLevelModuleName

Data TopLevelModuleName

Ord TopLevelModuleName

Show TopLevelModuleName

Typeable TopLevelModuleName

Arbitrary TopLevelModuleName

CoArbitrary TopLevelModuleName

Pretty TopLevelModuleName

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

isHole :: NamePart -> Bool

isPostfix :: Name -> Bool

isInfix :: Name -> Bool

isNonfix :: Name -> Bool

isPrefix :: Name -> Bool