1------------------------------------------------------------------------
2-- | Data type for all interactive responses
3------------------------------------------------------------------------
4
5module Agda.Interaction.Response
6  ( Response (..)
7  , RemoveTokenBasedHighlighting (..)
8  , MakeCaseVariant (..)
9  , DisplayInfo (..)
10  , GoalDisplayInfo(..)
11  , Goals
12  , WarningsAndNonFatalErrors
13  , Info_Error(..)
14  , GoalTypeAux(..)
15  , ResponseContextEntry(..)
16  , Status (..)
17  , GiveResult (..)
18  , InteractionOutputCallback
19  , defaultInteractionOutputCallback
20  ) where
21
22import Agda.Interaction.Base
23  (CommandState, OutputForm, ComputeMode, Rewrite, OutputConstraint, OutputConstraint')
24import Agda.Interaction.Highlighting.Precise
25import qualified Agda.Syntax.Abstract as A
26import Agda.Syntax.Common   (InteractionId(..), Arg)
27import Agda.Syntax.Concrete (Expr, Name)
28import Agda.Syntax.Concrete.Name (NameInScope)
29import Agda.Syntax.Scope.Base (AbstractModule, AbstractName, LocalVar)
30import qualified Agda.Syntax.Internal as I
31import {-# SOURCE #-} Agda.TypeChecking.Monad.Base
32  (TCM, TCErr, TCWarning, HighlightingMethod, ModuleToSource, NamedMeta, TCWarning, IPBoundary')
33import Agda.TypeChecking.Warnings (WarningsAndNonFatalErrors)
34import Agda.Utils.Impossible
35import Agda.Utils.Time
36
37import Control.Monad.Trans
38import Data.Int
39import System.IO
40
41-- | Responses for any interactive interface
42--
43--   Note that the response is given in pieces and incrementally,
44--   so the user can have timely response even during long computations.
45
46data Response
47    = Resp_HighlightingInfo
48        HighlightingInfo
49        RemoveTokenBasedHighlighting
50        HighlightingMethod
51        ModuleToSource
52    | Resp_Status Status
53    | Resp_JumpToError FilePath Int32
54    | Resp_InteractionPoints [InteractionId]
55    | Resp_GiveAction InteractionId GiveResult
56    | Resp_MakeCase InteractionId MakeCaseVariant [String]
57      -- ^ Response is list of printed clauses.
58    | Resp_SolveAll [(InteractionId, Expr)]
59      -- ^ Solution for one or more meta-variables.
60    | Resp_DisplayInfo DisplayInfo
61    | Resp_RunningInfo Int String
62      -- ^ The integer is the message's debug level.
63    | Resp_ClearRunningInfo
64    | Resp_ClearHighlighting TokenBased
65      -- ^ Clear highlighting of the given kind.
66    | Resp_DoneAborting
67      -- ^ A command sent when an abort command has completed
68      -- successfully.
69    | Resp_DoneExiting
70      -- ^ A command sent when an exit command is about to be
71      -- completed.
72
73-- | Should token-based highlighting be removed in conjunction with
74-- the application of new highlighting (in order to reduce the risk of
75-- flicker)?
76
77data RemoveTokenBasedHighlighting
78  = RemoveHighlighting
79    -- ^ Yes, remove all token-based highlighting from the file.
80  | KeepHighlighting
81    -- ^ No.
82
83-- | There are two kinds of \"make case\" commands.
84
85data MakeCaseVariant = Function | ExtendedLambda
86
87-- | Info to display at the end of an interactive command
88
89data DisplayInfo
90    = Info_CompilationOk WarningsAndNonFatalErrors
91    | Info_Constraints [OutputForm Expr Expr]
92    | Info_AllGoalsWarnings Goals WarningsAndNonFatalErrors
93    | Info_Time CPUTime
94    | Info_Error Info_Error
95        -- ^ When an error message is displayed this constructor should be
96        -- used, if appropriate.
97    | Info_Intro_NotFound
98    | Info_Intro_ConstructorUnknown [String]
99    | Info_Auto String
100        -- ^ 'Info_Auto' denotes either an error or a success (when 'Resp_GiveAction' is present)
101        --   TODO: split these into separate constructors
102    | Info_ModuleContents [Name] I.Telescope [(Name, I.Type)]
103    | Info_SearchAbout [(Name, I.Type)] String
104    | Info_WhyInScope String FilePath (Maybe LocalVar) [AbstractName] [AbstractModule]
105    | Info_NormalForm CommandState ComputeMode (Maybe CPUTime) A.Expr
106    | Info_InferredType CommandState (Maybe CPUTime) A.Expr
107    | Info_Context InteractionId [ResponseContextEntry]
108    | Info_Version
109    | Info_GoalSpecific InteractionId GoalDisplayInfo
110
111data GoalDisplayInfo
112    = Goal_HelperFunction (OutputConstraint' A.Expr A.Expr)
113    | Goal_NormalForm ComputeMode A.Expr
114    | Goal_GoalType Rewrite GoalTypeAux [ResponseContextEntry] [IPBoundary' Expr] [OutputForm Expr Expr]
115    | Goal_CurrentGoal Rewrite
116    | Goal_InferredType A.Expr
117
118-- | Goals & Warnings
119type Goals = ( [OutputConstraint A.Expr InteractionId] -- visible metas (goals)
120             , [OutputConstraint A.Expr NamedMeta]     -- hidden (unsolved) metas
121             )
122
123-- | Errors that goes into Info_Error
124--
125--   When an error message is displayed this constructor should be
126--   used, if appropriate.
127data Info_Error
128    = Info_GenericError TCErr
129    | Info_CompilationError [TCWarning]
130    | Info_HighlightingParseError InteractionId
131    | Info_HighlightingScopeCheckError InteractionId
132
133-- | Auxiliary information that comes with Goal Type
134
135data GoalTypeAux
136    = GoalOnly
137    | GoalAndHave A.Expr
138    | GoalAndElaboration I.Term
139
140-- | Entry in context.
141
142data ResponseContextEntry = ResponseContextEntry
143  { respOrigName :: Name        -- ^ The original concrete name.
144  , respReifName :: Name        -- ^ The name reified from abstract syntax.
145  , respType     :: Arg A.Expr  -- ^ The type.
146  , respLetValue :: Maybe A.Expr -- ^ The value (if it is a let-bound variable)
147  , respInScope  :: NameInScope -- ^ Whether the 'respReifName' is in scope.
148  }
149
150
151-- | Status information.
152
153data Status = Status
154  { sShowImplicitArguments :: Bool
155    -- ^ Are implicit arguments displayed?
156  , sShowIrrelevantArguments :: Bool
157    -- ^ Are irrelevant arguments displayed?
158  , sChecked               :: Bool
159    -- ^ Has the module been successfully type checked?
160  }
161
162-- | Give action result
163--
164--   Comment derived from agda2-mode.el
165--
166--   If 'GiveResult' is 'Give_String s', then the goal is replaced by 's',
167--   and otherwise the text inside the goal is retained (parenthesised
168--   if 'GiveResult' is 'Give_Paren').
169
170data GiveResult
171    = Give_String String
172    | Give_Paren
173    | Give_NoParen
174
175-- | Callback fuction to call when there is a response
176--   to give to the interactive frontend.
177--
178--   Note that the response is given in pieces and incrementally,
179--   so the user can have timely response even during long computations.
180--
181--   Typical 'InteractionOutputCallback' functions:
182--
183--    * Convert the response into a 'String' representation and
184--      print it on standard output
185--      (suitable for inter-process communication).
186--
187--    * Put the response into a mutable variable stored in the
188--      closure of the 'InteractionOutputCallback' function.
189--      (suitable for intra-process communication).
190
191type InteractionOutputCallback = Response -> TCM ()
192
193-- | The default 'InteractionOutputCallback' function prints certain
194-- things to stdout (other things generate internal errors).
195
196defaultInteractionOutputCallback :: InteractionOutputCallback
197defaultInteractionOutputCallback = \case
198  Resp_HighlightingInfo {}  -> __IMPOSSIBLE__
199  Resp_Status {}            -> __IMPOSSIBLE__
200  Resp_JumpToError {}       -> __IMPOSSIBLE__
201  Resp_InteractionPoints {} -> __IMPOSSIBLE__
202  Resp_GiveAction {}        -> __IMPOSSIBLE__
203  Resp_MakeCase {}          -> __IMPOSSIBLE__
204  Resp_SolveAll {}          -> __IMPOSSIBLE__
205  Resp_DisplayInfo {}       -> __IMPOSSIBLE__
206  Resp_RunningInfo _ s      -> liftIO $ do
207                                 putStr s
208                                 hFlush stdout
209  Resp_ClearRunningInfo {}  -> __IMPOSSIBLE__
210  Resp_ClearHighlighting {} -> __IMPOSSIBLE__
211  Resp_DoneAborting {}      -> __IMPOSSIBLE__
212  Resp_DoneExiting {}       -> __IMPOSSIBLE__
213