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

import Control.Concurrent.Async (race)
import Data.ByteString (ByteString)
import Data.Coerce (coerce)
import Data.Text (unpack)
import System.Directory (createDirectoryIfMissing, withCurrentDirectory)
import System.FilePath
import System.Process (readProcessWithExitCode)

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

import qualified Data.ByteString.Char8 as BS8
import qualified Data.Text.IO as Text

-- | Call Arend typechecker as CLI application.
-- It prepares the CLI command, executes it and waits for response.
callArend :: InterpreterState ArendSettings -> InterpreterRequest -> IO ByteString
callArend :: InterpreterState ArendSettings
-> InterpreterRequest -> IO ByteString
callArend InterpreterState{TBQueue InterpreterRequest
ArendSettings
input :: forall settings.
InterpreterState settings -> TBQueue InterpreterRequest
settings :: forall settings. InterpreterState settings -> settings
input :: TBQueue InterpreterRequest
settings :: ArendSettings
..} InterpreterRequest
ir = do
  let ArendSettings{FilePath
Text
ExternalInterpreterSettings
$sel:externalArend:ArendSettings :: ArendSettings -> ExternalInterpreterSettings
$sel:arendModuleName:ArendSettings :: ArendSettings -> FilePath
$sel:arendYamlContent:ArendSettings :: ArendSettings -> Text
$sel:arendYamlFilename:ArendSettings :: ArendSettings -> FilePath
$sel:arendRootProjectDir:ArendSettings :: ArendSettings -> FilePath
externalArend :: ExternalInterpreterSettings
arendModuleName :: FilePath
arendYamlContent :: Text
arendYamlFilename :: FilePath
arendRootProjectDir :: FilePath
..} = ArendSettings -> ArendSettings
coerce ArendSettings
settings
      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
..} = ExternalInterpreterSettings
externalArend
  FilePath
currentProjectDir <- ArendSettings -> InterpreterRequest -> IO FilePath
setArendProject ArendSettings
settings InterpreterRequest
ir
  FilePath -> IO ByteString -> IO ByteString
forall a. FilePath -> IO a -> IO a
withCurrentDirectory FilePath
arendRootProjectDir (IO ByteString -> IO ByteString) -> IO ByteString -> IO ByteString
forall a b. (a -> b) -> a -> b
$ do
    let fullArgs :: [FilePath]
fullArgs = (Text -> FilePath
unpack (Text -> FilePath) -> [Text] -> [FilePath]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CmdArgs -> [Text]
coerce CmdArgs
args) [FilePath] -> [FilePath] -> [FilePath]
forall a. Semigroup a => a -> a -> a
<> [FilePath
currentProjectDir]
        runProcess :: IO (ExitCode, FilePath, FilePath)
runProcess = FilePath
-> [FilePath] -> FilePath -> IO (ExitCode, FilePath, FilePath)
readProcessWithExitCode (Executable -> FilePath
forall a. Coercible a Text => a -> FilePath
t2s Executable
executable) [FilePath]
fullArgs FilePath
""
        asyncExecutable :: IO ByteString
asyncExecutable = do
          Priority -> IO ()
setPriority Priority
priority
          (ExitCode
_exitCode, FilePath
stdout, FilePath
stderr) <- IO (ExitCode, FilePath, FilePath)
runProcess
          ByteString -> IO ByteString
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ByteString -> IO ByteString)
-> ([FilePath] -> ByteString) -> [FilePath] -> IO ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> ByteString -> ByteString
validate FilePath
currentProjectDir (ByteString -> ByteString)
-> ([FilePath] -> ByteString) -> [FilePath] -> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> ByteString
toBS (FilePath -> ByteString)
-> ([FilePath] -> FilePath) -> [FilePath] -> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [FilePath] -> FilePath
unlines ([FilePath] -> IO ByteString) -> [FilePath] -> IO ByteString
forall a b. (a -> b) -> a -> b
$ [FilePath
stdout, FilePath
stderr]
        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

-- | Arend requires a project for every file to typecheck.
-- It reads project configuration, finds all files in a project directory
-- and tries to typecheck all of them.
-- 
-- Since we need to isolate different chats from each other we need to ensure
-- that every chat has its own project. And every project has its own configuration.
--
-- As result, project directory will be created, set and returned.
setArendProject :: ArendSettings -> InterpreterRequest -> IO FilePath
setArendProject :: ArendSettings -> InterpreterRequest -> IO FilePath
setArendProject ArendSettings{FilePath
Text
ExternalInterpreterSettings
externalArend :: ExternalInterpreterSettings
arendModuleName :: FilePath
arendYamlContent :: Text
arendYamlFilename :: FilePath
arendRootProjectDir :: FilePath
$sel:externalArend:ArendSettings :: ArendSettings -> ExternalInterpreterSettings
$sel:arendModuleName:ArendSettings :: ArendSettings -> FilePath
$sel:arendYamlContent:ArendSettings :: ArendSettings -> Text
$sel:arendYamlFilename:ArendSettings :: ArendSettings -> FilePath
$sel:arendRootProjectDir:ArendSettings :: ArendSettings -> FilePath
..} InterpreterRequest{ByteString
ChatId
MessageId
interpreterRequestMessage :: InterpreterRequest -> ByteString
interpreterRequestTelegramMessageId :: InterpreterRequest -> MessageId
interpreterRequestTelegramChatId :: InterpreterRequest -> ChatId
interpreterRequestMessage :: ByteString
interpreterRequestTelegramMessageId :: MessageId
interpreterRequestTelegramChatId :: ChatId
..} = do
  let ExternalInterpreterSettings{Natural
FilePath
ResourceSettings
Priority
Time
Executable
CmdArgs
inputSize :: Natural
fileExtension :: FilePath
tempFilePrefix :: FilePath
resources :: ResourceSettings
priority :: Priority
time :: Time
executable :: Executable
args :: 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
..} = ExternalInterpreterSettings
externalArend
      projectDir :: FilePath
projectDir = FilePath
arendRootProjectDir FilePath -> FilePath -> FilePath
</> (FilePath
tempFilePrefix  FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> ChatId -> FilePath
chatIdToString ChatId
interpreterRequestTelegramChatId)
      projectConfigPath :: FilePath
projectConfigPath = FilePath
projectDir FilePath -> FilePath -> FilePath
</> FilePath
arendYamlFilename
      projectSourcePath :: FilePath
projectSourcePath = FilePath
projectDir FilePath -> FilePath -> FilePath
</> FilePath
arendModuleName FilePath -> FilePath -> FilePath
<.> FilePath
fileExtension
  Bool -> FilePath -> IO ()
createDirectoryIfMissing Bool
True FilePath
projectDir
  FilePath -> Text -> IO ()
Text.writeFile FilePath
projectConfigPath Text
arendYamlContent
  FilePath -> ByteString -> IO ()
BS8.writeFile FilePath
projectSourcePath (ByteString -> IO ()) -> ByteString -> IO ()
forall a b. (a -> b) -> a -> b
$ ByteString -> ByteString
dropSubCommand ByteString
interpreterRequestMessage
  FilePath -> IO FilePath
forall (f :: * -> *) a. Applicative f => a -> f a
pure FilePath
projectDir