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

import Control.Concurrent.Async (race)
import Data.ByteString (ByteString)
import Data.Coerce (coerce)
import Data.Foldable (foldl')
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

import qualified Data.Text as Text

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 ls :: LeanSettings
ls@LeanSettings{FilePath
[Text]
ExternalInterpreterSettings
$sel:externalLean:LeanSettings :: LeanSettings -> ExternalInterpreterSettings
$sel:leanBlockList:LeanSettings :: LeanSettings -> [Text]
$sel:projectDir:LeanSettings :: LeanSettings -> FilePath
externalLean :: ExternalInterpreterSettings
leanBlockList :: [Text]
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 (LeanSettings -> InterpreterRequest -> InterpreterRequest
validateLean LeanSettings
ls 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

validateLean :: LeanSettings -> InterpreterRequest -> InterpreterRequest
validateLean :: LeanSettings -> InterpreterRequest -> InterpreterRequest
validateLean LeanSettings{FilePath
[Text]
ExternalInterpreterSettings
externalLean :: ExternalInterpreterSettings
leanBlockList :: [Text]
projectDir :: FilePath
$sel:externalLean:LeanSettings :: LeanSettings -> ExternalInterpreterSettings
$sel:leanBlockList:LeanSettings :: LeanSettings -> [Text]
$sel:projectDir:LeanSettings :: LeanSettings -> FilePath
..} ir :: InterpreterRequest
ir@InterpreterRequest{ByteString
ChatId
MessageId
interpreterRequestMessage :: InterpreterRequest -> ByteString
interpreterRequestTelegramMessageId :: InterpreterRequest -> MessageId
interpreterRequestTelegramChatId :: InterpreterRequest -> ChatId
interpreterRequestMessage :: ByteString
interpreterRequestTelegramMessageId :: MessageId
interpreterRequestTelegramChatId :: ChatId
..}
  = InterpreterRequest
ir { interpreterRequestMessage :: ByteString
interpreterRequestMessage = ByteString
validatedMsg }
  where
    remove :: Text -> Text -> Text
remove Text
txt Text
blockedPrefix = Text -> Text -> Text -> Text
Text.replace Text
blockedPrefix Text
"" Text
txt
    removeAllFromLine :: Text -> Text
removeAllFromLine Text
x = (Text -> Text -> Text) -> Text -> [Text] -> Text
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Text -> Text -> Text
remove Text
x [Text]
leanBlockList
    removeUnsafeImports :: ByteString -> ByteString
removeUnsafeImports = Text -> ByteString
textToBS (Text -> ByteString)
-> (ByteString -> Text) -> ByteString -> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Text
removeAllFromLine (Text -> Text) -> (ByteString -> Text) -> ByteString -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Text
bsToText

    validatedMsg :: ByteString
validatedMsg = ByteString -> ByteString
removeUnsafeImports ByteString
interpreterRequestMessage