{-# OPTIONS_GHC -Wno-missing-methods #-}

{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveGeneric #-}

module Agda
  ( start
  , runAgda
  , sendCommand
  , getCommandLineOptions
  ) where

import           Agda.Compiler.Backend          ( parseBackendOptions )
import           Agda.Compiler.Builtin          ( builtinBackends )
import           Agda.Convert                   ( fromResponse )
import           Agda.Interaction.Base          ( Command
                                                , Command'(Command, Done, Error)
                                                , CommandM
                                                , CommandState(optionsOnReload)
                                                , IOTCM
                                                , initCommandState
#if MIN_VERSION_Agda(2,6,3)
                                                , parseIOTCM
#endif
                                                )
import           Agda.Interaction.InteractionTop
                                                ( initialiseCommandQueue
                                                , maybeAbort
                                                , runInteraction
                                                )
import           Agda.Interaction.Options       ( CommandLineOptions
                                                  ( optAbsoluteIncludePaths
                                                  )
                                                , defaultOptions
                                                , runOptM
                                                )
import           Agda.TypeChecking.Errors       ( getAllWarningsOfTCErr
                                                , prettyError
                                                , prettyTCWarnings'
                                                )
import           Agda.TypeChecking.Monad        ( HasOptions
                                                , TCErr
                                                , commandLineOptions
                                                , runTCMTop'
                                                )
import           Agda.TypeChecking.Monad.Base   ( TCM )
import qualified Agda.TypeChecking.Monad.Benchmark
                                               as Bench
import           Agda.TypeChecking.Monad.State  ( setInteractionOutputCallback )
import           Agda.Utils.FileName            ( absolute )
import           Agda.Utils.Impossible          ( CatchImpossible
                                                  ( catchImpossible
                                                  )
                                                , Impossible
                                                )
import           Agda.VersionCommit             ( versionWithCommitInfo )
import           Control.Exception              ( SomeException
                                                , catch
                                                )
import           Control.Monad
import           Control.Monad.Except
import           Control.Monad.Reader
import           Control.Monad.State
import           Data.Aeson                     ( FromJSON
                                                , ToJSON(toJSON)
                                                , Value
                                                , fromJSON
                                                )
import qualified Data.Aeson                    as JSON
import           Data.Maybe                     ( listToMaybe )
import           Data.Text                      ( pack )
import           GHC.Generics                   ( Generic )
import           Language.LSP.Server            ( getConfig )
import           Monad
import           Options                        ( Config(configRawAgdaOptions)
                                                , Options(optRawAgdaOptions)
                                                )

getAgdaVersion :: String
getAgdaVersion :: String
getAgdaVersion = String
versionWithCommitInfo

start :: ServerM IO ()
start :: ServerM IO ()
start = do
  Env
env <- ReaderT Env IO Env
forall r (m :: * -> *). MonadReader r m => m r
ask

  Text -> ServerM IO ()
forall (m :: * -> *). (Monad m, MonadIO m) => Text -> ServerM m ()
writeLog Text
"[Agda] interaction start"

  Either String ()
result <- ServerM TCM () -> ServerM IO (Either String ())
forall (m :: * -> *) a.
MonadIO m =>
ServerM TCM a -> ServerM m (Either String a)
runAgda (ServerM TCM () -> ServerM IO (Either String ()))
-> ServerM TCM () -> ServerM IO (Either String ())
forall a b. (a -> b) -> a -> b
$ do
    -- decides how to output Response
    TCM () -> ServerM TCM ()
forall (m :: * -> *) a. Monad m => m a -> ReaderT Env m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM () -> ServerM TCM ()) -> TCM () -> ServerM TCM ()
forall a b. (a -> b) -> a -> b
$ InteractionOutputCallback -> TCM ()
setInteractionOutputCallback (InteractionOutputCallback -> TCM ())
-> InteractionOutputCallback -> TCM ()
forall a b. (a -> b) -> a -> b
$ \Response
response -> do
      Response
reaction <- Response -> TCM Response
fromResponse Response
response
      Env -> Response -> TCM ()
forall (m :: * -> *).
(Monad m, MonadIO m) =>
Env -> Response -> TCMT m ()
sendResponse Env
env Response
reaction

    -- keep reading command
    CommandQueue
commands <- IO CommandQueue -> ReaderT Env TCM CommandQueue
forall a. IO a -> ReaderT Env TCM a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO CommandQueue -> ReaderT Env TCM CommandQueue)
-> IO CommandQueue -> ReaderT Env TCM CommandQueue
forall a b. (a -> b) -> a -> b
$ IO Command -> IO CommandQueue
initialiseCommandQueue (Env -> IO Command
readCommand Env
env)

    -- get command line options
    CommandLineOptions
