Agda.Syntax.Abstract.Name

Abstract names carry unique identifiers and stuff.

Documentation

class MkName a where

Make a Name from some kind of string.

Minimal complete definition

mkName

Methods

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

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

mkName_ :: NameId -> a -> Name

Instances

MkName String

Defined in Agda.Syntax.Abstract.Name

Methods

mkName :: Range -> NameId -> String -> Name

mkName_ :: NameId -> String -> Name

class IsProjP a where

Check whether we are a projection pattern.

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

• unAmbQ :: NonEmpty QName

Instances

Eq AmbiguousQName

Defined in Agda.Syntax.Abstract.Name

Methods

(==) :: AmbiguousQName -> AmbiguousQName -> Bool

(/=) :: AmbiguousQName -> AmbiguousQName -> Bool

Data AmbiguousQName

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

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

Defined in Agda.Syntax.Abstract.Name

Methods

showsPrec :: Int -> AmbiguousQName -> ShowS

show :: AmbiguousQName -> String

showList :: [AmbiguousQName] -> ShowS

Pretty AmbiguousQName

Defined in Agda.Syntax.Abstract.Name

Methods

pretty :: AmbiguousQName -> Doc

prettyPrec :: Int -> AmbiguousQName -> Doc

prettyList :: [AmbiguousQName] -> Doc

KillRange AmbiguousQName

Defined in Agda.Syntax.Abstract.Name

Methods

killRange :: KillRangeT AmbiguousQName

HasRange AmbiguousQName

The range of an AmbiguousQName is the range of any of its disambiguations (they are the same concrete name).

Defined in Agda.Syntax.Abstract.Name

Methods

getRange :: AmbiguousQName -> Range

NumHoles AmbiguousQName

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

EmbPrj AmbiguousQName

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: AmbiguousQName -> S Int32

icod_ :: AmbiguousQName -> S Int32

value :: Int32 -> R AmbiguousQName

NamesIn AmbiguousQName

Defined in Agda.Syntax.Internal.Names

Methods

namesIn :: AmbiguousQName -> Set QName

UniverseBi Declaration AmbiguousQName

Defined in Agda.Syntax.Abstract

Methods

universeBi :: Declaration -> [AmbiguousQName]

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

• mnameToList :: [Name]

Instances

Eq ModuleName

Defined in Agda.Syntax.Abstract.Name

Methods

(==) :: ModuleName -> ModuleName -> Bool

(/=) :: ModuleName -> ModuleName -> Bool

Data ModuleName

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

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

Only use this show function in debugging! To convert an abstract ModuleName into a string use prettyShow.

Defined in Agda.Syntax.Abstract.Name

Methods

showsPrec :: Int -> ModuleName -> ShowS

show :: ModuleName -> String

showList :: [ModuleName] -> ShowS

NFData ModuleName

Defined in Agda.Syntax.Abstract.Name

Methods

rnf :: ModuleName -> ()

Sized ModuleName

Defined in Agda.Syntax.Abstract.Name

Methods

size :: ModuleName -> Int

Pretty ModuleName

Defined in Agda.Syntax.Abstract.Name

Methods

pretty :: ModuleName -> Doc

prettyPrec :: Int -> ModuleName -> Doc

prettyList :: [ModuleName] -> Doc

KillRange ModuleName

Defined in Agda.Syntax.Abstract.Name

Methods

killRange :: KillRangeT ModuleName

KillRange Sections

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT Sections

SetRange ModuleName

Defined in Agda.Syntax.Abstract.Name

Methods

setRange :: Range -> ModuleName -> ModuleName

HasRange ModuleName

Defined in Agda.Syntax.Abstract.Name

Methods

getRange :: ModuleName -> Range

SetBindingSite ModuleName

Sets the binding site of all names in the path.

Defined in Agda.Syntax.Scope.Base

Methods

setBindingSite :: Range -> ModuleName -> ModuleName

SubstExpr ModuleName

Defined in Agda.Syntax.Abstract

Methods

substExpr :: [(Name, Expr)] -> ModuleName -> ModuleName

