Safe Haskell | None |
---|---|
Language | Haskell2010 |
Agda.Syntax.Abstract.Name
Description
Abstract names carry unique identifiers and stuff.
Synopsis
- class MkName a where
- data Name = Name {}
- data QName = QName {}
- newtype ModuleName = MName {
- mnameToList :: [Name]
- class IsProjP a where
- isProjP :: a -> Maybe (ProjOrigin, AmbiguousQName)
- data Suffix
- data QNamed a = QNamed {}
- 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
- newtype AmbiguousQName = AmbQ {}
- 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
Make a Name
from some kind of string.
Minimal complete definition
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
DeclaredNames RecordDirectives Source # | |||||
Defined in Agda.Syntax.Abstract.Views Methods declaredNames :: Collection KName m => RecordDirectives -> m Source # | |||||
DeclaredNames KName Source # | |||||
Defined in Agda.Syntax.Abstract.Views Methods declaredNames :: Collection KName m => KName -> m Source # | |||||
ExprLike QName Source # | |||||
Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m QName Source # foldExpr :: FoldExprFn m QName Source # | |||||
LensFixity QName Source # | |||||
Defined in Agda.Syntax.Abstract.Name | |||||
LensFixity' QName Source # | |||||
Defined in Agda.Syntax.Abstract.Name | |||||
Pretty QName Source # | |||||
LensInScope QName Source # | |||||
Defined in Agda.Syntax.Abstract.Name Methods 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 # | |||||
TermLike QName Source # | |||||
NamesIn QName Source # | |||||
Defined in Agda.Syntax.Internal.Names | |||||
HasRange QName Source # | |||||
KillRange QName Source # | |||||
Defined in Agda.Syntax.Abstract.Name Methods | |||||
KillRange Definitions Source # | |||||
Defined in Agda.TypeChecking.Monad.Base Methods | |||||
KillRange RewriteRuleMap Source # | |||||
Defined in Agda.TypeChecking.Monad.Base Methods | |||||
SetRange QName Source # | |||||
SetBindingSite QName Source # | |||||
Defined in Agda.Syntax.Scope.Base | |||||
ToConcrete QName Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types
| |||||
Occurs QName Source # | |||||
PrettyTCM QName Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
FromTerm QName Source # | |||||
Defined in Agda.TypeChecking.Primitive | |||||
PrimTerm QName Source # | |||||
PrimType QName Source # | |||||
ToTerm QName Source # | |||||
InstantiateFull QName Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
EmbPrj QName Source # | |||||
Subst QName Source # | |||||
Defined in Agda.TypeChecking.Substitute.Class Associated Types
Methods applySubst :: Substitution' (SubstArg QName) -> QName -> QName Source # | |||||
Unquote QName Source # | |||||
Sized QName Source # | |||||
Show QName Source # | |||||
NFData QName Source # | |||||
Defined in Agda.Syntax.Abstract.Name | |||||
Eq QName Source # | |||||
Ord QName Source # | |||||
Hashable QName Source # | |||||
Defined in Agda.Syntax.Abstract.Name | |||||
Conversion TOM Clause (Maybe ([Pat O], MExp O)) Source # | |||||
Conversion TOM Term (MExp O) Source # | |||||
Conversion TOM Type (MExp O) Source # | |||||
Conversion TOM Args (MM (ArgList O) (RefInfo O)) Source # | |||||
Conversion MOT (Exp O) Term Source # | |||||
Conversion MOT (Exp O) Type Source # | |||||
Conversion TOM (Arg Pattern) (Pat O) Source # | |||||
Conversion TOM [Clause] [([Pat O], MExp O)] Source # | |||||
Conversion MOT a b => Conversion MOT (MM a (RefInfo O)) b Source # | |||||
ToConcrete (Maybe QName) Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete | |||||
type ConOfAbs QName Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete | |||||
type SubstArg QName Source # | |||||
Defined in Agda.TypeChecking.Substitute.Class | |||||
type ConOfAbs (Maybe QName) Source # | |||||
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
SubstExpr ModuleName Source # | |||||
Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name, Expr)] -> ModuleName -> ModuleName Source # | |||||
ExprLike ModuleName Source # | |||||
Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m ModuleName Source # foldExpr :: FoldExprFn m ModuleName Source # traverseExpr :: TraverseExprFn m ModuleName Source # mapExpr :: (Expr -> Expr) -> ModuleName -> ModuleName Source # | |||||
Pretty ModuleName Source # | |||||
Defined in Agda.Syntax.Abstract.Name Methods pretty :: ModuleName -> Doc Source # prettyPrec :: Int -> ModuleName -> Doc Source # prettyList :: [ModuleName] -> Doc Source # | |||||
HasRange ModuleName Source # | |||||
Defined in Agda.Syntax.Abstract.Name Methods getRange :: ModuleName -> Range Source # | |||||
KillRange ModuleName Source # | |||||
Defined in Agda.Syntax.Abstract.Name Methods | |||||
KillRange Sections Source # | |||||
Defined in Agda.TypeChecking.Monad.Base Methods | |||||
SetRange ModuleName Source # | |||||
Defined in Agda.Syntax.Abstract.Name Methods setRange :: Range -> ModuleName -> ModuleName Source # | |||||
SetBindingSite ModuleName Source # | Sets the binding site of all names in the path. | ||||
Defined in Agda.Syntax.Scope.Base Methods setBindingSite :: Range -> ModuleName -> ModuleName Source # | |||||
ToConcrete ModuleName Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types
Methods toConcrete :: ModuleName -> AbsToCon (ConOfAbs ModuleName) Source # bindToConcrete :: ModuleName -> (ConOfAbs ModuleName -> AbsToCon b) -> AbsToCon b Source # | |||||
PrettyTCM ModuleName Source # | |||||
Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => ModuleName -> m Doc Source # | |||||
InstantiateFull ModuleName Source # | |||||
Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: ModuleName -> ReduceM ModuleName Source # | |||||
EmbPrj ModuleName Source # | |||||
Defined in Agda.TypeChecking.Serialise.Instances.Common | |||||
Sized ModuleName Source # | |||||
Defined in Agda.Syntax.Abstract.Name | |||||
Show ModuleName Source # | |||||
Defined in Agda.Syntax.Abstract.Name Methods showsPrec :: Int -> ModuleName -> ShowS # show :: ModuleName -> String # showList :: [ModuleName] -> ShowS # | |||||
NFData ModuleName Source # | |||||
Defined in Agda.Syntax.Abstract.Name Methods rnf :: ModuleName -> () # | |||||
Eq ModuleName Source # | |||||
Defined in Agda.Syntax.Abstract.Name | |||||
Ord ModuleName Source # | |||||
Defined in Agda.Syntax.Abstract.Name Methods compare :: ModuleName -> ModuleName -> Ordering # (<) :: ModuleName -> ModuleName -> Bool # (<=) :: ModuleName -> ModuleName -> Bool # (>) :: ModuleName -> ModuleName -> Bool # (>=) :: ModuleName -> ModuleName -> Bool # max :: ModuleName -> ModuleName -> ModuleName # min :: ModuleName -> ModuleName -> ModuleName # | |||||
type ConOfAbs ModuleName Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete |
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
Foldable QNamed Source # | |||||
Defined in Agda.Syntax.Abstract.Name Methods fold :: Monoid m => QNamed m -> m # foldMap :: Monoid m => (a -> m) -> QNamed a -> 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 Source # | |||||
Functor QNamed Source # | |||||
Pretty a => Pretty (QNamed a) Source # | |||||
Reify (QNamed Clause) Source # | |||||
Defined in Agda.Syntax.Translation.InternalToAbstract Associated Types
| |||||
Reify (QNamed System) Source # | |||||
Defined in Agda.Syntax.Translation.InternalToAbstract Associated Types
| |||||
ToAbstract (QNamed Clause) Source # | |||||
Defined in Agda.Syntax.Translation.ReflectedToAbstract Associated Types
Methods toAbstract :: MonadReflectedToAbstract m => QNamed Clause -> m (AbsOfRef (QNamed Clause)) Source # | |||||
ToAbstract (List1 (QNamed Clause)) Source # | |||||
Defined in Agda.Syntax.Translation.ReflectedToAbstract | |||||
ToAbstract [QNamed Clause] Source # | |||||
Defined in Agda.Syntax.Translation.ReflectedToAbstract Associated Types
Methods toAbstract :: MonadReflectedToAbstract m => [QNamed Clause] -> m (AbsOfRef [QNamed Clause]) Source # | |||||
PrettyTCM (QNamed Clause) Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
Show a => Show (QNamed a) Source # | |||||
type ReifiesTo (QNamed Clause) Source # | |||||
Defined in Agda.Syntax.Translation.InternalToAbstract | |||||
type ReifiesTo (QNamed System) Source # | |||||
Defined in Agda.Syntax.Translation.InternalToAbstract | |||||
type AbsOfRef (QNamed Clause) Source # | |||||
Defined in Agda.Syntax.Translation.ReflectedToAbstract | |||||
type AbsOfRef (List1 (QNamed Clause)) Source # | |||||
type AbsOfRef [QNamed Clause] Source # | |||||
Defined in Agda.Syntax.Translation.ReflectedToAbstract |
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
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
Pretty AmbiguousQName Source # | |
Defined in Agda.Syntax.Abstract.Name Methods pretty :: AmbiguousQName -> Doc Source # prettyPrec :: Int -> AmbiguousQName -> Doc Source # prettyList :: [AmbiguousQName] -> Doc Source # | |
NumHoles AmbiguousQName Source # | We can have an instance for ambiguous names as all share a common concrete name. |
Defined in Agda.Syntax.Abstract.Name Methods numHoles :: AmbiguousQName -> Int Source # | |
NamesIn AmbiguousQName Source # | |
Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> AmbiguousQName -> m Source # | |
HasRange AmbiguousQName Source # | The range of an |
Defined in Agda.Syntax.Abstract.Name Methods getRange :: AmbiguousQName -> Range Source # | |
KillRange AmbiguousQName Source # | |
Defined in Agda.Syntax.Abstract.Name Methods | |
EmbPrj AmbiguousQName Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Common | |
Show AmbiguousQName Source # | |
Defined in Agda.Syntax.Abstract.Name Methods showsPrec :: Int -> AmbiguousQName -> ShowS # show :: AmbiguousQName -> String # showList :: [AmbiguousQName] -> ShowS # | |
NFData AmbiguousQName Source # | |
Defined in Agda.Syntax.Abstract.Name Methods rnf :: AmbiguousQName -> () # | |
Eq AmbiguousQName Source # | |
Defined in Agda.Syntax.Abstract.Name Methods (==) :: AmbiguousQName -> AmbiguousQName -> Bool # (/=) :: AmbiguousQName -> AmbiguousQName -> Bool # | |
Ord AmbiguousQName Source # | |
Defined in Agda.Syntax.Abstract.Name Methods compare :: AmbiguousQName -> AmbiguousQName -> Ordering # (<) :: AmbiguousQName -> AmbiguousQName -> Bool # (<=) :: AmbiguousQName -> AmbiguousQName -> Bool # (>) :: AmbiguousQName -> AmbiguousQName -> Bool # (>=) :: AmbiguousQName -> AmbiguousQName -> Bool # max :: AmbiguousQName -> AmbiguousQName -> AmbiguousQName # min :: AmbiguousQName -> AmbiguousQName -> AmbiguousQName # |
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, … |