Safe Haskell	None
Language	Haskell2010

Agda.Syntax.Common.Aspect

Synopsis

data Induction
- = Inductive
- | CoInductive
data Aspect
- = Comment
- | Keyword
- | String
- | Number
- | Hole
- | Symbol
- | PrimitiveType
- | Name (Maybe NameKind) Bool
- | Pragma
- | Background
- | Markup
data NameKind
- = Bound
- | Generalizable
- | Constructor Induction
- | Datatype
- | Field
- | Function
- | Module
- | Postulate
- | Primitive
- | Record
- | Argument
- | Macro
data OtherAspect
- = Error
- | ErrorWarning
- | DottedPattern
- | UnsolvedMeta
- | UnsolvedConstraint
- | TerminationProblem
- | PositivityProblem
- | Deadcode
- | ShadowingInTelescope
- | CoverageProblem
- | IncompletePattern
- | TypeChecks
- | MissingDefinition
- | CatchallClause
- | ConfluenceProblem
data Aspects = Aspects {
- aspect :: Maybe Aspect
- otherAspects :: Set OtherAspect
- note :: String
- definitionSite :: Maybe DefinitionSite
- tokenBased :: !TokenBased
}
data DefinitionSite = DefinitionSite {
- defSiteModule :: TopLevelModuleName' Range
- defSitePos :: Int
- defSiteHere :: Bool
- defSiteAnchor :: Maybe String
}
data TokenBased
- = TokenBased
- | NotOnlyTokenBased

Documentation

data Induction Source #

Constructors

Inductive
CoInductive

Instances

Instances details

PatternMatchingAllowed Induction Source #
Instance details Defined in Agda.Syntax.Common Methods patternMatchingAllowed :: Induction -> Bool Source #
Pretty Induction Source #
Instance details Defined in Agda.Syntax.Common Methods pretty :: Induction -> Doc Source # prettyPrec :: Int -> Induction -> Doc Source # prettyList :: [Induction] -> Doc Source #
HasRange Induction Source #
Instance details Defined in Agda.Syntax.Common Methods getRange :: Induction -> Range Source #
KillRange Induction Source #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT Induction Source #
EmbPrj Induction Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Induction -> S Int32 Source # icod_ :: Induction -> S Int32 Source # value :: Int32 -> R Induction Source #
NFData Induction Source #
Instance details Defined in Agda.Syntax.Common.Aspect Methods rnf :: Induction -> ()
Show Induction Source #
Instance details Defined in Agda.Syntax.Common.Aspect Methods showsPrec :: Int -> Induction -> ShowS show :: Induction -> String showList :: [Induction] -> ShowS
Eq Induction Source #
Instance details Defined in Agda.Syntax.Common.Aspect Methods (==) :: Induction -> Induction -> Bool (/=) :: Induction -> Induction -> Bool
Ord Induction Source #
Instance details Defined in Agda.Syntax.Common.Aspect Methods compare :: Induction -> Induction -> Ordering (<) :: Induction -> Induction -> Bool (<=) :: Induction -> Induction -> Bool (>) :: Induction -> Induction -> Bool (>=) :: Induction -> Induction -> Bool max :: Induction -> Induction -> Induction min :: Induction -> Induction -> Induction

data Aspect Source #

Constructors

Comment
Keyword
String
Number
Hole
Symbol	Symbols like forall, =, ->, etc.
PrimitiveType	Things like Set and Prop.
Name (Maybe NameKind) Bool	Is the name an operator part?
Pragma	Text occurring in pragmas that does not have a more specific aspect.
Background	Non-code contents in literate Agda
Markup	Delimiters used to separate the Agda code blocks from the other contents in literate Agda

Instances

Instances details

EmbPrj Aspect Source #

Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: Aspect -> S Int32 Source #

icod_ :: Aspect -> S Int32 Source #

value :: Int32 -> R Aspect Source #

NFData Aspect

Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

rnf :: Aspect -> ()

Semigroup Aspect Source #

NameKind in Name can get more precise.

Instance details

Defined in Agda.Syntax.Common.Aspect

Methods

(<>) :: Aspect -> Aspect -> Aspect #

sconcat :: NonEmpty Aspect -> Aspect

stimes :: Integral b => b -> Aspect -> Aspect

Generic Aspect Source #

Instance details

Defined in Agda.Syntax.Common.Aspect

Associated Types

type Rep Aspect

Instance details

Defined in Agda.Syntax.Common.Aspect

