module AgdaInterface
    ( InteractionState
    , initState
    , tcmAction_

    , Interaction (..)
    , Response (..), GiveResult (..)
    , Range, Range' (..)
    , InteractionId (..)
    ) where

import Agda.Interaction.InteractionTop
import Agda.Interaction.Response
import Agda.TypeChecking.Monad.Base hiding (initState)
import qualified Agda.TypeChecking.Monad.Base as Base
import Agda.Syntax.Position

import Data.IORef
import Control.Monad.State
import Control.Concurrent.MVar

-----------------------------

data InteractionState = InteractionState CommandState TCState

initState :: InteractionState
initState = InteractionState initCommandState Base.initState

tcmAction_
    :: FilePath
    -> Interaction
    -> StateT InteractionState IO [Response]
tcmAction_ filepath action = StateT $ \(InteractionState cs ts) -> do
    m <- newMVar []

    let ts_ = ts { stPersistent = (stPersistent ts) { stInteractionOutputCallback = log } }
        log x = liftIO $ modifyMVar_ m $ return . (x:)

    r <- newIORef ts_
    cs' <- unTCM (execStateT act cs) r initEnv
    ts' <- readIORef r

    rs <- fmap reverse $ takeMVar m
    return (rs, InteractionState cs' ts')
  where
    act = runInteraction $ IOTCM filepath Interactive Indirect action