ExprLike ModuleName

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> ModuleName -> m ModuleName

foldExpr :: Monoid m => (Expr -> m) -> ModuleName -> m

traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> ModuleName -> m ModuleName

mapExpr :: (Expr -> Expr) -> ModuleName -> ModuleName

EmbPrj ModuleName

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: ModuleName -> S Int32

icod_ :: ModuleName -> S Int32

value :: Int32 -> R ModuleName

PrettyTCM ModuleName

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => ModuleName -> m Doc

InstantiateFull ModuleName

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: ModuleName -> ReduceM ModuleName

UniverseBi Declaration ModuleName

Defined in Agda.Syntax.Abstract

Methods

universeBi :: Declaration -> [ModuleName]

ToConcrete ModuleName QName

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

toConcrete :: ModuleName -> AbsToCon QName

bindToConcrete :: ModuleName -> (QName -> AbsToCon b) -> AbsToCon b

ToAbstract OldModuleName ModuleName

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Methods

toAbstract :: OldModuleName -> ScopeM ModuleName

ToAbstract NewModuleQName ModuleName

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Methods

toAbstract :: NewModuleQName -> ScopeM ModuleName

ToAbstract NewModuleName ModuleName

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Methods

toAbstract :: NewModuleName -> ScopeM ModuleName

ToAbstract ModuleAssignment (ModuleName, [LetBinding])

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Methods

toAbstract :: ModuleAssignment -> ScopeM (ModuleName, [LetBinding])

data QNamed a

Something preceeded by a qualified name.

Constructors

QNamed

Fields

• qname :: QName
• qnamed :: a

Instances

Functor QNamed

Defined in Agda.Syntax.Abstract.Name

Methods

fmap :: (a -> b) -> QNamed a -> QNamed b

(<$) :: a -> QNamed b -> QNamed a

Foldable QNamed

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

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)

Use prettyShow to print names to the user.

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)

Defined in Agda.Syntax.Abstract.Name

Methods

pretty :: QNamed a -> Doc

prettyPrec :: Int -> QNamed a -> Doc

prettyList :: [QNamed a] -> Doc

PrettyTCM (QNamed Clause)

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => QNamed Clause -> m Doc

ToAbstract (QNamed Clause) Clause

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Methods

toAbstract :: MonadReflectedToAbstract m => QNamed Clause0 -> m Clause

Reify (QNamed Clause) Clause

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: MonadReify m => QNamed Clause0 -> m Clause

reifyWhen :: MonadReify m => Bool -> QNamed Clause0 -> m Clause

ToAbstract [QNamed Clause] [Clause]

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Methods

toAbstract :: MonadReflectedToAbstract m => [QNamed Clause0] -> m [Clause]

Reify (QNamed System) [Clause]

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: MonadReify m => QNamed System -> m [Clause]

reifyWhen :: MonadReify m => Bool -> QNamed System -> m [Clause]

data QName

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

Eq QName

Defined in Agda.Syntax.Abstract.Name

Methods

(==) :: QName -> QName -> Bool

(/=) :: QName -> QName -> Bool

Data QName

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

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

Only use this show function in debugging! To convert an abstract QName into a string use prettyShow.

Defined in Agda.Syntax.Abstract.Name

Methods

showsPrec :: Int -> QName -> ShowS

show :: QName -> String

showList :: [QName] -> ShowS

Hashable QName

Defined in Agda.Syntax.Abstract.Name

Methods

hashWithSalt :: Int -> QName -> Int

hash :: QName -> Int

NFData QName

Defined in Agda.Syntax.Abstract.Name

Methods

rnf :: QName -> ()

Sized QName

Defined in Agda.Syntax.Abstract.Name

Methods

size :: QName -> Int

Pretty QName

Defined in Agda.Syntax.Abstract.Name

Methods

pretty :: QName -> Doc

prettyPrec :: Int -> QName -> Doc

prettyList :: [QName] -> Doc

KillRange QName

Defined in Agda.Syntax.Abstract.Name

Methods

killRange :: KillRangeT QName

