Safe Haskell	None
Language	Haskell2010

Agda.Syntax.Abstract.Name

Description

Abstract names carry unique identifiers and stuff.

Synopsis

class MkName a where
- mkName :: Range -> NameId -> a -> Name
- mkName_ :: NameId -> a -> Name
class IsProjP a where
- isProjP :: a -> Maybe (ProjOrigin, AmbiguousQName)
newtype AmbiguousQName = AmbQ {
- unAmbQ :: NonEmpty QName
}
newtype ModuleName = MName {
- mnameToList :: [Name]
}
data QNamed a = QNamed {
- qname :: QName
- qnamed :: a
}
data QName = QName {
- qnameModule :: ModuleName
- qnameName :: Name
}
data Name = Name {
- nameId :: !NameId
- nameConcrete :: Name
- nameBindingSite :: Range
- nameFixity :: Fixity'
- nameIsRecordName :: Bool
}
uglyShowName :: Name -> String
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
isLeParentModuleOf :: ModuleName -> ModuleName -> Bool
isLtParentModuleOf :: ModuleName -> ModuleName -> Bool
isLeChildModuleOf :: ModuleName -> ModuleName -> Bool
isLtChildModuleOf :: ModuleName -> ModuleName -> Bool
isInModule :: QName -> ModuleName -> Bool
nextName :: Name -> Name
sameRoot :: Name -> Name -> Bool
lensQNameName :: Lens' Name QName
nameToArgName :: Name -> ArgName
namedArgName :: NamedArg Name -> ArgName
class IsNoName a where
- isNoName :: a -> Bool

Documentation

class MkName a where Source #

Make a Name from some kind of string.

Minimal complete definition

mkName

Methods

mkName :: Range -> NameId -> a -> Name Source #

The Range sets the definition site of the name, not the use site.

mkName_ :: NameId -> a -> Name Source #

Instances

Instances details

MkName String Source #
Instance details Defined in Agda.Syntax.Abstract.Name Methods mkName :: Range -> NameId -> String -> Name Source # mkName_ :: NameId -> String -> Name Source #

class IsProjP a where Source #

Check whether we are a projection pattern.

Methods

isProjP :: a -> Maybe (ProjOrigin, AmbiguousQName) Source #

Instances

Instances details

