Safe Haskell | None |
---|---|
Language | Haskell98 |
Names in the concrete syntax are just strings (or lists of strings for qualified names).
- data Name
- data NamePart
- data QName
- newtype TopLevelModuleName = TopLevelModuleName {
- moduleNameParts :: [String]
- nameToRawName :: Name -> RawName
- nameParts :: Name -> [NamePart]
- nameStringParts :: Name -> [RawName]
- stringNameParts :: String -> [NamePart]
- class NumHoles a where
- isOperator :: Name -> Bool
- isHole :: NamePart -> Bool
- isPrefix :: Name -> Bool
- isPostfix :: Name -> Bool
- isInfix :: Name -> Bool
- isNonfix :: Name -> Bool
- qualify :: QName -> Name -> QName
- unqualify :: QName -> Name
- qnameParts :: QName -> [Name]
- toTopLevelModuleName :: QName -> TopLevelModuleName
- moduleNameToFileName :: TopLevelModuleName -> String -> FilePath
- projectRoot :: AbsolutePath -> TopLevelModuleName -> AbsolutePath
- noName_ :: Name
- noName :: Range -> Name
- class IsNoName a where
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.
Eq Name Source # | Define equality on Is there a reason not to do this? -Jeff No. But there are tons of reasons to do it. For instance, when using names as keys in maps you really don't want to have to get the range right to be able to do a lookup. -Ulf |
Ord Name Source # | |
Show Name Source # | |
Arbitrary Name Source # | |
CoArbitrary Name Source # | |
NFData Name Source # | Ranges are not forced. |
Pretty Name Source # | |
KillRange Name Source # | |
SetRange Name Source # | |
HasRange Name Source # | |
Underscore Name Source # | |
IsNoName Name Source # | |
NumHoles Name Source # | |
ExprLike Name Source # | |
SubstExpr Name Source # | |
PrettyTCM Name Source # | |
ToConcrete Name Name Source # | |
ToAbstract (NewName Name) Name Source # | |
ToConcrete (Maybe QName) (Maybe Name) Source # | |
Mixfix identifiers are composed of words and holes,
e.g. _+_
or if_then_else_
or [_/_]
.
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. Used in connection with the file system.
Invariant: The list must not be empty.
Operations on Name
and NamePart
nameToRawName :: Name -> RawName Source #
nameStringParts :: Name -> [RawName] Source #
stringNameParts :: String -> [NamePart] Source #
Parse a string to parts of a concrete name.
Note: stringNameParts "_" == [Id "_"] == nameParts NoName{}
isOperator :: Name -> Bool Source #
Is the name an operator?
Operations on qualified names
qnameParts :: QName -> [Name] Source #
qnameParts A.B.x = [A, B, x]
Operations on 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.