{-# LANGUAGE OverloadedLabels  #-}
{-# LANGUAGE OverloadedStrings #-}

module Cornelis.Agda where

import           Control.Concurrent.Chan.Unagi (newChan, readChan, writeChan)
import           Control.Lens
import           Control.Monad (forever, replicateM_, when)
import           Control.Monad.IO.Class
import           Control.Monad.State
import           Cornelis.Debug (reportExceptions)
import           Cornelis.InfoWin (buildInfoBuffer)
import           Cornelis.Types
import           Cornelis.Types.Agda
import           Cornelis.Utils
import           Data.Aeson
import           Data.IORef
import qualified Data.Map as M
import qualified Data.Text as T
import qualified Data.Text.Lazy as LT
import           Data.Text.Lazy.Encoding (encodeUtf8)
import qualified Data.Text.Lazy.IO as LT
import           Neovim hiding (err)
import           Neovim.API.Text
import           System.IO hiding (hGetLine)
import           System.Process


------------------------------------------------------------------------------
-- | When true, dump out received JSON as it arrives.
debugJson :: Bool
debugJson :: Bool
debugJson = Bool
False


------------------------------------------------------------------------------
-- | Create an 'Agda' environment for the given buffer. This spawns an
-- asynchronous thread that keeps an agda process alive as long as vim is open.
--
-- TODO(sandy): This leaks the process when the buffer is closed.
spawnAgda :: Buffer -> Neovim CornelisEnv Agda
spawnAgda :: Buffer -> Neovim CornelisEnv Agda
spawnAgda Buffer
buffer = do
  (Maybe Handle
m_in, Maybe Handle
m_out, Maybe Handle
_, ProcessHandle
hdl) <-
    IO (Maybe Handle, Maybe Handle, Maybe Handle, ProcessHandle)
-> Neovim
     CornelisEnv
     (Maybe Handle, Maybe Handle, Maybe Handle, ProcessHandle)
forall a. IO a -> Neovim CornelisEnv a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Maybe Handle, Maybe Handle, Maybe Handle, ProcessHandle)
 -> Neovim
      CornelisEnv
      (Maybe Handle, Maybe Handle, Maybe Handle, ProcessHandle))
-> IO (Maybe Handle, Maybe Handle, Maybe Handle, ProcessHandle)
-> Neovim
     CornelisEnv
     (Maybe Handle, Maybe Handle, Maybe Handle, ProcessHandle)
forall a b. (a -> b) -> a -> b
$ CreateProcess
-> IO (Maybe Handle, Maybe Handle, Maybe Handle, ProcessHandle)
createProcess (CreateProcess
 -> IO (Maybe Handle, Maybe Handle, Maybe Handle, ProcessHandle))
-> CreateProcess
-> IO (Maybe Handle, Maybe Handle, Maybe Handle, ProcessHandle)
forall a b. (a -> b) -> a -> b
$
      (FilePath -> [FilePath] -> CreateProcess
proc FilePath
"agda" [FilePath
"--interaction-json"])
        { std_in = CreatePipe , std_out = CreatePipe }
  (InChan FilePath
c_in, OutChan FilePath
c_out) <- IO (InChan FilePath, OutChan FilePath)
-> Neovim CornelisEnv (InChan FilePath, OutChan FilePath)
forall a. IO a -> Neovim CornelisEnv a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO (InChan FilePath, OutChan FilePath)
forall a. IO (InChan a, OutChan a)
newChan
  IORef Bool
ready <- IO (IORef Bool) -> Neovim CornelisEnv (IORef Bool)
forall a. IO a -> Neovim CornelisEnv a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (IORef Bool) -> Neovim CornelisEnv (IORef Bool))
-> IO (IORef Bool) -> Neovim CornelisEnv (IORef Bool)
forall a b. (a -> b) -> a -> b
$ Bool -> IO (IORef Bool)
forall a. a -> IO (IORef a)
newIORef Bool
True
  case (Maybe Handle
m_in, Maybe Handle
m_out) of
    (Just Handle
hin, Just Handle
hout) -> do
      IO () -> Neovim CornelisEnv ()
