|
Agda.Syntax.Concrete.Name |
|
|
Description |
Names in the concrete syntax are just strings (or lists of strings for
qualified names).
|
|
Synopsis |
|
|
|
Documentation |
|
|
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 | |
|
|
|
|
|
|
noName_ = noName noRange |
|
|
noName r = Name r [Hole] |
|
|
|
|
Is the name an operator?
|
|
|
|
|
qualify A.B x == A.B.x |
|
|
unqualify A.B.x == x The range is preserved.
|
|
|
qnameParts A.B.x = [A, B, x] |
|
|
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 | |
|
|
newtype TopLevelModuleName | Source |
|
Top-level module names.
Invariant: The list must not be empty.
| Constructors | |
|
|
|
Turns a qualified name into a TopLevelModuleName. The qualified
name is assumed to represent a top-level module name.
|
|
|
Turns a top-level module name into a file name with the given
suffix.
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
|
|
Produced by Haddock version 2.6.1 |