Agda- A dependently typed functional programming language and proof assistant

Safe HaskellNone




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



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.


Name !Range [NamePart]

A (mixfix) identifier.

NoName !Range NameId



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

Ord Name Source 
Show Name Source 
NFData Name Source 
CoArbitrary Name Source 
Arbitrary Name Source 
Pretty Name Source 
KillRange Name Source 
SetRange Name Source 
HasRange Name Source 
Underscore Name Source 
IsNoName Name Source 
ExprLike Name Source 
SubstExpr Name Source 
PrettyTCM Name Source 
EmbPrj Name Source 
ToConcrete Name Name Source 
ToAbstract (NewName Name) Name Source 
ToConcrete (Maybe QName) (Maybe Name) Source 

data NamePart Source

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



_ part.

Id RawName

Identifier part.

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


Qual Name QName

QName Name


newtype TopLevelModuleName Source

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

Invariant: The list must not be empty.




moduleNameParts :: [String]

Operations on Name and NamePart

stringNameParts :: String -> [NamePart] Source

Parse a string to parts of a concrete name.

isOperator :: Name -> Bool Source

Is the name an operator?

Operations on qualified names

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

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

Operations on TopLevelModuleName

toTopLevelModuleName :: QName -> TopLevelModuleName Source

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

moduleNameToFileName :: TopLevelModuleName -> String -> FilePath Source

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

projectRoot :: AbsolutePath -> TopLevelModuleName -> AbsolutePath Source

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 :: Range -> Name Source

noName r = Name r [Hole]

class IsNoName a where Source

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


isNoName :: a -> Bool Source


IsNoName String Source 
IsNoName ByteString Source 
IsNoName QName Source 
IsNoName Name Source 
IsNoName Name Source

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

Showing names

Printing names

QuickCheck instances

Range instances