IsProjP Void Source #
Instance details Defined in Agda.Syntax.Abstract.Name Methods isProjP :: Void -> Maybe (ProjOrigin, AmbiguousQName) Source #
IsProjP Expr Source #
Instance details Defined in Agda.Syntax.Abstract Methods isProjP :: Expr -> Maybe (ProjOrigin, AmbiguousQName) Source #
IsProjP a => IsProjP (Arg a) Source #
Instance details Defined in Agda.Syntax.Abstract.Name Methods isProjP :: Arg a -> Maybe (ProjOrigin, AmbiguousQName) Source #
IsProjP (Pattern' a) Source #
Instance details Defined in Agda.Syntax.Internal Methods isProjP :: Pattern' a -> Maybe (ProjOrigin, AmbiguousQName) Source #
IsProjP (Pattern' e) Source #
Instance details Defined in Agda.Syntax.Abstract Methods isProjP :: Pattern' e -> Maybe (ProjOrigin, AmbiguousQName) Source #
IsProjP a => IsProjP (Named n a) Source #
Instance details Defined in Agda.Syntax.Abstract.Name Methods isProjP :: Named n a -> Maybe (ProjOrigin, AmbiguousQName) Source #

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).

Constructors

AmbQ
Fields unAmbQ :: NonEmpty QName

Instances

Instances details

Eq AmbiguousQName Source #
Instance details Defined in Agda.Syntax.Abstract.Name Methods (==) :: AmbiguousQName -> AmbiguousQName -> Bool # (/=) :: AmbiguousQName -> AmbiguousQName -> Bool #
Data AmbiguousQName Source #
Instance details Defined in Agda.Syntax.Abstract.Name Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> AmbiguousQName -> c AmbiguousQName # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c AmbiguousQName # toConstr :: AmbiguousQName -> Constr # dataTypeOf :: AmbiguousQName -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c AmbiguousQName) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c AmbiguousQName) # gmapT :: (forall b. Data b => b -> b) -> AmbiguousQName -> AmbiguousQName # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> AmbiguousQName -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> AmbiguousQName -> r # gmapQ :: (forall d. Data d => d -> u) -> AmbiguousQName -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> AmbiguousQName -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> AmbiguousQName -> m AmbiguousQName # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> AmbiguousQName -> m AmbiguousQName # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> AmbiguousQName -> m AmbiguousQName #
Ord AmbiguousQName Source #
Instance details 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 #
Show AmbiguousQName Source #
Instance details Defined in Agda.Syntax.Abstract.Name Methods showsPrec :: Int -> AmbiguousQName -> ShowS # show :: AmbiguousQName -> String # showList :: [AmbiguousQName] -> ShowS #
Pretty AmbiguousQName Source #
Instance details Defined in Agda.Syntax.Abstract.Name Methods pretty :: AmbiguousQName -> Doc Source # prettyPrec :: Int -> AmbiguousQName -> Doc Source # prettyList :: [AmbiguousQName] -> Doc Source #
KillRange AmbiguousQName Source #
Instance details Defined in Agda.Syntax.Abstract.Name Methods killRange :: KillRangeT AmbiguousQName Source #
HasRange AmbiguousQName Source #	The range of an `AmbiguousQName` is the range of any of its disambiguations (they are the same concrete name).
Instance details Defined in Agda.Syntax.Abstract.Name Methods getRange :: AmbiguousQName -> Range Source #
NumHoles AmbiguousQName Source #	We can have an instance for ambiguous names as all share a common concrete name.
Instance details Defined in Agda.Syntax.Abstract.Name Methods numHoles :: AmbiguousQName -> Int Source #
EmbPrj AmbiguousQName Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: AmbiguousQName -> S Int32 Source # icod_ :: AmbiguousQName -> S Int32 Source # value :: Int32 -> R AmbiguousQName Source #
NamesIn AmbiguousQName Source #
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: AmbiguousQName -> Set QName Source #
UniverseBi Declaration AmbiguousQName
Instance details Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [AmbiguousQName]

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 mnameToList :: [Name]

Instances

Instances details

Eq ModuleName Source #
Instance details Defined in Agda.Syntax.Abstract.Name Methods (==) :: ModuleName -> ModuleName -> Bool # (/=) :: ModuleName -> ModuleName -> Bool #
Data ModuleName Source #
Instance details Defined in Agda.Syntax.Abstract.Name Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ModuleName -> c ModuleName # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ModuleName # toConstr :: ModuleName -> Constr # dataTypeOf :: ModuleName -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ModuleName) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ModuleName) # gmapT :: (forall b. Data b => b -> b) -> ModuleName -> ModuleName # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ModuleName -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ModuleName -> r # gmapQ :: (forall d. Data d => d -> u) -> ModuleName -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> ModuleName -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> ModuleName -> m ModuleName # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ModuleName -> m ModuleName # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ModuleName -> m ModuleName #
Ord ModuleName Source #
Instance details 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 #
Show ModuleName Source #	Only use this `show` function in debugging! To convert an abstract `ModuleName` into a string use `prettyShow`.
Instance details Defined in Agda.Syntax.Abstract.Name Methods showsPrec :: Int -> ModuleName -> ShowS # show :: ModuleName -> String # showList :: [ModuleName] -> ShowS #
NFData ModuleName Source #
Instance details Defined in Agda.Syntax.Abstract.Name Methods rnf :: ModuleName -> () #
Sized ModuleName Source #
Instance details Defined in Agda.Syntax.Abstract.Name Methods size :: ModuleName -> Int Source #
Pretty ModuleName Source #
Instance details Defined in Agda.Syntax.Abstract.Name Methods pretty :: ModuleName -> Doc Source # prettyPrec :: Int -> ModuleName -> Doc Source # prettyList :: [ModuleName] -> Doc Source #
KillRange ModuleName Source #
Instance details Defined in Agda.Syntax.Abstract.Name Methods killRange :: KillRangeT ModuleName Source #
KillRange Sections Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT Sections Source #
SetRange ModuleName Source #
Instance details Defined in Agda.Syntax.Abstract.Name Methods setRange :: Range -> ModuleName -> ModuleName Source #
HasRange ModuleName Source #
Instance details Defined in Agda.Syntax.Abstract.Name Methods getRange :: ModuleName -> Range Source #
SetBindingSite ModuleName Source #	Sets the binding site of all names in the path.
Instance details Defined in Agda.Syntax.Scope.Base Methods setBindingSite :: Range -> ModuleName -> ModuleName Source #
SubstExpr ModuleName Source #
Instance details Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name, Expr)] -> ModuleName -> ModuleName Source #
ExprLike ModuleName Source #
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> ModuleName -> m ModuleName Source # foldExpr :: Monoid m => (Expr -> m) -> ModuleName -> m Source # traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> ModuleName -> m ModuleName Source # mapExpr :: (Expr -> Expr) -> ModuleName -> ModuleName Source #
EmbPrj ModuleName Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: ModuleName -> S Int32 Source # icod_ :: ModuleName -> S Int32 Source # value :: Int32 -> R ModuleName Source #
PrettyTCM ModuleName Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => ModuleName -> m Doc Source #
InstantiateFull ModuleName Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: ModuleName -> ReduceM ModuleName Source #
UniverseBi Declaration ModuleName
Instance details Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [ModuleName]
ToConcrete ModuleName QName Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: ModuleName -> AbsToCon QName Source # bindToConcrete :: ModuleName -> (QName -> AbsToCon b) -> AbsToCon b Source #
ToAbstract OldModuleName ModuleName Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: OldModuleName -> ScopeM ModuleName Source #
ToAbstract NewModuleQName ModuleName Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: NewModuleQName -> ScopeM ModuleName Source #
ToAbstract NewModuleName ModuleName Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: NewModuleName -> ScopeM ModuleName Source #
ToAbstract ModuleAssignment (ModuleName, [LetBinding]) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: ModuleAssignment -> ScopeM (ModuleName, [LetBinding]) Source #

