Safe Haskell	Safe-Inferred
Language	Haskell2010

Agda.IR

Description

Intermediate Representation for Agda's types

Synopsis

class FromAgda a b | a -> b where
- fromAgda :: a -> b
class FromAgdaTCM a b | a -> b where
- fromAgdaTCM :: a -> TCM b
data Response
data DisplayInfo
- = DisplayInfoGeneric String [Block]
- | DisplayInfoAllGoalsWarnings String [Block] [Block] [String] [String]
- | DisplayInfoCurrentGoal Block
- | DisplayInfoInferredType Block
- | DisplayInfoCompilationOk [String] [String]
- | DisplayInfoAuto String
- | DisplayInfoError String
- | DisplayInfoTime String
- | DisplayInfoNormalForm String
data GiveResult
- = GiveString String
- | GiveParen
- | GiveNoParen
data HighlightingInfo = HighlightingInfo Int Int [String] Bool String (Maybe (FilePath, Int))
data HighlightingInfos = HighlightingInfos Bool [HighlightingInfo]

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

ToJSON Response Source #
Instance details Defined in Agda.IR Methods toJSON :: Response -> Value # toEncoding :: Response -> Encoding # toJSONList :: [Response] -> Value # toEncodingList :: [Response] -> Encoding #
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.2.6.2-GEMsKgeRG8f5Pv7LGY4Jhr" '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 Methods toJSON :: DisplayInfo -> Value # toEncoding :: DisplayInfo -> Encoding # toJSONList :: [DisplayInfo] -> Value # toEncodingList :: [DisplayInfo] -> Encoding #
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 #
type Rep DisplayInfo Source #
Instance details Defined in Agda.IR type Rep DisplayInfo = D1 ('MetaData "DisplayInfo" "Agda.IR" "agda-language-server-0.2.2.6.2-GEMsKgeRG8f5Pv7LGY4Jhr" '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

ToJSON GiveResult Source #
Instance details Defined in Agda.IR Methods toJSON :: GiveResult -> Value # toEncoding :: GiveResult -> Encoding # toJSONList :: [GiveResult] -> Value # toEncodingList :: [GiveResult] -> Encoding #
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 #
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.2.6.2-GEMsKgeRG8f5Pv7LGY4Jhr" '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

ToJSON HighlightingInfo Source #
Instance details Defined in Agda.IR Methods toJSON :: HighlightingInfo -> Value # toEncoding :: HighlightingInfo -> Encoding # toJSONList :: [HighlightingInfo] -> Value # toEncodingList :: [HighlightingInfo] -> Encoding #
Generic HighlightingInfo Source #
Instance details Defined in Agda.IR Associated Types type Rep HighlightingInfo :: Type -> Type # Methods from :: HighlightingInfo -> Rep HighlightingInfo x # to :: Rep HighlightingInfo x -> HighlightingInfo #
Show HighlightingInfo Source #
Instance details Defined in Agda.IR Methods showsPrec :: Int -> HighlightingInfo -> ShowS # show :: HighlightingInfo -> String # showList :: [HighlightingInfo] -> ShowS #
type Rep HighlightingInfo Source #
Instance details Defined in Agda.IR type Rep HighlightingInfo = D1 ('MetaData "HighlightingInfo" "Agda.IR" "agda-language-server-0.2.2.6.2-GEMsKgeRG8f5Pv7LGY4Jhr" '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

ToJSON HighlightingInfos Source #
Instance details Defined in Agda.IR Methods toJSON :: HighlightingInfos -> Value # toEncoding :: HighlightingInfos -> Encoding # toJSONList :: [HighlightingInfos] -> Value # toEncodingList :: [HighlightingInfos] -> Encoding #
Generic HighlightingInfos Source #
Instance details Defined in Agda.IR Associated Types type Rep HighlightingInfos :: Type -> Type # Methods from :: HighlightingInfos -> Rep HighlightingInfos x # to :: Rep HighlightingInfos x -> HighlightingInfos #
Show HighlightingInfos Source #
Instance details Defined in Agda.IR Methods showsPrec :: Int -> HighlightingInfos -> ShowS # show :: HighlightingInfos -> String # showList :: [HighlightingInfos] -> ShowS #
type Rep HighlightingInfos Source #
Instance details Defined in Agda.IR type Rep HighlightingInfos = D1 ('MetaData "HighlightingInfos" "Agda.IR" "agda-language-server-0.2.2.6.2-GEMsKgeRG8f5Pv7LGY4Jhr" '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])))

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

DisplayInfoGeneric String [Block]
DisplayInfoAllGoalsWarnings String [Block] [Block] [String] [String]
DisplayInfoCurrentGoal Block
DisplayInfoInferredType Block
DisplayInfoCompilationOk [String] [String]
DisplayInfoAuto String
DisplayInfoError String
DisplayInfoTime String
DisplayInfoNormalForm String