Safe Haskell	Safe-Inferred
Language	Haskell2010

Agda.Interaction.Response

Description

Data type for all interactive responses

Synopsis

data Response
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 WhyInScopeData
- | 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] [IPFace' Expr] [OutputForm Expr Expr]
- | Goal_CurrentGoal Rewrite
- | Goal_InferredType Expr
type Goals = ([OutputConstraint Expr InteractionId], [OutputConstraint Expr NamedMeta])
data WarningsAndNonFatalErrors
data Info_Error
data GoalTypeAux
- = GoalOnly
- | GoalAndHave Expr [IPFace' 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 # omitField :: MakeCaseVariant -> Bool #

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

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 [IPFace' 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 # omitField :: Status -> Bool #

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 # omitField :: GiveResult -> Bool #

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

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

Goal_HelperFunction (OutputConstraint' Expr Expr)
Goal_NormalForm ComputeMode Expr
Goal_GoalType Rewrite GoalTypeAux [ResponseContextEntry] [IPFace' Expr] [OutputForm Expr Expr]
Goal_CurrentGoal Rewrite
Goal_InferredType Expr