data QNamed a Source #

Something preceeded by a qualified name.

Constructors

QNamed
Fields qname :: QName qnamed :: a

Instances

Instances details

Functor QNamed Source #
Instance details Defined in Agda.Syntax.Abstract.Name Methods fmap :: (a -> b) -> QNamed a -> QNamed b # (<$) :: a -> QNamed b -> QNamed a #
Foldable QNamed Source #
Instance details 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 # toList :: QNamed a -> [a] # null :: QNamed a -> Bool # length :: QNamed a -> Int # elem :: Eq a => a -> QNamed a -> Bool # maximum :: Ord a => QNamed a -> a # minimum :: Ord a => QNamed a -> a # sum :: Num a => QNamed a -> a # product :: Num a => QNamed a -> a #
Traversable QNamed Source #
Instance details Defined in Agda.Syntax.Abstract.Name Methods traverse :: Applicative f => (a -> f b) -> QNamed a -> f (QNamed b) # sequenceA :: Applicative f => QNamed (f a) -> f (QNamed a) # mapM :: Monad m => (a -> m b) -> QNamed a -> m (QNamed b) # sequence :: Monad m => QNamed (m a) -> m (QNamed a) #
Show a => Show (QNamed a) Source #	Use `prettyShow` to print names to the user.
Instance details Defined in Agda.Syntax.Abstract.Name Methods showsPrec :: Int -> QNamed a -> ShowS # show :: QNamed a -> String # showList :: [QNamed a] -> ShowS #
Pretty a => Pretty (QNamed a) Source #
Instance details Defined in Agda.Syntax.Abstract.Name Methods pretty :: QNamed a -> Doc Source # prettyPrec :: Int -> QNamed a -> Doc Source # prettyList :: [QNamed a] -> Doc Source #
PrettyTCM (QNamed Clause) Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => QNamed Clause -> m Doc Source #
ToAbstract (QNamed Clause) Clause Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: MonadReflectedToAbstract m => QNamed Clause0 -> m Clause Source #
Reify (QNamed Clause) Clause Source #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: MonadReify m => QNamed Clause0 -> m Clause Source # reifyWhen :: MonadReify m => Bool -> QNamed Clause0 -> m Clause Source #
ToAbstract [QNamed Clause] [Clause] Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: MonadReflectedToAbstract m => [QNamed Clause0] -> m [Clause] Source #
Reify (QNamed System) [Clause] Source #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: MonadReify m => QNamed System -> m [Clause] Source # reifyWhen :: MonadReify m => Bool -> QNamed System -> m [Clause] Source #

