Agda-2.2.10: A dependently typed functional programming language and proof assistant



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] 
NoName !Range NameId 

noName :: Range -> NameSource

noName r = Name r [Hole]

isOperator :: Name -> BoolSource

Is the name an operator?

qualify :: QName -> Name -> QNameSource

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

unqualify :: QName -> NameSource

unqualify A.B.x == x

The range is preserved.

qnameParts :: QName -> [Name]Source

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

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 

toTopLevelModuleName :: QName -> TopLevelModuleNameSource

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

moduleNameToFileName :: TopLevelModuleName -> String -> FilePathSource

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

projectRoot :: AbsolutePath -> TopLevelModuleName -> AbsolutePathSource

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.