Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Names in the concrete syntax are just strings (or lists of strings for qualified names).
Synopsis
- data Name
- type NameParts = List1 NamePart
- isOpenMixfix :: Name -> Bool
- data NamePart
- data QName
- simpleName :: RawName -> Name
- simpleBinaryOperator :: RawName -> Name
- simpleHole :: Name
- lensNameParts :: Lens' Name NameParts
- nameToRawName :: Name -> RawName
- nameParts :: Name -> NameParts
- nameStringParts :: Name -> [RawName]
- stringNameParts :: String -> NameParts
- class NumHoles a where
- isOperator :: Name -> Bool
- isHole :: NamePart -> Bool
- isPrefix :: Name -> Bool
- isPostfix :: Name -> Bool
- isInfix :: Name -> Bool
- isNonfix :: Name -> Bool
- data NameInScope
- class LensInScope a where
- lensInScope :: Lens' a NameInScope
- isInScope :: a -> NameInScope
- mapInScope :: (NameInScope -> NameInScope) -> a -> a
- setInScope :: a -> a
- setNotInScope :: a -> a
- data FreshNameMode
- nextRawName :: FreshNameMode -> RawName -> RawName
- nextName :: FreshNameMode -> Name -> Name
- lastIdPart :: Lens' NameParts RawName
- firstNonTakenName :: FreshNameMode -> (Name -> Bool) -> Name -> Name
- nameSuffix :: Lens' Name (Maybe Suffix)
- nameSuffixView :: Name -> (Maybe Suffix, Name)
- setNameSuffix :: Maybe Suffix -> Name -> Name
- nameRoot :: Name -> RawName
- sameRoot :: Name -> Name -> Bool
- lensQNameName :: Lens' QName Name
- qualify :: QName -> Name -> QName
- unqualify :: QName -> Name
- qnameParts :: QName -> List1 Name
- isQualified :: QName -> Bool
- isUnqualified :: QName -> Maybe Name
- 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.
Instances
isOpenMixfix :: Name -> Bool Source #
An open mixfix identifier is either prefix, infix, or suffix.
That is to say: at least one of its extremities is a Hole
Mixfix identifiers are composed of words and holes,
e.g. _+_
or if_then_else_
or [_/_]
.
Instances
Pretty NamePart Source # | |
NumHoles NameParts Source # | |
EmbPrj NamePart Source # | |
Generic NamePart Source # | |
Show NamePart Source # | |
NFData NamePart Source # | |
Defined in Agda.Syntax.Concrete.Name | |
Eq NamePart Source # | |
Ord NamePart Source # | |
Defined in Agda.Syntax.Concrete.Name | |
type Rep NamePart Source # | |
Defined in Agda.Syntax.Concrete.Name type Rep NamePart = D1 ('MetaData "NamePart" "Agda.Syntax.Concrete.Name" "Agda-2.6.3.20230805-inplace" 'False) (C1 ('MetaCons "Hole" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Id" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RawName))) |
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).
Instances
Underscore QName Source # | |
Defined in Agda.Syntax.Concrete.Name underscore :: QName Source # isUnderscore :: QName -> Bool Source # | |
Pretty QName Source # | |
ExprLike QName Source # | |
IsNoName QName Source # | |
LensInScope QName Source # | |
Defined in Agda.Syntax.Concrete.Name lensInScope :: Lens' QName NameInScope Source # isInScope :: QName -> NameInScope Source # mapInScope :: (NameInScope -> NameInScope) -> QName -> QName Source # setInScope :: QName -> QName Source # setNotInScope :: QName -> QName Source # | |
NumHoles QName Source # | |
HasRange QName Source # | |
KillRange QName Source # | |
Defined in Agda.Syntax.Concrete.Name | |
SetRange QName Source # | |
PrettyTCM QName Source # | |
Defined in Agda.TypeChecking.Pretty | |
EmbPrj QName Source # | |
Show QName Source # | |
NFData QName Source # | |
Defined in Agda.Syntax.Concrete.Name | |
Eq QName Source # | |
Ord QName Source # | |
Constructing simple Name
s.
simpleBinaryOperator :: RawName -> Name Source #
Create a binary operator name in scope.
Operations on Name
and NamePart
nameToRawName :: Name -> RawName Source #
nameStringParts :: Name -> [RawName] Source #
stringNameParts :: String -> NameParts Source #
Parse a string to parts of a concrete name.
Note: stringNameParts "_" == [Id "_"] == nameParts NoName{}
class NumHoles a where Source #
Number of holes in a Name
(i.e., arity of a mixfix-operator).
Instances
NumHoles AmbiguousQName Source # | We can have an instance for ambiguous names as all share a common concrete name. |
Defined in Agda.Syntax.Abstract.Name numHoles :: AmbiguousQName -> Int Source # | |
NumHoles Name Source # | |
NumHoles QName Source # | |
NumHoles Name Source # | |
NumHoles NameParts Source # | |
NumHoles QName Source # | |
Keeping track of which names are (not) in scope
data NameInScope Source #
Instances
class LensInScope a where Source #
lensInScope :: Lens' a NameInScope Source #
isInScope :: a -> NameInScope Source #
mapInScope :: (NameInScope -> NameInScope) -> a -> a Source #
setInScope :: a -> a Source #
setNotInScope :: a -> a Source #
Instances
Generating fresh names
data FreshNameMode Source #
Method by which to generate fresh unshadowed names.
UnicodeSubscript | Append an integer Unicode subscript: x, x₁, x₂, … |
AsciiCounter | Append an integer ASCII counter: x, x1, x2, … |
nextRawName :: FreshNameMode -> RawName -> RawName Source #
nextName :: FreshNameMode -> Name -> Name Source #
Get the next version of the concrete name. For instance,
nextName "x" = "x₁"
. The name must not be a NoName
.
firstNonTakenName :: FreshNameMode -> (Name -> Bool) -> Name -> Name Source #
Get the first version of the concrete name that does not satisfy the given predicate.
nameSuffix :: Lens' Name (Maybe Suffix) Source #
Lens for accessing and modifying the suffix of a name.
The suffix of a NoName
is always Nothing
, and should not be
changed.
setNameSuffix :: Maybe Suffix -> Name -> Name Source #
Replaces the suffix of a name. Unless the suffix is Nothing
,
the name should not be NoName
.
nameRoot :: Name -> RawName Source #
Get a raw version of the name with all suffixes removed. For
instance, nameRoot "x₁₂₃" = "x"
.
Operations on qualified names
isQualified :: QName -> Bool Source #
Is the name (un)qualified?
No name stuff
class IsNoName a where Source #
Check whether a name is the empty name "_".
Nothing
Instances
IsNoName Name Source # | An abstract name is empty if its concrete name is empty. |
IsNoName Name Source # | |
IsNoName QName Source # | |
IsNoName RawTopLevelModuleName Source # | |
Defined in Agda.Syntax.TopLevelModuleName isNoName :: RawTopLevelModuleName -> Bool Source # | |
IsNoName ByteString Source # | |
Defined in Agda.Syntax.Concrete.Name isNoName :: ByteString -> Bool Source # | |
IsNoName String Source # | |
IsNoName a => IsNoName (Ranged a) Source # | |
IsNoName a => IsNoName (WithOrigin a) Source # | |
Defined in Agda.Syntax.Concrete.Name isNoName :: WithOrigin a -> Bool Source # |