Agda-2.2.6: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.Syntax.Concrete.Name
Description
Names in the concrete syntax are just strings (or lists of strings for qualified names).
Synopsis
data Name
= Name !Range [NamePart]
| NoName !Range NameId
data NamePart
= Hole
| Id String
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
= Qual Name QName
| QName Name
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
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.

Constructors
Name !Range [NamePart]
NoName !Range NameId
show/hide Instances
data NamePart Source
Constructors
Hole
Id String
show/hide Instances
noName_ :: NameSource
noName_ = noName noRange
noName :: Range -> NameSource
noName r = Name r [Hole]
isNoName :: Name -> BoolSource
isOperator :: Name -> BoolSource
Is the name an operator?
nameParts :: Name -> [NamePart]Source
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).
Constructors
Qual Name QName
QName Name
show/hide Instances
newtype TopLevelModuleName Source

Top-level module names.

Invariant: The list must not be empty.

Constructors
TopLevelModuleName
moduleNameParts :: [String]
show/hide Instances
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.

isHole :: NamePart -> BoolSource
isPostfix :: Name -> BoolSource
isInfix :: Name -> BoolSource
isNonfix :: Name -> BoolSource
isPrefix :: Name -> BoolSource
Produced by Haddock version 2.4.2