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

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

import Idris.Interaction.Command
import Proof.Assistant.Helpers
import Proof.Assistant.Request
import Proof.Assistant.ResourceLimit
import Proof.Assistant.Settings
import Proof.Assistant.State

import qualified Data.ByteString.Char8 as BS8

-- | Call Idris 2 as CLI application.
-- It prepares the CLI command, executes it and waits for response.
callIdris2 :: InterpreterState IdrisSettings -> InterpreterRequest -> IO ByteString
callIdris2 :: InterpreterState IdrisSettings
-> InterpreterRequest -> IO ByteString
callIdris2 InterpreterState{TBQueue InterpreterRequest
IdrisSettings
input :: forall settings.
InterpreterState settings -> TBQueue InterpreterRequest
settings :: forall settings. InterpreterState settings -> settings
input :: TBQueue InterpreterRequest
settings :: IdrisSettings
..} ir :: InterpreterRequest
ir@InterpreterRequest{ByteString
ChatId
MessageId
interpreterRequestMessage :: InterpreterRequest -> ByteString
interpreterRequestTelegramMessageId :: InterpreterRequest -> MessageId
interpreterRequestTelegramChatId :: InterpreterRequest -> ChatId
interpreterRequestMessage :: ByteString
interpreterRequestTelegramMessageId :: MessageId
interpreterRequestTelegramChatId :: ChatId
..}
  = case ByteString
-> Either ByteString (Either () IdrisCommand, ByteString)
parseRequest ByteString
interpreterRequestMessage of
      Left ByteString
err -> ByteString -> IO ByteString
forall (f :: * -> *) a. Applicative f => a -> f a
pure ByteString
err
      Right (Either () IdrisCommand
ecmd, ByteString
request) -> do
        let s :: ExternalInterpreterSettings
s@ExternalInterpreterSettings{Natural
FilePath
ResourceSettings
Priority
Time
Executable
CmdArgs
$sel:inputSize:ExternalInterpreterSettings :: ExternalInterpreterSettings -> Natural
$sel:fileExtension:ExternalInterpreterSettings :: ExternalInterpreterSettings -> FilePath
$sel:tempFilePrefix:ExternalInterpreterSettings :: ExternalInterpreterSettings -> FilePath
$sel:resources:ExternalInterpreterSettings :: ExternalInterpreterSettings -> ResourceSettings
$sel:priority:ExternalInterpreterSettings :: ExternalInterpreterSettings -> Priority
$sel:time:ExternalInterpreterSettings :: ExternalInterpreterSettings -> Time
$sel:executable:ExternalInterpreterSettings :: ExternalInterpreterSettings -> Executable
$sel:args:ExternalInterpreterSettings :: ExternalInterpreterSettings -> CmdArgs
inputSize :: Natural
fileExtension :: FilePath
tempFilePrefix :: FilePath
resources :: ResourceSettings
priority :: Priority
time :: Time
executable :: Executable
args :: CmdArgs
..} = IdrisSettings -> ExternalInterpreterSettings
coerce IdrisSettings
settings
        IO (ExitCode, FilePath, FilePath)
action <- ExternalInterpreterSettings
-> InterpreterRequest
-> Either () IdrisCommand
-> ByteString
-> IO (IO (ExitCode, FilePath, FilePath))
chooseCommand ExternalInterpreterSettings
s InterpreterRequest
ir Either () IdrisCommand
ecmd ByteString
request
        let asyncExecutable :: IO ByteString
asyncExecutable = do
              Priority -> IO ()
setPriority Priority
priority
              (ExitCode
_exitCode, FilePath
stdout, FilePath
stderr) <- IO (ExitCode, FilePath, FilePath)
action
              let response :: FilePath
response = [FilePath] -> FilePath
unlines [if FilePath
stdout FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath
"\n" then FilePath
"Done." else FilePath
stdout, FilePath
stderr]
              ByteString -> IO ByteString
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ByteString -> IO ByteString) -> ByteString -> IO ByteString
forall a b. (a -> b) -> a -> b
$ FilePath -> ByteString
toBS FilePath
response
            asyncTimer :: IO ()
asyncTimer = Time -> IO ()
asyncWait Time
time
        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
asyncExecutable)
        case Either () ByteString
eresult of
          Left ()  -> ByteString -> IO ByteString
forall (f :: * -> *) a. Applicative f => a -> f a
pure ByteString
"Time limit exceeded"
          Right ByteString
bs -> ByteString -> IO ByteString
forall (f :: * -> *) a. Applicative f => a -> f a
pure ByteString
bs

-- | Parse command. It could be unknown command or 'IdrisCommand' sub-command with its arguments
-- or even expression to evaluate.
parseRequest :: ByteString -> Either ByteString (Either () IdrisCommand, ByteString)
parseRequest :: ByteString
-> Either ByteString (Either () IdrisCommand, ByteString)
parseRequest ByteString
rawCmd = case ByteString -> [ByteString]
BS8.words ByteString
rawSubCommand of
  [] -> ByteString
-> Either ByteString (Either () IdrisCommand, ByteString)
forall a b. a -> Either a b
Left ByteString
"empty command"
  ByteString
cmd : [ByteString]
_ -> if ByteString -> ByteString -> Bool
BS8.isPrefixOf ByteString
"/" ByteString
cmd
    then case ByteString -> Maybe IdrisCommand
matchSupported ByteString
cmd of
           Maybe IdrisCommand
Nothing -> ByteString
-> Either ByteString (Either () IdrisCommand, ByteString)
forall a b. a -> Either a b
Left (ByteString
 -> Either ByteString (Either () IdrisCommand, ByteString))
-> ByteString
-> Either ByteString (Either () IdrisCommand, ByteString)
forall a b. (a -> b) -> a -> b
$ ByteString
"Unknown command: " ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
<> ByteString
cmd
           Just IdrisCommand
aCmd -> (Either () IdrisCommand, ByteString)
-> Either ByteString (Either () IdrisCommand, ByteString)
forall a b. b -> Either a b
Right (IdrisCommand -> Either () IdrisCommand
forall a b. b -> Either a b
Right IdrisCommand
aCmd, ByteString -> ByteString
dropCommand ByteString
rawSubCommand)
    else (Either () IdrisCommand, ByteString)
-> Either ByteString (Either () IdrisCommand, ByteString)
forall a b. b -> Either a b
Right (() -> Either () IdrisCommand
forall a b. a -> Either a b
Left (), ByteString
rawSubCommand)
  where
    rawSubCommand :: ByteString
rawSubCommand = ByteString -> ByteString
dropCommand ByteString
rawCmd