Safe Haskell	None
Language	Haskell2010

Agda.Interaction.Response.Base

Description

Data type for all interactive responses

Synopsis

data Response_boot tcErr tcWarning warningsAndNonFatalErrors
- = Resp_HighlightingInfo HighlightingInfo RemoveTokenBasedHighlighting HighlightingMethod ModuleToSource
- | Resp_Status Status
- | Resp_JumpToError FilePath Int32
- | Resp_InteractionPoints [InteractionId]
- | Resp_GiveAction InteractionId GiveResult
- | Resp_MakeCase InteractionId MakeCaseVariant [String]
- | Resp_SolveAll [(InteractionId, Expr)]
- | Resp_Mimer InteractionId (Maybe String)
- | Resp_DisplayInfo (DisplayInfo_boot tcErr tcWarning warningsAndNonFatalErrors)
- | Resp_RunningInfo Int String
- | Resp_ClearRunningInfo
- | Resp_ClearHighlighting TokenBased
- | Resp_DoneAborting
- | Resp_DoneExiting
data RemoveTokenBasedHighlighting
- = RemoveHighlighting
- | KeepHighlighting
data MakeCaseVariant
- = Function
- | ExtendedLambda
data DisplayInfo_boot tcErr tcWarning warningsAndNonFatalErrors
- = Info_CompilationOk CompilerBackend warningsAndNonFatalErrors
- | Info_Constraints [OutputForm_boot tcErr Expr Expr]
- | Info_AllGoalsWarnings (Goals_boot tcErr) warningsAndNonFatalErrors
- | Info_Time CPUTime
- | Info_Error (Info_Error_boot tcErr tcWarning)
- | Info_Intro_NotFound
- | Info_Intro_ConstructorUnknown [String]
- | Info_Auto String
- | Info_ModuleContents [Name] Telescope [(Name, Type)]
- | Info_SearchAbout [(Name, Type)] String
- | Info_WhyInScope WhyInScopeData
- | Info_NormalForm CommandState ComputeMode (Maybe CPUTime) Expr
- | Info_InferredType CommandState (Maybe CPUTime) Expr
- | Info_Context InteractionId [ResponseContextEntry]
- | Info_Version
- | Info_GoalSpecific InteractionId (GoalDisplayInfo_boot tcErr)
data GoalDisplayInfo_boot tcErr
- = Goal_HelperFunction (OutputConstraint' Expr Expr)
- | Goal_NormalForm ComputeMode Expr
- | Goal_GoalType Rewrite GoalTypeAux [ResponseContextEntry] [IPFace' Expr] [OutputForm_boot tcErr Expr Expr]
- | Goal_CurrentGoal Rewrite
- | Goal_InferredType Expr
type Goals_boot tcErr = ([OutputConstraint_boot tcErr Expr InteractionId], [OutputConstraint_boot tcErr Expr NamedMeta])
data Info_Error_boot tcErr tcWarning
- = Info_GenericError tcErr
- | Info_CompilationError [tcWarning]
- | Info_HighlightingParseError InteractionId
- | Info_HighlightingScopeCheckError InteractionId
data GoalTypeAux
- = GoalOnly
- | GoalAndHave Expr [IPFace' Expr]
- | GoalAndElaboration Term
data ResponseContextEntry = ResponseContextEntry {
- respOrigName :: Name
- respReifName :: Name
- respType :: Arg Expr
- respLetValue :: Maybe Expr
- respInScope :: NameInScope
}
data Status = Status {
- sShowImplicitArguments :: Bool
- sShowIrrelevantArguments :: Bool
- sChecked :: Bool
}
data GiveResult
- = Give_String String
- | Give_Paren
- | Give_NoParen

Documentation

data Response_boot tcErr tcWarning warningsAndNonFatalErrors Source #

Responses for any interactive interface

Note that the response is given in pieces and incrementally, so the user can have timely response even during long computations.

Constructors

Resp_HighlightingInfo HighlightingInfo RemoveTokenBasedHighlighting HighlightingMethod ModuleToSource
Resp_Status Status
Resp_JumpToError FilePath Int32
Resp_InteractionPoints [InteractionId]
Resp_GiveAction InteractionId GiveResult
Resp_MakeCase InteractionId MakeCaseVariant [String]	Response is list of printed clauses.
Resp_SolveAll [(InteractionId, Expr)]	Solution for one or more meta-variables.
Resp_Mimer InteractionId (Maybe String)
Resp_DisplayInfo (DisplayInfo_boot tcErr tcWarning warningsAndNonFatalErrors)
Resp_RunningInfo Int String	The integer is the message's debug level.
Resp_ClearRunningInfo
Resp_ClearHighlighting TokenBased	Clear highlighting of the given kind.
Resp_DoneAborting	A command sent when an abort command has completed successfully.
Resp_DoneExiting	A command sent when an exit command is about to be completed.

Instances

Instances details

EncodeTCM Response Source #
Instance details Defined in Agda.Interaction.JSONTop Methods encodeTCM :: Response -> TCM Value Source #

data RemoveTokenBasedHighlighting Source #

Should token-based highlighting be removed in conjunction with the application of new highlighting (in order to reduce the risk of flicker)?

Constructors

RemoveHighlighting	Yes, remove all token-based highlighting from the file.
KeepHighlighting	No.

data MakeCaseVariant Source #

There are two kinds of "make case" commands.

Constructors

Function
ExtendedLambda

Instances

Instances details

EncodeTCM MakeCaseVariant Source #
Instance details Defined in Agda.Interaction.JSONTop Methods encodeTCM :: MakeCaseVariant -> TCM Value Source #
ToJSON MakeCaseVariant Source #
Instance details Defined in Agda.Interaction.JSONTop Methods toJSON :: MakeCaseVariant -> Value # toEncoding :: MakeCaseVariant -> Encoding # toJSONList :: [MakeCaseVariant] -> Value # toEncodingList :: [MakeCaseVariant] -> Encoding # omitField :: MakeCaseVariant -> Bool #

data DisplayInfo_boot tcErr tcWarning warningsAndNonFatalErrors Source #

Info to display at the end of an interactive command

Constructors

Info_CompilationOk CompilerBackend warningsAndNonFatalErrors
Info_Constraints [OutputForm_boot tcErr Expr Expr]
Info_AllGoalsWarnings (Goals_boot tcErr) warningsAndNonFatalErrors
Info_Time CPUTime
Info_Error (Info_Error_boot tcErr tcWarning)	When an error message is displayed this constructor should be used, if appropriate.
Info_Intro_NotFound
Info_Intro_ConstructorUnknown [String]
Info_Auto String	`Info_Auto` denotes either an error or a success (when `Resp_GiveAction` is present) TODO: split these into separate constructors
Info_ModuleContents [Name] Telescope [(Name, Type)]
Info_SearchAbout [(Name, Type)] String
Info_WhyInScope WhyInScopeData
Info_NormalForm CommandState ComputeMode (Maybe CPUTime) Expr
Info_InferredType CommandState (Maybe CPUTime) Expr
Info_Context InteractionId [ResponseContextEntry]
Info_Version
Info_GoalSpecific InteractionId (GoalDisplayInfo_boot tcErr)

Instances

Instances details

EncodeTCM DisplayInfo Source #
Instance details Defined in Agda.Interaction.JSONTop Methods encodeTCM :: DisplayInfo -> TCM Value Source #

data GoalDisplayInfo_boot tcErr Source #

type Goals_boot tcErr = ([OutputConstraint_boot tcErr Expr InteractionId], [OutputConstraint_boot tcErr Expr NamedMeta]) Source #

Goals & Warnings

data Info_Error_boot tcErr tcWarning Source #

Errors that goes into Info_Error

When an error message is displayed this constructor should be used, if appropriate.

Constructors

Info_GenericError tcErr
Info_CompilationError [tcWarning]
Info_HighlightingParseError InteractionId
Info_HighlightingScopeCheckError InteractionId

Instances

Instances details

EncodeTCM Info_Error Source #
Instance details Defined in Agda.Interaction.JSONTop Methods encodeTCM :: Info_Error -> TCM Value Source #

data GoalTypeAux Source #

Auxiliary information that comes with Goal Type

Constructors

GoalOnly
GoalAndHave Expr [IPFace' Expr]
GoalAndElaboration Term

Instances

Instances details

EncodeTCM GoalTypeAux Source #
Instance details Defined in Agda.Interaction.JSONTop Methods encodeTCM :: GoalTypeAux -> TCM Value Source #

data ResponseContextEntry Source #

Entry in context.

Constructors

ResponseContextEntry
Fields respOrigName :: Name The original concrete name. respReifName :: Name The name reified from abstract syntax. respType :: Arg Expr The type. respLetValue :: Maybe Expr The value (if it is a let-bound variable) respInScope :: NameInScope Whether the `respReifName` is in scope.

Instances

Instances details

EncodeTCM ResponseContextEntry Source #
Instance details Defined in Agda.Interaction.JSONTop Methods encodeTCM :: ResponseContextEntry -> TCM Value Source #

data Status Source #

Status information.

Constructors

Status
Fields sShowImplicitArguments :: Bool Are implicit arguments displayed? sShowIrrelevantArguments :: Bool Are irrelevant arguments displayed? sChecked :: Bool Has the module been successfully type checked?

Instances

Instances details

EncodeTCM Status Source #
Instance details Defined in Agda.Interaction.JSONTop Methods encodeTCM :: Status -> TCM Value Source #
ToJSON Status Source #
Instance details Defined in Agda.Interaction.JSONTop Methods toJSON :: Status -> Value # toEncoding :: Status -> Encoding # toJSONList :: [Status] -> Value # toEncodingList :: [Status] -> Encoding # omitField :: Status -> Bool #

data GiveResult Source #

Give action result

Comment derived from agda2-mode.el

If GiveResult is 'Give_String s', then the goal is replaced by s, and otherwise the text inside the goal is retained (parenthesised if GiveResult is Give_Paren).

Constructors

Give_String String
Give_Paren
Give_NoParen

Instances

Instances details

EncodeTCM GiveResult Source #
Instance details Defined in Agda.Interaction.JSONTop Methods encodeTCM :: GiveResult -> TCM Value Source #
ToJSON GiveResult Source #
Instance details Defined in Agda.Interaction.JSONTop Methods toJSON :: GiveResult -> Value # toEncoding :: GiveResult -> Encoding # toJSONList :: [GiveResult] -> Value # toEncodingList :: [GiveResult] -> Encoding # omitField :: GiveResult -> Bool #

Goal_HelperFunction (OutputConstraint' Expr Expr)
Goal_NormalForm ComputeMode Expr
Goal_GoalType Rewrite GoalTypeAux [ResponseContextEntry] [IPFace' Expr] [OutputForm_boot tcErr Expr Expr]
Goal_CurrentGoal Rewrite
Goal_InferredType Expr