Agda.Interaction.Response.Base

Data type for all interactive responses

Documentation

data Response_boot tcErr tcWarning warningsAndNonFatalErrors

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

EncodeTCM Response

Defined in Agda.Interaction.JSONTop

Methods

encodeTCM :: Response -> TCM Value

data RemoveTokenBasedHighlighting

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

There are two kinds of "make case" commands.

Constructors

Function

ExtendedLambda

Instances

EncodeTCM MakeCaseVariant

Defined in Agda.Interaction.JSONTop

Methods

encodeTCM :: MakeCaseVariant -> TCM Value

ToJSON MakeCaseVariant

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

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

EncodeTCM DisplayInfo

Defined in Agda.Interaction.JSONTop

Methods

encodeTCM :: DisplayInfo -> TCM Value

data GoalDisplayInfo_boot tcErr

Constructors

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])

Goals & Warnings

data Info_Error_boot tcErr tcWarning

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

EncodeTCM Info_Error

Defined in Agda.Interaction.JSONTop

Methods

encodeTCM :: Info_Error -> TCM Value

data GoalTypeAux

Auxiliary information that comes with Goal Type

Constructors

GoalOnly

GoalAndHave Expr [IPFace' Expr]

GoalAndElaboration Term

Instances

EncodeTCM GoalTypeAux

Defined in Agda.Interaction.JSONTop

Methods

encodeTCM :: GoalTypeAux -> TCM Value

data ResponseContextEntry

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

EncodeTCM ResponseContextEntry

Defined in Agda.Interaction.JSONTop

Methods

encodeTCM :: ResponseContextEntry -> TCM Value

data Status

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

EncodeTCM Status

Defined in Agda.Interaction.JSONTop

Methods

encodeTCM :: Status -> TCM Value

ToJSON Status

Defined in Agda.Interaction.JSONTop

Methods

toJSON :: Status -> Value

toEncoding :: Status -> Encoding

toJSONList :: [Status] -> Value

toEncodingList :: [Status] -> Encoding

omitField :: Status -> Bool

data GiveResult

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

EncodeTCM GiveResult

Defined in Agda.Interaction.JSONTop

Methods

encodeTCM :: GiveResult -> TCM Value

ToJSON GiveResult

Defined in Agda.Interaction.JSONTop

Methods

toJSON :: GiveResult -> Value

toEncoding :: GiveResult -> Encoding

toJSONList :: [GiveResult] -> Value

toEncodingList :: [GiveResult] -> Encoding

omitField :: GiveResult -> Bool