forall a. IO a -> Neovim CornelisEnv a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> Neovim CornelisEnv ()) -> IO () -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ do
        Handle -> BufferMode -> IO ()
hSetBuffering Handle
hin BufferMode
NoBuffering
        Handle -> BufferMode -> IO ()
hSetBuffering Handle
hout BufferMode
NoBuffering

      let whenReady :: IO () -> m ()
whenReady IO ()
act = IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ do
            -- Agda outputs "JSON> " when it is ready
            -- We skip it, and set the ready flag
            Char
c <- Handle -> IO Char
hLookAhead Handle
hout
            case Char
c of
              Char
'J' -> Int -> IO Char -> IO ()
forall (m :: * -> *) a. Applicative m => Int -> m a -> m ()
replicateM_ Int
6 (Handle -> IO Char
hGetChar Handle
hout) IO () -> IO () -> IO ()
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IO ()
act
              Char
_ -> () -> IO ()
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

      -- On the first load, we make ourselves ready before Agda tells us anything
      Neovim CornelisEnv (Async Any) -> Neovim CornelisEnv ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Neovim CornelisEnv (Async Any) -> Neovim CornelisEnv ())
-> Neovim CornelisEnv (Async Any) -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ Neovim CornelisEnv Any -> Neovim CornelisEnv (Async Any)
forall (m :: * -> *) a. MonadUnliftIO m => m a -> m (Async a)
neovimAsync (Neovim CornelisEnv Any -> Neovim CornelisEnv (Async Any))
-> Neovim CornelisEnv Any -> Neovim CornelisEnv (Async Any)
forall a b. (a -> b) -> a -> b
$ (IO () -> Neovim CornelisEnv ()
forall {m :: * -> *}. MonadIO m => IO () -> m ()
whenReady (() -> IO ()
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()) >>) (Neovim CornelisEnv Any -> Neovim CornelisEnv Any)
-> (Neovim CornelisEnv () -> Neovim CornelisEnv Any)
-> Neovim CornelisEnv ()
-> Neovim CornelisEnv Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Neovim CornelisEnv () -> Neovim CornelisEnv Any
forall (f :: * -> *) a b. Applicative f => f a -> f b
forever (Neovim CornelisEnv () -> Neovim CornelisEnv Any)
-> Neovim CornelisEnv () -> Neovim CornelisEnv Any
forall a b. (a -> b) -> a -> b
$ Neovim CornelisEnv () -> Neovim CornelisEnv ()
forall env. Neovim env () -> Neovim env ()
reportExceptions (Neovim CornelisEnv () -> Neovim CornelisEnv ())
-> Neovim CornelisEnv () -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ do
        IO () -> Neovim CornelisEnv ()
forall {m :: * -> *}. MonadIO m => IO () -> m ()
whenReady (IO () -> Neovim CornelisEnv ()) -> IO () -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ IORef Bool -> Bool -> IO ()
forall a. IORef a -> a -> IO ()
atomicWriteIORef IORef Bool
ready Bool
True
        Text
resp <- IO Text -> Neovim CornelisEnv Text
forall a. IO a -> Neovim CornelisEnv a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Text -> Neovim CornelisEnv Text)
-> IO Text -> Neovim CornelisEnv Text
forall a b. (a -> b) -> a -> b
$ Handle -> IO Text
LT.hGetLine Handle
hout
        InChan AgdaResp
chan <- (CornelisEnv -> InChan AgdaResp)
-> Neovim CornelisEnv (InChan AgdaResp)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks CornelisEnv -> InChan AgdaResp
ce_stream
        case forall a. FromJSON a => ByteString -> Either FilePath a
eitherDecode @Response (ByteString -> Either FilePath Response)
-> ByteString -> Either FilePath Response
forall a b. (a -> b) -> a -> b
$ Text -> ByteString
encodeUtf8 Text
resp of
          Either FilePath Response
