{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RecordWildCards #-}
module Proof.Assistant.Arend where

import Control.Concurrent.Async (race)
import Data.Coerce (coerce)
import Data.Text (unpack)
import System.Directory (createDirectoryIfMissing, withCurrentDirectory)
import System.FilePath
import System.Process (readProcessWithExitCode)

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

import qualified Data.ByteString.Char8 as BS8
import qualified Data.Text.IO as Text

-- | Call Arend typechecker as CLI application.
-- It prepares the CLI command, executes it and waits for response.
callArend :: InterpreterState ArendSettings -> InterpreterRequest -> IO BotResponse
callArend InterpreterState{..} ir = do
  let ArendSettings{..} = coerce settings
      ExternalInterpreterSettings{..} = externalArend
  currentProjectDir <- setArendProject settings ir
  withCurrentDirectory arendRootProjectDir $ do
    let fullArgs = (unpack <$> coerce args) <> [currentProjectDir]
        runProcess = readProcessWithExitCode (t2s executable) fullArgs ""
        asyncExecutable = do
          setPriority priority
          (_exitCode, stdout, stderr) <- runProcess
          pure . validate currentProjectDir . toBS . unlines $ [stdout, stderr]
        asyncTimer = asyncWait time
    eresult <- race asyncTimer (handleErrorMaybe asyncExecutable)
    case eresult of
      Left ()  -> pure (TextResponse "Time limit exceeded")
      Right bs -> pure (TextResponse bs)

-- | Arend requires a project for every file to typecheck.
-- It reads project configuration, finds all files in a project directory
-- and tries to typecheck all of them.
-- 
-- Since we need to isolate different chats from each other we need to ensure
-- that every chat has its own project. And every project has its own configuration.
--
-- As result, project directory will be created, set and returned.
setArendProject :: ArendSettings -> InterpreterRequest -> IO FilePath
setArendProject ArendSettings{..} InterpreterRequest{..} = do
  let ExternalInterpreterSettings{..} = externalArend
      projectDir = arendRootProjectDir </> (tempFilePrefix  <> chatIdToString interpreterRequestTelegramChatId)
      projectConfigPath = projectDir </> arendYamlFilename
      projectSourcePath = projectDir </> arendModuleName <.> fileExtension
  createDirectoryIfMissing True projectDir
  Text.writeFile projectConfigPath arendYamlContent
  BS8.writeFile projectSourcePath $ dropSubCommand interpreterRequestMessage
  pure projectDir