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)

data Suffix

A name suffix

Constructors

NoSuffix

Suffix !Integer

Instances

Eq Suffix

Defined in Agda.Syntax.Abstract.Name

Methods

(==) :: Suffix -> Suffix -> Bool

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

Data Suffix

Defined in Agda.Syntax.Abstract.Name

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Suffix -> c Suffix

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Suffix

toConstr :: Suffix -> Constr

dataTypeOf :: Suffix -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Suffix)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Suffix)

gmapT :: (forall b. Data b => b -> b) -> Suffix -> Suffix

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Suffix -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Suffix -> r

gmapQ :: (forall d. Data d => d -> u) -> Suffix -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Suffix -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Suffix -> m Suffix

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Suffix -> m Suffix

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Suffix -> m Suffix

Ord Suffix

Defined in Agda.Syntax.Abstract.Name

Methods

compare :: Suffix -> Suffix -> Ordering

(<) :: Suffix -> Suffix -> Bool

(<=) :: Suffix -> Suffix -> Bool

(>) :: Suffix -> Suffix -> Bool

(>=) :: Suffix -> Suffix -> Bool

max :: Suffix -> Suffix -> Suffix

min :: Suffix -> Suffix -> Suffix

Show Suffix

Defined in Agda.Syntax.Abstract.Name

Methods

showsPrec :: Int -> Suffix -> ShowS

show :: Suffix -> String

showList :: [Suffix] -> ShowS

NFData Suffix

Defined in Agda.Syntax.Abstract.Name

Methods

rnf :: Suffix -> ()

Pretty Suffix

Defined in Agda.Syntax.Scope.Base

Methods

pretty :: Suffix -> Doc

prettyPrec :: Int -> Suffix -> Doc

prettyList :: [Suffix] -> Doc

KillRange Suffix

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT Suffix

EmbPrj Suffix

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: Suffix -> S Int32

icod_ :: Suffix -> S Int32

value :: Int32 -> R Suffix

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

NFData AmbiguousQName

Defined in Agda.Syntax.Abstract.Name

Methods

rnf :: AmbiguousQName -> ()

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' :: Monoid m => (QName -> m) -> AmbiguousQName -> m

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

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 :: RecurseExprFn m ModuleName

foldExpr :: FoldExprFn m ModuleName

traverseExpr :: TraverseExprFn 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

ToConcrete ModuleName

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs ModuleName

Methods

toConcrete :: ModuleName -> AbsToCon (ConOfAbs ModuleName)

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

InstantiateFull ModuleName

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: ModuleName -> ReduceM ModuleName

type ConOfAbs ModuleName

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs ModuleName = QName

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)

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]

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef [QNamed Clause]

Methods

toAbstract :: MonadReflectedToAbstract m => [QNamed Clause] -> m (AbsOfRef [QNamed Clause])

ToAbstract (List1 (QNamed Clause))

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef (List1 (QNamed Clause))

Methods

toAbstract :: MonadReflectedToAbstract m => List1 (QNamed Clause) -> m (AbsOfRef (List1 (QNamed Clause)))

ToAbstract (QNamed Clause)

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef (QNamed Clause)

Methods

toAbstract :: MonadReflectedToAbstract m => QNamed Clause -> m (AbsOfRef (QNamed Clause))

Reify (QNamed Clause)

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo (QNamed Clause)

Methods

reify :: MonadReify m => QNamed Clause -> m (ReifiesTo (QNamed Clause))

reifyWhen :: MonadReify m => Bool -> QNamed Clause -> m (ReifiesTo (QNamed Clause))

Reify (QNamed System)

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo (QNamed System)

Methods

reify :: MonadReify m => QNamed System -> m (ReifiesTo (QNamed System))

reifyWhen :: MonadReify m => Bool -> QNamed System -> m (ReifiesTo (QNamed System))

type AbsOfRef [QNamed Clause]

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef [QNamed Clause] = [Clause]

type AbsOfRef (List1 (QNamed Clause))

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef (List1 (QNamed Clause)) = List1 Clause

type AbsOfRef (QNamed Clause)

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef (QNamed Clause) = Clause

type ReifiesTo (QNamed Clause)

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo (QNamed Clause) = Clause

type ReifiesTo (QNamed System)

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo (QNamed System) = [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

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

Subst QName

Defined in Agda.TypeChecking.Substitute.Class

Associated Types

type SubstArg QName

Methods

applySubst :: Substitution' (SubstArg QName) -> 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

DeclaredNames RecordDirectives

Defined in Agda.Syntax.Abstract.Views

Methods

declaredNames :: Collection KName m => RecordDirectives -> m

DeclaredNames KName

Defined in Agda.Syntax.Abstract.Views

Methods

declaredNames :: Collection KName m => KName -> m

ExprLike QName

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: RecurseExprFn m QName

foldExpr :: FoldExprFn m QName

traverseExpr :: TraverseExprFn 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' :: Monoid m => (QName -> m) -> QName -> m

ToConcrete QName

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs QName

Methods

toConcrete :: QName -> AbsToCon (ConOfAbs QName)

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

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

PrimType QName

Defined in Agda.TypeChecking.Primitive

Methods

primType :: QName -> TCM Type

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

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

ToConcrete (Maybe QName)

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Maybe QName)

Methods

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

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

type SubstArg QName

Defined in Agda.TypeChecking.Substitute.Class

type SubstArg QName = Term

type ConOfAbs QName

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs QName = QName

type ConOfAbs (Maybe QName)

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs (Maybe QName) = Maybe Name

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

  The concrete name used for this instance

• nameCanonical :: Name

  The concrete name in the original definition (needed by primShowQName, see #4735)

• 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

Use prettyShow to print names to the user.

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

Subst Name

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg Name

Methods

applySubst :: Substitution' (SubstArg Name) -> Name -> Name

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

ToConcrete Name

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs Name

Methods

toConcrete :: Name -> AbsToCon (ConOfAbs Name)

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

InstantiateFull Name

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Name -> ReduceM Name

Reify Name

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Name

Methods

reify :: MonadReify m => Name -> m (ReifiesTo Name)

reifyWhen :: MonadReify m => Bool -> Name -> m (ReifiesTo Name)

PrettyTCM (Dom (Name, Type))

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Dom (Name, Type) -> m Doc

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

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 (List1 (NamedArg Name), Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

contextSize :: (List1 (NamedArg Name), Type) -> Nat

AddContext (List1 (Arg Name), Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

contextSize :: (List1 (Arg Name), Type) -> Nat

AddContext (List1 (WithHiding Name), Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (List1 Name, Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

contextSize :: (List1 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, AbsOfRef r ~ Expr) => ToAbstract (Dom r, Name)

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef (Dom r, Name)

Methods

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

type SubstArg Name

Defined in Agda.TypeChecking.Substitute

type SubstArg Name = Term

type ConOfAbs Name

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs Name = Name

type ReifiesTo Name

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo Name = Name

type AbsOfRef (Dom r, Name)

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef (Dom r, Name) = 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 -> List1 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

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

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

data FreshNameMode

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