Agda-2.6.20240714: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.Interaction.Highlighting.Precise

Description

Types used for precise syntax highlighting.

Synopsis

Highlighting information

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

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

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.20240714-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.20240714-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 #

newtype RangePair Source #

A limited kind of syntax highlighting information: a pair consisting of Ranges and Aspects.

Note the invariant which RangePairs should satisfy (rangePairInvariant).

Constructors

RangePair 

Fields

Instances

Instances details
NFData RangePair Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

rnf :: RangePair -> ()

Show RangePair Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

showsPrec :: Int -> RangePair -> ShowS

show :: RangePair -> String

showList :: [RangePair] -> ShowS

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 #

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 #

Convert (DelayedMerge RangePair) PositionMap Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

convert :: DelayedMerge RangePair -> PositionMap Source #

Convert (DelayedMerge RangePair) (RangeMap Aspects) Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

convert :: DelayedMerge RangePair -> RangeMap Aspects Source #

rangePairInvariant :: RangePair -> Bool Source #

Invariant for RangePair.

newtype PositionMap Source #

Syntax highlighting information, represented by maps from positions to Aspects.

The first position in the file has number 1.

Constructors

PositionMap 

Fields

Instances

Instances details
NFData PositionMap Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

rnf :: PositionMap -> ()

Monoid PositionMap Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

mempty :: PositionMap

mappend :: PositionMap -> PositionMap -> PositionMap

mconcat :: [PositionMap] -> PositionMap

Semigroup PositionMap Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

(<>) :: PositionMap -> PositionMap -> PositionMap #

sconcat :: NonEmpty PositionMap -> PositionMap

stimes :: Integral b => b -> PositionMap -> PositionMap

Show PositionMap Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

showsPrec :: Int -> PositionMap -> ShowS

show :: PositionMap -> String

showList :: [PositionMap] -> ShowS

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 #

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 #

Convert (DelayedMerge RangePair) PositionMap Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

convert :: DelayedMerge RangePair -> PositionMap Source #

Convert (DelayedMerge PositionMap) (RangeMap Aspects) Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

convert :: DelayedMerge PositionMap -> RangeMap Aspects Source #

newtype DelayedMerge hl Source #

Highlighting info with delayed merging.

Merging large sets of highlighting info repeatedly might be costly. The idea of this type is to accumulate small pieces of highlighting information, and then to merge them all at the end.

Note the invariant which values of this type should satisfy (delayedMergeInvariant).

Constructors

DelayedMerge (Endo [hl]) 

Instances

Instances details
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 #

Semigroup a => IsBasicRangeMap a (DelayedMerge (RangeMap a)) Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

singleton :: Ranges -> a -> DelayedMerge (RangeMap a) Source #

toMap :: DelayedMerge (RangeMap a) -> IntMap a Source #

toList :: DelayedMerge (RangeMap a) -> [(Range, a)] Source #

coveringRange :: DelayedMerge (RangeMap a) -> Maybe Range Source #

Monoid (DelayedMerge hl) Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

mempty :: DelayedMerge hl

mappend :: DelayedMerge hl -> DelayedMerge hl -> DelayedMerge hl

mconcat :: [DelayedMerge hl] -> DelayedMerge hl

Semigroup (DelayedMerge hl) Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

(<>) :: DelayedMerge hl -> DelayedMerge hl -> DelayedMerge hl #

sconcat :: NonEmpty (DelayedMerge hl) -> DelayedMerge hl

stimes :: Integral b => b -> DelayedMerge hl -> DelayedMerge hl

Show hl => Show (DelayedMerge hl) Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

showsPrec :: Int -> DelayedMerge hl -> ShowS

show :: DelayedMerge hl -> String

showList :: [DelayedMerge hl] -> ShowS

Convert (DelayedMerge RangePair) PositionMap Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

convert :: DelayedMerge RangePair -> PositionMap Source #

Monoid hl => Convert (DelayedMerge hl) hl Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

convert :: DelayedMerge hl -> hl Source #

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 #

delayedMergeInvariant :: (hl -> Bool) -> DelayedMerge hl -> Bool Source #

Invariant for DelayedMerge hl, parametrised by the invariant for hl.

Additionally the endofunction should be extensionally equal to (fs ++) for some list fs.

type HighlightingInfo = RangeMap Aspects Source #

Highlighting information.

Note the invariant which values of this type should satisfy (highlightingInfoInvariant).

This is a type synonym in order to make it easy to change to another representation.

highlightingInfoInvariant :: HighlightingInfo -> Bool Source #

The invariant for HighlightingInfo.

type HighlightingInfoBuilder = DelayedMerge RangePair Source #