KillRange RewriteRuleMap

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT RewriteRuleMap

KillRange Definitions

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT Definitions

SetRange QName

Defined in Agda.Syntax.Abstract.Name

Methods

setRange :: Range -> QName -> QName

HasRange QName

Defined in Agda.Syntax.Abstract.Name

Methods

getRange :: QName -> Range

LensFixity' QName

Defined in Agda.Syntax.Abstract.Name

Methods

lensFixity' :: Lens' Fixity' QName

LensFixity QName

Defined in Agda.Syntax.Abstract.Name

Methods

lensFixity :: Lens' Fixity QName

LensInScope QName

Defined in Agda.Syntax.Abstract.Name

Methods

lensInScope :: Lens' NameInScope QName

isInScope :: QName -> NameInScope

mapInScope :: (NameInScope -> NameInScope) -> QName -> QName

setInScope :: QName -> QName

setNotInScope :: QName -> QName

NumHoles QName

Defined in Agda.Syntax.Abstract.Name

Methods

numHoles :: QName -> Int

SetBindingSite QName

Defined in Agda.Syntax.Scope.Base

Methods

setBindingSite :: Range -> QName -> QName

TermLike QName

Defined in Agda.Syntax.Internal.Generic

Methods

traverseTermM :: Monad m => (Term -> m Term) -> QName -> m QName

foldTerm :: Monoid m => (Term -> m) -> QName -> m

AllNames QName

Defined in Agda.Syntax.Abstract

Methods

allNames :: QName -> Seq QName

ExprLike QName

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> QName -> m QName

foldExpr :: Monoid m => (Expr -> m) -> QName -> m

traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> QName -> m QName

mapExpr :: (Expr -> Expr) -> QName -> QName

EmbPrj QName

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: QName -> S Int32

icod_ :: QName -> S Int32

value :: Int32 -> R QName

PrettyTCM QName

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => QName -> m Doc

NamesIn QName

Defined in Agda.Syntax.Internal.Names

Methods

namesIn :: QName -> Set QName

InstantiateFull QName

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: QName -> ReduceM QName

FromTerm QName

Defined in Agda.TypeChecking.Primitive

Methods

fromTerm :: TCM (FromTermFunction QName)

ToTerm QName

Defined in Agda.TypeChecking.Primitive

Methods

toTerm :: TCM (QName -> Term)

toTermR :: TCM (QName -> ReduceM Term)

PrimTerm QName

Defined in Agda.TypeChecking.Primitive

Methods

primTerm :: QName -> TCM Term

Occurs QName

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

occurs :: QName -> OccursM QName

metaOccurs :: MetaId -> QName -> TCM ()

Unquote QName

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM QName

UniverseBi Declaration QName

Defined in Agda.Syntax.Abstract

Methods

universeBi :: Declaration -> [QName]

Subst Term QName

Defined in Agda.TypeChecking.Substitute.Class

Methods

applySubst :: Substitution' Term -> QName -> QName

ToConcrete QName QName

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

toConcrete :: QName -> AbsToCon QName0

bindToConcrete :: QName -> (QName0 -> AbsToCon b) -> AbsToCon b

Conversion TOM Clause (Maybe ([Pat O], MExp O))

Defined in Agda.Auto.Convert

Methods

convert :: Clause -> TOM (Maybe ([Pat O], MExp O))

Conversion TOM Type (MExp O)

Defined in Agda.Auto.Convert

Methods

convert :: Type -> TOM (MExp O)

Conversion TOM Term (MExp O)

Defined in Agda.Auto.Convert

Methods

convert :: Term -> TOM (MExp O)

Conversion TOM Args (MM (ArgList O) (RefInfo O))

Defined in Agda.Auto.Convert

Methods

convert :: Args -> TOM (MM (ArgList O) (RefInfo O))

Conversion MOT (Exp O) Type

Defined in Agda.Auto.Convert

Methods

convert :: Exp O -> MOT Type

Conversion MOT (Exp O) Term

Defined in Agda.Auto.Convert

Methods

convert :: Exp O -> MOT Term

