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

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.Interaction.Response

Description

Data type for all interactive responses

Synopsis

- data Response
  - = 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_DisplayInfo DisplayInfo
  - | Resp_RunningInfo Int String
  - | Resp_ClearRunningInfo
  - | Resp_ClearHighlighting TokenBased
  - | Resp_DoneAborting
  - | Resp_DoneExiting
- data RemoveTokenBasedHighlighting
  - = RemoveHighlighting
  - | KeepHighlighting
- data MakeCaseVariant
  - = Function
  - | ExtendedLambda
- data DisplayInfo
  - = Info_CompilationOk CompilerBackend WarningsAndNonFatalErrors
  - | Info_Constraints [OutputForm Expr Expr]
  - | Info_AllGoalsWarnings Goals WarningsAndNonFatalErrors
  - | Info_Time CPUTime
  - | Info_Error Info_Error
  - | Info_Intro_NotFound
  - | Info_Intro_ConstructorUnknown [String]
  - | Info_Auto String
  - | 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
- data GoalDisplayInfo
  - = 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])
- data WarningsAndNonFatalErrors
- data Info_Error
  - = Info_GenericError TCErr
  - | Info_CompilationError [TCWarning]
  - | Info_HighlightingParseError InteractionId
  - | Info_HighlightingScopeCheckError InteractionId
- data GoalTypeAux
  - = GoalOnly
  - | GoalAndHave 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
- type InteractionOutputCallback = Response -> TCM ()
- defaultInteractionOutputCallback :: InteractionOutputCallback

# Documentation

data Response 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_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

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 #

data DisplayInfo Source #

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

Instances details

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

data GoalDisplayInfo Source #

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

Goals & Warnings

data WarningsAndNonFatalErrors Source #

Assorted warnings and errors to be displayed to the user

data Info_Error 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 |
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 #

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 #

type InteractionOutputCallback = Response -> TCM () Source #

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 Source #

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