_ | Text -> Bool
LT.null Text
resp -> () -> Neovim CornelisEnv ()
forall a. a -> Neovim CornelisEnv a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
          Left FilePath
err -> Text -> Neovim CornelisEnv ()
forall env. Text -> Neovim env ()
vim_report_error (Text -> Neovim CornelisEnv ()) -> Text -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ FilePath -> Text
T.pack FilePath
err
          Right Response
res -> do
            case Response
res of
              HighlightingInfo Bool
_ [Highlight]
_ -> () -> Neovim CornelisEnv ()
forall a. a -> Neovim CornelisEnv a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
              Response
_ -> Bool -> Neovim CornelisEnv () -> Neovim CornelisEnv ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
debugJson (Neovim CornelisEnv () -> Neovim CornelisEnv ())
-> Neovim CornelisEnv () -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ Text -> Neovim CornelisEnv ()
forall env. Text -> Neovim env ()
vim_report_error (Text -> Neovim CornelisEnv ()) -> Text -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ FilePath -> Text
T.pack (FilePath -> Text) -> FilePath -> Text
forall a b. (a -> b) -> a -> b
$ Text -> FilePath
forall a. Show a => a -> FilePath
show Text
resp
            IO () -> Neovim CornelisEnv ()
forall a. IO a -> Neovim CornelisEnv a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> Neovim CornelisEnv ()) -> IO () -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ InChan AgdaResp -> AgdaResp -> IO ()
forall a. InChan a -> a -> IO ()
writeChan InChan AgdaResp
chan (AgdaResp -> IO ()) -> AgdaResp -> IO ()
forall a b. (a -> b) -> a -> b
$ Buffer -> Response -> AgdaResp
AgdaResp Buffer
buffer Response
res

      Neovim CornelisEnv (Async Any) -> Neovim CornelisEnv ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Neovim CornelisEnv (Async Any) -> Neovim CornelisEnv ())
-> Neovim CornelisEnv (Async Any) -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ Neovim CornelisEnv Any -> Neovim CornelisEnv (Async Any)
forall (m :: * -> *) a. MonadUnliftIO m => m a -> m (Async a)
neovimAsync (Neovim CornelisEnv Any -> Neovim CornelisEnv (Async Any))
-> Neovim CornelisEnv Any -> Neovim CornelisEnv (Async Any)
forall a b. (a -> b) -> a -> b
$ IO Any -> Neovim CornelisEnv Any
forall a. IO a -> Neovim CornelisEnv a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Any -> Neovim CornelisEnv Any)
-> IO Any -> Neovim CornelisEnv Any
forall a b. (a -> b) -> a -> b
$ IO () -> IO Any
forall (f :: * -> *) a b. Applicative f => f a -> f b
forever (IO () -> IO Any) -> IO () -> IO Any
forall a b. (a -> b) -> a -> b
$ do
        FilePath
msg <- OutChan FilePath -> IO FilePath
forall a. OutChan a -> IO a
readChan OutChan FilePath
c_out
        IORef Bool -> Bool -> IO ()
forall a. IORef a -> a -> IO ()
atomicWriteIORef IORef Bool
ready Bool
False
        Handle -> FilePath -> IO ()
hPutStrLn Handle
hin FilePath
msg

      Agda -> Neovim CornelisEnv Agda
forall a. a -> Neovim CornelisEnv a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Agda -> Neovim CornelisEnv Agda)
-> Agda -> Neovim CornelisEnv Agda
forall a b. (a -> b) -> a -> b
$ Buffer -> IORef Bool -> InChan FilePath -> ProcessHandle -> Agda
Agda Buffer
buffer IORef Bool
ready InChan FilePath
c_in ProcessHandle
hdl
    (Maybe Handle
_, Maybe Handle
_) -> FilePath -> Neovim CornelisEnv Agda
forall a. HasCallStack => FilePath -> a
error FilePath
"can't start agda"