type Rep Aspect = D1 ('MetaData "Aspect" "Agda.Syntax.Common.Aspect" "Agda-2.6.20240731-inplace" 'False) (((C1 ('MetaCons "Comment" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Keyword" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "String" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Number" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Hole" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "Symbol" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "PrimitiveType" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Name" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe NameKind)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))) :+: (C1 ('MetaCons "Pragma" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Background" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Markup" 'PrefixI 'False) (U1 :: Type -> Type)))))

Methods

from :: Aspect -> Rep Aspect x

to :: Rep Aspect x -> Aspect

Show Aspect Source #

Instance details

Defined in Agda.Syntax.Common.Aspect

Methods

showsPrec :: Int -> Aspect -> ShowS

show :: Aspect -> String

showList :: [Aspect] -> ShowS

Eq Aspect Source #

Instance details

Defined in Agda.Syntax.Common.Aspect

Methods

(==) :: Aspect -> Aspect -> Bool

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

type Rep Aspect Source #

Instance details

Defined in Agda.Syntax.Common.Aspect

type Rep Aspect = D1 ('MetaData "Aspect" "Agda.Syntax.Common.Aspect" "Agda-2.6.20240731-inplace" 'False) (((C1 ('MetaCons "Comment" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Keyword" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "String" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Number" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Hole" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "Symbol" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "PrimitiveType" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Name" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe NameKind)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))) :+: (C1 ('MetaCons "Pragma" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Background" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Markup" 'PrefixI 'False) (U1 :: Type -> Type)))))

data NameKind Source #

NameKinds are figured out during scope checking.

Constructors

Bound	Bound variable.
Generalizable	Generalizable variable. (This includes generalizable variables that have been generalized).
Constructor Induction	Inductive or coinductive constructor.
Datatype
Field	Record field.
Function
Module	Module name.
Postulate
Primitive	Primitive.
Record	Record type.
Argument	Named argument, like x in {x = v}
Macro	Macro.

Instances

Instances details

EmbPrj NameKind Source #

Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: NameKind -> S Int32 Source #

icod_ :: NameKind -> S Int32 Source #

value :: Int32 -> R NameKind Source #

NFData NameKind Source #

Instance details

Defined in Agda.Syntax.Common.Aspect

Methods

rnf :: NameKind -> ()

Semigroup NameKind Source #

Some NameKinds are more informative than others.

Instance details

Defined in Agda.Syntax.Common.Aspect

Methods

(<>) :: NameKind -> NameKind -> NameKind #

sconcat :: NonEmpty NameKind -> NameKind

stimes :: Integral b => b -> NameKind -> NameKind

Generic NameKind Source #

Instance details

Defined in Agda.Syntax.Common.Aspect

Associated Types

type Rep NameKind

Instance details

Defined in Agda.Syntax.Common.Aspect

type Rep NameKind = D1 ('MetaData "NameKind" "Agda.Syntax.Common.Aspect" "Agda-2.6.20240731-inplace" 'False) (((C1 ('MetaCons "Bound" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Generalizable" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Constructor" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Induction)))) :+: (C1 ('MetaCons "Datatype" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Field" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Function" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "Module" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Postulate" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Primitive" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "Record" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Argument" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Macro" 'PrefixI 'False) (U1 :: Type -> Type)))))

Methods

from :: NameKind -> Rep NameKind x

to :: Rep NameKind x -> NameKind

Show NameKind Source #

Instance details

Defined in Agda.Syntax.Common.Aspect

Methods

showsPrec :: Int -> NameKind -> ShowS

show :: NameKind -> String

showList :: [NameKind] -> ShowS

Eq NameKind Source #

Instance details

Defined in Agda.Syntax.Common.Aspect

Methods

(==) :: NameKind -> NameKind -> Bool

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

type Rep NameKind Source #

Instance details

Defined in Agda.Syntax.Common.Aspect

type Rep NameKind = D1 ('MetaData "NameKind" "Agda.Syntax.Common.Aspect" "Agda-2.6.20240731-inplace" 'False) (((C1 ('MetaCons "Bound" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Generalizable" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Constructor" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Induction)))) :+: (C1 ('MetaCons "Datatype" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Field" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Function" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "Module" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Postulate" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Primitive" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "Record" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Argument" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Macro" 'PrefixI 'False) (U1 :: Type -> Type)))))

data OtherAspect Source #

Other aspects, generated by type checking. (These can overlap with each other and with Aspects.)

