{-# LANGUAGE CPP #-}

------------------------------------------------------------------------
-- | Data type for all interactive responses
------------------------------------------------------------------------

module Agda.Interaction.Response
  ( Response (..)
  , RemoveTokenBasedHighlighting (..)
  , MakeCaseVariant (..)
  , DisplayInfo (..)
  , Status (..)
  , GiveResult (..)
  , InteractionOutputCallback
  , defaultInteractionOutputCallback
  ) where

import Agda.Interaction.Highlighting.Precise
import {-# SOURCE #-} Agda.TypeChecking.Monad.Base
import Agda.Syntax.Common   (InteractionId(..))
import Agda.Syntax.Concrete (Expr)
import Agda.Utils.Pretty

import Control.Monad.Trans
import Data.Int
import System.IO

#include "undefined.h"
import Agda.Utils.Impossible

-- | 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 Response
    = Resp_HighlightingInfo
        HighlightingInfo
        RemoveTokenBasedHighlighting
        HighlightingMethod
        ModuleToSource
    | Resp_Status Status
    | Resp_JumpToError FilePath Int32
    | Resp_InteractionPoints [InteractionId]
    | Resp_GiveAction InteractionId GiveResult
    | Resp_MakeCase MakeCaseVariant [String]
    | 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.

-- | Should token-based highlighting be removed in conjunction with
-- the application of new highlighting (in order to reduce the risk of
-- flicker)?

data RemoveTokenBasedHighlighting
  = RemoveHighlighting
    -- ^ Yes, remove all token-based highlighting from the file.
  | KeepHighlighting
    -- ^ No.

-- | There are two kinds of \"make case\" commands.

data MakeCaseVariant = Function | ExtendedLambda

-- | Info to display at the end of an interactive command

data DisplayInfo
    = Info_CompilationOk String String
      -- ^ Strings are the warnings and the (non-fatal) errors
    | Info_Constraints String
    | Info_AllGoalsWarnings String String String
        -- ^ Strings are the goals, the warnings and the (non-fatal) errors
    | Info_Time Doc
    | 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_SearchAbout Doc
    | Info_WhyInScope Doc
    | Info_NormalForm Doc
    | Info_GoalType Doc
    | Info_CurrentGoal Doc
    | Info_InferredType Doc
    | Info_Context Doc
    | Info_HelperFunction Doc
    | Info_Version
        deriving Show

-- | Status information.

data Status = Status
  { sShowImplicitArguments :: Bool
    -- ^ Are implicit arguments displayed?
  , sChecked               :: Bool
    -- ^ Has the module been successfully type checked?
  }

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

data GiveResult
    = Give_String String
    | Give_Paren
    | Give_NoParen

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

type InteractionOutputCallback = Response -> TCM ()

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

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__