{-# 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.Request
import Proof.Assistant.Settings
import Proof.Assistant.State

import qualified Data.ByteString.Char8 as BS8

-- | Call Agda with its state. It will parse and execute command from the 'InterpreterRequest'.
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
forall a. ChatId -> AgdaState -> IO a -> IO a
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

-- | Since every chat associated with its own Agda state, we need to modify 'TCEnv'
-- by setting 'envCurrentPath' with an absolute path to the corresponding file.
withChat :: ChatId -> AgdaState -> IO a -> IO a
withChat :: ChatId -> AgdaState -> IO a -> IO a
withChat ChatId
chatId AgdaState
state IO a
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
  IO a
action

-- | Parse user input as command and execute in Agda.
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

-- | Parse command. It could be unknown command or 'AgdaCommand' sub-command with its arguments
-- or even expression to evaluate.
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