{-# LANGUAGE FlexibleContexts #-}
module Monad where

import           Agda.IR

import           Agda.Interaction.Base          ( IOTCM )
import           Agda.TypeChecking.Monad        ( TCMT )
import           Control.Concurrent
import           Control.Monad.Reader
import           Data.Text                      ( Text
                                                , pack
                                                )
import           Server.CommandController       ( CommandController )
import qualified Server.CommandController      as CommandController
import           Server.ResponseController      ( ResponseController )
import qualified Server.ResponseController     as ResponseController

import           Data.IORef                     ( IORef
                                                , modifyIORef'
                                                , newIORef
                                                , readIORef
                                                , writeIORef
                                                )
import           Data.Maybe                     ( isJust )
import           Language.LSP.Server            ( MonadLsp
                                                , getConfig
                                                )
import qualified Language.LSP.Types            as LSP
import           Options

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

data Env = Env
  { Env -> Options
envOptions            :: Options
  , Env -> Bool
envDevMode            :: Bool
  , Env -> Config
envConfig             :: Config
  , Env -> Chan Text
envLogChan            :: Chan Text
  , Env -> CommandController
envCommandController  :: CommandController
  , Env -> Chan Response
envResponseChan       :: Chan Response
  , Env -> ResponseController
envResponseController :: ResponseController
  }

createInitEnv :: (MonadIO m, MonadLsp Config m) => Options -> m Env
createInitEnv :: forall (m :: * -> *).
(MonadIO m, MonadLsp Config m) =>
Options -> m Env
createInitEnv Options
options =
  Options
-> Bool
-> Config
-> Chan Text
-> CommandController
-> Chan Response
-> ResponseController
-> Env
Env Options
options (Maybe Int -> Bool
forall a. Maybe a -> Bool
isJust (Options -> Maybe Int
optViaTCP Options
options))
    (Config
 -> Chan Text
 -> CommandController
 -> Chan Response
 -> ResponseController
 -> Env)
-> m Config
-> m (Chan Text
      -> CommandController -> Chan Response -> ResponseController -> Env)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Config
forall config (m :: * -> *). MonadLsp config m => m config
getConfig
    m (Chan Text
   -> CommandController -> Chan Response -> ResponseController -> Env)
-> m (Chan Text)
-> m (CommandController
      -> Chan Response -> ResponseController -> Env)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> IO (Chan Text) -> m (Chan Text)
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO (Chan Text)
forall a. IO (Chan a)
newChan
    m (CommandController -> Chan Response -> ResponseController -> Env)
-> m CommandController
-> m (Chan Response -> ResponseController -> Env)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> IO CommandController -> m CommandController
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO CommandController
CommandController.new
    m (Chan Response -> ResponseController -> Env)
-> m (Chan Response) -> m (ResponseController -> Env)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> IO (Chan Response) -> m (Chan Response)
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO (Chan Response)
forall a. IO (Chan a)
newChan
    m (ResponseController -> Env) -> m ResponseController -> m Env
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> IO ResponseController -> m ResponseController
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO ResponseController
ResponseController.new

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

-- | OUR monad
type ServerM m = ReaderT Env m

runServerM :: Env -> ServerM m a -> m a
runServerM :: forall (m :: * -> *) a. Env -> ServerM m a -> m a
runServerM = (ServerM m a -> Env -> m a) -> Env -> ServerM m a -> m a
forall a b c. (a -> b -> c) -> b -> a -> c
flip ServerM m a -> Env -> m a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT

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

writeLog :: (Monad m, MonadIO m) => Text -> ServerM m ()
writeLog :: forall (m :: * -> *). (Monad m, MonadIO m) => Text -> ServerM m ()
writeLog Text
msg = do
  Chan Text
chan <- (Env -> Chan Text) -> ReaderT Env m (Chan Text)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Env -> Chan Text
envLogChan
  IO () -> ServerM m ()
forall a. IO a -> ReaderT Env m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> ServerM m ()) -> IO () -> ServerM m ()
forall a b. (a -> b) -> a -> b
$ Chan Text -> Text -> IO ()
forall a. Chan a -> a -> IO ()
writeChan Chan Text
chan Text
msg

writeLog' :: (Monad m, MonadIO m, Show a) => a -> ServerM m ()
writeLog' :: forall (m :: * -> *) a.
(Monad m, MonadIO m, Show a) =>
a -> ServerM m ()
writeLog' a
x = do
  Chan Text
