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

import Control.Concurrent.Async (race)
import Data.ByteString (ByteString)
import Data.Coerce (coerce)
import Data.Text (unpack)
import System.Directory (withCurrentDirectory)
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

callLean :: InterpreterState LeanSettings -> InterpreterRequest -> IO ByteString
callLean :: InterpreterState LeanSettings
-> InterpreterRequest -> IO ByteString
callLean InterpreterState{TBQueue InterpreterRequest
LeanSettings
input :: forall settings.
InterpreterState settings -> TBQueue InterpreterRequest
settings :: forall settings. InterpreterState settings -> settings
input :: TBQueue InterpreterRequest
settings :: LeanSettings
..} InterpreterRequest
ir = do
  let LeanSettings{FilePath
ExternalInterpreterSettings
$sel:externalLean:LeanSettings :: LeanSettings -> ExternalInterpreterSettings
$sel:projectDir:LeanSettings :: LeanSettings -> FilePath
externalLean :: ExternalInterpreterSettings
projectDir :: FilePath
..} = LeanSettings -> LeanSettings
coerce LeanSettings
settings
      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
..} = ExternalInterpreterSettings
externalLean
  (FilePath
dir, FilePath
path) <- ExternalInterpreterSettings
-> InterpreterRequest -> Maybe FilePath -> IO (FilePath, FilePath)
refreshTmpFile ExternalInterpreterSettings
s InterpreterRequest
ir (FilePath -> Maybe FilePath
forall a. a -> Maybe a
Just FilePath
projectDir)
  FilePath -> IO ByteString -> IO ByteString
forall a. FilePath -> IO a -> IO a
withCurrentDirectory FilePath
dir (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
path]
        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
path (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