module Agda.Interaction.Response
( Response (..)
, RemoveTokenBasedHighlighting (..)
, MakeCaseVariant (..)
, DisplayInfo (..)
, GoalDisplayInfo(..)
, Goals
, WarningsAndNonFatalErrors
, Info_Error(..)
, GoalTypeAux(..)
, ResponseContextEntry(..)
, Status (..)
, GiveResult (..)
, InteractionOutputCallback
, defaultInteractionOutputCallback
) where
import Agda.Interaction.Base
(CommandState, OutputForm, ComputeMode, Rewrite, OutputConstraint, OutputConstraint')
import Agda.Interaction.Highlighting.Precise
import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Common (InteractionId(..), Arg)
import Agda.Syntax.Concrete (Expr, Name)
import Agda.Syntax.Concrete.Name (NameInScope)
import Agda.Syntax.Scope.Base (AbstractModule, AbstractName, LocalVar)
import qualified Agda.Syntax.Internal as I
import {-# SOURCE #-} Agda.TypeChecking.Monad.Base
(TCM, TCErr, TCWarning, HighlightingMethod, ModuleToSource, NamedMeta, TCWarning, IPBoundary')
import Agda.TypeChecking.Warnings (WarningsAndNonFatalErrors)
import Agda.Utils.Impossible
import Agda.Utils.Time
import Control.Monad.Trans
import Data.Int
import System.IO
import Agda.Utils.Pretty (Doc)
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 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] I.Telescope [(Name, I.Type)]
| Info_SearchAbout [(Name, I.Type)] String
| Info_WhyInScope String FilePath (Maybe LocalVar) [AbstractName] [AbstractModule]
| Info_NormalForm CommandState ComputeMode (Maybe CPUTime) A.Expr
| Info_InferredType CommandState (Maybe CPUTime) A.Expr
| Info_Context InteractionId [ResponseContextEntry]
| Info_Version
| Info_GoalSpecific InteractionId GoalDisplayInfo
data GoalDisplayInfo
= Goal_HelperFunction (OutputConstraint' A.Expr A.Expr)
| Goal_NormalForm ComputeMode A.Expr
| Goal_GoalType Rewrite GoalTypeAux [ResponseContextEntry] [IPBoundary' Expr] [OutputForm Expr Expr]
| Goal_CurrentGoal Rewrite
| Goal_InferredType A.Expr
type Goals = ( [OutputConstraint A.Expr InteractionId]
, [OutputConstraint A.Expr NamedMeta]
)
data Info_Error
= Info_GenericError TCErr
| Info_CompilationError [TCWarning]
| Info_HighlightingParseError InteractionId
| Info_HighlightingScopeCheckError InteractionId
data GoalTypeAux
= GoalOnly
| GoalAndHave A.Expr
| GoalAndElaboration I.Term
data ResponseContextEntry = ResponseContextEntry
{ respOrigName :: Name
, respReifName :: Name
, respType :: Arg A.Expr
, respLetValue :: Maybe A.Expr
, respInScope :: NameInScope
}
data Status = Status
{ sShowImplicitArguments :: Bool
, sChecked :: Bool
}
data GiveResult
= Give_String String
| Give_Paren
| Give_NoParen
type InteractionOutputCallback = Response -> TCM ()
defaultInteractionOutputCallback :: InteractionOutputCallback
defaultInteractionOutputCallback r = case r of
Resp_HighlightingInfo {} -> __IMPOSSIBLE__
Resp_Status {} -> __IMPOSSIBLE__
Resp_JumpToError {} -> __IMPOSSIBLE__
Resp_InteractionPoints {} -> __IMPOSSIBLE__
Resp_GiveAction {} -> __IMPOSSIBLE__
Resp_MakeCase {} -> __IMPOSSIBLE__
Resp_SolveAll {} -> __IMPOSSIBLE__
Resp_DisplayInfo {} -> __IMPOSSIBLE__
Resp_RunningInfo _ s -> liftIO $ do
putStr s
hFlush stdout
Resp_ClearRunningInfo {} -> __IMPOSSIBLE__
Resp_ClearHighlighting {} -> __IMPOSSIBLE__
Resp_DoneAborting {} -> __IMPOSSIBLE__
Resp_DoneExiting {} -> __IMPOSSIBLE__