| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Agda.Syntax.Abstract.Name
Description
Abstract names carry unique identifiers and stuff.
Synopsis
- data Name = Name {}
- data QName = QName {}
- class IsProjP a where
- isProjP :: a -> Maybe (ProjOrigin, AmbiguousQName)
- data Suffix
- data QNamed a = QNamed {}
- newtype ModuleName = MName {
- mnameToList :: [Name]
- newtype AmbiguousQName = AmbQ {}
- class MkName a where
- nextName :: FreshNameMode -> Name -> Name
- qualify :: ModuleName -> Name -> QName
- unambiguous :: QName -> AmbiguousQName
- isOperator :: QName -> Bool
- sameRoot :: Name -> Name -> Bool
- lensQNameName :: Lens' QName Name
- uglyShowName :: Name -> String
- headAmbQ :: AmbiguousQName -> QName
- isAmbiguous :: AmbiguousQName -> Bool
- getUnambiguous :: AmbiguousQName -> Maybe QName
- isAnonymousModuleName :: ModuleName -> Bool
- withRangesOf :: ModuleName -> List1 Name -> ModuleName
- withRangesOfQ :: ModuleName -> QName -> ModuleName
- mnameFromList :: [Name] -> ModuleName
- mnameFromList1 :: List1 Name -> ModuleName
- mnameToList1 :: ModuleName -> List1 Name
- noModuleName :: ModuleName
- commonParentModule :: ModuleName -> ModuleName -> ModuleName
- makeName :: NameId -> Name -> Range -> Fixity' -> Bool -> Name
- qnameToList0 :: QName -> [Name]
- qnameToList :: QName -> List1 Name
- qnameFromList :: List1 Name -> QName
- qnameToMName :: QName -> ModuleName
- mnameToQName :: ModuleName -> QName
- showQNameId :: QName -> String
- qnameToConcrete :: QName -> QName
- mnameToConcrete :: ModuleName -> QName
- qualifyM :: ModuleName -> ModuleName -> ModuleName
- qualifyQ :: ModuleName -> QName -> QName
- qualify_ :: Name -> QName
- isLeParentModuleOf :: ModuleName -> ModuleName -> Bool
- isLtParentModuleOf :: ModuleName -> ModuleName -> Bool
- isLeChildModuleOf :: ModuleName -> ModuleName -> Bool
- isLtChildModuleOf :: ModuleName -> ModuleName -> Bool
- isInModule :: QName -> ModuleName -> Bool
- nameToArgName :: Name -> ArgName
- namedArgName :: NamedArg Name -> ArgName
- class IsNoName a where
- data FreshNameMode
Documentation
A name is a unique identifier and a suggestion for a concrete name. The concrete name contains the source location (if any) of the name. The source location of the binding site is also recorded.
Constructors
| Name | |
Fields
| |
Instances
Qualified names are non-empty lists of names. Equality on qualified names are just equality on the last name, i.e. the module part is just for show.
The SetRange instance for qualified names sets all individual
ranges (including those of the module prefix) to the given one.
Constructors
| QName | |
Fields
| |
Instances
class IsProjP a where Source #
Check whether we are a projection pattern.
Methods
isProjP :: a -> Maybe (ProjOrigin, AmbiguousQName) Source #
Instances
| IsProjP Expr Source # | |
Defined in Agda.Syntax.Abstract Methods isProjP :: Expr -> Maybe (ProjOrigin, AmbiguousQName) Source # | |
| IsProjP Void Source # | |
Defined in Agda.Syntax.Abstract.Name Methods isProjP :: Void -> Maybe (ProjOrigin, AmbiguousQName) Source # | |
| IsProjP (Pattern' e) Source # | |
Defined in Agda.Syntax.Abstract Methods isProjP :: Pattern' e -> Maybe (ProjOrigin, AmbiguousQName) Source # | |
| IsProjP a => IsProjP (Arg a) Source # | |
Defined in Agda.Syntax.Abstract.Name Methods isProjP :: Arg a -> Maybe (ProjOrigin, AmbiguousQName) Source # | |
| IsProjP (Pattern' a) Source # | |
Defined in Agda.Syntax.Internal Methods isProjP :: Pattern' a -> Maybe (ProjOrigin, AmbiguousQName) Source # | |
| IsProjP a => IsProjP (Named n a) Source # | |
Defined in Agda.Syntax.Abstract.Name Methods isProjP :: Named n a -> Maybe (ProjOrigin, AmbiguousQName) Source # | |
A name suffix
Something preceeded by a qualified name.
Instances
newtype ModuleName Source #
A module name is just a qualified name.
The SetRange instance for module names sets all individual ranges
to the given one.
Constructors
| MName | |
Fields
| |
Instances
newtype AmbiguousQName Source #
Ambiguous qualified names. Used for overloaded constructors.
Invariant: All the names in the list must have the same concrete,
unqualified name. (This implies that they all have the same Range').
Instances
Make a Name from some kind of string.
Minimal complete definition
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.
unambiguous :: QName -> AmbiguousQName Source #
A singleton "ambiguous" name.
isOperator :: QName -> Bool Source #
Is the name an operator?
uglyShowName :: Name -> String Source #
Useful for debugging scoping problems
headAmbQ :: AmbiguousQName -> QName Source #
Get the first of the ambiguous names.
isAmbiguous :: AmbiguousQName -> Bool Source #
Is a name ambiguous.
getUnambiguous :: AmbiguousQName -> Maybe QName Source #
Get the name if unambiguous.
isAnonymousModuleName :: ModuleName -> Bool Source #
A module is anonymous if the qualification path ends in an underscore.
withRangesOf :: ModuleName -> List1 Name -> ModuleName Source #
Sets the ranges of the individual names in the module name to
match those of the corresponding concrete names. If the concrete
names are fewer than the number of module name name parts, then the
initial name parts get the range noRange.
C.D.E `withRangesOf` [A, B] returns C.D.E but with ranges set
as follows:
C:noRange.D: the range ofA.E: the range ofB.
Precondition: The number of module name name parts has to be at least as large as the length of the list.
withRangesOfQ :: ModuleName -> QName -> ModuleName Source #
Like withRangesOf, but uses the name parts (qualifier + name)
of the qualified name as the list of concrete names.
mnameFromList :: [Name] -> ModuleName Source #
mnameFromList1 :: List1 Name -> ModuleName Source #
mnameToList1 :: ModuleName -> List1 Name Source #
commonParentModule :: ModuleName -> ModuleName -> ModuleName Source #
qnameToList0 :: QName -> [Name] Source #
qnameToMName :: QName -> ModuleName Source #
mnameToQName :: ModuleName -> QName Source #
showQNameId :: QName -> String Source #
qnameToConcrete :: QName -> QName Source #
Turn a qualified name into a concrete name. This should only be used as a fallback when looking up the right concrete name in the scope fails.
mnameToConcrete :: ModuleName -> QName Source #
qualifyM :: ModuleName -> ModuleName -> ModuleName Source #
isLeParentModuleOf :: ModuleName -> ModuleName -> Bool Source #
Is the first module a weak parent of the second?
isLtParentModuleOf :: ModuleName -> ModuleName -> Bool Source #
Is the first module a proper parent of the second?
isLeChildModuleOf :: ModuleName -> ModuleName -> Bool Source #
Is the first module a weak child of the second?
isLtChildModuleOf :: ModuleName -> ModuleName -> Bool Source #
Is the first module a proper child of the second?
isInModule :: QName -> ModuleName -> Bool Source #
nameToArgName :: Name -> ArgName Source #
class IsNoName a where Source #
Check whether a name is the empty name "_".
Minimal complete definition
Nothing
Methods
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 Methods isNoName :: RawTopLevelModuleName -> Bool Source # | |
| IsNoName ByteString Source # | |
Defined in Agda.Syntax.Concrete.Name Methods 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 Methods isNoName :: WithOrigin a -> Bool Source # | |
data FreshNameMode Source #
Method by which to generate fresh unshadowed names.
Constructors
| UnicodeSubscript | Append an integer Unicode subscript: x, x₁, x₂, … |
| AsciiCounter | Append an integer ASCII counter: x, x1, x2, … |