chan <- (Env -> Chan Text) -> ReaderT Env m (Chan Text)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Env -> Chan Text
envLogChan
  IO () -> ServerM m ()
forall a. IO a -> ReaderT Env m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> ServerM m ()) -> IO () -> ServerM m ()
forall a b. (a -> b) -> a -> b
$ Chan Text -> Text -> IO ()
forall a. Chan a -> a -> IO ()
writeChan Chan Text
chan (Text -> IO ()) -> Text -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> Text
pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ a -> String
forall a. Show a => a -> String
show a
x

-- | Provider
provideCommand :: (Monad m, MonadIO m) => IOTCM -> ServerM m ()
provideCommand :: forall (m :: * -> *). (Monad m, MonadIO m) => IOTCM -> ServerM m ()
provideCommand IOTCM
iotcm = do
  CommandController
controller <- (Env -> CommandController) -> ReaderT Env m CommandController
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Env -> CommandController
envCommandController
  IO () -> ServerM m ()
forall a. IO a -> ReaderT Env m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> ServerM m ()) -> IO () -> ServerM m ()
forall a b. (a -> b) -> a -> b
$ CommandController -> IOTCM -> IO ()
CommandController.put CommandController
controller IOTCM
iotcm

-- | Consumter
consumeCommand :: (Monad m, MonadIO m) => Env -> m IOTCM
consumeCommand :: forall (m :: * -> *). (Monad m, MonadIO m) => Env -> m IOTCM
consumeCommand Env
env = IO IOTCM -> m IOTCM
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO IOTCM -> m IOTCM) -> IO IOTCM -> m IOTCM
forall a b. (a -> b) -> a -> b
$ CommandController -> IO IOTCM
CommandController.take (Env -> CommandController
envCommandController Env
env)

waitUntilResponsesSent :: (Monad m, MonadIO m) => ServerM m ()
waitUntilResponsesSent :: forall (m :: * -> *). (Monad m, MonadIO m) => ServerM m ()
waitUntilResponsesSent = do
  ResponseController
controller <- (Env -> ResponseController) -> ReaderT Env m ResponseController
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Env -> ResponseController
envResponseController
  IO () -> ServerM m ()
forall a. IO a -> ReaderT Env m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> ServerM m ()) -> IO () -> ServerM m ()
forall a b. (a -> b) -> a -> b
$ ResponseController -> IO ()
ResponseController.setCheckpointAndWait ResponseController
controller

signalCommandFinish :: (Monad m, MonadIO m) => ServerM m ()
signalCommandFinish :: forall (m :: * -> *). (Monad m, MonadIO m) => ServerM m ()
signalCommandFinish = do
  Text -> ServerM m ()
forall (m :: * -> *). (Monad m, MonadIO m) => Text -> ServerM m ()
writeLog Text
"[Command] Finished"
  -- send `ResponseEnd`
  Env
env <- ReaderT Env m Env
forall r (m :: * -> *). MonadReader r m => m r
ask
  IO () -> ServerM m ()
forall a. IO a -> ReaderT Env m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> ServerM m ()) -> IO () -> ServerM m ()
forall a b. (a -> b) -> a -> b
$ Chan Response -> Response -> IO ()
forall a. Chan a -> a -> IO ()
writeChan (Env -> Chan Response
envResponseChan Env
env) Response
ResponseEnd
  -- allow the next Command to be consumed
  IO () -> ServerM m ()
forall a. IO a -> ReaderT Env m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> ServerM m ()) -> IO () -> ServerM m ()
forall a b. (a -> b) -> a -> b
$ CommandController -> IO ()
CommandController.release (Env -> CommandController
envCommandController Env
env)

-- | Sends a Response to the client via "envResponseChan"
sendResponse :: (Monad m, MonadIO m) => Env -> Response -> TCMT m ()
sendResponse :: forall (m :: * -> *).
(Monad m, MonadIO m) =>
Env -> Response -> TCMT m ()
sendResponse Env
env Response
response = IO () -> TCMT m ()
forall a. IO a -> TCMT m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> TCMT m ()) -> IO () -> TCMT m ()
forall a b. (a -> b) -> a -> b
$ Chan Response -> Response -> IO ()
forall a. Chan a -> a -> IO ()
writeChan (Env -> Chan Response
envResponseChan Env
env) Response
response