{-# 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