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
- = 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
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

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

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
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.1-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

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

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
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.1-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
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.2.2.1-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 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
ToJSON HighlightingInfo Source #
Instance details Defined in Agda.IR Methods toJSON :: HighlightingInfo -> Value toEncoding :: HighlightingInfo -> Encoding toJSONList :: [HighlightingInfo] -> Value toEncodingList :: [HighlightingInfo] -> Encoding
type Rep HighlightingInfo Source #
Instance details Defined in Agda.IR type Rep HighlightingInfo = D1 ('MetaData "HighlightingInfo" "Agda.IR" "agda-language-server-0.2.6.2.2.1-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 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
ToJSON HighlightingInfos Source #
Instance details Defined in Agda.IR Methods toJSON :: HighlightingInfos -> Value toEncoding :: HighlightingInfos -> Encoding toJSONList :: [HighlightingInfos] -> Value toEncodingList :: [HighlightingInfos] -> Encoding
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.1-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])))