{-# 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
debugJson :: Bool
debugJson :: Bool
debugJson = Bool
False
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
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 ()
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"
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
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
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)
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
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
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
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