Agda.Interaction.Response

Data type for all interactive responses

Documentation

data Response

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_DisplayInfo DisplayInfo

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

data DisplayInfo

Info to display at the end of an interactive command

Constructors

Info_CompilationOk CompilerBackend WarningsAndNonFatalErrors

Info_Constraints [OutputForm Expr Expr]

Info_AllGoalsWarnings Goals WarningsAndNonFatalErrors

Info_Time CPUTime

Info_Error Info_Error

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 String FilePath (Maybe LocalVar) [AbstractName] [AbstractModule]

Info_NormalForm CommandState ComputeMode (Maybe CPUTime) Expr

Info_InferredType CommandState (Maybe CPUTime) Expr

Info_Context InteractionId [ResponseContextEntry]

Info_Version

Info_GoalSpecific InteractionId GoalDisplayInfo

Instances

EncodeTCM DisplayInfo

Defined in Agda.Interaction.JSONTop

Methods

encodeTCM :: DisplayInfo -> TCM Value

data GoalDisplayInfo

Constructors

Goal_HelperFunction (OutputConstraint' Expr Expr)

Goal_NormalForm ComputeMode Expr

Goal_GoalType Rewrite GoalTypeAux [ResponseContextEntry] [IPBoundary' Expr] [OutputForm Expr Expr]

Goal_CurrentGoal Rewrite

Goal_InferredType Expr

type Goals = ([OutputConstraint Expr InteractionId], [OutputConstraint Expr NamedMeta])

Goals & Warnings

data WarningsAndNonFatalErrors

Assorted warnings and errors to be displayed to the user

data Info_Error

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

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

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

type InteractionOutputCallback = Response -> TCM ()

Callback fuction to call when there is a response to give to the interactive frontend.

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

Typical InteractionOutputCallback functions:

• Convert the response into a Aspect representation and print it on standard output (suitable for inter-process communication).
• Put the response into a mutable variable stored in the closure of the InteractionOutputCallback function. (suitable for intra-process communication).

defaultInteractionOutputCallback :: InteractionOutputCallback

The default InteractionOutputCallback function prints certain things to stdout (other things generate internal errors).