data QName Source #

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 qnameModule :: ModuleName qnameName :: Name

Instances

Instances details

Eq QName Source #
Instance details Defined in Agda.Syntax.Abstract.Name Methods (==) :: QName -> QName -> Bool # (/=) :: QName -> QName -> Bool #
Data QName Source #
Instance details Defined in Agda.Syntax.Abstract.Name Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> QName -> c QName # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c QName # toConstr :: QName -> Constr # dataTypeOf :: QName -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c QName) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c QName) # gmapT :: (forall b. Data b => b -> b) -> QName -> QName # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> QName -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> QName -> r # gmapQ :: (forall d. Data d => d -> u) -> QName -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> QName -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> QName -> m QName # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> QName -> m QName # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> QName -> m QName #
Ord QName Source #
Instance details Defined in Agda.Syntax.Abstract.Name Methods compare :: QName -> QName -> Ordering # (<) :: QName -> QName -> Bool # (<=) :: QName -> QName -> Bool # (>) :: QName -> QName -> Bool # (>=) :: QName -> QName -> Bool # max :: QName -> QName -> QName # min :: QName -> QName -> QName #
Show QName Source #	Only use this `show` function in debugging! To convert an abstract `QName` into a string use `prettyShow`.
Instance details Defined in Agda.Syntax.Abstract.Name Methods showsPrec :: Int -> QName -> ShowS # show :: QName -> String # showList :: [QName] -> ShowS #
NFData QName Source #
Instance details Defined in Agda.Syntax.Abstract.Name Methods rnf :: QName -> () #
Hashable QName Source #
Instance details Defined in Agda.Syntax.Abstract.Name Methods hashWithSalt :: Int -> QName -> Int hash :: QName -> Int
Sized QName Source #
Instance details Defined in Agda.Syntax.Abstract.Name Methods size :: QName -> Int Source #
Pretty QName Source #
Instance details Defined in Agda.Syntax.Abstract.Name Methods pretty :: QName -> Doc Source # prettyPrec :: Int -> QName -> Doc Source # prettyList :: [QName] -> Doc Source #
KillRange QName Source #
Instance details Defined in Agda.Syntax.Abstract.Name Methods killRange :: KillRangeT QName Source #
KillRange RewriteRuleMap Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT RewriteRuleMap Source #
KillRange Definitions Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT Definitions Source #
SetRange QName Source #
Instance details Defined in Agda.Syntax.Abstract.Name Methods setRange :: Range -> QName -> QName Source #
HasRange QName Source #
Instance details Defined in Agda.Syntax.Abstract.Name Methods getRange :: QName -> Range Source #
LensFixity' QName Source #
Instance details Defined in Agda.Syntax.Abstract.Name Methods lensFixity' :: Lens' Fixity' QName Source #
LensFixity QName Source #
Instance details Defined in Agda.Syntax.Abstract.Name Methods lensFixity :: Lens' Fixity QName Source #
LensInScope QName Source #
Instance details Defined in Agda.Syntax.Abstract.Name Methods lensInScope :: Lens' NameInScope QName Source # isInScope :: QName -> NameInScope Source # mapInScope :: (NameInScope -> NameInScope) -> QName -> QName Source # setInScope :: QName -> QName Source # setNotInScope :: QName -> QName Source #
NumHoles QName Source #
Instance details Defined in Agda.Syntax.Abstract.Name Methods numHoles :: QName -> Int Source #
SetBindingSite QName Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods setBindingSite :: Range -> QName -> QName Source #
TermLike QName Source #
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> QName -> m QName Source # foldTerm :: Monoid m => (Term -> m) -> QName -> m Source #
AllNames QName Source #
Instance details Defined in Agda.Syntax.Abstract Methods allNames :: QName -> Seq QName Source #
ExprLike QName Source #
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> QName -> m QName Source # foldExpr :: Monoid m => (Expr -> m) -> QName -> m Source # traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> QName -> m QName Source # mapExpr :: (Expr -> Expr) -> QName -> QName Source #
EmbPrj QName Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: QName -> S Int32 Source # icod_ :: QName -> S Int32 Source # value :: Int32 -> R QName Source #
PrettyTCM QName Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => QName -> m Doc Source #
NamesIn QName Source #
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: QName -> Set QName Source #
InstantiateFull QName Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: QName -> ReduceM QName Source #
FromTerm QName Source #
Instance details Defined in Agda.TypeChecking.Primitive Methods fromTerm :: TCM (FromTermFunction QName) Source #
ToTerm QName Source #
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (QName -> Term) Source # toTermR :: TCM (QName -> ReduceM Term) Source #
PrimTerm QName Source #
Instance details Defined in Agda.TypeChecking.Primitive Methods primTerm :: QName -> TCM Term Source #
Occurs QName Source #
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: QName -> OccursM QName Source # metaOccurs :: MetaId -> QName -> TCM () Source #
Unquote QName Source #
Instance details Defined in Agda.TypeChecking.Unquote Methods unquote :: Term -> UnquoteM QName Source #
UniverseBi Declaration QName
Instance details Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [QName]
Subst Term QName Source #
Instance details Defined in Agda.TypeChecking.Substitute.Class Methods applySubst :: Substitution' Term -> QName -> QName Source #
ToConcrete QName QName Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: QName -> AbsToCon QName0 Source # bindToConcrete :: QName -> (QName0 -> AbsToCon b) -> AbsToCon b Source #
Conversion TOM Clause (Maybe ([Pat O], MExp O)) Source #
Instance details Defined in Agda.Auto.Convert Methods convert :: Clause -> TOM (Maybe ([Pat O], MExp O)) Source #
Conversion TOM Type (MExp O) Source #
Instance details Defined in Agda.Auto.Convert Methods convert :: Type -> TOM (MExp O) Source #
Conversion TOM Term (MExp O) Source #
Instance details Defined in Agda.Auto.Convert Methods convert :: Term -> TOM (MExp O) Source #
Conversion TOM Args (MM (ArgList O) (RefInfo O)) Source #
Instance details Defined in Agda.Auto.Convert Methods convert :: Args -> TOM (MM (ArgList O) (RefInfo O)) Source #
Conversion MOT (Exp O) Type Source #
Instance details Defined in Agda.Auto.Convert Methods convert :: Exp O -> MOT Type Source #
Conversion MOT (Exp O) Term Source #
Instance details Defined in Agda.Auto.Convert Methods convert :: Exp O -> MOT Term Source #
Conversion TOM [Clause] [([Pat O], MExp O)] Source #
Instance details Defined in Agda.Auto.Convert Methods convert :: [Clause] -> TOM [([Pat O], MExp O)] Source #
Conversion TOM (Arg Pattern) (Pat O) Source #
Instance details Defined in Agda.Auto.Convert Methods convert :: Arg Pattern -> TOM (Pat O) Source #
Conversion MOT a b => Conversion MOT (MM a (RefInfo O)) b Source #
Instance details Defined in Agda.Auto.Convert Methods convert :: MM a (RefInfo O) -> MOT b Source #
(Show a, ToQName a) => ToAbstract (OldName a) QName Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: OldName a -> ScopeM QName Source #
ToConcrete (Maybe QName) (Maybe Name) Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: Maybe QName -> AbsToCon (Maybe Name) Source # bindToConcrete :: Maybe QName -> (Maybe Name -> AbsToCon b) -> AbsToCon b Source #
ToAbstract (RewriteEqn' () Pattern Expr) RewriteEqn Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: RewriteEqn' () Pattern Expr -> ScopeM RewriteEqn Source #

data Name Source #

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 nameId :: !NameId nameConcrete :: Name nameBindingSite :: Range nameFixity :: Fixity' nameIsRecordName :: Bool Is this the name of the invisible record variable `self`? Should not be printed or displayed in the context, see issue #3584.

Instances

Instances details

Eq Name Source #
Instance details Defined in Agda.Syntax.Abstract.Name Methods (==) :: Name -> Name -> Bool # (/=) :: Name -> Name -> Bool #
Data Name Source #
Instance details Defined in Agda.Syntax.Abstract.Name Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Name -> c Name # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Name # toConstr :: Name -> Constr # dataTypeOf :: Name -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Name) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Name) # gmapT :: (forall b. Data b => b -> b) -> Name -> Name # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Name -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Name -> r # gmapQ :: (forall d. Data d => d -> u) -> Name -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Name -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Name -> m Name # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Name -> m Name # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Name -> m Name #
Ord Name Source #
Instance details Defined in Agda.Syntax.Abstract.Name Methods compare :: Name -> Name -> Ordering # (<) :: Name -> Name -> Bool # (<=) :: Name -> Name -> Bool # (>) :: Name -> Name -> Bool # (>=) :: Name -> Name -> Bool # max :: Name -> Name -> Name # min :: Name -> Name -> Name #
Show Name Source #	Only use this `show` function in debugging! To convert an abstract `Name` into a string use `prettyShow`.
Instance details Defined in Agda.Syntax.Abstract.Name Methods showsPrec :: Int -> Name -> ShowS # show :: Name -> String # showList :: [Name] -> ShowS #
NFData Name Source #	The range is not forced.
Instance details Defined in Agda.Syntax.Abstract.Name Methods rnf :: Name -> () #
Hashable Name Source #
Instance details Defined in Agda.Syntax.Abstract.Name Methods hashWithSalt :: Int -> Name -> Int hash :: Name -> Int
Pretty Name Source #
Instance details Defined in Agda.Syntax.Abstract.Name Methods pretty :: Name -> Doc Source # prettyPrec :: Int -> Name -> Doc Source # prettyList :: [Name] -> Doc Source #
KillRange Name Source #
Instance details Defined in Agda.Syntax.Abstract.Name Methods killRange :: KillRangeT Name Source #
SetRange Name Source #
Instance details Defined in Agda.Syntax.Abstract.Name Methods setRange :: Range -> Name -> Name Source #
HasRange Name Source #
Instance details Defined in Agda.Syntax.Abstract.Name Methods getRange :: Name -> Range Source #
LensFixity' Name Source #
Instance details Defined in Agda.Syntax.Abstract.Name Methods lensFixity' :: Lens' Fixity' Name Source #
LensFixity Name Source #
Instance details Defined in Agda.Syntax.Abstract.Name Methods lensFixity :: Lens' Fixity Name Source #
IsNoName Name Source #	An abstract name is empty if its concrete name is empty.
Instance details Defined in Agda.Syntax.Abstract.Name Methods isNoName :: Name -> Bool Source #
LensInScope Name Source #
Instance details Defined in Agda.Syntax.Abstract.Name Methods lensInScope :: Lens' NameInScope Name Source # isInScope :: Name -> NameInScope Source # mapInScope :: (NameInScope -> NameInScope) -> Name -> Name Source # setInScope :: Name -> Name Source # setNotInScope :: Name -> Name Source #
NumHoles Name Source #
Instance details Defined in Agda.Syntax.Abstract.Name Methods numHoles :: Name -> Int Source #
SetBindingSite Name Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods setBindingSite :: Range -> Name -> Name Source #
Suggest Name Source #
Instance details Defined in Agda.Syntax.Internal Methods suggestName :: Name -> Maybe String Source #
EmbPrj Name Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Name -> S Int32 Source # icod_ :: Name -> S Int32 Source # value :: Int32 -> R Name Source #
PrettyTCM Name Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Name -> m Doc Source #
AddContext Name Source #
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => Name -> m a -> m a Source # contextSize :: Name -> Nat Source #
InstantiateFull Name Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Name -> ReduceM Name Source #
Subst Term Name Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> Name -> Name Source #
ToConcrete Name Name Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: Name -> AbsToCon Name0 Source # bindToConcrete :: Name -> (Name0 -> AbsToCon b) -> AbsToCon b Source #
Reify Name Name Source #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: MonadReify m => Name -> m Name Source # reifyWhen :: MonadReify m => Bool -> Name -> m Name Source #
ToAbstract Pattern (Names, Pattern) Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: MonadReflectedToAbstract m => Pattern0 -> m (Names, Pattern) Source #
AddContext (Dom (Name, Type)) Source #
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => Dom (Name, Type) -> m a -> m a Source # contextSize :: Dom (Name, Type) -> Nat Source #
ToAbstract (NewName Name) Name Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: NewName Name0 -> ScopeM Name Source #
ToAbstract r a => ToAbstract (Abs r) (a, Name) Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: MonadReflectedToAbstract m => Abs r -> m (a, Name) Source #
(Free i, Reify i a) => Reify (Abs i) (Name, a) Source #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: MonadReify m => Abs i -> m (Name, a) Source # reifyWhen :: MonadReify m => Bool -> Abs i -> m (Name, a) Source #
AddContext ([NamedArg Name], Type) Source #
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => ([NamedArg Name], Type) -> m a -> m a Source # contextSize :: ([NamedArg Name], Type) -> Nat Source #
AddContext ([Arg Name], Type) Source #
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => ([Arg Name], Type) -> m a -> m a Source # contextSize :: ([Arg Name], Type) -> Nat Source #
AddContext ([WithHiding Name], Dom Type) Source #
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => ([WithHiding Name], Dom Type) -> m a -> m a Source # contextSize :: ([WithHiding Name], Dom Type) -> Nat Source #
AddContext ([Name], Dom Type) Source #
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => ([Name], Dom Type) -> m a -> m a Source # contextSize :: ([Name], Dom Type) -> Nat Source #
AddContext (Name, Dom Type) Source #
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => (Name, Dom Type) -> m a -> m a Source # contextSize :: (Name, Dom Type) -> Nat Source #
ToAbstract r Expr => ToAbstract (Dom r, Name) TypedBinding Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: MonadReflectedToAbstract m => (Dom r, Name) -> m TypedBinding Source #

uglyShowName :: Name -> String Source #

Useful for debugging scoping problems

unambiguous :: QName -> AmbiguousQName Source #

A singleton "ambiguous" name.

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 -> [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 of A.
E: the range of B.

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 #

noModuleName :: ModuleName Source #

commonParentModule :: ModuleName -> ModuleName -> ModuleName Source #

qnameToList :: QName -> [Name] Source #

qnameFromList :: [Name] -> QName 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 #

toTopLevelModuleName :: ModuleName -> TopLevelModuleName Source #

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 Source #

qualifyQ :: ModuleName -> QName -> QName Source #

qualify :: ModuleName -> Name -> QName Source #

qualify_ :: Name -> QName Source #

Convert a Name to a QName (add no module name).

isOperator :: QName -> Bool Source #

Is the name an operator?

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 #

nextName :: Name -> Name Source #

Get the next version of the concrete name. For instance, nextName "x" = "x₁". The name must not be a NoName.

sameRoot :: Name -> Name -> Bool Source #

lensQNameName :: Lens' Name QName Source #

nameToArgName :: Name -> ArgName Source #

namedArgName :: NamedArg Name -> ArgName Source #

class IsNoName a where Source #

Check whether a name is the empty name "_".

Minimal complete definition

Nothing

Methods

isNoName :: a -> Bool Source #

default isNoName :: (Foldable t, IsNoName b, t b ~ a) => a -> Bool Source #

Instances

Instances details

IsNoName String Source #
Instance details Defined in Agda.Syntax.Concrete.Name Methods isNoName :: String -> Bool Source #
IsNoName ByteString Source #
Instance details Defined in Agda.Syntax.Concrete.Name Methods isNoName :: ByteString -> Bool Source #
IsNoName QName Source #
Instance details Defined in Agda.Syntax.Concrete.Name Methods isNoName :: QName -> Bool Source #
IsNoName Name Source #
Instance details Defined in Agda.Syntax.Concrete.Name Methods isNoName :: Name -> Bool Source #
IsNoName Name Source #	An abstract name is empty if its concrete name is empty.
Instance details Defined in Agda.Syntax.Abstract.Name Methods isNoName :: Name -> Bool Source #
IsNoName a => IsNoName (Ranged a) Source #
Instance details Defined in Agda.Syntax.Concrete.Name Methods isNoName :: Ranged a -> Bool Source #
IsNoName a => IsNoName (WithOrigin a) Source #
Instance details Defined in Agda.Syntax.Concrete.Name Methods isNoName :: WithOrigin a -> Bool Source #