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

Safe HaskellNone
LanguageHaskell98

Agda.Interaction.Response

Description

Data type for all interactive responses

Synopsis

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.

data MakeCaseVariant Source

There are two kinds of "make case" commands.

Constructors

Function 
ExtendedLambda 

data DisplayInfo Source

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_WhyInScope Doc 
Info_NormalForm Doc 
Info_GoalType Doc 
Info_CurrentGoal Doc 
Info_InferredType Doc 
Info_Context Doc 
Info_HelperFunction Doc 
Info_Version 

data Status Source

Status information.

Constructors

Status 

Fields

sShowImplicitArguments :: Bool

Are implicit arguments displayed?

sChecked :: Bool

Has the module been successfully type checked?

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).

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).