agda-language-server-0.2.6.3.0: 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

Methods

fromAgda :: GiveResult0 -> GiveResult Source #

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

Methods

fromAgdaTCM :: a -> TCM b Source #

data Response Source #

IR for IOCTM

Instances

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

ToJSON Response Source # 
Instance details

Defined in Agda.IR

Methods

toJSON :: Response -> Value

toEncoding :: Response -> Encoding

toJSONList :: [Response] -> Value

toEncodingList :: [Response] -> Encoding

omitField :: Response -> Bool

type Rep Response Source # 
Instance details

Defined in Agda.IR

type Rep Response = D1 ('MetaData "Response" "Agda.IR" "agda-language-server-0.2.6.3.0-inplace" '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
Generic DisplayInfo Source # 
Instance details

Defined in Agda.IR

Associated Types

type Rep DisplayInfo :: Type -> Type

Methods

from :: DisplayInfo -> Rep DisplayInfo x

to :: Rep DisplayInfo x -> DisplayInfo

ToJSON DisplayInfo Source # 
Instance details

Defined in Agda.IR

Methods

toJSON :: DisplayInfo -> Value

toEncoding :: DisplayInfo -> Encoding

toJSONList :: [DisplayInfo] -> Value

toEncodingList :: [DisplayInfo] -> Encoding

omitField :: DisplayInfo -> Bool

type Rep DisplayInfo Source # 
Instance details

Defined in Agda.IR

type Rep DisplayInfo = D1 ('MetaData "DisplayInfo" "Agda.IR" "agda-language-server-0.2.6.3.0-inplace" '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

Constructors

GiveString String 
GiveParen 
GiveNoParen 

Instances

Instances details
Generic GiveResult Source # 
Instance details

Defined in Agda.IR

Associated Types

type Rep GiveResult :: Type -> Type

Methods

from :: GiveResult -> Rep GiveResult x

to :: Rep GiveResult x -> GiveResult

ToJSON GiveResult Source # 
Instance details

Defined in Agda.IR

Methods

toJSON :: GiveResult -> Value

toEncoding :: GiveResult -> Encoding

toJSONList :: [GiveResult] -> Value

toEncodingList :: [GiveResult] -> Encoding

omitField :: GiveResult -> Bool

FromAgda GiveResult GiveResult Source # 
Instance details

Defined in Agda.IR

Methods

fromAgda :: GiveResult0 -> GiveResult Source #

type Rep GiveResult Source # 
Instance details

Defined in Agda.IR

type Rep GiveResult = D1 ('MetaData "GiveResult" "Agda.IR" "agda-language-server-0.2.6.3.0-inplace" '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

Constructors

HighlightingInfo Int Int [String] Bool String (Maybe (FilePath, Int)) 

Instances

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

Methods

showsPrec :: Int -> HighlightingInfo -> ShowS

show :: HighlightingInfo -> String

showList :: [HighlightingInfo] -> ShowS

ToJSON HighlightingInfo Source # 
Instance details

Defined in Agda.IR

type Rep HighlightingInfo Source # 
Instance details

Defined in Agda.IR

type Rep HighlightingInfo = D1 ('MetaData "HighlightingInfo" "Agda.IR" "agda-language-server-0.2.6.3.0-inplace" 'False) (C1 ('MetaCons "HighlightingInfo" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [String]))) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe (FilePath, Int)))))))

data HighlightingInfos Source #

Constructors

HighlightingInfos Bool [HighlightingInfo] 

Instances

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

Methods

showsPrec :: Int -> HighlightingInfos -> ShowS

show :: HighlightingInfos -> String

showList :: [HighlightingInfos] -> ShowS

ToJSON 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.3.0-inplace" '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])))