------------------------------------------------------------------------------
-- | Drop a prefix from the text, if it exists.
dropPrefix :: LT.Text -> LT.Text -> LT.Text
dropPrefix :: Text -> Text -> Text
dropPrefix Text
pref Text
msg
  | Text -> Text -> Bool
LT.isPrefixOf Text
pref Text
msg = Int64 -> Text -> Text
LT.drop (Text -> Int64
LT.length Text
pref) Text
msg
  | Bool
otherwise = Text
msg


------------------------------------------------------------------------------
-- | Send an 'Interaction' to an 'Agda'.
runIOTCM :: Interaction -> Agda -> Neovim env ()
runIOTCM :: forall env. Interaction -> Agda -> Neovim env ()
runIOTCM Interaction
i Agda
agda = do
  IOTCM
iotcm <- Interaction -> Buffer -> Neovim env IOTCM
forall env. Interaction -> Buffer -> Neovim env IOTCM
buildIOTCM Interaction
i (Buffer -> Neovim env IOTCM) -> Buffer -> Neovim env IOTCM
forall a b. (a -> b) -> a -> b
$ Agda -> Buffer
a_buffer Agda
agda
  -- liftIO $ appendFile "/tmp/agda.spy" $ show iotcm
  IO () -> Neovim env ()
forall a. IO a -> Neovim env a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> Neovim env ()) -> IO () -> Neovim env ()
forall a b. (a -> b) -> a -> b
$ InChan FilePath -> FilePath -> IO ()
forall a. InChan a -> a -> IO ()
writeChan (Agda -> InChan FilePath
a_req Agda
agda) (IOTCM -> FilePath
forall a. Show a => a -> FilePath
show IOTCM
iotcm)


------------------------------------------------------------------------------
-- | Construct an 'IOTCM' for a buffer.
buildIOTCM :: Interaction -> Buffer -> Neovim env IOTCM
buildIOTCM :: forall env. Interaction -> Buffer -> Neovim env IOTCM
buildIOTCM Interaction
i Buffer
buffer = do
  Text
fp <- Buffer -> Neovim env Text
forall env. Buffer -> Neovim env Text
buffer_get_name Buffer
buffer
  IOTCM -> Neovim env IOTCM
forall a. a -> Neovim env a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (IOTCM -> Neovim env IOTCM) -> IOTCM -> Neovim env IOTCM
forall a b. (a -> b) -> a -> b
$ Text
-> HighlightingLevel -> HighlightingMethod -> Interaction -> IOTCM
forall range.
Text
-> HighlightingLevel
-> HighlightingMethod
-> Interaction' range
-> IOTCM' range
IOTCM Text
fp HighlightingLevel
NonInteractive HighlightingMethod
Direct Interaction
i


------------------------------------------------------------------------------
-- | Get the current buffer and run the continuation.
withCurrentBuffer :: (Buffer -> Neovim env a) -> Neovim env a
withCurrentBuffer :: forall env a. (Buffer -> Neovim env a) -> Neovim env a
withCurrentBuffer Buffer -> Neovim env a
f = Neovim env Buffer
forall env. Neovim env Buffer
vim_get_current_buffer Neovim env Buffer -> (Buffer -> Neovim env a) -> Neovim env a
forall a b. Neovim env a -> (a -> Neovim env b) -> Neovim env b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Buffer -> Neovim env a
f


------------------------------------------------------------------------------
-- | Ensure we have a 'BufferStuff' attached to the current buffer.
withAgda :: Neovim CornelisEnv a -> Neovim CornelisEnv a
withAgda :: forall a. Neovim CornelisEnv a -> Neovim CornelisEnv a
withAgda Neovim CornelisEnv a
m = do
  Buffer
buffer <- Neovim CornelisEnv Buffer
forall env. Neovim env Buffer
vim_get_current_buffer
  (CornelisState -> Maybe BufferStuff)
