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

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 Word32
  - | 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 (Set tcWarning)
  - | Info_HighlightingParseError InteractionId
  - | Info_HighlightingScopeCheckError InteractionId
- data GoalTypeAux
  - = GoalOnly
  - | GoalAndHave Expr [IPFace' Expr]
  - | GoalAndElaboration Expr
- 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 Word32 |
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 Source # toEncoding :: MakeCaseVariant -> Encoding Source # toJSONList :: [MakeCaseVariant] -> Value Source # toEncodingList :: [MakeCaseVariant] -> Encoding Source # omitField :: MakeCaseVariant -> Bool Source #

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 #

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]) 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 (Set 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 Expr |

#### 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 Source # toEncoding :: Status -> Encoding Source # toJSONList :: [Status] -> Value Source # toEncodingList :: [Status] -> Encoding Source # omitField :: Status -> Bool Source #

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 Source # toEncoding :: GiveResult -> Encoding Source # toJSONList :: [GiveResult] -> Value Source # toEncodingList :: [GiveResult] -> Encoding Source # omitField :: GiveResult -> Bool Source #