{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
module Proof.Assistant.Agda where
import Control.Concurrent.Async
import Data.ByteString (ByteString)
import Data.Coerce
import System.Directory (getTemporaryDirectory)
import System.FilePath ((</>), (<.>))
import System.Mem
import Telegram.Bot.API (ChatId (..))
import Agda.Interaction.Command
import Agda.Interaction.State
import Agda.TypeChecking.Monad.Base (envCurrentPath)
import Agda.Utils.FileName (absolute)
import Proof.Assistant.Helpers
import Proof.Assistant.RefreshFile (validate)
import Proof.Assistant.Request
import Proof.Assistant.Settings
import Proof.Assistant.State
import qualified Data.ByteString.Char8 as BS8
callAgda :: AgdaState -> InterpreterRequest -> IO ByteString
callAgda :: AgdaState -> InterpreterRequest -> IO ByteString
callAgda currentAgdaState :: AgdaState
currentAgdaState@AgdaState{IORef TCState
IORef TCEnv
InterpreterState AgdaSettings
agdaStateRef :: AgdaState -> IORef TCState
agdaEnvRef :: AgdaState -> IORef TCEnv
interpreterState :: AgdaState -> InterpreterState AgdaSettings
agdaStateRef :: IORef TCState
agdaEnvRef :: IORef TCEnv
interpreterState :: InterpreterState AgdaSettings
..} InterpreterRequest{ByteString
ChatId
MessageId
interpreterRequestMessage :: InterpreterRequest -> ByteString
interpreterRequestTelegramMessageId :: InterpreterRequest -> MessageId
interpreterRequestTelegramChatId :: InterpreterRequest -> ChatId
interpreterRequestMessage :: ByteString
interpreterRequestTelegramMessageId :: MessageId
interpreterRequestTelegramChatId :: ChatId
..} = do
let InternalInterpreterSettings{Natural
FilePath
$sel:sourceFileExtension:InternalInterpreterSettings :: InternalInterpreterSettings -> FilePath
$sel:sourceFilePrefix:InternalInterpreterSettings :: InternalInterpreterSettings -> FilePath
$sel:inputSize:InternalInterpreterSettings :: InternalInterpreterSettings -> Natural
$sel:allocations:InternalInterpreterSettings :: InternalInterpreterSettings -> Natural
$sel:timeout:InternalInterpreterSettings :: InternalInterpreterSettings -> Natural
sourceFileExtension :: FilePath
sourceFilePrefix :: FilePath
inputSize :: Natural
allocations :: Natural
timeout :: Natural
..} = AgdaSettings -> InternalInterpreterSettings
internal (InterpreterState AgdaSettings -> AgdaSettings
forall settings. InterpreterState settings -> settings
settings InterpreterState AgdaSettings
interpreterState)
asyncApi :: IO ByteString
asyncApi = ChatId -> AgdaState -> IO ByteString -> IO ByteString
withChat ChatId
interpreterRequestTelegramChatId AgdaState
currentAgdaState (IO ByteString -> IO ByteString) -> IO ByteString -> IO ByteString
forall a b. (a -> b) -> a -> b
$ do
IO ()
enableAllocationLimit
Int64 -> IO ()
setAllocationCounter (Natural -> Int64
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
allocations)
AgdaState -> ByteString -> IO ByteString
interpretAgda AgdaState
currentAgdaState ByteString
interpreterRequestMessage
asyncTimer :: IO ()
asyncTimer = Time -> IO ()
asyncWait (Natural -> Time
coerce Natural
timeout)
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
asyncApi)
case Either () ByteString
eresult of
Left () -> ByteString -> IO ByteString
forall (f :: * -> *) a. Applicative f => a -> f a
pure ByteString
"Time limit exceeded"
Right ByteString
result -> ByteString -> IO ByteString
forall (f :: * -> *) a. Applicative f => a -> f a
pure ByteString
result
withChat :: ChatId -> AgdaState -> IO ByteString -> IO ByteString
withChat :: ChatId -> AgdaState -> IO ByteString -> IO ByteString
withChat ChatId
chatId AgdaState
state IO ByteString
action = do
FilePath
tmpDir <- IO FilePath
getTemporaryDirectory
let InternalInterpreterSettings{Natural
FilePath
sourceFileExtension :: FilePath
sourceFilePrefix :: FilePath
inputSize :: Natural
allocations :: Natural
timeout :: Natural
$sel:sourceFileExtension:InternalInterpreterSettings :: InternalInterpreterSettings -> FilePath
$sel:sourceFilePrefix:InternalInterpreterSettings :: InternalInterpreterSettings -> FilePath
$sel:inputSize:InternalInterpreterSettings :: InternalInterpreterSettings -> Natural
$sel:allocations:InternalInterpreterSettings :: InternalInterpreterSettings -> Natural
$sel:timeout:InternalInterpreterSettings :: InternalInterpreterSettings -> Natural
..} = (AgdaSettings -> InternalInterpreterSettings
internal (AgdaSettings -> InternalInterpreterSettings)
-> (AgdaState -> AgdaSettings)
-> AgdaState
-> InternalInterpreterSettings
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InterpreterState AgdaSettings -> AgdaSettings
forall settings. InterpreterState settings -> settings
settings (InterpreterState AgdaSettings -> AgdaSettings)
-> (AgdaState -> InterpreterState AgdaSettings)
-> AgdaState
-> AgdaSettings
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AgdaState -> InterpreterState AgdaSettings
interpreterState) AgdaState
state
chatIdToString :: ChatId -> FilePath
chatIdToString = Integer -> FilePath
forall a. Show a => a -> FilePath
show (Integer -> FilePath) -> (ChatId -> Integer) -> ChatId -> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Coercible ChatId Integer => ChatId -> Integer
coerce @ChatId @Integer
sourceFile :: FilePath
sourceFile = FilePath
tmpDir
FilePath -> FilePath -> FilePath
</> FilePath
sourceFilePrefix
FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> ChatId -> FilePath
chatIdToString ChatId
chatId
FilePath -> FilePath -> FilePath
<.> FilePath
sourceFileExtension
AbsolutePath
absSourceFile <- FilePath -> IO AbsolutePath
absolute FilePath
sourceFile
let modifiedEnv :: TCEnv -> TCEnv
modifiedEnv TCEnv
s = TCEnv
s { envCurrentPath :: Maybe AbsolutePath
envCurrentPath = AbsolutePath -> Maybe AbsolutePath
forall a. a -> Maybe a
Just AbsolutePath
absSourceFile }
AgdaState -> (TCEnv -> TCEnv) -> IO ()
setEnv AgdaState
state TCEnv -> TCEnv
modifiedEnv
ByteString -> IO ByteString
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ByteString -> IO ByteString)
-> (ByteString -> ByteString) -> ByteString -> IO ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> ByteString -> ByteString
validate FilePath
sourceFile (ByteString -> IO ByteString) -> IO ByteString -> IO ByteString
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< IO ByteString
action
interpretAgda :: AgdaState -> ByteString -> IO ByteString
interpretAgda :: AgdaState -> ByteString -> IO ByteString
interpretAgda AgdaState
state ByteString
req = case ByteString -> Either ByteString (Either () AgdaCommand, ByteString)
parseRequest ByteString
req of
Left ByteString
err -> ByteString -> IO ByteString
forall (f :: * -> *) a. Applicative f => a -> f a
pure ByteString
err
Right (Either () AgdaCommand
ecmd, ByteString
request) -> do
let fetchResponse :: ByteString -> IO (TCM ByteString)
fetchResponse = AgdaState
-> Either () AgdaCommand -> ByteString -> IO (TCM ByteString)
chooseCommand AgdaState
state Either () AgdaCommand
ecmd
AgdaState -> TCM ByteString -> IO ByteString
runAgda AgdaState
state (TCM ByteString -> IO ByteString)
-> IO (TCM ByteString) -> IO ByteString
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ByteString -> IO (TCM ByteString)
fetchResponse ByteString
request
parseRequest :: ByteString -> Either ByteString (Either () AgdaCommand, ByteString)
parseRequest :: ByteString -> Either ByteString (Either () AgdaCommand, ByteString)
parseRequest ByteString
rawCmd = case ByteString -> [ByteString]
BS8.words ByteString
rawSubCommand of
[] -> ByteString -> Either ByteString (Either () AgdaCommand, 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 AgdaCommand
matchSupported ByteString
cmd of
Maybe AgdaCommand
Nothing -> ByteString -> Either ByteString (Either () AgdaCommand, ByteString)
forall a b. a -> Either a b
Left (ByteString
-> Either ByteString (Either () AgdaCommand, ByteString))
-> ByteString
-> Either ByteString (Either () AgdaCommand, ByteString)
forall a b. (a -> b) -> a -> b
$ ByteString
"Unknown command: " ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
<> ByteString
cmd
Just AgdaCommand
aCmd -> (Either () AgdaCommand, ByteString)
-> Either ByteString (Either () AgdaCommand, ByteString)
forall a b. b -> Either a b
Right (AgdaCommand -> Either () AgdaCommand
forall a b. b -> Either a b
Right AgdaCommand
aCmd, ByteString -> ByteString
dropCommand ByteString
rawSubCommand)
else (Either () AgdaCommand, ByteString)
-> Either ByteString (Either () AgdaCommand, ByteString)
forall a b. b -> Either a b
Right (() -> Either () AgdaCommand
forall a b. a -> Either a b
Left (), ByteString
rawSubCommand)
where
rawSubCommand :: ByteString
rawSubCommand = ByteString -> ByteString
dropCommand ByteString
rawCmd