Agda.IR

Intermediate Representation for Agda's types

Documentation

class FromAgda a b | a -> b where

Typeclass for converting Agda values into IR

Methods

fromAgda :: a -> b

Instances

FromAgda GiveResult GiveResult

Defined in Agda.IR

Methods

fromAgda :: GiveResult0 -> GiveResult

class FromAgdaTCM a b | a -> b where

Methods

fromAgdaTCM :: a -> TCM b

data Response

IR for IOCTM

Constructors

ResponseHighlightingInfoDirect HighlightingInfos

ResponseHighlightingInfoIndirect FilePath

ResponseDisplayInfo DisplayInfo

ResponseStatus Bool Bool

ResponseClearHighlightingTokenBased

ResponseClearHighlightingNotOnlyTokenBased

ResponseRunningInfo Int String

ResponseClearRunningInfo

ResponseDoneAborting

ResponseDoneExiting

ResponseGiveAction Int GiveResult

ResponseInteractionPoints [Int]

ResponseMakeCaseFunction [String]

ResponseMakeCaseExtendedLambda [String]

ResponseSolveAll [(Int, String)]

ResponseJumpToError FilePath Int

ResponseEnd

Instances

Generic Response

Defined in Agda.IR

Associated Types

type Rep Response :: Type -> Type

Methods

from :: Response -> Rep Response x

to :: Rep Response x -> Response

ToJSON Response

Defined in Agda.IR

Methods

toJSON :: Response -> Value

toEncoding :: Response -> Encoding

toJSONList :: [Response] -> Value

toEncodingList :: [Response] -> Encoding

type Rep Response

Defined in Agda.IR

type Rep Response = D1 ('MetaData "Response" "Agda.IR" "agda-language-server-0.2.1-99xGnOcQUAiDPMFa3Og6t4" '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

IR for DisplayInfo

Constructors

DisplayInfoGeneric String [Block]

DisplayInfoAllGoalsWarnings String [Block] [Block] [String] [String]

DisplayInfoCurrentGoal Block

DisplayInfoInferredType Block

DisplayInfoCompilationOk [String] [String]

DisplayInfoAuto String

DisplayInfoError String

DisplayInfoTime String

DisplayInfoNormalForm String

Instances

Generic DisplayInfo

Defined in Agda.IR

Associated Types

type Rep DisplayInfo :: Type -> Type

Methods

from :: DisplayInfo -> Rep DisplayInfo x

to :: Rep DisplayInfo x -> DisplayInfo

ToJSON DisplayInfo

Defined in Agda.IR

Methods

toJSON :: DisplayInfo -> Value

toEncoding :: DisplayInfo -> Encoding

toJSONList :: [DisplayInfo] -> Value

toEncodingList :: [DisplayInfo] -> Encoding

type Rep DisplayInfo

Defined in Agda.IR

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

GiveResult

Constructors

GiveString String

GiveParen

GiveNoParen

Instances

Generic GiveResult

Defined in Agda.IR

Associated Types

type Rep GiveResult :: Type -> Type

Methods

from :: GiveResult -> Rep GiveResult x

to :: Rep GiveResult x -> GiveResult

ToJSON GiveResult

Defined in Agda.IR

Methods

toJSON :: GiveResult -> Value

toEncoding :: GiveResult -> Encoding

toJSONList :: [GiveResult] -> Value

toEncodingList :: [GiveResult] -> Encoding

FromAgda GiveResult GiveResult

Defined in Agda.IR

Methods

fromAgda :: GiveResult0 -> GiveResult

type Rep GiveResult

Defined in Agda.IR

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

IR for HighlightingInfo

Constructors

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

Instances

Show HighlightingInfo

Defined in Agda.IR

Methods

showsPrec :: Int -> HighlightingInfo -> ShowS

show :: HighlightingInfo -> String

showList :: [HighlightingInfo] -> ShowS

Generic HighlightingInfo

Defined in Agda.IR

Associated Types

type Rep HighlightingInfo :: Type -> Type

Methods

from :: HighlightingInfo -> Rep HighlightingInfo x

to :: Rep HighlightingInfo x -> HighlightingInfo

ToJSON HighlightingInfo

Defined in Agda.IR

Methods

toJSON :: HighlightingInfo -> Value

toEncoding :: HighlightingInfo -> Encoding

toJSONList :: [HighlightingInfo] -> Value

toEncodingList :: [HighlightingInfo] -> Encoding

type Rep HighlightingInfo

Defined in Agda.IR

type Rep HighlightingInfo = D1 ('MetaData "HighlightingInfo" "Agda.IR" "agda-language-server-0.2.1-99xGnOcQUAiDPMFa3Og6t4" '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

Constructors

HighlightingInfos Bool [HighlightingInfo]

Instances

Show HighlightingInfos

Defined in Agda.IR

Methods

showsPrec :: Int -> HighlightingInfos -> ShowS

show :: HighlightingInfos -> String

showList :: [HighlightingInfos] -> ShowS

Generic HighlightingInfos

Defined in Agda.IR

Associated Types

type Rep HighlightingInfos :: Type -> Type

Methods

from :: HighlightingInfos -> Rep HighlightingInfos x

to :: Rep HighlightingInfos x -> HighlightingInfos

ToJSON HighlightingInfos

Defined in Agda.IR

Methods

toJSON :: HighlightingInfos -> Value

toEncoding :: HighlightingInfos -> Encoding

toJSONList :: [HighlightingInfos] -> Value

toEncodingList :: [HighlightingInfos] -> Encoding

type Rep HighlightingInfos

Defined in Agda.IR

type Rep HighlightingInfos = D1 ('MetaData "HighlightingInfos" "Agda.IR" "agda-language-server-0.2.1-99xGnOcQUAiDPMFa3Og6t4" '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])))