Constructors

Error
ErrorWarning	A warning that is considered fatal in the end.
DottedPattern
UnsolvedMeta
UnsolvedConstraint	Unsolved constraint not connected to meta-variable. This could for instance be an emptyness constraint.
TerminationProblem
PositivityProblem
Deadcode	Used for highlighting unreachable clauses, unreachable RHS (because of an absurd pattern), etc.
ShadowingInTelescope	Used for shadowed repeated variable names in telescopes.
CoverageProblem
IncompletePattern	When this constructor is used it is probably a good idea to include a `note` explaining why the pattern is incomplete.
TypeChecks	Code which is being type-checked.
MissingDefinition	Function declaration without matching definition NB: We put CatchallClause last so that it is overwritten by other, more important, aspects in the emacs mode.
CatchallClause
ConfluenceProblem

Instances

Instances details

EmbPrj OtherAspect Source #

Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: OtherAspect -> S Int32 Source #

icod_ :: OtherAspect -> S Int32 Source #

value :: Int32 -> R OtherAspect Source #

NFData OtherAspect

Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

rnf :: OtherAspect -> ()

Bounded OtherAspect Source #

Instance details

Defined in Agda.Syntax.Common.Aspect

Methods

minBound :: OtherAspect

maxBound :: OtherAspect

Enum OtherAspect Source #

Instance details

Defined in Agda.Syntax.Common.Aspect

Methods

succ :: OtherAspect -> OtherAspect

pred :: OtherAspect -> OtherAspect

toEnum :: Int -> OtherAspect

fromEnum :: OtherAspect -> Int

enumFrom :: OtherAspect -> [OtherAspect]

enumFromThen :: OtherAspect -> OtherAspect -> [OtherAspect]

enumFromTo :: OtherAspect -> OtherAspect -> [OtherAspect]

enumFromThenTo :: OtherAspect -> OtherAspect -> OtherAspect -> [OtherAspect]

Generic OtherAspect Source #

Instance details

Defined in Agda.Syntax.Common.Aspect

Associated Types

type Rep OtherAspect

Instance details

Defined in Agda.Syntax.Common.Aspect

