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

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

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