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

import Control.Concurrent.Async (race)
import Data.ByteString (ByteString)
import Data.Coerce (coerce)
import System.Mem

import Rzk.Polylingual

import Proof.Assistant.Helpers
import Proof.Assistant.Request
import Proof.Assistant.Settings
import Proof.Assistant.State

-- | Call Polilyngual API. Rzk will do all the job and return response or an error as result.
callRzk :: InterpreterState InternalInterpreterSettings -> InterpreterRequest -> IO ByteString
callRzk :: InterpreterState InternalInterpreterSettings
-> InterpreterRequest -> IO ByteString
callRzk InterpreterState{TBQueue InterpreterRequest
InternalInterpreterSettings
input :: forall settings.
InterpreterState settings -> TBQueue InterpreterRequest
settings :: forall settings. InterpreterState settings -> settings
input :: TBQueue InterpreterRequest
settings :: InternalInterpreterSettings
..} InterpreterRequest
ir = do
  let InternalInterpreterSettings{Natural
FilePath
$sel:sourceFileExtension:InternalInterpreterSettings :: InternalInterpreterSettings -> FilePath
$sel:sourceFilePrefix:InternalInterpreterSettings :: InternalInterpreterSettings -> FilePath
$sel:inputSize:InternalInterpreterSettings :: InternalInterpreterSettings -> Natural
$sel:allocations:InternalInterpreterSettings :: InternalInterpreterSettings -> Natural
$sel:timeout:InternalInterpreterSettings :: InternalInterpreterSettings -> Natural
sourceFileExtension :: FilePath
sourceFilePrefix :: FilePath
inputSize :: Natural
allocations :: Natural
timeout :: Natural
..} = InternalInterpreterSettings
settings
      asyncApi :: IO ByteString
asyncApi = do
        IO ()
enableAllocationLimit
        Int64 -> IO ()
setAllocationCounter (Natural -> Int64
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
allocations)
        let makeResult :: ByteString -> IO ByteString
makeResult = ByteString -> IO ByteString
forall (f :: * -> *) a. Applicative f => a -> f a
pure
              (ByteString -> IO ByteString)
-> (ByteString -> ByteString) -> ByteString -> IO ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FilePath -> ByteString)
-> (SomeModule -> ByteString)
-> Either FilePath SomeModule
-> ByteString
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either FilePath -> ByteString
toBS (FilePath -> ByteString
toBS (FilePath -> ByteString)
-> (SomeModule -> FilePath) -> SomeModule -> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SomeModule -> FilePath
compileSomeModule)
              (Either FilePath SomeModule -> ByteString)
-> (ByteString -> Either FilePath SomeModule)
-> ByteString
-> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> Either FilePath SomeModule
safeParseSomeModule (FilePath -> Either FilePath SomeModule)
-> (ByteString -> FilePath)
-> ByteString
-> Either FilePath SomeModule
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> FilePath
fromBS (ByteString -> FilePath)
-> (ByteString -> ByteString) -> ByteString -> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> ByteString
dropCommand
        ByteString -> IO ByteString
makeResult (InterpreterRequest -> ByteString
interpreterRequestMessage InterpreterRequest
ir)
      asyncTimer :: IO ()
asyncTimer = Time -> IO ()
asyncWait (Natural -> Time
coerce Natural
timeout)
  Either () ByteString
eresult <- IO () -> IO ByteString -> IO (Either () ByteString)
forall a b. IO a -> IO b -> IO (Either a b)
race IO ()
asyncTimer (IO ByteString -> IO ByteString
handleErrorMaybe IO ByteString
asyncApi)
  case Either () ByteString
eresult of
    Left () -> ByteString -> IO ByteString
forall (f :: * -> *) a. Applicative f => a -> f a
pure ByteString
"Time limit exceeded"
    Right ByteString
result -> ByteString -> IO ByteString
forall (f :: * -> *) a. Applicative f => a -> f a
pure ByteString
result