{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RecordWildCards #-}
module Proof.Assistant.Transport where

import Control.Concurrent.STM (TBQueue, atomically, newTBQueueIO, readTBQueue, writeTBQueue)

import Agda.Interaction.State

import Proof.Assistant.Request (InterpreterRequest)
import Proof.Assistant.Response (InterpreterResponse)
import Proof.Assistant.Settings hiding (InterpretersSettings)
import Proof.Assistant.State

import qualified Proof.Assistant.Settings as Settings

-- | Combination of all supported backend interpreters.
data Interpreters = Interpreters
  { Interpreters -> AgdaState
agda  :: !AgdaState
  , Interpreters -> InterpreterState ArendSettings
arend :: !(InterpreterState ArendSettings)
  , Interpreters -> InterpreterState IdrisSettings
idris :: !(InterpreterState IdrisSettings)
  , Interpreters -> ExternalState
coq   :: !ExternalState
  , Interpreters -> InterpreterState LeanSettings
lean  :: !(InterpreterState LeanSettings)
  , Interpreters -> InternalState
rzk   :: !InternalState
  }

-- | Initiate new interpreters from settings.
newInterpreters :: Settings.InterpretersSettings -> IO Interpreters
newInterpreters :: InterpretersSettings -> IO Interpreters
newInterpreters InterpretersSettings
settings = do
  AgdaState
agda <- AgdaSettings -> IO AgdaState
newAgdaState (AgdaSettings -> IO AgdaState) -> AgdaSettings -> IO AgdaState
forall a b. (a -> b) -> a -> b
$ InterpretersSettings -> AgdaSettings
Settings.agda InterpretersSettings
settings
  InterpreterState ArendSettings
arend <- ArendSettings -> IO (InterpreterState ArendSettings)
forall settings.
ToInterpreterState settings =>
settings -> IO (InterpreterState settings)
newInterpreterState (ArendSettings -> IO (InterpreterState ArendSettings))
-> ArendSettings -> IO (InterpreterState ArendSettings)
forall a b. (a -> b) -> a -> b
$ InterpretersSettings -> ArendSettings
Settings.arend InterpretersSettings
settings
  InterpreterState IdrisSettings
idris <- IdrisSettings -> IO (InterpreterState IdrisSettings)
forall settings.
ToInterpreterState settings =>
settings -> IO (InterpreterState settings)
newInterpreterState (IdrisSettings -> IO (InterpreterState IdrisSettings))
-> IdrisSettings -> IO (InterpreterState IdrisSettings)
forall a b. (a -> b) -> a -> b
$ InterpretersSettings -> IdrisSettings
Settings.idris InterpretersSettings
settings
  ExternalState
coq <- ExternalInterpreterSettings -> IO ExternalState
forall settings.
ToInterpreterState settings =>
settings -> IO (InterpreterState settings)
newInterpreterState (ExternalInterpreterSettings -> IO ExternalState)
-> ExternalInterpreterSettings -> IO ExternalState
forall a b. (a -> b) -> a -> b
$ InterpretersSettings -> ExternalInterpreterSettings
Settings.coq InterpretersSettings
settings
  InterpreterState LeanSettings
lean <- LeanSettings -> IO (InterpreterState LeanSettings)
forall settings.
ToInterpreterState settings =>
settings -> IO (InterpreterState settings)
newInterpreterState (LeanSettings -> IO (InterpreterState LeanSettings))
-> LeanSettings -> IO (InterpreterState LeanSettings)
forall a b. (a -> b) -> a -> b
$ InterpretersSettings -> LeanSettings
Settings.lean InterpretersSettings
settings
  InternalState
rzk <- InternalInterpreterSettings -> IO InternalState
forall settings.
ToInterpreterState settings =>
settings -> IO (InterpreterState settings)
newInterpreterState (InternalInterpreterSettings -> IO InternalState)
-> InternalInterpreterSettings -> IO InternalState
forall a b. (a -> b) -> a -> b
$ InterpretersSettings -> InternalInterpreterSettings
Settings.rzk InterpretersSettings
settings
  Interpreters -> IO Interpreters
forall (f :: * -> *) a. Applicative f => a -> f a
pure Interpreters :: AgdaState
-> InterpreterState ArendSettings
-> InterpreterState IdrisSettings
-> ExternalState
-> InterpreterState LeanSettings
-> InternalState
-> Interpreters
Interpreters{InterpreterState IdrisSettings
InterpreterState ArendSettings
InterpreterState LeanSettings
InternalState
ExternalState
AgdaState
rzk :: InternalState
lean :: InterpreterState LeanSettings
coq :: ExternalState
idris :: InterpreterState IdrisSettings
arend :: InterpreterState ArendSettings
agda :: AgdaState
rzk :: InternalState
lean :: InterpreterState LeanSettings
coq :: ExternalState
idris :: InterpreterState IdrisSettings
arend :: InterpreterState ArendSettings
agda :: AgdaState
..}

type ExternalState = InterpreterState ExternalInterpreterSettings

type InternalState = InterpreterState InternalInterpreterSettings

-- | Bot has its own state.
data BotState = BotState
  { BotState -> TBQueue InterpreterResponse
output       :: !(TBQueue InterpreterResponse) -- ^ Queue to read messages from backend interpreters.
  , BotState -> Settings
botSettings  :: !Settings -- ^ Bot settings.
  , BotState -> Interpreters
interpreters :: !Interpreters -- ^ All interpreters with their states.
  }

-- | Initiate 'BotState' from 'Settings'.
newBotState :: Settings -> IO BotState
newBotState :: Settings -> IO BotState
newBotState botSettings :: Settings
botSettings@Settings{Natural
Text
HashMap Text Text
InterpretersSettings
$sel:interpretersSettings:Settings :: Settings -> InterpretersSettings
$sel:version:Settings :: Settings -> Text
$sel:helpMessages:Settings :: Settings -> HashMap Text Text
$sel:help:Settings :: Settings -> Text
$sel:outputSize:Settings :: Settings -> Natural
$sel:botToken:Settings :: Settings -> Text
$sel:botName:Settings :: Settings -> Text
interpretersSettings :: InterpretersSettings
version :: Text
helpMessages :: HashMap Text Text
help :: Text
outputSize :: Natural
botToken :: Text
botName :: Text
..} = do
  TBQueue InterpreterResponse
output <- Natural -> IO (TBQueue InterpreterResponse)
forall a. Natural -> IO (TBQueue a)
newTBQueueIO Natural
outputSize
  Interpreters
interpreters <- InterpretersSettings -> IO Interpreters
newInterpreters InterpretersSettings
interpretersSettings
  BotState -> IO BotState
forall (f :: * -> *) a. Applicative f => a -> f a
pure BotState :: TBQueue InterpreterResponse -> Settings -> Interpreters -> BotState
BotState{TBQueue InterpreterResponse
Settings
Interpreters
interpreters :: Interpreters
output :: TBQueue InterpreterResponse
botSettings :: Settings
interpreters :: Interpreters
botSettings :: Settings
output :: TBQueue InterpreterResponse
..}

-- | Read message from "input" queue.
readInput :: InterpreterState settings -> IO InterpreterRequest
readInput :: InterpreterState settings -> IO InterpreterRequest
readInput InterpreterState settings
state = STM InterpreterRequest -> IO InterpreterRequest
forall a. STM a -> IO a
atomically (STM InterpreterRequest -> IO InterpreterRequest)
-> STM InterpreterRequest -> IO InterpreterRequest
forall a b. (a -> b) -> a -> b
$! TBQueue InterpreterRequest -> STM InterpreterRequest
forall a. TBQueue a -> STM a
readTBQueue (InterpreterState settings -> TBQueue InterpreterRequest
forall settings.
InterpreterState settings -> TBQueue InterpreterRequest
input InterpreterState settings
state)

-- | Read message from "output" queue.
readOutput :: BotState -> IO InterpreterResponse
readOutput :: BotState -> IO InterpreterResponse
readOutput BotState
state = STM InterpreterResponse -> IO InterpreterResponse
forall a. STM a -> IO a
atomically (STM InterpreterResponse -> IO InterpreterResponse)
-> STM InterpreterResponse -> IO InterpreterResponse
forall a b. (a -> b) -> a -> b
$! TBQueue InterpreterResponse -> STM InterpreterResponse
forall a. TBQueue a -> STM a
readTBQueue (BotState -> TBQueue InterpreterResponse
output BotState
state)

-- | Write message to "input" queue.
writeInput :: InterpreterRequest -> InterpreterState settings -> IO ()
writeInput :: InterpreterRequest -> InterpreterState settings -> IO ()
writeInput InterpreterRequest
message InterpreterState settings
state = STM () -> IO ()
forall a. STM a -> IO a
atomically (STM () -> IO ()) -> STM () -> IO ()
forall a b. (a -> b) -> a -> b
$! TBQueue InterpreterRequest -> InterpreterRequest -> STM ()
forall a. TBQueue a -> a -> STM ()
writeTBQueue (InterpreterState settings -> TBQueue InterpreterRequest
forall settings.
InterpreterState settings -> TBQueue InterpreterRequest
input InterpreterState settings
state) InterpreterRequest
message

-- | Write message to "output" queue.
writeOutput :: InterpreterResponse -> BotState -> IO ()
writeOutput :: InterpreterResponse -> BotState -> IO ()
writeOutput InterpreterResponse
message BotState
state = STM () -> IO ()
forall a. STM a -> IO a
atomically (STM () -> IO ()) -> STM () -> IO ()
forall a b. (a -> b) -> a -> b
$! TBQueue InterpreterResponse -> InterpreterResponse -> STM ()
forall a. TBQueue a -> a -> STM ()
writeTBQueue (BotState -> TBQueue InterpreterResponse
output BotState
state) InterpreterResponse
message