{-# 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 (forall a. Maybe a -> Bool
isJust (Options -> Maybe Int
optViaTCP Options
options))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall config (m :: * -> *). MonadLsp config m => m config
getConfig
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a. IO (Chan a)
newChan
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO CommandController
CommandController.new
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a. IO (Chan a)
newChan
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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 = forall a b c. (a -> b -> c) -> b -> a -> c
flip 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 <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Env -> Chan Text
envLogChan
  forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ 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 <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Env -> Chan Text
envLogChan
  forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall a. Chan a -> a -> IO ()
writeChan Chan Text
chan forall a b. (a -> b) -> a -> b
$ String -> Text
pack forall a b. (a -> b) -> a -> b
$ 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 <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Env -> CommandController
envCommandController
  forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO 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 = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO 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 <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Env -> ResponseController
envResponseController
  forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO 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
  forall (m :: * -> *). (Monad m, MonadIO m) => Text -> ServerM m ()
writeLog Text
"[Command] Finished"
  -- send `ResponseEnd`
  Env
env <- forall r (m :: * -> *). MonadReader r m => m r
ask
  forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall a. Chan a -> a -> IO ()
writeChan (Env -> Chan Response
envResponseChan Env
env) Response
ResponseEnd
  -- allow the next Command to be consumed
  forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO 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 = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall a. Chan a -> a -> IO ()
writeChan (Env -> Chan Response
envResponseChan Env
env) Response
response