type Rep OtherAspect = D1 ('MetaData "OtherAspect" "Agda.Syntax.Common.Aspect" "Agda-2.6.20240731-inplace" 'False) (((C1 ('MetaCons "Error" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "ErrorWarning" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "DottedPattern" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "UnsolvedMeta" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UnsolvedConstraint" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "TerminationProblem" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PositivityProblem" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "Deadcode" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ShadowingInTelescope" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "CoverageProblem" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "IncompletePattern" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "TypeChecks" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "MissingDefinition" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "CatchallClause" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ConfluenceProblem" 'PrefixI 'False) (U1 :: Type -> Type)))))

Methods

from :: OtherAspect -> Rep OtherAspect x

to :: Rep OtherAspect x -> OtherAspect

Show OtherAspect Source #

Instance details

Defined in Agda.Syntax.Common.Aspect

Methods

showsPrec :: Int -> OtherAspect -> ShowS

show :: OtherAspect -> String

showList :: [OtherAspect] -> ShowS

Eq OtherAspect Source #

Instance details

Defined in Agda.Syntax.Common.Aspect

Methods

(==) :: OtherAspect -> OtherAspect -> Bool

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

Ord OtherAspect Source #

Instance details

Defined in Agda.Syntax.Common.Aspect

Methods

compare :: OtherAspect -> OtherAspect -> Ordering

(<) :: OtherAspect -> OtherAspect -> Bool

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

(>) :: OtherAspect -> OtherAspect -> Bool

(>=) :: OtherAspect -> OtherAspect -> Bool

max :: OtherAspect -> OtherAspect -> OtherAspect

min :: OtherAspect -> OtherAspect -> OtherAspect

type Rep OtherAspect Source #

Instance details

Defined in Agda.Syntax.Common.Aspect

type Rep OtherAspect = D1 ('MetaData "OtherAspect" "Agda.Syntax.Common.Aspect" "Agda-2.6.20240731-inplace" 'False) (((C1 ('MetaCons "Error" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "ErrorWarning" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "DottedPattern" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "UnsolvedMeta" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UnsolvedConstraint" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "TerminationProblem" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PositivityProblem" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "Deadcode" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ShadowingInTelescope" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "CoverageProblem" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "IncompletePattern" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "TypeChecks" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "MissingDefinition" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "CatchallClause" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ConfluenceProblem" 'PrefixI 'False) (U1 :: Type -> Type)))))

data Aspects Source #

Syntactic aspects of the code. (These cannot overlap.)

Meta information which can be associated with a character/character range.

Constructors

Aspects

Fields

aspect :: Maybe Aspect
otherAspects :: Set OtherAspect
note :: String
This note, if not null, can be displayed as a tool-tip or something like that. It should contain useful information about the range (like the module containing a certain identifier, or the fixity of an operator).
definitionSite :: Maybe DefinitionSite
The definition site of the annotated thing, if applicable and known.
tokenBased :: !TokenBased
Is this entry token-based?

Instances

Instances details

EncodeTCM Doc Source #

Instance details

Defined in Agda.Interaction.JSON

Methods

encodeTCM :: Doc -> TCM Value Source #

Underscore Doc Source #

Instance details

Defined in Agda.Syntax.Common

Methods

underscore :: Doc Source #

isUnderscore :: Doc -> Bool Source #

ReportS Doc Source #

Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

reportS :: MonadDebug m => VerboseKey -> VerboseLevel -> Doc -> m () Source #

TraceS Doc Source #

Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

traceS :: MonadDebug m => VerboseKey -> VerboseLevel -> Doc -> m c -> m c Source #

EmbPrj Aspects Source #

Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: Aspects -> S Int32 Source #

icod_ :: Aspects -> S Int32 Source #

value :: Int32 -> R Aspects Source #

EmbPrj Doc Source #

Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: Doc -> S Int32 Source #

icod_ :: Doc -> S Int32 Source #

value :: Int32 -> R Doc Source #

NFData Aspects

Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

rnf :: Aspects -> ()

Monoid Aspects

Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

mempty :: Aspects

mappend :: Aspects -> Aspects -> Aspects

mconcat :: [Aspects] -> Aspects

Semigroup Aspects Source #

Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

(<>) :: Aspects -> Aspects -> Aspects #

sconcat :: NonEmpty Aspects -> Aspects

stimes :: Integral b => b -> Aspects -> Aspects

Generic Aspects Source #

Instance details

Defined in Agda.Syntax.Common.Aspect

Associated Types

type Rep Aspects

Instance details

Defined in Agda.Syntax.Common.Aspect

type Rep Aspects = D1 ('MetaData "Aspects" "Agda.Syntax.Common.Aspect" "Agda-2.6.20240731-inplace" 'False) (C1 ('MetaCons "Aspects" 'PrefixI 'True) ((S1 ('MetaSel ('Just "aspect") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Aspect)) :*: S1 ('MetaSel ('Just "otherAspects") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set OtherAspect))) :*: (S1 ('MetaSel ('Just "note") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: (S1 ('MetaSel ('Just "definitionSite") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe DefinitionSite)) :*: S1 ('MetaSel ('Just "tokenBased") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 TokenBased)))))

Methods

from :: Aspects -> Rep Aspects x

to :: Rep Aspects x -> Aspects

Show Aspects Source #

Instance details

Defined in Agda.Syntax.Common.Aspect

Methods

showsPrec :: Int -> Aspects -> ShowS

show :: Aspects -> String

showList :: [Aspects] -> ShowS

Eq Aspects Source #

Instance details

Defined in Agda.Syntax.Common.Aspect

Methods

(==) :: Aspects -> Aspects -> Bool

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

ToJSON Doc Source #

Instance details

Defined in Agda.Interaction.JSON

Methods

toJSON :: Doc -> Value #

toEncoding :: Doc -> Encoding #

toJSONList :: [Doc] -> Value #

toEncodingList :: [Doc] -> Encoding #

omitField :: Doc -> Bool #

IsBasicRangeMap Aspects PositionMap Source #

Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

singleton :: Ranges -> Aspects -> PositionMap Source #

toMap :: PositionMap -> IntMap Aspects Source #

toList :: PositionMap -> [(Range, Aspects)] Source #

coveringRange :: PositionMap -> Maybe Range Source #

IsBasicRangeMap Aspects RangePair Source #

Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

singleton :: Ranges -> Aspects -> RangePair Source #

toMap :: RangePair -> IntMap Aspects Source #

toList :: RangePair -> [(Range, Aspects)] Source #

coveringRange :: RangePair -> Maybe Range Source #

Convert PositionMap (RangeMap Aspects) Source #

Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

convert :: PositionMap -> RangeMap Aspects Source #

IsBasicRangeMap Aspects (DelayedMerge PositionMap) Source #

Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

singleton :: Ranges -> Aspects -> DelayedMerge PositionMap Source #

toMap :: DelayedMerge PositionMap -> IntMap Aspects Source #

toList :: DelayedMerge PositionMap -> [(Range, Aspects)] Source #

coveringRange :: DelayedMerge PositionMap -> Maybe Range Source #

IsBasicRangeMap Aspects (DelayedMerge RangePair) Source #

Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

singleton :: Ranges -> Aspects -> DelayedMerge RangePair Source #

toMap :: DelayedMerge RangePair -> IntMap Aspects Source #

toList :: DelayedMerge RangePair -> [(Range, Aspects)] Source #

coveringRange :: DelayedMerge RangePair -> Maybe Range Source #

ReportS (TCM Doc) Source #

Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

reportS :: MonadDebug m => VerboseKey -> VerboseLevel -> TCM Doc -> m () Source #

ReportS [Doc] Source #

Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

reportS :: MonadDebug m => VerboseKey -> VerboseLevel -> [Doc] -> m () Source #

ReportS [TCM Doc] Source #

Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

reportS :: MonadDebug m => VerboseKey -> VerboseLevel -> [TCM Doc] -> m () Source #

TraceS (TCM Doc) Source #

Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

traceS :: MonadDebug m => VerboseKey -> VerboseLevel -> TCM Doc -> m c -> m c Source #

TraceS [Doc] Source #

Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

traceS :: MonadDebug m => VerboseKey -> VerboseLevel -> [Doc] -> m c -> m c Source #

TraceS [TCM Doc] Source #

Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

traceS :: MonadDebug m => VerboseKey -> VerboseLevel -> [TCM Doc] -> m c -> m c Source #

Null (AbsToCon Doc) Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

empty :: AbsToCon Doc Source #

null :: AbsToCon Doc -> Bool Source #

Null (TCM Doc) Source #

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

empty :: TCM Doc Source #

null :: TCM Doc -> Bool Source #

Semigroup (AbsToCon Doc) Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

(<>) :: AbsToCon Doc -> AbsToCon Doc -> AbsToCon Doc #

sconcat :: NonEmpty (AbsToCon Doc) -> AbsToCon Doc

stimes :: Integral b => b -> AbsToCon Doc -> AbsToCon Doc

Semigroup (TCM Doc) Source #

This instance is more specific than a generic instance Semigroup a => Semigroup (TCM a).

Instance details

Defined in Agda.TypeChecking.Pretty

Methods

(<>) :: TCM Doc -> TCM Doc -> TCM Doc #

sconcat :: NonEmpty (TCM Doc) -> TCM Doc

stimes :: Integral b => b -> TCM Doc -> TCM Doc

IsString (AbsToCon Doc)

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

fromString :: String -> AbsToCon Doc

Convert (DelayedMerge PositionMap) (RangeMap Aspects) Source #

Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

convert :: DelayedMerge PositionMap -> RangeMap Aspects Source #

Convert (DelayedMerge RangePair) (RangeMap Aspects) Source #

Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

convert :: DelayedMerge RangePair -> RangeMap Aspects Source #

Convert (RangeMap Aspects) (RangeMap Aspects) Source #

Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

convert :: RangeMap Aspects -> RangeMap Aspects Source #

Monad m => Null (PureConversionT m Doc) Source #

Instance details

Defined in Agda.TypeChecking.Conversion.Pure

Methods

empty :: PureConversionT m Doc Source #

null :: PureConversionT m Doc -> Bool Source #

type Rep Aspects Source #

Instance details

Defined in Agda.Syntax.Common.Aspect

type Rep Aspects = D1 ('MetaData "Aspects" "Agda.Syntax.Common.Aspect" "Agda-2.6.20240731-inplace" 'False) (C1 ('MetaCons "Aspects" 'PrefixI 'True) ((S1 ('MetaSel ('Just "aspect") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Aspect)) :*: S1 ('MetaSel ('Just "otherAspects") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set OtherAspect))) :*: (S1 ('MetaSel ('Just "note") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: (S1 ('MetaSel ('Just "definitionSite") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe DefinitionSite)) :*: S1 ('MetaSel ('Just "tokenBased") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 TokenBased)))))

data DefinitionSite Source #

Constructors

DefinitionSite
Fields defSiteModule :: TopLevelModuleName' Range The defining module. defSitePos :: Int The file position in that module. File positions are counted from 1. defSiteHere :: Bool Has this `DefinitionSite` been created at the defining site of the name? defSiteAnchor :: Maybe String A pretty name for the HTML linking.

Instances

Instances details

EmbPrj DefinitionSite Source #

Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: DefinitionSite -> S Int32 Source #

icod_ :: DefinitionSite -> S Int32 Source #

value :: Int32 -> R DefinitionSite Source #

NFData DefinitionSite

Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

rnf :: DefinitionSite -> ()

Semigroup DefinitionSite Source #

Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

(<>) :: DefinitionSite -> DefinitionSite -> DefinitionSite #

sconcat :: NonEmpty DefinitionSite -> DefinitionSite

stimes :: Integral b => b -> DefinitionSite -> DefinitionSite

Generic DefinitionSite Source #

Instance details

Defined in Agda.Syntax.Common.Aspect

Associated Types

type Rep DefinitionSite

Instance details

Defined in Agda.Syntax.Common.Aspect

type Rep DefinitionSite = D1 ('MetaData "DefinitionSite" "Agda.Syntax.Common.Aspect" "Agda-2.6.20240731-inplace" 'False) (C1 ('MetaCons "DefinitionSite" 'PrefixI 'True) ((S1 ('MetaSel ('Just "defSiteModule") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TopLevelModuleName' Range)) :*: S1 ('MetaSel ('Just "defSitePos") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)) :*: (S1 ('MetaSel ('Just "defSiteHere") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "defSiteAnchor") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe String)))))

Methods

from :: DefinitionSite -> Rep DefinitionSite x

to :: Rep DefinitionSite x -> DefinitionSite

Show DefinitionSite Source #

Instance details

Defined in Agda.Syntax.Common.Aspect

Methods

showsPrec :: Int -> DefinitionSite -> ShowS

show :: DefinitionSite -> String

showList :: [DefinitionSite] -> ShowS

Eq DefinitionSite Source #

Instance details

Defined in Agda.Syntax.Common.Aspect

Methods

(==) :: DefinitionSite -> DefinitionSite -> Bool

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

type Rep DefinitionSite Source #

Instance details

Defined in Agda.Syntax.Common.Aspect

type Rep DefinitionSite = D1 ('MetaData "DefinitionSite" "Agda.Syntax.Common.Aspect" "Agda-2.6.20240731-inplace" 'False) (C1 ('MetaCons "DefinitionSite" 'PrefixI 'True) ((S1 ('MetaSel ('Just "defSiteModule") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TopLevelModuleName' Range)) :*: S1 ('MetaSel ('Just "defSitePos") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)) :*: (S1 ('MetaSel ('Just "defSiteHere") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "defSiteAnchor") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe String)))))

data TokenBased Source #

Is the highlighting "token-based", i.e. based only on information from the lexer?

Constructors

TokenBased
NotOnlyTokenBased

Instances

Instances details

EncodeTCM TokenBased Source #
Instance details Defined in Agda.Interaction.Highlighting.JSON Methods encodeTCM :: TokenBased -> TCM Value Source #
EmbPrj TokenBased Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Highlighting Methods icode :: TokenBased -> S Int32 Source # icod_ :: TokenBased -> S Int32 Source # value :: Int32 -> R TokenBased Source #
Monoid TokenBased
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods mempty :: TokenBased mappend :: TokenBased -> TokenBased -> TokenBased mconcat :: [TokenBased] -> TokenBased
Semigroup TokenBased Source #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods (<>) :: TokenBased -> TokenBased -> TokenBased # sconcat :: NonEmpty TokenBased -> TokenBased stimes :: Integral b => b -> TokenBased -> TokenBased
Show TokenBased Source #
Instance details Defined in Agda.Syntax.Common.Aspect Methods showsPrec :: Int -> TokenBased -> ShowS show :: TokenBased -> String showList :: [TokenBased] -> ShowS
Eq TokenBased Source #
Instance details Defined in Agda.Syntax.Common.Aspect Methods (==) :: TokenBased -> TokenBased -> Bool (/=) :: TokenBased -> TokenBased -> Bool
ToJSON TokenBased Source #
Instance details Defined in Agda.Interaction.Highlighting.JSON Methods toJSON :: TokenBased -> Value # toEncoding :: TokenBased -> Encoding # toJSONList :: [TokenBased] -> Value # toEncodingList :: [TokenBased] -> Encoding # omitField :: TokenBased -> Bool #