agda-language-server-0.2.6.2.2: An implementation of language server protocal (LSP) for Agda 2.
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.IR

Description

Intermediate Representation for Agda's types

Synopsis

Documentation

class FromAgda a b | a -> b where Source #

Typeclass for converting Agda values into IR

Methods

fromAgda :: a -> b Source #

Instances

Instances details
FromAgda GiveResult GiveResult Source # 
Instance details

Defined in Agda.IR

class FromAgdaTCM a b | a -> b where Source #

Methods

fromAgdaTCM :: a -> TCM b Source #

data Response Source #

IR for IOCTM

Instances

Instances details
ToJSON Response Source # 
Instance details

Defined in Agda.IR

Generic Response Source # 
Instance details

Defined in Agda.IR

Associated Types

type Rep Response :: Type -> Type #

Methods

from :: Response -> Rep Response x #

to :: Rep Response x -> Response #

type Rep Response Source # 
Instance details

Defined in Agda.IR

type Rep Response = D1 ('MetaData "Response" "Agda.IR" "agda-language-server-0.2.6.2.2-9Wn4gKfYowo7ISMsjxvlzN" 'False) ((((C1 ('MetaCons "ResponseHighlightingInfoDirect" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 HighlightingInfos)) :+: C1 ('MetaCons "ResponseHighlightingInfoIndirect" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FilePath))) :+: (C1 ('MetaCons "ResponseDisplayInfo" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DisplayInfo)) :+: C1 ('MetaCons "ResponseStatus" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))) :+: ((C1 ('MetaCons "ResponseClearHighlightingTokenBased" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ResponseClearHighlightingNotOnlyTokenBased" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "ResponseRunningInfo" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)) :+: C1 ('MetaCons "ResponseClearRunningInfo" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "ResponseDoneAborting" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ResponseDoneExiting" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "ResponseGiveAction" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 GiveResult)) :+: C1 ('MetaCons "ResponseInteractionPoints" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Int])))) :+: ((C1 ('MetaCons "ResponseMakeCaseFunction" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [String])) :+: C1 ('MetaCons "ResponseMakeCaseExtendedLambda" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [String]))) :+: (C1 ('MetaCons "ResponseSolveAll" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(Int, String)])) :+: (C1 ('MetaCons "ResponseJumpToError" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FilePath) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)) :+: C1 ('MetaCons "ResponseEnd" 'PrefixI 'False) (U1 :: Type -> Type))))))

data DisplayInfo Source #

IR for DisplayInfo

Instances

Instances details
ToJSON DisplayInfo Source # 
Instance details

Defined in Agda.IR

Generic DisplayInfo Source # 
Instance details

Defined in Agda.IR

Associated Types

type Rep DisplayInfo :: Type -> Type #

type Rep DisplayInfo Source # 
Instance details

Defined in Agda.IR

type Rep DisplayInfo = D1 ('MetaData "DisplayInfo" "Agda.IR" "agda-language-server-0.2.6.2.2-9Wn4gKfYowo7ISMsjxvlzN" 'False) (((C1 ('MetaCons "DisplayInfoGeneric" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Block])) :+: C1 ('MetaCons "DisplayInfoAllGoalsWarnings" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Block])) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Block]) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [String]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [String]))))) :+: (C1 ('MetaCons "DisplayInfoCurrentGoal" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Block)) :+: C1 ('MetaCons "DisplayInfoInferredType" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Block)))) :+: ((C1 ('MetaCons "DisplayInfoCompilationOk" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [String]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [String])) :+: C1 ('MetaCons "DisplayInfoAuto" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String))) :+: (C1 ('MetaCons "DisplayInfoError" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)) :+: (C1 ('MetaCons "DisplayInfoTime" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)) :+: C1 ('MetaCons "DisplayInfoNormalForm" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String))))))

data GiveResult Source #

GiveResult

Instances

Instances details
ToJSON GiveResult Source # 
Instance details

Defined in Agda.IR

Generic GiveResult Source # 
Instance details

Defined in Agda.IR

Associated Types

type Rep GiveResult :: Type -> Type #

FromAgda GiveResult GiveResult Source # 
Instance details

Defined in Agda.IR

type Rep GiveResult Source # 
Instance details

Defined in Agda.IR

type Rep GiveResult = D1 ('MetaData "GiveResult" "Agda.IR" "agda-language-server-0.2.6.2.2-9Wn4gKfYowo7ISMsjxvlzN" 'False) (C1 ('MetaCons "GiveString" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)) :+: (C1 ('MetaCons "GiveParen" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "GiveNoParen" 'PrefixI 'False) (U1 :: Type -> Type)))

data HighlightingInfo Source #

IR for HighlightingInfo

Instances

Instances details
ToJSON HighlightingInfo Source # 
Instance details

Defined in Agda.IR

Generic HighlightingInfo Source # 
Instance details

Defined in Agda.IR

Associated Types

type Rep HighlightingInfo :: Type -> Type #

Show HighlightingInfo Source # 
Instance details

Defined in Agda.IR

type Rep HighlightingInfo Source # 
Instance details

Defined in Agda.IR

data HighlightingInfos Source #

Instances

Instances details
ToJSON HighlightingInfos Source # 
Instance details

Defined in Agda.IR

Generic HighlightingInfos Source # 
Instance details

Defined in Agda.IR

Associated Types

type Rep HighlightingInfos :: Type -> Type #

Show HighlightingInfos Source # 
Instance details

Defined in Agda.IR

type Rep HighlightingInfos Source # 
Instance details

Defined in Agda.IR

type Rep HighlightingInfos = D1 ('MetaData "HighlightingInfos" "Agda.IR" "agda-language-server-0.2.6.2.2-9Wn4gKfYowo7ISMsjxvlzN" 'False) (C1 ('MetaCons "HighlightingInfos" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [HighlightingInfo])))