{-# LANGUAGE RecordWildCards #-}

module Agda.Interaction.State where

import Agda.Interaction.Options
import Agda.Syntax.Translation.ConcreteToAbstract (importPrimitives)
import Agda.TypeChecking.Errors (prettyError)
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.Options (setCommandLineOptions)
import Control.Monad.Except (MonadError(..))
import Data.ByteString (ByteString)
import Data.IORef (IORef, newIORef, readIORef, atomicWriteIORef, atomicModifyIORef')
import System.Directory (getTemporaryDirectory, withCurrentDirectory)

import Proof.Assistant.Helpers (toBS)
import Proof.Assistant.Settings
import Proof.Assistant.State

-- | Agda has its own env ('TCEnv') and state ('TCState').
-- We are using them in combination with communication channel between Agda and bot.
data AgdaState = AgdaState
  { AgdaState -> InterpreterState AgdaSettings
interpreterState :: !(InterpreterState AgdaSettings)
  , AgdaState -> IORef TCEnv
agdaEnvRef       :: !(IORef TCEnv)
  , AgdaState -> IORef TCState
agdaStateRef     :: !(IORef TCState)
  }

-- | Initiate 'AgdaState' from 'AgdaSettings'.
newAgdaState :: AgdaSettings -> IO AgdaState
newAgdaState :: AgdaSettings -> IO AgdaState
newAgdaState AgdaSettings
settings = do
  InterpreterState AgdaSettings
interpreterState <- AgdaSettings -> IO (InterpreterState AgdaSettings)
forall settings.
ToInterpreterState settings =>
settings -> IO (InterpreterState settings)
newInterpreterState (AgdaSettings -> IO (InterpreterState AgdaSettings))
-> AgdaSettings -> IO (InterpreterState AgdaSettings)
forall a b. (a -> b) -> a -> b
$ AgdaSettings
settings
  let state0 :: TCState
state0 = TCState
initState
      env :: TCEnv
env = TCEnv
initEnv
  FilePath
tmpDir <- IO FilePath
getTemporaryDirectory
  ([Declaration]
_, TCState
state1) <- FilePath
-> IO ([Declaration], TCState) -> IO ([Declaration], TCState)
forall a. FilePath -> IO a -> IO a
withCurrentDirectory FilePath
tmpDir
    (IO ([Declaration], TCState) -> IO ([Declaration], TCState))
-> IO ([Declaration], TCState) -> IO ([Declaration], TCState)
forall a b. (a -> b) -> a -> b
$ TCEnv
-> TCState -> TCMT IO [Declaration] -> IO ([Declaration], TCState)
forall (m :: * -> *) a.
MonadIO m =>
TCEnv -> TCState -> TCMT m a -> m (a, TCState)
runTCM TCEnv
env TCState
state0
    (TCMT IO [Declaration] -> IO ([Declaration], TCState))
-> TCMT IO [Declaration] -> IO ([Declaration], TCState)
forall a b. (a -> b) -> a -> b
$ CommandLineOptions -> TCM ()
setCommandLineOptions CommandLineOptions
defaultOptions TCM () -> TCMT IO [Declaration] -> TCMT IO [Declaration]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> TCMT IO [Declaration]
importPrimitives
    
  IORef TCState
agdaStateRef <- TCState -> IO (IORef TCState)
forall a. a -> IO (IORef a)
newIORef TCState
state1
  IORef TCEnv
agdaEnvRef <- TCEnv -> IO (IORef TCEnv)
forall a. a -> IO (IORef a)
newIORef TCEnv
env
  AgdaState -> IO AgdaState
forall (f :: * -> *) a. Applicative f => a -> f a
pure AgdaState :: InterpreterState AgdaSettings
-> IORef TCEnv -> IORef TCState -> AgdaState
AgdaState {IORef TCState
IORef TCEnv
InterpreterState AgdaSettings
agdaEnvRef :: IORef TCEnv
agdaStateRef :: IORef TCState
interpreterState :: InterpreterState AgdaSettings
agdaStateRef :: IORef TCState
agdaEnvRef :: IORef TCEnv
interpreterState :: InterpreterState AgdaSettings
..}

-- | Helper to get access to 'TCState'.
readTCState :: AgdaState -> IO TCState
readTCState :: AgdaState -> IO TCState
readTCState = IORef TCState -> IO TCState
forall a. IORef a -> IO a
readIORef (IORef TCState -> IO TCState)
-> (AgdaState -> IORef TCState) -> AgdaState -> IO TCState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AgdaState -> IORef TCState
agdaStateRef

-- | Helper to store new 'TCState'.
writeTCState :: TCState -> AgdaState -> IO ()
writeTCState :: TCState -> AgdaState -> IO ()
writeTCState TCState
tcState AgdaState
state = IORef TCState -> TCState -> IO ()
forall a. IORef a -> a -> IO ()
atomicWriteIORef (AgdaState -> IORef TCState
agdaStateRef AgdaState
state) (TCState -> IO ()) -> TCState -> IO ()
forall a b. (a -> b) -> a -> b
$! TCState
tcState

-- | Helper to get access to 'TCEnv'.
readTCEnv :: AgdaState -> IO TCEnv
readTCEnv :: AgdaState -> IO TCEnv
readTCEnv = IORef TCEnv -> IO TCEnv
forall a. IORef a -> IO a
readIORef (IORef TCEnv -> IO TCEnv)
-> (AgdaState -> IORef TCEnv) -> AgdaState -> IO TCEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AgdaState -> IORef TCEnv
agdaEnvRef

-- | Helper to store new 'TCEnv'.
writeTCEnv :: TCEnv -> AgdaState -> IO ()
writeTCEnv :: TCEnv -> AgdaState -> IO ()
writeTCEnv TCEnv
tcEnv AgdaState
state = IORef TCEnv -> TCEnv -> IO ()
forall a. IORef a -> a -> IO ()
atomicWriteIORef (AgdaState -> IORef TCEnv
agdaEnvRef AgdaState
state) (TCEnv -> IO ()) -> TCEnv -> IO ()
forall a b. (a -> b) -> a -> b
$! TCEnv
tcEnv

-- | Run chosen typechecking action in the typechecking monad ('TCM').
runAgda :: AgdaState -> TCM ByteString -> IO ByteString
runAgda :: AgdaState -> TCM ByteString -> IO ByteString
runAgda AgdaState
as TCM ByteString
action = do
  TCState
tcState <- AgdaState -> IO TCState
readTCState AgdaState
as
  TCEnv
tcEnv   <- AgdaState -> IO TCEnv
readTCEnv AgdaState
as
  (ByteString
response, TCState
newTCState) <- TCEnv -> TCState -> TCM ByteString -> IO (ByteString, TCState)
forall (m :: * -> *) a.
MonadIO m =>
TCEnv -> TCState -> TCMT m a -> m (a, TCState)
runTCM TCEnv
tcEnv TCState
tcState (TCM ByteString
action TCM ByteString -> (TCErr -> TCM ByteString) -> TCM ByteString
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` TCErr -> TCM ByteString
forall (m :: * -> *). MonadTCM m => TCErr -> m ByteString
catchAgdaError)
  TCState -> AgdaState -> IO ()
writeTCState TCState
newTCState AgdaState
as
  ByteString -> IO ByteString
forall (f :: * -> *) a. Applicative f => a -> f a
pure ByteString
response

-- | Catch error from Agda and make it looks pretty.
catchAgdaError :: MonadTCM m => TCErr -> m ByteString
catchAgdaError :: TCErr -> m ByteString
catchAgdaError TCErr
e = do
  FilePath
s <- TCErr -> m FilePath
forall (tcm :: * -> *). MonadTCM tcm => TCErr -> tcm FilePath
prettyError TCErr
e
  ByteString -> m ByteString
forall (m :: * -> *) a. Monad m => a -> m a
return (ByteString -> m ByteString) -> ByteString -> m ByteString
forall a b. (a -> b) -> a -> b
$ FilePath -> ByteString
toBS FilePath
s

-- | Helper to modify 'TCEnv'.
setEnv :: AgdaState -> (TCEnv -> TCEnv) -> IO ()
setEnv :: AgdaState -> (TCEnv -> TCEnv) -> IO ()
setEnv AgdaState
state TCEnv -> TCEnv
modifier =
  let modify :: TCEnv -> (TCEnv, ())
modify TCEnv
st = (TCEnv -> TCEnv
modifier TCEnv
st, ())
  in IORef TCEnv -> (TCEnv -> (TCEnv, ())) -> IO ()
forall a b. IORef a -> (a -> (a, b)) -> IO b
atomicModifyIORef' (AgdaState -> IORef TCEnv
agdaEnvRef AgdaState
state) ((TCEnv -> (TCEnv, ())) -> IO ())
-> (TCEnv -> (TCEnv, ())) -> IO ()
forall a b. (a -> b) -> a -> b
$ TCEnv -> (TCEnv, ())
modify