Agda-2.8.0: A dependently typed functional programming language and proof assistant

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
  - | InstanceProblem
  - | CosmeticProblem
  - | 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 Word32 Source # icod_ :: Induction -> S Word32 Source # value :: Word32 -> R Induction Source #
NFData Induction Source # |
Instance details Defined in Agda.Syntax.Common.Aspect Methods rnf :: Induction -> () Source #
Show Induction Source # |
Instance details Defined in Agda.Syntax.Common.Aspect Methods showsPrec :: Int -> Induction -> ShowS Source # show :: Induction -> String Source # showList :: [Induction] -> ShowS Source #
Eq Induction Source # |
Instance details Defined in Agda.Syntax.Common.Aspect Methods (==) :: Induction -> Induction -> Bool Source # (/=) :: Induction -> Induction -> Bool Source #
Ord Induction Source # |

Instance details

Defined in Agda.Syntax.Common.Aspect

Methods

compare :: Induction -> Induction -> Ordering Source #

(<) :: Induction -> Induction -> Bool Source #

(<=) :: Induction -> Induction -> Bool Source #

(>) :: Induction -> Induction -> Bool Source #

(>=) :: Induction -> Induction -> Bool Source #

max :: Induction -> Induction -> Induction Source #

min :: Induction -> Induction -> Induction Source #

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 Word32 Source # icod_ :: Aspect -> S Word32 Source # value :: Word32 -> R Aspect Source #
NFData Aspect Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods rnf :: Aspect -> () Source #
Semigroup Aspect Source # | `NameKind` in `Name` can get more precise.
Instance details Defined in Agda.Syntax.Common.Aspect Methods (<>) :: Aspect -> Aspect -> Aspect Source # sconcat :: NonEmpty Aspect -> Aspect Source # stimes :: Integral b => b -> Aspect -> Aspect Source #
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.8.0-DJrTbcOFazJDzri4fKrI2F" '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 Source #

to :: Rep Aspect x -> Aspect Source #

Show Aspect Source # |
Instance details Defined in Agda.Syntax.Common.Aspect Methods showsPrec :: Int -> Aspect -> ShowS Source # show :: Aspect -> String Source # showList :: [Aspect] -> ShowS Source #
Eq Aspect Source # |
Instance details Defined in Agda.Syntax.Common.Aspect Methods (==) :: Aspect -> Aspect -> Bool Source # (/=) :: Aspect -> Aspect -> Bool Source #
type Rep Aspect Source # |

Instance details

Defined in Agda.Syntax.Common.Aspect