A type that is intended to be used when constructing highlighting information.

Note the invariant which values of this type should satisfy (highlightingInfoBuilderInvariant).

This is a type synonym in order to make it easy to change to another representation.

The type should be an instance of IsBasicRangeMap Aspects, Semigroup and Monoid, and there should be an instance of Convert HighlightingInfoBuilder HighlightingInfo.

highlightingInfoBuilderInvariant :: HighlightingInfoBuilder -> Bool Source #

The invariant for HighlightingInfoBuilder.

Additionally the endofunction should be extensionally equal to (fs ++) for some list fs.

Operations

parserBased :: Aspects Source #

A variant of mempty with tokenBased set to NotOnlyTokenBased.

kindOfNameToNameKind :: KindOfName -> NameKind Source #

Conversion from classification of the scope checker.

class IsBasicRangeMap a m | m -> a where Source #

A class that is intended to make it easy to swap between different range map implementations.

Note that some RangeMap operations are not included in this class.

Minimal complete definition

singleton, toMap, toList

Methods

singleton :: Ranges -> a -> m Source #

The map singleton rs x contains the ranges from rs, and every position in those ranges is associated with x.

toMap :: m -> IntMap a Source #

Converts range maps to IntMaps from positions to values.

toList :: m -> [(Range, a)] Source #

Converts the map to a list. The ranges are non-overlapping and non-empty, and earlier ranges precede later ones in the list.

coveringRange :: m -> Maybe Range Source #

Returns the smallest range covering everything in the map (or Nothing, if the range would be empty).

Note that the default implementation of this operation might be inefficient.

Instances

Instances details
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 #

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 #

Semigroup a => IsBasicRangeMap a (DelayedMerge (RangeMap a)) Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

singleton :: Ranges -> a -> DelayedMerge (RangeMap a) Source #

toMap :: DelayedMerge (RangeMap a) -> IntMap a Source #

toList :: DelayedMerge (RangeMap a) -> [(Range, a)] Source #

coveringRange :: DelayedMerge (RangeMap a) -> Maybe Range Source #

IsBasicRangeMap a (RangeMap a) Source # 
Instance details

Defined in Agda.Utils.RangeMap

Methods

singleton :: Ranges -> a -> RangeMap a Source #

toMap :: RangeMap a -> IntMap a Source #

toList :: RangeMap a -> [(Range, a)] Source #

coveringRange :: RangeMap a -> Maybe Range Source #

several :: (IsBasicRangeMap a hl, Monoid hl) => [Ranges] -> a -> hl Source #

Like singleton, but with several Ranges instead of only one.

class Convert a b where Source #

Conversion between different types.

Methods

convert :: a -> b Source #

Instances

Instances details
Convert PositionMap (RangeMap Aspects) Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

convert :: PositionMap -> RangeMap Aspects Source #

Convert (DelayedMerge RangePair) PositionMap Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

convert :: DelayedMerge RangePair -> PositionMap Source #

Monoid hl => Convert (DelayedMerge hl) hl Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

convert :: DelayedMerge hl -> hl Source #

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 #

insideAndOutside :: Range -> RangeMap a -> (RangeMap a, RangeMap a) Source #

Returns a RangeMap overlapping the given range, as well as the rest of the map.

restrictTo :: Range -> RangeMap a -> RangeMap a Source #

Restricts the RangeMap to the given range.

Orphan instances

NFData Aspect Source # 
Instance details

Methods

rnf :: Aspect -> ()

NFData Aspects Source # 
Instance details

Methods

rnf :: Aspects -> ()

NFData DefinitionSite Source # 
Instance details

Methods

rnf :: DefinitionSite -> ()

NFData OtherAspect Source # 
Instance details

Methods

rnf :: OtherAspect -> ()

Monoid Aspects Source # 
Instance details

Methods

mempty :: Aspects

mappend :: Aspects -> Aspects -> Aspects

mconcat :: [Aspects] -> Aspects

Monoid TokenBased Source # 
Instance details

Methods

mempty :: TokenBased

mappend :: TokenBased -> TokenBased -> TokenBased

mconcat :: [TokenBased] -> TokenBased

Semigroup Aspects Source # 
Instance details

Methods

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

sconcat :: NonEmpty Aspects -> Aspects

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

Semigroup DefinitionSite Source # 
Instance details

Methods

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

sconcat :: NonEmpty DefinitionSite -> DefinitionSite

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

Semigroup TokenBased Source # 
Instance details

Methods

(<>) :: TokenBased -> TokenBased -> TokenBased #

sconcat :: NonEmpty TokenBased -> TokenBased

stimes :: Integral b => b -> TokenBased -> TokenBased