| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

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 `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.
Constructors

Name !Range [NamePart] |
NoName !Range NameId |

Instances

Eq Name
Data Name
Ord Name
Show Name
Typeable Name
Pretty Name
KillRange Name
SetRange Name
HasRange Name
EmbPrj Name
ToConcrete Name Name

data NamePart | Source

Constructors

Hole |
Id String |

Instances

Eq NamePart
Data NamePart
Ord NamePart
Show NamePart
Typeable NamePart
EmbPrj NamePart

noName_ :: Name | Source

    noName_ = noName noRange

noName :: Range -> Name | Source

    noName r = Name r [Hole]

isNoName :: Name -> Bool | Source

isOperator :: Name -> Bool | Source

Is the name an operator?

nameParts :: Name -> [NamePart] | Source

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]

data QName | Source

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

Qual Name QName |
QName Name |

Instances

Eq QName
Data QName
Ord QName
Show QName
Typeable QName
Pretty QName
KillRange QName
HasRange QName
EmbPrj QName
ToConcrete ModuleName QName
ToConcrete QName QName

newtype TopLevelModuleName | Source

Top-level module names. Invariant: The list must not be empty.
Constructors

TopLevelModuleName |

moduleNameParts :: [String] |

Instances

Eq TopLevelModuleName
Data TopLevelModuleName
Ord TopLevelModuleName
Show TopLevelModuleName
Typeable TopLevelModuleName
Arbitrary TopLevelModuleName
CoArbitrary TopLevelModuleName
Pretty TopLevelModuleName
EmbPrj 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.

isHole :: NamePart -> Bool | Source

isPostfix :: Name -> Bool | Source

isInfix :: Name -> Bool | Source

isNonfix :: Name -> Bool | Source

isPrefix :: Name -> Bool | Source

Produced by Haddock version 2.4.2