{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeSynonymInstances #-}
module Proof.Assistant.Interpreter where

import Control.Concurrent.Async
import Control.Monad (forever)
import Data.ByteString (ByteString)
import Data.Coerce (coerce)
import Data.Text (unpack)
import System.Directory
import System.Process

import Agda.Interaction.State

import Proof.Assistant.Agda
import Proof.Assistant.Arend
import Proof.Assistant.Idris
import Proof.Assistant.Lean
import Proof.Assistant.Rzk

import Proof.Assistant.Helpers
import Proof.Assistant.Request
import Proof.Assistant.RefreshFile
import Proof.Assistant.ResourceLimit
import Proof.Assistant.Response
import Proof.Assistant.Settings
import Proof.Assistant.State
import Proof.Assistant.Transport

-- | Main worker function. Reads input from Telegram, calls CLI or API, could be anything.
-- Returns 'ByteString', wraps it in 'InterpreterResponse' and sends back to Telegram.
runInterpreter :: (Interpreter state settings) => BotState -> state -> IO ()
runInterpreter :: BotState -> state -> IO ()
runInterpreter BotState
botState state
is = IO () -> IO ()
forall (f :: * -> *) a b. Applicative f => f a -> f b
forever (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
  InterpreterRequest
incomingMessage <- InterpreterState settings -> IO InterpreterRequest
forall settings. InterpreterState settings -> IO InterpreterRequest
readInput (state -> InterpreterState settings
forall state settings.
Interpreter state settings =>
state -> InterpreterState settings
getSettings state
is)
  ByteString
response <- state -> InterpreterRequest -> IO ByteString
forall state settings.
Interpreter state settings =>
state -> InterpreterRequest -> IO ByteString
interpretSafe state
is InterpreterRequest
incomingMessage
  let telegramResponse :: InterpreterResponse
telegramResponse = InterpreterRequest -> ByteString -> InterpreterResponse
makeTelegramResponse InterpreterRequest
incomingMessage ByteString
response
  InterpreterResponse -> BotState -> IO ()
writeOutput InterpreterResponse
telegramResponse BotState
botState

-- | Worker abstraction over Proof assistant as Interpreter.
-- Could be CLI, Haskell function, network, whatever.
-- It should have the @state@ and associated @settings@ with the @state@.
class Interpreter state settings | state -> settings where
  interpretSafe :: state -> InterpreterRequest -> IO ByteString
  getSettings :: state -> InterpreterState settings

instance Interpreter InternalState InternalInterpreterSettings  where
  interpretSafe :: InternalState -> InterpreterRequest -> IO ByteString
interpretSafe InternalState
state InterpreterRequest
request = InternalState -> InterpreterRequest -> IO ByteString
callRzk InternalState
state InterpreterRequest
request
  getSettings :: InternalState -> InternalState
getSettings = InternalState -> InternalState
forall a. a -> a
id

instance Interpreter AgdaState AgdaSettings where
  interpretSafe :: AgdaState -> InterpreterRequest -> IO ByteString
interpretSafe AgdaState
state InterpreterRequest
request = AgdaState -> InterpreterRequest -> IO ByteString
callAgda AgdaState
state InterpreterRequest
request
  getSettings :: AgdaState -> InterpreterState AgdaSettings
getSettings AgdaState
state = AgdaState -> InterpreterState AgdaSettings
interpreterState AgdaState
state

instance Interpreter ExternalState ExternalInterpreterSettings where
  interpretSafe :: ExternalState -> InterpreterRequest -> IO ByteString
interpretSafe ExternalState
is InterpreterRequest
request = do
    let settings' :: ExternalInterpreterSettings
settings' = ExternalState -> ExternalInterpreterSettings
forall settings. InterpreterState settings -> settings
settings ExternalState
is
    (FilePath, FilePath)
tmpFilePath <- ExternalInterpreterSettings
-> InterpreterRequest -> Maybe FilePath -> IO (FilePath, FilePath)
refreshTmpFile ExternalInterpreterSettings
settings' InterpreterRequest
request Maybe FilePath
forall a. Maybe a
Nothing
    ExternalInterpreterSettings
-> (FilePath, FilePath) -> IO ByteString
callExternalInterpreter ExternalInterpreterSettings
settings' (FilePath, FilePath)
tmpFilePath
  getSettings :: ExternalState -> ExternalState
getSettings = ExternalState -> ExternalState
forall a. a -> a
id

instance Interpreter (InterpreterState IdrisSettings) IdrisSettings where
  interpretSafe :: InterpreterState IdrisSettings
-> InterpreterRequest -> IO ByteString
interpretSafe InterpreterState IdrisSettings
state InterpreterRequest
request = InterpreterState IdrisSettings
-> InterpreterRequest -> IO ByteString
callIdris2 InterpreterState IdrisSettings
state InterpreterRequest
request
  getSettings :: InterpreterState IdrisSettings -> InterpreterState IdrisSettings
getSettings = InterpreterState IdrisSettings -> InterpreterState IdrisSettings
forall a. a -> a
id

instance Interpreter (InterpreterState LeanSettings) LeanSettings where
  interpretSafe :: InterpreterState LeanSettings
-> InterpreterRequest -> IO ByteString
interpretSafe InterpreterState LeanSettings
state InterpreterRequest
request = InterpreterState LeanSettings
-> InterpreterRequest -> IO ByteString
callLean InterpreterState LeanSettings
state InterpreterRequest
request
  getSettings :: InterpreterState LeanSettings -> InterpreterState LeanSettings
getSettings = InterpreterState LeanSettings -> InterpreterState LeanSettings
forall a. a -> a
id

instance Interpreter (InterpreterState ArendSettings) ArendSettings where
  interpretSafe :: InterpreterState ArendSettings
-> InterpreterRequest -> IO ByteString
interpretSafe InterpreterState ArendSettings
state InterpreterRequest
request = InterpreterState ArendSettings
-> InterpreterRequest -> IO ByteString
callArend InterpreterState ArendSettings
state InterpreterRequest
request
  getSettings :: InterpreterState ArendSettings -> InterpreterState ArendSettings
getSettings = InterpreterState ArendSettings -> InterpreterState ArendSettings
forall a. a -> a
id

-- ** External Interpreter

-- | Call some external CLI application, probably Coq.
callExternalInterpreter
  :: ExternalInterpreterSettings -> (FilePath, FilePath) -> IO ByteString
callExternalInterpreter :: ExternalInterpreterSettings
-> (FilePath, FilePath) -> IO ByteString
callExternalInterpreter 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
..} (FilePath
dir, FilePath
path)
  = 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
      FilePath
contents <- FilePath -> IO FilePath
readFile FilePath
path
      let asyncExecutable :: IO ByteString
asyncExecutable = do
            Priority -> IO ()
setPriority Priority
priority
            (ExitCode
_exitCode, FilePath
stdout, FilePath
stderr) <- FilePath
-> [FilePath] -> FilePath -> IO (ExitCode, FilePath, FilePath)
readProcessWithExitCode (Executable -> FilePath
forall a. Coercible a Text => a -> FilePath
t2s Executable
executable) (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
contents
            ByteString -> IO ByteString
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ByteString -> IO ByteString) -> ByteString -> IO ByteString
forall a b. (a -> b) -> a -> b
$ FilePath -> ByteString
toBS (FilePath -> ByteString) -> FilePath -> ByteString
forall a b. (a -> b) -> a -> b
$ [FilePath] -> FilePath
unlines [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