Agda-2.6.2.0.20211129: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.Interaction.Highlighting.Precise

Description

Types used for precise syntax highlighting.

Synopsis

Highlighting information

data Aspect Source #

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

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

Semigroup Aspect Source #

NameKind in Name can get more precise.

Instance details

Defined in Agda.Interaction.Highlighting.Precise

Generic Aspect Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Associated Types

type Rep Aspect :: Type -> Type #

Methods

from :: Aspect -> Rep Aspect x #

to :: Rep Aspect x -> Aspect #

Show Aspect Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

NFData Aspect Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

rnf :: Aspect -> () #

Eq Aspect Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

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

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

type Rep Aspect Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

type Rep Aspect = D1 ('MetaData "Aspect" "Agda.Interaction.Highlighting.Precise" "Agda-2.6.2.0.20211129-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

Semigroup NameKind Source #

Some NameKinds are more informative than others.

Instance details

Defined in Agda.Interaction.Highlighting.Precise

Generic NameKind Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Associated Types

type Rep NameKind :: Type -> Type #

Methods

from :: NameKind -> Rep NameKind x #

to :: Rep NameKind x -> NameKind #

Show NameKind Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

NFData NameKind Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

rnf :: NameKind -> () #

Eq NameKind Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

type Rep NameKind Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

type Rep NameKind = D1 ('MetaData "NameKind" "Agda.Interaction.Highlighting.Precise" "Agda-2.6.2.0.20211129-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

Bounded OtherAspect Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Enum OtherAspect Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Generic OtherAspect Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Associated Types

type Rep OtherAspect :: Type -> Type #

Show OtherAspect Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

NFData OtherAspect Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

rnf :: OtherAspect -> () #

Eq OtherAspect Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Ord OtherAspect Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

type Rep OtherAspect Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

type Rep OtherAspect = D1 ('MetaData "OtherAspect" "Agda.Interaction.Highlighting.Precise" "Agda-2.6.2.0.20211129-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 #

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

Constructors

Aspects 

Fields

Instances

Instances details
EmbPrj Aspects Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Monoid Aspects Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Semigroup Aspects Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Generic Aspects Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Associated Types

type Rep Aspects :: Type -> Type #

Methods

from :: Aspects -> Rep Aspects x #

to :: Rep Aspects x -> Aspects #

Show Aspects Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

NFData Aspects Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

rnf :: Aspects -> () #

Eq Aspects Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

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

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

IsBasicRangeMap Aspects PositionMap Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

IsBasicRangeMap Aspects RangePair Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Convert PositionMap (RangeMap Aspects) Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

IsBasicRangeMap Aspects (DelayedMerge PositionMap) Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

IsBasicRangeMap Aspects (DelayedMerge RangePair) Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

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

Defined in Agda.Interaction.Highlighting.Precise

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

Defined in Agda.Interaction.Highlighting.Precise

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

Defined in Agda.Interaction.Highlighting.Precise

type Rep Aspects Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

data DefinitionSite Source #

Constructors

DefinitionSite 

Fields

Instances

Instances details
EmbPrj DefinitionSite Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Semigroup DefinitionSite Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Generic DefinitionSite Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Associated Types

type Rep DefinitionSite :: Type -> Type #

Show DefinitionSite Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

NFData DefinitionSite Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

rnf :: DefinitionSite -> () #

Eq DefinitionSite Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

type Rep DefinitionSite Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

type Rep DefinitionSite = D1 ('MetaData "DefinitionSite" "Agda.Interaction.Highlighting.Precise" "Agda-2.6.2.0.20211129-inplace" 'False) (C1 ('MetaCons "DefinitionSite" 'PrefixI 'True) ((S1 ('MetaSel ('Just "defSiteModule") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TopLevelModuleName) :*: 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?

Instances

Instances details
EncodeTCM TokenBased Source # 
Instance details

Defined in Agda.Interaction.Highlighting.JSON

EmbPrj TokenBased Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Monoid TokenBased Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Semigroup TokenBased Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Show TokenBased Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Eq TokenBased Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

ToJSON TokenBased Source # 
Instance details

Defined in Agda.Interaction.Highlighting.JSON

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

newtype PositionMap Source #

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

The first position in the file has number 1.

Constructors

PositionMap 

Instances

Instances details
Monoid PositionMap Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Semigroup PositionMap Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Show PositionMap Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

NFData PositionMap Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

rnf :: PositionMap -> () #

IsBasicRangeMap Aspects PositionMap Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Convert PositionMap (RangeMap Aspects) Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

IsBasicRangeMap Aspects (DelayedMerge PositionMap) Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Convert (DelayedMerge RangePair) PositionMap Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

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

Defined in Agda.Interaction.Highlighting.Precise

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

IsBasicRangeMap Aspects (DelayedMerge RangePair) Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

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

Defined in Agda.Interaction.Highlighting.Precise

Monoid (DelayedMerge hl) Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Semigroup (DelayedMerge hl) Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

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

Defined in Agda.Interaction.Highlighting.Precise

Convert (DelayedMerge RangePair) PositionMap Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

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

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

Defined in Agda.Interaction.Highlighting.Precise

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.

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

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

IsBasicRangeMap Aspects RangePair Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

IsBasicRangeMap Aspects (DelayedMerge PositionMap) Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

IsBasicRangeMap Aspects (DelayedMerge RangePair) Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

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

Defined in Agda.Interaction.Highlighting.Precise

IsBasicRangeMap a (RangeMap a) Source # 
Instance details

Defined in Agda.Utils.RangeMap

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

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

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.