-> Neovim CornelisEnv (Maybe BufferStuff)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (Buffer -> Map Buffer BufferStuff -> Maybe BufferStuff
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Buffer
buffer (Map Buffer BufferStuff -> Maybe BufferStuff)
-> (CornelisState -> Map Buffer BufferStuff)
-> CornelisState
-> Maybe BufferStuff
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CornelisState -> Map Buffer BufferStuff
cs_buffers) Neovim CornelisEnv (Maybe BufferStuff)
-> (Maybe BufferStuff -> Neovim CornelisEnv a)
-> Neovim CornelisEnv a
forall a b.
Neovim CornelisEnv a
-> (a -> Neovim CornelisEnv b) -> Neovim CornelisEnv b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just BufferStuff
_ -> Neovim CornelisEnv a
m
    Maybe BufferStuff
Nothing -> do
      Agda
agda <- Buffer -> Neovim CornelisEnv Agda
spawnAgda Buffer
buffer
      InfoBuffer
iw <- Neovim CornelisEnv InfoBuffer
forall env. Neovim env InfoBuffer
buildInfoBuffer
      (CornelisState -> CornelisState) -> Neovim CornelisEnv ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' ((CornelisState -> CornelisState) -> Neovim CornelisEnv ())
-> (CornelisState -> CornelisState) -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ ASetter
  CornelisState
  CornelisState
  (Map Buffer BufferStuff)
  (Map Buffer BufferStuff)
#cs_buffers ASetter
  CornelisState
  CornelisState
  (Map Buffer BufferStuff)
  (Map Buffer BufferStuff)
-> (Map Buffer BufferStuff -> Map Buffer BufferStuff)
-> CornelisState
-> CornelisState
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ Buffer
-> BufferStuff -> Map Buffer BufferStuff -> Map Buffer BufferStuff
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Buffer
buffer BufferStuff
        { bs_agda_proc :: Agda
bs_agda_proc = Agda
agda
        , bs_ips :: Map InteractionId (InteractionPoint Identity)
bs_ips = Map InteractionId (InteractionPoint Identity)
forall a. Monoid a => a
mempty
        , bs_ip_exts :: Map InteractionId Extmark
bs_ip_exts = Map InteractionId Extmark
forall a. Monoid a => a
mempty
        , bs_goto_sites :: Map Extmark DefinitionSite
bs_goto_sites = Map Extmark DefinitionSite
forall a. Monoid a => a
mempty
        , bs_goals :: DisplayInfo
bs_goals = [GoalInfo (InteractionPoint Identity)]
-> [GoalInfo NamedPoint] -> [Message] -> [Message] -> DisplayInfo
AllGoalsWarnings [] [] [] []
        , bs_info_win :: InfoBuffer
bs_info_win = InfoBuffer
iw
        , bs_code_map :: LineIntervals
bs_code_map = LineIntervals
forall a. Monoid a => a
mempty
        }
      Neovim CornelisEnv a
m


------------------------------------------------------------------------------
-- | Get the 'Agda' environment for a given buffer.
getAgda :: Buffer -> Neovim CornelisEnv Agda
getAgda :: Buffer -> Neovim CornelisEnv Agda
getAgda Buffer
buffer = (CornelisState -> Agda) -> Neovim CornelisEnv Agda
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ((CornelisState -> Agda) -> Neovim CornelisEnv Agda)
-> (CornelisState -> Agda) -> Neovim CornelisEnv Agda
forall a b. (a -> b) -> a -> b
$ BufferStuff -> Agda
bs_agda_proc (BufferStuff -> Agda)
-> (CornelisState -> BufferStuff) -> CornelisState -> Agda
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map Buffer BufferStuff -> Buffer -> BufferStuff
forall k a. Ord k => Map k a -> k -> a
M.! Buffer
buffer) (Map Buffer BufferStuff -> BufferStuff)
-> (CornelisState -> Map Buffer BufferStuff)
-> CornelisState
-> BufferStuff
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CornelisState -> Map Buffer BufferStuff
cs_buffers