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

Agda.Syntax.Common.Aspect

Synopsis

Documentation

data Induction Source #

Constructors

Inductive 
CoInductive 

Instances

Instances details
PatternMatchingAllowed Induction Source # 
Instance details

Defined in Agda.Syntax.Common

Pretty Induction Source # 
Instance details

Defined in Agda.Syntax.Common

HasRange Induction Source # 
Instance details

Defined in Agda.Syntax.Common

KillRange Induction Source # 
Instance details

Defined in Agda.Syntax.Common

EmbPrj Induction Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Show Induction Source # 
Instance details

Defined in Agda.Syntax.Common.Aspect

NFData Induction Source # 
Instance details

Defined in Agda.Syntax.Common.Aspect

Methods

rnf :: Induction -> () #

Eq Induction Source # 
Instance details

Defined in Agda.Syntax.Common.Aspect

Ord Induction Source # 
Instance details

Defined in Agda.Syntax.Common.Aspect

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

Semigroup Aspect Source #

NameKind in Name can get more precise.

Instance details

Defined in Agda.Syntax.Common.Aspect

Generic Aspect Source # 
Instance details

Defined in Agda.Syntax.Common.Aspect

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.Syntax.Common.Aspect

NFData Aspect Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

rnf :: Aspect -> () #

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.3.20230914-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.Syntax.Common.Aspect

Generic NameKind Source # 
Instance details

Defined in Agda.Syntax.Common.Aspect

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.Syntax.Common.Aspect

NFData NameKind Source # 
Instance details

Defined in Agda.Syntax.Common.Aspect

Methods

rnf :: NameKind -> () #

Eq NameKind Source # 
Instance details

Defined in Agda.Syntax.Common.Aspect

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.3.20230914-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.Syntax.Common.Aspect

Enum OtherAspect Source # 
Instance details

Defined in Agda.Syntax.Common.Aspect

Generic OtherAspect Source # 
Instance details

Defined in Agda.Syntax.Common.Aspect

Associated Types

type Rep OtherAspect :: Type -> Type #

Show OtherAspect Source # 
Instance details

Defined in Agda.Syntax.Common.Aspect

NFData OtherAspect Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

rnf :: OtherAspect -> () #

Eq OtherAspect Source # 
Instance details

Defined in Agda.Syntax.Common.Aspect

Ord OtherAspect Source # 
Instance details

Defined in Agda.Syntax.Common.Aspect

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

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

EmbPrj Doc Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

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.Syntax.Common.Aspect

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.Syntax.Common.Aspect

NFData Aspects Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

rnf :: Aspects -> () #

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

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

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

Null (TCM Doc) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

IsString (AbsToCon Doc) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Semigroup (AbsToCon Doc) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

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 #

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

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

Defined in Agda.TypeChecking.Conversion.Pure

type Rep Aspects Source # 
Instance details

Defined in Agda.Syntax.Common.Aspect

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.Syntax.Common.Aspect

Associated Types

type Rep DefinitionSite :: Type -> Type #

Show DefinitionSite Source # 
Instance details

Defined in Agda.Syntax.Common.Aspect

NFData DefinitionSite Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

rnf :: DefinitionSite -> () #

Eq DefinitionSite Source # 
Instance details

Defined in Agda.Syntax.Common.Aspect

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.3.20230914-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.Syntax.Common.Aspect

Eq TokenBased Source # 
Instance details

Defined in Agda.Syntax.Common.Aspect

ToJSON TokenBased Source # 
Instance details

Defined in Agda.Interaction.Highlighting.JSON