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

Safe Haskell | None
Language | Haskell2010

Agda.Interaction.Response

Synopsis

- type Response = Response_boot TCErr TCWarning WarningsAndNonFatalErrors
- type Goals = Goals_boot TCErr
- type Info_Error = Info_Error_boot TCErr TCWarning
- type DisplayInfo = DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
- type GoalDisplayInfo = GoalDisplayInfo_boot TCErr
- module Agda.Interaction.Response.Base
- data WarningsAndNonFatalErrors
- type InteractionOutputCallback = Response_boot TCErr TCWarning WarningsAndNonFatalErrors -> TCM ()
- defaultInteractionOutputCallback :: InteractionOutputCallback

# Documentation

type Response = Response_boot TCErr TCWarning WarningsAndNonFatalErrors Source #

type Goals = Goals_boot TCErr Source #

type Info_Error = Info_Error_boot TCErr TCWarning Source #

type DisplayInfo = DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors Source #

type GoalDisplayInfo = GoalDisplayInfo_boot TCErr Source #

module Agda.Interaction.Response.Base

data WarningsAndNonFatalErrors Source #

Assorted warnings and errors to be displayed to the user

#### Instances

Instances details

EncodeTCM DisplayInfo Source # |
Instance details Defined in Agda.Interaction.JSONTop Methods encodeTCM :: DisplayInfo -> TCM Value Source #
EncodeTCM Response Source # |
Instance details Defined in Agda.Interaction.JSONTop Methods encodeTCM :: Response -> TCM Value Source #
Null WarningsAndNonFatalErrors Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods empty :: WarningsAndNonFatalErrors Source # null :: WarningsAndNonFatalErrors -> Bool Source #

type InteractionOutputCallback = Response_boot TCErr TCWarning WarningsAndNonFatalErrors -> 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).