    module Agda.Interaction.JSONTop
        ( jsonREPL
        ) where
    import Control.Monad.State

    import Data.Aeson hiding (Result(..))
    import Data.ByteString.Lazy (ByteString)
    import qualified Data.ByteString.Lazy.Char8 as BS

    import Agda.Interaction.AgdaTop
    import Agda.Interaction.Response as R
    import Agda.Interaction.EmacsCommand hiding (putResponse)
    import Agda.Interaction.Highlighting.JSON
    import Agda.Interaction.Highlighting.Precise (TokenBased(..))
    import Agda.Syntax.Common
    import Agda.TypeChecking.Monad
    import Agda.Utils.Pretty
    import Agda.VersionCommit

    ----------------------------------

    -- | 'jsonREPL' is a interpreter like 'mimicGHCi', but outputs JSON-encoded strings.
    --
    --   'jsonREPL' reads Haskell values (that starts from 'IOTCM' ...) from stdin,
    --   interprets them, and outputs JSON-encoded strings. into stdout.

    jsonREPL :: TCM () -> TCM ()
    jsonREPL = repl (liftIO . BS.putStrLn <=< liftIO . jsonifyResponse) "JSON> "

    instance ToJSON Status where
      toJSON status = object
        [ "showImplicitArguments" .= sShowImplicitArguments status
        , "checked" .= sChecked status
        ]

    instance ToJSON InteractionId where
      toJSON (InteractionId i) = toJSON i

    instance ToJSON GiveResult where
      toJSON (Give_String s) = toJSON s
      toJSON Give_Paren = toJSON True
      toJSON Give_NoParen = toJSON False

    instance ToJSON MakeCaseVariant where
      toJSON R.Function = String "Function"
      toJSON R.ExtendedLambda = String "ExtendedLambda"

    instance ToJSON DisplayInfo where
      toJSON (Info_CompilationOk warnings errors) = object
        [ "kind"        .= String "CompilationOk"
        , "warnings"    .= warnings
        , "errors"      .= errors
        ]
      toJSON (Info_Constraints constraints) = object
        [ "kind"        .= String "Constraints"
        , "constraints" .= constraints
        ]
      toJSON (Info_AllGoalsWarnings goals warnings errors) = object
        [ "kind"        .= String "AllGoalsWarnings"
        , "goals"       .= goals
        , "warnings"    .= warnings
        , "errors"      .= errors
        ]
      toJSON (Info_Time doc) = object [ "kind" .= String "Time", "payload" .= render doc ]
      toJSON (Info_Error msg) = object [ "kind" .= String "Error", "payload" .= msg ]
      toJSON (Info_Intro doc) = object [ "kind" .= String "Intro", "payload" .= render doc ]
      toJSON (Info_Auto msg) = object [ "kind" .= String "Auto", "payload" .= msg ]
      toJSON (Info_ModuleContents doc) = object [ "kind" .= String "ModuleContents", "payload" .= render doc ]
      toJSON (Info_SearchAbout doc) = object [ "kind" .= String "SearchAbout", "payload" .= render doc ]
      toJSON (Info_WhyInScope doc) = object [ "kind" .= String "WhyInScope", "payload" .= render doc ]
      toJSON (Info_NormalForm doc) = object [ "kind" .= String "NormalForm", "payload" .= render doc ]
      toJSON (Info_GoalType doc) = object [ "kind" .= String "GoalType", "payload" .= render doc ]
      toJSON (Info_CurrentGoal doc) = object [ "kind" .= String "CurrentGoal", "payload" .= render doc ]
      toJSON (Info_InferredType doc) = object [ "kind" .= String "InferredType", "payload" .= render doc ]
      toJSON (Info_Context doc) = object [ "kind" .= String "Context", "payload" .= render doc ]
      toJSON (Info_HelperFunction doc) = object [ "kind" .= String "HelperFunction", "payload" .= render doc ]
      toJSON Info_Version = object
        [ "kind" .= String "Version"
        , "version" .= (("Agda version " ++ versionWithCommitInfo) :: String)
        ]

    -- | Convert Response to an JSON value for interactive editor frontends.
    jsonifyResponse :: Response -> IO ByteString
    jsonifyResponse (Resp_HighlightingInfo info remove method modFile) =
       encode <$> jsonifyHighlightingInfo info remove method modFile
    jsonifyResponse (Resp_DisplayInfo info) = return $ encode $ object
      [ "kind" .= String "DisplayInfo"
      , "info" .= info
      ]
    jsonifyResponse (Resp_ClearHighlighting tokenBased) = return $ encode $ object
      [ "kind"          .= String "ClearHighlighting"
      , "tokenBased"    .= tokenBased
      ]
    jsonifyResponse Resp_DoneAborting = return $ encode $ object [ "kind" .= String "DoneAborting" ]
    jsonifyResponse Resp_ClearRunningInfo = return $ encode $ object [ "kind" .= String "ClearRunningInfo" ]
    jsonifyResponse (Resp_RunningInfo debugLevel msg) = return $ encode $ object
      [ "kind"          .= String "RunningInfo"
      , "debugLevel"    .= debugLevel
      , "message"       .= msg
      ]
    jsonifyResponse (Resp_Status status) = return $ encode $ object
      [ "kind"          .= String "Status"
      , "status"        .= status
      ]
    jsonifyResponse (Resp_JumpToError filepath position) = return $ encode $ object
      [ "kind"          .= String "JumpToError"
      , "filepath"      .= filepath
      , "position"      .= position
      ]
    jsonifyResponse (Resp_InteractionPoints interactionPoints) = return $ encode $ object
      [ "kind"              .= String "InteractionPoints"
      , "interactionPoints" .= interactionPoints
      ]
    jsonifyResponse (Resp_GiveAction i giveResult) = return $ encode $ object
      [ "kind"              .= String "GiveAction"
      , "interactionPoint"  .= i
      , "giveResult"        .= giveResult
      ]
    jsonifyResponse (Resp_MakeCase variant clauses) = return $ encode $ object
      [ "kind"          .= String "MakeCase"
      , "variant"       .= variant
      , "clauses"       .= clauses
      ]
    jsonifyResponse (Resp_SolveAll solutions) = return $ encode $ object
      [ "kind"          .= String "SolveAll"
      , "solutions"     .= map encodeSolution solutions
      ]
      where
        encodeSolution (i, expr) = object
          [ "interactionPoint"  .= i
          , "expression"        .= show expr
          ]