Conversion TOM [Clause] [([Pat O], MExp O)]

Defined in Agda.Auto.Convert

Methods

convert :: [Clause] -> TOM [([Pat O], MExp O)]

Conversion TOM (Arg Pattern) (Pat O)

Defined in Agda.Auto.Convert

Methods

convert :: Arg Pattern -> TOM (Pat O)

Conversion MOT a b => Conversion MOT (MM a (RefInfo O)) b

Defined in Agda.Auto.Convert

Methods

convert :: MM a (RefInfo O) -> MOT b

(Show a, ToQName a) => ToAbstract (OldName a) QName

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Methods

toAbstract :: OldName a -> ScopeM QName

ToConcrete (Maybe QName) (Maybe Name)

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

toConcrete :: Maybe QName -> AbsToCon (Maybe Name)

bindToConcrete :: Maybe QName -> (Maybe Name -> AbsToCon b) -> AbsToCon b

ToAbstract (RewriteEqn' () Pattern Expr) RewriteEqn

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Methods

toAbstract :: RewriteEqn' () Pattern Expr -> ScopeM RewriteEqn

data Name

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

Eq Name

Defined in Agda.Syntax.Abstract.Name

Methods

(==) :: Name -> Name -> Bool

(/=) :: Name -> Name -> Bool

Data Name

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

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

Only use this show function in debugging! To convert an abstract Name into a string use prettyShow.

Defined in Agda.Syntax.Abstract.Name

Methods

showsPrec :: Int -> Name -> ShowS

show :: Name -> String

showList :: [Name] -> ShowS

Hashable Name

Defined in Agda.Syntax.Abstract.Name

Methods

hashWithSalt :: Int -> Name -> Int

hash :: Name -> Int

NFData Name

The range is not forced.

Defined in Agda.Syntax.Abstract.Name

Methods

rnf :: Name -> ()

Pretty Name

Defined in Agda.Syntax.Abstract.Name

Methods

pretty :: Name -> Doc

prettyPrec :: Int -> Name -> Doc

prettyList :: [Name] -> Doc

KillRange Name

Defined in Agda.Syntax.Abstract.Name

Methods

killRange :: KillRangeT Name

SetRange Name

Defined in Agda.Syntax.Abstract.Name

Methods

setRange :: Range -> Name -> Name

HasRange Name

Defined in Agda.Syntax.Abstract.Name

Methods

getRange :: Name -> Range

LensFixity' Name

Defined in Agda.Syntax.Abstract.Name

Methods

lensFixity' :: Lens' Fixity' Name

LensFixity Name

Defined in Agda.Syntax.Abstract.Name

Methods

lensFixity :: Lens' Fixity Name

IsNoName Name

An abstract name is empty if its concrete name is empty.

Defined in Agda.Syntax.Abstract.Name

Methods

isNoName :: Name -> Bool

LensInScope Name

Defined in Agda.Syntax.Abstract.Name

Methods

lensInScope :: Lens' NameInScope Name

isInScope :: Name -> NameInScope

mapInScope :: (NameInScope -> NameInScope) -> Name -> Name

setInScope :: Name -> Name

setNotInScope :: Name -> Name

NumHoles Name

Defined in Agda.Syntax.Abstract.Name

Methods

numHoles :: Name -> Int

SetBindingSite Name

Defined in Agda.Syntax.Scope.Base

Methods

setBindingSite :: Range -> Name -> Name

Suggest Name

Defined in Agda.Syntax.Internal

Methods

suggestName :: Name -> Maybe String

EmbPrj Name

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Name -> S Int32

icod_ :: Name -> S Int32

value :: Int32 -> R Name

PrettyTCM Name

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Name -> m Doc

AddContext Name

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => Name -> m a -> m a

contextSize :: Name -> Nat

InstantiateFull Name

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Name -> ReduceM Name

Subst Term Name

Defined in Agda.TypeChecking.Substitute

Methods

applySubst :: Substitution' Term -> Name -> Name

ToConcrete Name Name

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

toConcrete :: Name -> AbsToCon Name0

bindToConcrete :: Name -> (Name0 -> AbsToCon b) -> AbsToCon b

Reify Name Name

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: MonadReify m => Name -> m Name

reifyWhen :: MonadReify m => Bool -> Name -> m Name

ToAbstract Pattern (Names, Pattern)

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Methods

toAbstract :: MonadReflectedToAbstract m => Pattern0 -> m (Names, Pattern)

AddContext (Dom (Name, Type))

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => Dom (Name, Type) -> m a -> m a

contextSize :: Dom (Name, Type) -> Nat

ToAbstract (NewName Name) Name

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Methods

toAbstract :: NewName Name0 -> ScopeM Name

ToAbstract r a => ToAbstract (Abs r) (a, Name)

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Methods

toAbstract :: MonadReflectedToAbstract m => Abs r -> m (a, Name)

(Free i, Reify i a) => Reify (Abs i) (Name, a)

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: MonadReify m => Abs i -> m (Name, a)

reifyWhen :: MonadReify m => Bool -> Abs i -> m (Name, a)

AddContext ([NamedArg Name], Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => ([NamedArg Name], Type) -> m a -> m a

contextSize :: ([NamedArg Name], Type) -> Nat

AddContext ([Arg Name], Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => ([Arg Name], Type) -> m a -> m a

contextSize :: ([Arg Name], Type) -> Nat

AddContext ([WithHiding Name], Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => ([WithHiding Name], Dom Type) -> m a -> m a

contextSize :: ([WithHiding Name], Dom Type) -> Nat

AddContext ([Name], Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => ([Name], Dom Type) -> m a -> m a

contextSize :: ([Name], Dom Type) -> Nat

AddContext (Name, Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => (Name, Dom Type) -> m a -> m a

contextSize :: (Name, Dom Type) -> Nat

ToAbstract r Expr => ToAbstract (Dom r, Name) TypedBinding

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Methods

toAbstract :: MonadReflectedToAbstract m => (Dom r, Name) -> m TypedBinding

uglyShowName :: Name -> String

Useful for debugging scoping problems

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

Like withRangesOf, but uses the name parts (qualifier + name) of the qualified name as the list of concrete names.

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

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

qualify_ :: Name -> QName

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

isOperator :: QName -> Bool

Is the name an operator?

isLeParentModuleOf :: ModuleName -> ModuleName -> Bool

Is the first module a weak parent of the second?

isLtParentModuleOf :: ModuleName -> ModuleName -> Bool

Is the first module a proper parent of the second?

isLeChildModuleOf :: ModuleName -> ModuleName -> Bool

Is the first module a weak child of the second?

isLtChildModuleOf :: ModuleName -> ModuleName -> Bool

Is the first module a proper child of the second?

isInModule :: QName -> ModuleName -> Bool

nextName :: Name -> Name

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

sameRoot :: Name -> Name -> Bool

lensQNameName :: Lens' Name QName

nameToArgName :: Name -> ArgName

namedArgName :: NamedArg Name -> ArgName

class IsNoName a where

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

Minimal complete definition

Nothing

Methods

isNoName :: a -> Bool

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

Instances

IsNoName ByteString

Defined in Agda.Syntax.Concrete.Name

Methods

isNoName :: ByteString -> Bool

IsNoName String

Defined in Agda.Syntax.Concrete.Name

Methods

isNoName :: String -> Bool

IsNoName QName

Defined in Agda.Syntax.Concrete.Name

Methods

isNoName :: QName -> Bool

IsNoName Name

Defined in Agda.Syntax.Concrete.Name

Methods

isNoName :: Name -> Bool

IsNoName Name

An abstract name is empty if its concrete name is empty.

Defined in Agda.Syntax.Abstract.Name

Methods

isNoName :: Name -> Bool

IsNoName a => IsNoName (Ranged a)

Defined in Agda.Syntax.Concrete.Name

Methods

isNoName :: Ranged a -> Bool

IsNoName a => IsNoName (WithOrigin a)

Defined in Agda.Syntax.Concrete.Name

Methods

isNoName :: WithOrigin a -> Bool