type Rep Aspect = D1 ('MetaData "Aspect" "Agda.Syntax.Common.Aspect" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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 #

`NameKind`s 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 Word32 Source # icod_ :: NameKind -> S Word32 Source # value :: Word32 -> R NameKind Source #
NFData NameKind Source # |
Instance details Defined in Agda.Syntax.Common.Aspect Methods rnf :: NameKind -> () Source #
Semigroup NameKind Source # | Some `NameKind`s are more informative than others.
Instance details Defined in Agda.Syntax.Common.Aspect Methods (<>) :: NameKind -> NameKind -> NameKind Source # sconcat :: NonEmpty NameKind -> NameKind Source # stimes :: Integral b => b -> NameKind -> NameKind Source #
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.8.0-DJrTbcOFazJDzri4fKrI2F" '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 Source #

to :: Rep NameKind x -> NameKind Source #

Show NameKind Source # |
Instance details Defined in Agda.Syntax.Common.Aspect Methods showsPrec :: Int -> NameKind -> ShowS Source # show :: NameKind -> String Source # showList :: [NameKind] -> ShowS Source #
Eq NameKind Source # |
Instance details Defined in Agda.Syntax.Common.Aspect Methods (==) :: NameKind -> NameKind -> Bool Source # (/=) :: NameKind -> NameKind -> Bool Source #
type Rep NameKind Source # |

Instance details

Defined in Agda.Syntax.Common.Aspect

type Rep NameKind = D1 ('MetaData "NameKind" "Agda.Syntax.Common.Aspect" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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 `Aspect`s.)

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.
InstanceProblem | Unusable instance etc.
CosmeticProblem | Nothing serious, just a beauty flaw.
CatchallClause |
ConfluenceProblem |

#### Instances

Instances details

EmbPrj OtherAspect Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Highlighting Methods icode :: OtherAspect -> S Word32 Source # icod_ :: OtherAspect -> S Word32 Source # value :: Word32 -> R OtherAspect Source #
NFData OtherAspect Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods rnf :: OtherAspect -> () Source #
Bounded OtherAspect Source # |
Instance details Defined in Agda.Syntax.Common.Aspect Methods minBound :: OtherAspect Source # maxBound :: OtherAspect Source #
Enum OtherAspect Source # |

Instance details

Defined in Agda.Syntax.Common.Aspect

Methods

succ :: OtherAspect -> OtherAspect Source #

pred :: OtherAspect -> OtherAspect Source #

toEnum :: Int -> OtherAspect Source #

fromEnum :: OtherAspect -> Int Source #

enumFrom :: OtherAspect -> [OtherAspect] Source #

enumFromThen :: OtherAspect -> OtherAspect -> [OtherAspect] Source #

enumFromTo :: OtherAspect -> OtherAspect -> [OtherAspect] Source #

enumFromThenTo :: OtherAspect -> OtherAspect -> OtherAspect -> [OtherAspect] Source #

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.8.0-DJrTbcOFazJDzri4fKrI2F" '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 "InstanceProblem" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "CosmeticProblem" '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 Source #

to :: Rep OtherAspect x -> OtherAspect Source #

Show OtherAspect Source # |
Instance details Defined in Agda.Syntax.Common.Aspect Methods showsPrec :: Int -> OtherAspect -> ShowS Source # show :: OtherAspect -> String Source # showList :: [OtherAspect] -> ShowS Source #
Eq OtherAspect Source # |
Instance details Defined in Agda.Syntax.Common.Aspect Methods (==) :: OtherAspect -> OtherAspect -> Bool Source # (/=) :: OtherAspect -> OtherAspect -> Bool Source #
Ord OtherAspect Source # |

Instance details

Defined in Agda.Syntax.Common.Aspect

Methods

compare :: OtherAspect -> OtherAspect -> Ordering Source #

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

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

(>) :: OtherAspect -> OtherAspect -> Bool Source #

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

max :: OtherAspect -> OtherAspect -> OtherAspect Source #

min :: OtherAspect -> OtherAspect -> OtherAspect Source #

type Rep OtherAspect Source # |

Instance details

Defined in Agda.Syntax.Common.Aspect

type Rep OtherAspect = D1 ('MetaData "OtherAspect" "Agda.Syntax.Common.Aspect" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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 "InstanceProblem" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "CosmeticProblem" '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 Word32 Source # icod_ :: Aspects -> S Word32 Source # value :: Word32 -> R Aspects Source #
EmbPrj Doc Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: Doc -> S Word32 Source # icod_ :: Doc -> S Word32 Source # value :: Word32 -> R Doc Source #
ToJSON Doc Source # |
Instance details Defined in Agda.Interaction.JSON Methods toJSON :: Doc -> Value Source # toEncoding :: Doc -> Encoding Source # toJSONList :: [Doc] -> Value Source # toEncodingList :: [Doc] -> Encoding Source # omitField :: Doc -> Bool Source #
NFData Aspects Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods rnf :: Aspects -> () Source #
Monoid Aspects Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods mempty :: Aspects Source # mappend :: Aspects -> Aspects -> Aspects Source # mconcat :: [Aspects] -> Aspects Source #
Semigroup Aspects Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods (<>) :: Aspects -> Aspects -> Aspects Source # sconcat :: NonEmpty Aspects -> Aspects Source # stimes :: Integral b => b -> Aspects -> Aspects Source #
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.8.0-DJrTbcOFazJDzri4fKrI2F" '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 Source #

to :: Rep Aspects x -> Aspects Source #

Show Aspects Source # |
Instance details Defined in Agda.Syntax.Common.Aspect Methods showsPrec :: Int -> Aspects -> ShowS Source # show :: Aspects -> String Source # showList :: [Aspects] -> ShowS Source #
Eq Aspects Source # |
Instance details Defined in Agda.Syntax.Common.Aspect Methods (==) :: Aspects -> Aspects -> Bool Source # (/=) :: Aspects -> Aspects -> Bool Source #
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 (TCM Doc) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods empty :: TCM Doc Source # null :: TCM Doc -> Bool Source #
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 Source # sconcat :: NonEmpty (TCM Doc) -> TCM Doc Source # stimes :: Integral b => b -> TCM Doc -> TCM Doc 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 #
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.8.0-DJrTbcOFazJDzri4fKrI2F" '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 Word32 Source # icod_ :: DefinitionSite -> S Word32 Source # value :: Word32 -> R DefinitionSite Source #
NFData DefinitionSite Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods rnf :: DefinitionSite -> () Source #
Semigroup DefinitionSite Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods (<>) :: DefinitionSite -> DefinitionSite -> DefinitionSite Source # sconcat :: NonEmpty DefinitionSite -> DefinitionSite Source # stimes :: Integral b => b -> DefinitionSite -> DefinitionSite Source #
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.8.0-DJrTbcOFazJDzri4fKrI2F" '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 Source #

to :: Rep DefinitionSite x -> DefinitionSite Source #

Show DefinitionSite Source # |
Instance details Defined in Agda.Syntax.Common.Aspect Methods showsPrec :: Int -> DefinitionSite -> ShowS Source # show :: DefinitionSite -> String Source # showList :: [DefinitionSite] -> ShowS Source #
Eq DefinitionSite Source # |
Instance details Defined in Agda.Syntax.Common.Aspect Methods (==) :: DefinitionSite -> DefinitionSite -> Bool Source # (/=) :: DefinitionSite -> DefinitionSite -> Bool Source #
type Rep DefinitionSite Source # |

Instance details

Defined in Agda.Syntax.Common.Aspect

type Rep DefinitionSite = D1 ('MetaData "DefinitionSite" "Agda.Syntax.Common.Aspect" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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 Word32 Source # icod_ :: TokenBased -> S Word32 Source # value :: Word32 -> R TokenBased Source #
ToJSON TokenBased Source # |
Instance details Defined in Agda.Interaction.Highlighting.JSON Methods toJSON :: TokenBased -> Value Source # toEncoding :: TokenBased -> Encoding Source # toJSONList :: [TokenBased] -> Value Source # toEncodingList :: [TokenBased] -> Encoding Source # omitField :: TokenBased -> Bool Source #
Monoid TokenBased Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods mempty :: TokenBased Source # mappend :: TokenBased -> TokenBased -> TokenBased Source # mconcat :: [TokenBased] -> TokenBased Source #
Semigroup TokenBased Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods (<>) :: TokenBased -> TokenBased -> TokenBased Source # sconcat :: NonEmpty TokenBased -> TokenBased Source # stimes :: Integral b => b -> TokenBased -> TokenBased Source #
Show TokenBased Source # |
Instance details Defined in Agda.Syntax.Common.Aspect Methods showsPrec :: Int -> TokenBased -> ShowS Source # show :: TokenBased -> String Source # showList :: [TokenBased] -> ShowS Source #
Eq TokenBased Source # |
Instance details Defined in Agda.Syntax.Common.Aspect Methods (==) :: TokenBased -> TokenBased -> Bool Source # (/=) :: TokenBased -> TokenBased -> Bool Source #