Agda-2.3.2: A dependently typed functional programming language and proof assistant

Safe Haskell | None

Agda.Interaction.Response

Description

Data type for all interactive responses

Synopsis

- data Response
  - = Resp_HighlightingInfo HighlightingInfo ModuleToSource
  - | Resp_Status Status
  - | Resp_JumpToError FilePath Int32
  - | Resp_InteractionPoints [InteractionId]
  - | Resp_GiveAction InteractionId GiveResult
  - | Resp_MakeCaseAction [String]
  - | Resp_MakeCase String [String]
  - | Resp_SolveAll [(InteractionId, Expr)]
  - | Resp_DisplayInfo DisplayInfo
  - | Resp_RunningInfo String
  - | Resp_ClearRunningInfo
  - | Resp_ClearHighlighting
- data DisplayInfo
  - = Info_CompilationOk
  - | Info_Constraints String
  - | Info_AllGoals String
  - | Info_Error String
  - | Info_Intro Doc
  - | Info_Auto String
  - | Info_ModuleContents Doc
  - | Info_NormalForm Doc
  - | Info_GoalType Doc
  - | Info_CurrentGoal Doc
  - | Info_InferredType Doc
  - | Info_Context Doc
- data Status = Status {
  - sShowImplicitArguments :: Bool
  - sChecked :: Bool
  }
- data GiveResult
  - = Give_String String
  - | Give_Paren
  - | Give_NoParen
- type InteractionOutputCallback = Response -> TCM ()
- defaultInteractionOutputCallback :: InteractionOutputCallback

# 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 ModuleToSource |
Resp_Status Status |
Resp_JumpToError FilePath Int32 |
Resp_InteractionPoints [InteractionId] |
Resp_GiveAction InteractionId GiveResult |
Resp_MakeCaseAction [String] |
Resp_MakeCase String [String] |
Resp_SolveAll [(InteractionId, Expr)] |
Resp_DisplayInfo DisplayInfo |
Resp_RunningInfo String |
Resp_ClearRunningInfo |
Resp_ClearHighlighting |

data DisplayInfo

Info to display at the end of an interactive command

Constructors

Info_CompilationOk |
Info_Constraints String |
Info_AllGoals String |
Info_Error String | When an error message is displayed this constructor should be used, if appropriate.
Info_Intro Doc | `Info_Intro` denotes two different types of errors TODO: split these into separate constructors
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 Doc |
Info_NormalForm Doc |
Info_GoalType Doc |
Info_CurrentGoal Doc |
Info_InferredType Doc |
Info_Context Doc |

Instances

Show DisplayInfo |

data Status

Status information.

Constructors

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

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 |

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 `String` 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 is set to `__``IMPOSSIBLE__` because in this way it is easier to recognize that some response is lost due to an uninitialized `InteractionOutputCallback` function.