options  <- ServerM TCM CommandLineOptions
forall (m :: * -> *).
(HasOptions m, MonadIO m) =>
ServerM m CommandLineOptions
getCommandLineOptions

    -- start the loop
    let commandState :: CommandState
commandState = (CommandQueue -> CommandState
initCommandState CommandQueue
commands)
          { optionsOnReload = options { optAbsoluteIncludePaths = [] }
          }

    ((), CommandState)
_ <- (StateT CommandState TCM () -> TCM ((), CommandState))
-> ReaderT Env CommandM () -> ReaderT Env TCM ((), CommandState)
forall (m :: * -> *) a (n :: * -> *) b r.
(m a -> n b) -> ReaderT r m a -> ReaderT r n b
mapReaderT (StateT CommandState TCM ()
-> CommandState -> TCM ((), CommandState)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
`runStateT` CommandState
commandState) (Env -> ReaderT Env CommandM ()
loop Env
env)

    () -> ServerM TCM ()
forall a. a -> ReaderT Env TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  -- TODO: we should examine the result
  case Either String ()
result of
    Left  String
_err -> () -> ServerM IO ()
forall a. a -> ReaderT Env IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Right ()
_val -> () -> ServerM IO ()
forall a. a -> ReaderT Env IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
 where
  loop :: Env -> ServerM CommandM ()
  loop :: Env -> ReaderT Env CommandM ()
loop Env
env = do
    ReaderT Env CommandM ()
forall (m :: * -> *). MonadBench m => m ()
Bench.reset
    Bool
done <- Account (BenchPhase (ReaderT Env CommandM))
-> ReaderT Env CommandM Bool -> ReaderT Env CommandM Bool
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [] (ReaderT Env CommandM Bool -> ReaderT Env CommandM Bool)
-> ReaderT Env CommandM Bool -> ReaderT Env CommandM Bool
forall a b. (a -> b) -> a -> b
$ do
      Command' (Maybe ())
