| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Syntax.Abstract.Name
Description
Abstract names carry unique identifiers and stuff.
Synopsis
- class MkName a where
- class IsProjP a where
- newtype AmbiguousQName = AmbQ {}
- newtype ModuleName = MName {
- mnameToList :: [Name]
- data QNamed a = QNamed {}
- data QName = QName {}
- data Name = Name {
- nameId :: !NameId
- nameConcrete :: Name
- nameBindingSite :: Range
- nameFixity :: Fixity'
- unambiguous :: QName -> AmbiguousQName
- headAmbQ :: AmbiguousQName -> QName
- isAmbiguous :: AmbiguousQName -> Bool
- getUnambiguous :: AmbiguousQName -> Maybe QName
- isAnonymousModuleName :: ModuleName -> Bool
- withRangesOf :: ModuleName -> [Name] -> ModuleName
- withRangesOfQ :: ModuleName -> QName -> ModuleName
- mnameFromList :: [Name] -> ModuleName
- noModuleName :: ModuleName
- commonParentModule :: ModuleName -> ModuleName -> ModuleName
- qnameToList :: QName -> [Name]
- qnameFromList :: [Name] -> QName
- qnameToMName :: QName -> ModuleName
- mnameToQName :: ModuleName -> QName
- showQNameId :: QName -> String
- qnameToConcrete :: QName -> QName
- mnameToConcrete :: ModuleName -> QName
- toTopLevelModuleName :: ModuleName -> TopLevelModuleName
- qualifyM :: ModuleName -> ModuleName -> ModuleName
- qualifyQ :: ModuleName -> QName -> QName
- qualify :: ModuleName -> Name -> QName
- qualify_ :: Name -> QName
- isOperator :: QName -> Bool
- isSubModuleOf :: ModuleName -> ModuleName -> Bool
- isInModule :: QName -> ModuleName -> Bool
- nextName :: Name -> Name
- class IsNoName a where
Documentation
Make a Name from some kind of string.
Minimal complete definition
Check whether we are a projection pattern.
Minimal complete definition
Methods
isProjP :: a -> Maybe (ProjOrigin, AmbiguousQName) #
Instances
| IsProjP Void # | |
Defined in Agda.Syntax.Abstract.Name Methods isProjP :: Void -> Maybe (ProjOrigin, AmbiguousQName) # | |
| IsProjP Expr # | |
Defined in Agda.Syntax.Abstract Methods isProjP :: Expr -> Maybe (ProjOrigin, AmbiguousQName) # | |
| IsProjP a => IsProjP (Arg a) # | |
Defined in Agda.Syntax.Abstract.Name Methods isProjP :: Arg a -> Maybe (ProjOrigin, AmbiguousQName) # | |
| IsProjP (Pattern' a) # | |
Defined in Agda.Syntax.Internal Methods isProjP :: Pattern' a -> Maybe (ProjOrigin, AmbiguousQName) # | |
| IsProjP (Pattern' e) # | |
Defined in Agda.Syntax.Abstract Methods isProjP :: Pattern' e -> Maybe (ProjOrigin, AmbiguousQName) # | |
| IsProjP a => IsProjP (Named n a) # | |
Defined in Agda.Syntax.Abstract.Name Methods isProjP :: Named n a -> Maybe (ProjOrigin, AmbiguousQName) # | |
newtype AmbiguousQName #
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).
Constructors
| AmbQ | |
Fields | |
Instances
newtype ModuleName #
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
Something preceeded by a qualified name.
Instances
| Functor QNamed # | |
| Foldable QNamed # | |
Defined in Agda.Syntax.Abstract.Name Methods fold :: Monoid m => QNamed m -> m # foldMap :: Monoid m => (a -> m) -> QNamed a -> m # foldr :: (a -> b -> b) -> b -> QNamed a -> b # foldr' :: (a -> b -> b) -> b -> QNamed a -> b # foldl :: (b -> a -> b) -> b -> QNamed a -> b # foldl' :: (b -> a -> b) -> b -> QNamed a -> b # foldr1 :: (a -> a -> a) -> QNamed a -> a # foldl1 :: (a -> a -> a) -> QNamed a -> a # elem :: Eq a => a -> QNamed a -> Bool # maximum :: Ord a => QNamed a -> a # minimum :: Ord a => QNamed a -> a # | |
| Traversable QNamed # | |
| Show a => Show (QNamed a) # | Use |
| Pretty a => Pretty (QNamed a) # | |
Defined in Agda.Syntax.Abstract.Name | |
| PrettyTCM (QNamed Clause) # | |
| Reify (QNamed Clause) Clause # | |
| ToAbstract (QNamed Clause) Clause # | |
Defined in Agda.Syntax.Translation.ReflectedToAbstract | |
| ToAbstract [QNamed Clause] [Clause] # | |
Defined in Agda.Syntax.Translation.ReflectedToAbstract | |
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
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
unambiguous :: QName -> AmbiguousQName #
A singleton "ambiguous" name.
headAmbQ :: AmbiguousQName -> QName #
Get the first of the ambiguous names.
isAmbiguous :: AmbiguousQName -> Bool #
Is a name ambiguous.
getUnambiguous :: AmbiguousQName -> Maybe QName #
Get the name if unambiguous.
isAnonymousModuleName :: ModuleName -> Bool #
A module is anonymous if the qualification path ends in an underscore.
withRangesOf :: ModuleName -> [Name] -> ModuleName #
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 #
Like withRangesOf, but uses the name parts (qualifier + name)
of the qualified name as the list of concrete names.
mnameFromList :: [Name] -> ModuleName #
commonParentModule :: ModuleName -> ModuleName -> ModuleName #
qnameToList :: QName -> [Name] #
qnameFromList :: [Name] -> QName #
qnameToMName :: QName -> ModuleName #
mnameToQName :: ModuleName -> QName #
showQNameId :: QName -> String #
qnameToConcrete :: QName -> QName #
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 #
toTopLevelModuleName :: ModuleName -> TopLevelModuleName #
Computes the TopLevelModuleName corresponding to the given
module name, which is assumed to represent a top-level module name.
Precondition: The module name must be well-formed.
qualifyM :: ModuleName -> ModuleName -> ModuleName #
qualifyQ :: ModuleName -> QName -> QName #
qualify :: ModuleName -> Name -> QName #
isOperator :: QName -> Bool #
Is the name an operator?
isSubModuleOf :: ModuleName -> ModuleName -> Bool #
isInModule :: QName -> ModuleName -> Bool #
Get the next version of the concrete name. For instance, nextName "x" = "x₁".
The name must not be a NoName.
Check whether a name is the empty name "_".
Minimal complete definition
Instances
| IsNoName String # | |
Defined in Agda.Syntax.Concrete.Name | |
| IsNoName ByteString # | |
Defined in Agda.Syntax.Concrete.Name Methods isNoName :: ByteString -> Bool # | |
| IsNoName QName # | |
Defined in Agda.Syntax.Concrete.Name | |
| IsNoName Name # | |
Defined in Agda.Syntax.Concrete.Name | |
| IsNoName Name # | An abstract name is empty if its concrete name is empty. |
Defined in Agda.Syntax.Abstract.Name | |