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

Safe Haskell | None

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]
- nameStringParts :: Name -> [String]
- 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
- isPrefix :: Name -> Bool
- isNonfix :: Name -> Bool
- isInfix :: Name -> Bool
- isPostfix :: Name -> Bool

# Documentation

data Name

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 |
Ord Name |
Show Name |
Typeable Name |
Pretty Name |
KillRange Name |
SetRange Name |
HasRange Name |
PrettyTCM Name |
EmbPrj Name |
ToConcrete Name Name |
Pretty (ThingWithFixity Name) |
ToAbstract (NewName Name) Name |
ToConcrete (Maybe QName) (Maybe Name) |

data NamePart

Constructors

Hole |
Id String |

Instances

Eq NamePart |
Ord NamePart |
Show NamePart |
Typeable NamePart |
EmbPrj NamePart |

noName_ :: Name

    noName_ = noName noRange

noName :: Range -> Name

    noName r = Name r [Hole]

isNoName :: Name -> Bool

isOperator :: Name -> Bool

Is the name an operator?

nameParts :: Name -> [NamePart]

nameStringParts :: Name -> [String]

qualify :: QName -> Name -> QName

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

unqualify :: QName -> Name

    unqualify A.B.x == x

The range is preserved.

qnameParts :: QName -> [Name]

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

data QName

`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 |
Ord QName |
Show QName |
Typeable QName |
Pretty QName |
KillRange QName |
SetRange QName |
HasRange QName |
EmbPrj QName |
ToConcrete ModuleName QName |
ToConcrete QName QName |

newtype TopLevelModuleName

Top-level module names.

Invariant: The list must not be empty.

Constructors

TopLevelModuleName |

Fields

moduleNameParts :: [String]

Instances

Eq TopLevelModuleName |
Ord TopLevelModuleName |
Show TopLevelModuleName |
Typeable TopLevelModuleName |
Arbitrary TopLevelModuleName |
CoArbitrary TopLevelModuleName |
Pretty TopLevelModuleName |
EmbPrj TopLevelModuleName |

toTopLevelModuleName :: QName -> TopLevelModuleName

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

moduleNameToFileName :: TopLevelModuleName -> String -> FilePath

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

projectRoot :: AbsolutePath -> TopLevelModuleName -> AbsolutePath

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

isPrefix :: Name -> Bool

isNonfix :: Name -> Bool

isInfix :: Name -> Bool

isPostfix :: Name -> Bool