Names in the concrete syntax are just strings (or lists of strings for qualified names).
- data Name
- data NamePart
- noName_ :: Name
- noName :: Range -> Name
- isNoName :: Name -> Bool
- isOperator :: Name -> Bool
- nameParts :: Name -> [NamePart]
- qualify :: QName -> Name -> QName
- unqualify :: QName -> Name
- qnameParts :: QName -> [Name]
- data QName
- newtype TopLevelModuleName = TopLevelModuleName {
- moduleNameParts :: [String]
- toTopLevelModuleName :: QName -> TopLevelModuleName
- moduleNameToFileName :: TopLevelModuleName -> String -> FilePath
- projectRoot :: AbsolutePath -> TopLevelModuleName -> AbsolutePath
- isHole :: NamePart -> Bool
- isPostfix :: Name -> Bool
- isInfix :: Name -> Bool
- isNonfix :: Name -> Bool
- isPrefix :: Name -> Bool
Documentation
A name is a non-empty list of alternating Id
s and Hole
s. A normal name
is represented by a singleton list, and operators are represented by a list
with Hole
s where the arguments should go. For instance: [Hole,Id +,Hole]
is infix addition.
Equality and ordering on Name
s are defined to ignore range so same names
in different locations are equal.
isOperator :: Name -> BoolSource
Is the name an operator?
qnameParts :: QName -> [Name]Source
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 Name
s 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).
newtype TopLevelModuleName Source
Top-level module names.
Invariant: The list must not be empty.
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.