r <- CommandM (Command' (Maybe ()))
-> ReaderT Env CommandM (Command' (Maybe ()))
forall (m :: * -> *) a. Monad m => m a -> ReaderT Env m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (CommandM (Command' (Maybe ()))
 -> ReaderT Env CommandM (Command' (Maybe ())))
-> CommandM (Command' (Maybe ()))
-> ReaderT Env CommandM (Command' (Maybe ()))
forall a b. (a -> b) -> a -> b
$ (IOTCM -> StateT CommandState TCM ())
-> CommandM (Command' (Maybe ()))
forall a. (IOTCM -> CommandM a) -> CommandM (Command' (Maybe a))
maybeAbort IOTCM -> StateT CommandState TCM ()
runInteraction
      case Command' (Maybe ())
r of
        Command' (Maybe ())
Done    -> Bool -> ReaderT Env CommandM Bool
forall a. a -> ReaderT Env CommandM a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True -- Done.
        Error String
s -> do
          Text -> ReaderT Env CommandM ()
forall (m :: * -> *). (Monad m, MonadIO m) => Text -> ServerM m ()
writeLog (Text
"Error " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
pack String
s)
          Bool -> ReaderT Env CommandM Bool
forall a. a -> ReaderT Env CommandM a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
        Command Maybe ()
_ -> do
          Text -> ReaderT Env CommandM ()
forall (m :: * -> *). (Monad m, MonadIO m) => Text -> ServerM m ()
writeLog Text
"[Response] Finished sending, waiting for them to complete"
          ReaderT Env CommandM ()
forall (m :: * -> *). (Monad m, MonadIO m) => ServerM m ()
waitUntilResponsesSent
          ReaderT Env CommandM ()
forall (m :: * -> *). (Monad m, MonadIO m) => ServerM m ()
signalCommandFinish
          Bool -> ReaderT Env CommandM Bool
forall a. a -> ReaderT Env CommandM a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

    StateT CommandState TCM () -> ReaderT Env CommandM ()
forall (m :: * -> *) a. Monad m => m a -> ReaderT Env m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift StateT CommandState TCM ()
forall (tcm :: * -> *). MonadTCM tcm => tcm ()
Bench.print
    Bool -> ReaderT Env CommandM () -> ReaderT Env CommandM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
done (Env -> ReaderT Env CommandM ()
loop Env
env)

  -- Reads the next command from the Channel
  readCommand :: Env -> IO Command
  readCommand :: Env -> IO Command
readCommand Env
env = IOTCM -> Command
forall a. a -> Command' a
Command (IOTCM -> Command) -> IO IOTCM -> IO Command
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Env -> IO IOTCM
forall (m :: * -> *). (Monad m, MonadIO m) => Env -> m IOTCM
consumeCommand Env
env

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

-- | Convert "CommandReq" to "CommandRes"

sendCommand :: MonadIO m => Value -> ServerM m Value
sendCommand :: forall (m :: * -> *). MonadIO m => Value -> ServerM m Value
sendCommand Value
value = do
    -- JSON Value => Request => Response
  case Value -> Result CommandReq
forall a. FromJSON a => Value -> Result a
fromJSON Value
value of
    JSON.Error String
msg ->
      Value -> ServerM m Value
forall a. a -> ReaderT Env m a
forall (m :: * -> *) a. Monad m => a -> m a
return
        (Value -> ServerM m Value) -> Value -> ServerM m Value
forall a b. (a -> b) -> a -> b
$  CommandRes -> Value
forall a. ToJSON a => a -> Value
toJSON
        (CommandRes -> Value) -> CommandRes -> Value
forall a b. (a -> b) -> a -> b
$  Maybe CommandErr -> CommandRes
CmdRes
        (Maybe CommandErr -> CommandRes) -> Maybe CommandErr -> CommandRes
forall a b. (a -> b) -> a -> b
$  CommandErr -> Maybe CommandErr
forall a. a -> Maybe a
Just
        (CommandErr -> Maybe CommandErr) -> CommandErr -> Maybe CommandErr
forall a b. (a -> b) -> a -> b
$  String -> CommandErr
CmdErrCannotDecodeJSON
        (String -> CommandErr) -> String -> CommandErr
forall a b. (a -> b) -> a -> b
$  String -> String
forall a. Show a => a -> String
show String
msg
        String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n"
        String -> String -> String
forall a. [a] -> [a] -> [a]
++ Value -> String
forall a. Show a => a -> String
show Value
value
    JSON.Success CommandReq
request -> CommandRes -> Value
forall a. ToJSON a => a -> Value
toJSON (CommandRes -> Value)
-> ReaderT Env m CommandRes -> ServerM m Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CommandReq -> ReaderT Env m CommandRes
forall (m :: * -> *).
MonadIO m =>
CommandReq -> ServerM m CommandRes
handleCommandReq CommandReq
request


handleCommandReq :: MonadIO m => CommandReq -> ServerM m CommandRes
handleCommandReq :: forall (m :: * -> *).
MonadIO m =>
CommandReq -> ServerM m CommandRes
handleCommandReq CommandReq
CmdReqSYN    = CommandRes -> ReaderT Env m CommandRes
forall a. a -> ReaderT Env m a
forall (m :: * -> *) a. Monad m => a -> m a
return (CommandRes -> ReaderT Env m CommandRes)
-> CommandRes -> ReaderT Env m CommandRes
forall a b. (a -> b) -> a -> b
$ String -> CommandRes
CmdResACK String
Agda.getAgdaVersion
handleCommandReq (CmdReq String
cmd) = do
  case String -> Either String IOTCM
parseIOTCM String
cmd of
    Left String
err -> do
      Text -> ServerM m ()
forall (m :: * -> *). (Monad m, MonadIO m) => Text -> ServerM m ()
writeLog (Text -> ServerM m ()) -> Text -> ServerM m ()
forall a b. (a -> b) -> a -> b
$ Text
"[Error] CmdErrCannotParseCommand:\n" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
pack String
err
      CommandRes -> ReaderT Env m CommandRes
forall a. a -> ReaderT Env m a
forall (m :: * -> *) a. Monad m => a -> m a
return (CommandRes -> ReaderT Env m CommandRes)
-> CommandRes -> ReaderT Env m CommandRes
forall a b. (a -> b) -> a -> b
$ Maybe CommandErr -> CommandRes
CmdRes (CommandErr -> Maybe CommandErr
forall a. a -> Maybe a
Just (String -> CommandErr
CmdErrCannotParseCommand String
err))
    Right IOTCM
iotcm -> do
      Text -> ServerM m ()
forall (m :: * -> *). (Monad m, MonadIO m) => Text -> ServerM m ()
writeLog (Text -> ServerM m ()) -> Text -> ServerM m ()
forall a b. (a -> b) -> a -> b
$ Text
"[Request] " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
pack (String -> String
forall a. Show a => a -> String
show String
cmd)
      IOTCM -> ServerM m ()
forall (m :: * -> *). (Monad m, MonadIO m) => IOTCM -> ServerM m ()
provideCommand IOTCM
iotcm
      CommandRes -> ReaderT Env m CommandRes
forall a. a -> ReaderT Env m a
forall (m :: * -> *) a. Monad m => a -> m a
return (CommandRes -> ReaderT Env m CommandRes)
-> CommandRes -> ReaderT Env m CommandRes
forall a b. (a -> b) -> a -> b
$ Maybe CommandErr -> CommandRes
CmdRes Maybe CommandErr
forall a. Maybe a
Nothing

#if !MIN_VERSION_Agda(2,6,3)
parseIOTCM :: String -> Either String IOTCM
parseIOTCM raw = case listToMaybe $ reads raw of
  Just (x, ""     ) -> Right x
  Just (_, remnent) -> Left $ "not consumed: " ++ remnent
  _                 -> Left $ "cannot read: " ++ raw
#endif

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

getCommandLineOptions
  :: (HasOptions m, MonadIO m) => ServerM m CommandLineOptions
getCommandLineOptions :: forall (m :: * -> *).
(HasOptions m, MonadIO m) =>
ServerM m CommandLineOptions
getCommandLineOptions = do
  -- command line options from ARGV
  [String]
argv   <- (Env -> [String]) -> ReaderT Env m [String]
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (Options -> [String]
optRawAgdaOptions (Options -> [String]) -> (Env -> Options) -> Env -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env -> Options
envOptions)
  -- command line options from agda-mode
  [String]
config <- (Env -> [String]) -> ReaderT Env m [String]
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (Config -> [String]
configRawAgdaOptions (Config -> [String]) -> (Env -> Config) -> Env -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env -> Config
envConfig)
  -- concatenate both
  let merged :: [String]
merged = [String]
argv [String] -> [String] -> [String]
forall a. Semigroup a => a -> a -> a
<> [String]
config

  Either String CommandLineOptions
result <- ExceptT String (ReaderT Env m) CommandLineOptions
-> ReaderT Env m (Either String CommandLineOptions)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT String (ReaderT Env m) CommandLineOptions
 -> ReaderT Env m (Either String CommandLineOptions))
-> ExceptT String (ReaderT Env m) CommandLineOptions
-> ReaderT Env m (Either String CommandLineOptions)
forall a b. (a -> b) -> a -> b
$ do
    let p :: OptM ([Backend], CommandLineOptions)
p = [Backend]
-> [String]
-> CommandLineOptions
-> OptM ([Backend], CommandLineOptions)
parseBackendOptions [Backend]
builtinBackends [String]
merged CommandLineOptions
defaultOptions
#if MIN_VERSION_Agda(2,6,3)
    let (Either String ([Backend], CommandLineOptions)
r, OptionWarnings
_warns) = OptM ([Backend], CommandLineOptions)
-> (Either String ([Backend], CommandLineOptions), OptionWarnings)
forall opts. OptM opts -> (Either String opts, OptionWarnings)
runOptM OptM ([Backend], CommandLineOptions)
p
    ([Backend]
bs, CommandLineOptions
opts) <- ReaderT Env m (Either String ([Backend], CommandLineOptions))
-> ExceptT String (ReaderT Env m) ([Backend], CommandLineOptions)
forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
ExceptT (ReaderT Env m (Either String ([Backend], CommandLineOptions))
 -> ExceptT String (ReaderT Env m) ([Backend], CommandLineOptions))
-> ReaderT Env m (Either String ([Backend], CommandLineOptions))
-> ExceptT String (ReaderT Env m) ([Backend], CommandLineOptions)
forall a b. (a -> b) -> a -> b
$ Either String ([Backend], CommandLineOptions)
-> ReaderT Env m (Either String ([Backend], CommandLineOptions))
forall a. a -> ReaderT Env m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Either String ([Backend], CommandLineOptions)
r
#else
    (bs, opts) <- ExceptT $ runOptM p
#endif
    CommandLineOptions
-> ExceptT String (ReaderT Env m) CommandLineOptions
forall a. a -> ExceptT String (ReaderT Env m) a
forall (m :: * -> *) a. Monad m => a -> m a
return CommandLineOptions
opts
  case Either String CommandLineOptions
result of
    -- something bad happened, use the default options instead
    Left  String
_    -> ServerM m CommandLineOptions
forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions
    Right CommandLineOptions
opts -> CommandLineOptions -> ServerM m CommandLineOptions
forall a. a -> ReaderT Env m a
forall (m :: * -> *) a. Monad m => a -> m a
return CommandLineOptions
opts

-- | Run a TCM action in IO and throw away all of the errors
-- TODO: handle the caught errors
runAgda :: MonadIO m => ServerM TCM a -> ServerM m (Either String a)
runAgda :: forall (m :: * -> *) a.
MonadIO m =>
ServerM TCM a -> ServerM m (Either String a)
runAgda ServerM TCM a
p = do
  Env
env <- ReaderT Env m Env
forall r (m :: * -> *). MonadReader r m => m r
ask
  let p' :: TCM a
p' = Env -> ServerM TCM a -> TCM a
forall (m :: * -> *) a. Env -> ServerM m a -> m a
runServerM Env
env ServerM TCM a
p
  IO (Either String a) -> ServerM m (Either String a)
forall a. IO a -> ReaderT Env m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO
    (IO (Either String a) -> ServerM m (Either String a))
-> IO (Either String a) -> ServerM m (Either String a)
forall a b. (a -> b) -> a -> b
$       TCMT IO (Either String a) -> IO (Either String a)
forall (m :: * -> *) a. MonadIO m => TCMT m a -> m a
runTCMTop'
              (                 (a -> Either String a
forall a b. b -> Either a b
Right (a -> Either String a) -> TCM a -> TCMT IO (Either String a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM a
p')
              TCMT IO (Either String a)
-> (TCErr -> TCMT IO (Either String a))
-> TCMT IO (Either String a)
forall a. TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError`      TCErr -> TCMT IO (Either String a)
forall a. TCErr -> TCM (Either String a)
handleTCErr
              TCMT IO (Either String a)
-> (Impossible -> TCMT IO (Either String a))
-> TCMT IO (Either String a)
forall a. TCMT IO a -> (Impossible -> TCMT IO a) -> TCMT IO a
forall (m :: * -> *) a.
CatchImpossible m =>
m a -> (Impossible -> m a) -> m a
`catchImpossible` Impossible -> TCMT IO (Either String a)
forall a. Impossible -> TCM (Either String a)
handleImpossible
              )
    IO (Either String a)
-> (SomeException -> IO (Either String a)) -> IO (Either String a)
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`catch` SomeException -> IO (Either String a)
forall a. SomeException -> IO (Either String a)
catchException
 where
  handleTCErr :: TCErr -> TCM (Either String a)
  handleTCErr :: forall a. TCErr -> TCM (Either String a)
handleTCErr TCErr
err = do
    [String]
s2s <- [TCWarning] -> TCM [String]
prettyTCWarnings' ([TCWarning] -> TCM [String])
-> TCMT IO [TCWarning] -> TCM [String]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCErr -> TCMT IO [TCWarning]
getAllWarningsOfTCErr TCErr
err
    String
s1  <- TCErr -> TCMT IO String
forall (tcm :: * -> *). MonadTCM tcm => TCErr -> tcm String
prettyError TCErr
err
    let ss :: [String]
ss       = (String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (String -> Bool) -> String -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ [String]
s2s [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
s1]
    let errorMsg :: String
errorMsg = [String] -> String
unlines [String]
ss
    Either String a -> TCM (Either String a)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Either String a
forall a b. a -> Either a b
Left String
errorMsg)

  handleImpossible :: Impossible -> TCM (Either String a)
  handleImpossible :: forall a. Impossible -> TCM (Either String a)
handleImpossible = Either String a -> TCMT IO (Either String a)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either String a -> TCMT IO (Either String a))
-> (Impossible -> Either String a)
-> Impossible
-> TCMT IO (Either String a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Either String a
forall a b. a -> Either a b
Left (String -> Either String a)
-> (Impossible -> String) -> Impossible -> Either String a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Impossible -> String
forall a. Show a => a -> String
show

  catchException :: SomeException -> IO (Either String a)
  catchException :: forall a. SomeException -> IO (Either String a)
catchException SomeException
e = Either String a -> IO (Either String a)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either String a -> IO (Either String a))
-> Either String a -> IO (Either String a)
forall a b. (a -> b) -> a -> b
$ String -> Either String a
forall a b. a -> Either a b
Left (String -> Either String a) -> String -> Either String a
forall a b. (a -> b) -> a -> b
$ SomeException -> String
forall a. Show a => a -> String
show SomeException
e

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

data CommandReq
  = CmdReqSYN -- ^ For client to initiate a 2-way handshake
  | CmdReq String
  deriving ((forall x. CommandReq -> Rep CommandReq x)
-> (forall x. Rep CommandReq x -> CommandReq) -> Generic CommandReq
forall x. Rep CommandReq x -> CommandReq
forall x. CommandReq -> Rep CommandReq x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. CommandReq -> Rep CommandReq x
from :: forall x. CommandReq -> Rep CommandReq x
$cto :: forall x. Rep CommandReq x -> CommandReq
to :: forall x. Rep CommandReq x -> CommandReq
Generic)

instance FromJSON CommandReq

data CommandRes
  = CmdResACK -- ^ For server to complete a 2-way handshake
      String   -- ^ Version number of Agda
  | CmdRes -- ^ Response for 'CmdReq'
      (Maybe CommandErr) -- ^ 'Nothing' to indicate success
  deriving ((forall x. CommandRes -> Rep CommandRes x)
-> (forall x. Rep CommandRes x -> CommandRes) -> Generic CommandRes
forall x. Rep CommandRes x -> CommandRes
forall x. CommandRes -> Rep CommandRes x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. CommandRes -> Rep CommandRes x
from :: forall x. CommandRes -> Rep CommandRes x
$cto :: forall x. Rep CommandRes x -> CommandRes
to :: forall x. Rep CommandRes x -> CommandRes
Generic)

instance ToJSON CommandRes

data CommandErr
  = CmdErrCannotDecodeJSON String
  | CmdErrCannotParseCommand String
  deriving ((forall x. CommandErr -> Rep CommandErr x)
-> (forall x. Rep CommandErr x -> CommandErr) -> Generic CommandErr
forall x. Rep CommandErr x -> CommandErr
forall x. CommandErr -> Rep CommandErr x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. CommandErr -> Rep CommandErr x
from :: forall x. CommandErr -> Rep CommandErr x
$cto :: forall x. Rep CommandErr x -> CommandErr
to :: forall x. Rep CommandErr x -> CommandErr
Generic)

instance ToJSON CommandErr