{-# LANGUAGE DataKinds         #-}
{-# LANGUAGE LambdaCase        #-}
{-# LANGUAGE OverloadedLabels  #-}
{-# LANGUAGE OverloadedStrings #-}

module Plugin where

import           Control.Lens
import           Control.Monad ((>=>))
import           Control.Monad.State.Class
import           Control.Monad.Trans
import           Cornelis.Agda (withCurrentBuffer, runIOTCM, withAgda, getAgda)
import           Cornelis.Diff (resetDiff, recordUpdate, Replace(..), Colline(..), Vallee(..))
import           Cornelis.Goals
import           Cornelis.Highlighting (getExtmarks, highlightInterval, updateLineIntervals)
import           Cornelis.InfoWin (showInfoWindow, closeInfoWindows)
import           Cornelis.Offsets
import           Cornelis.Pretty (prettyGoals, HighlightGroup (CornelisHole))
import           Cornelis.Types
import           Cornelis.Types.Agda hiding (Error)
import           Cornelis.Utils
import           Cornelis.Vim
import           Data.Bool (bool)
import           Data.Foldable (for_, fold, toList)
import           Data.IORef (IORef, readIORef, atomicModifyIORef)
import           Data.List
import qualified Data.Map as M
import           Data.Ord
import qualified Data.Text as T
import           Data.Traversable (for)
import qualified Data.Vector as V
import           Neovim
import           Neovim.API.Text
import           Neovim.User.Input (input)
import           System.Process (terminateProcess)
import           Text.Read (readMaybe)


runInteraction :: Interaction -> Neovim CornelisEnv ()
runInteraction :: Interaction -> Neovim CornelisEnv ()
runInteraction Interaction
interaction = (Buffer -> Neovim CornelisEnv ()) -> Neovim CornelisEnv ()
forall env a. (Buffer -> Neovim env a) -> Neovim env a
withCurrentBuffer ((Buffer -> Neovim CornelisEnv ()) -> Neovim CornelisEnv ())
-> (Buffer -> Neovim CornelisEnv ()) -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ \Buffer
b -> do
    Agda
agda <- Buffer -> Neovim CornelisEnv Agda
getAgda Buffer
b
    Interaction -> Agda -> Neovim CornelisEnv ()
forall env. Interaction -> Agda -> Neovim env ()
runIOTCM Interaction
interaction Agda
agda


getDefinitionSites :: Buffer -> AgdaPos -> Neovim CornelisEnv (First DefinitionSite)
getDefinitionSites :: Buffer -> AgdaPos -> Neovim CornelisEnv (First DefinitionSite)
getDefinitionSites Buffer
b AgdaPos
p = Buffer
-> (BufferStuff -> Neovim CornelisEnv (First DefinitionSite))
-> Neovim CornelisEnv (First DefinitionSite)
forall a.
Monoid a =>
Buffer
-> (BufferStuff -> Neovim CornelisEnv a) -> Neovim CornelisEnv a
withBufferStuff Buffer
b ((BufferStuff -> Neovim CornelisEnv (First DefinitionSite))
 -> Neovim CornelisEnv (First DefinitionSite))
-> (BufferStuff -> Neovim CornelisEnv (First DefinitionSite))
-> Neovim CornelisEnv (First DefinitionSite)
forall a b. (a -> b) -> a -> b
$ \BufferStuff
bs -> do
  [ExtmarkStuff]
marks <- Buffer -> AgdaPos -> Neovim CornelisEnv [ExtmarkStuff]
getExtmarks Buffer
b AgdaPos
p
  First DefinitionSite -> Neovim CornelisEnv (First DefinitionSite)
forall a. a -> Neovim CornelisEnv a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (First DefinitionSite -> Neovim CornelisEnv (First DefinitionSite))
-> First DefinitionSite
-> Neovim CornelisEnv (First DefinitionSite)
forall a b. (a -> b) -> a -> b
$ ((ExtmarkStuff -> First DefinitionSite)
 -> [ExtmarkStuff] -> First DefinitionSite)
-> [ExtmarkStuff]
-> (ExtmarkStuff -> First DefinitionSite)
-> First DefinitionSite
forall a b c. (a -> b -> c) -> b -> a -> c
flip (ExtmarkStuff -> First DefinitionSite)
-> [ExtmarkStuff] -> First DefinitionSite
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap [ExtmarkStuff]
marks ((ExtmarkStuff -> First DefinitionSite) -> First DefinitionSite)
-> (ExtmarkStuff -> First DefinitionSite) -> First DefinitionSite
forall a b. (a -> b) -> a -> b
$ \ExtmarkStuff
es ->
    Maybe DefinitionSite -> First DefinitionSite
forall a. Maybe a -> First a
First (Maybe DefinitionSite -> First DefinitionSite)
-> Maybe DefinitionSite -> First DefinitionSite
forall a b. (a -> b) -> a -> b
$ Extmark -> Map Extmark DefinitionSite -> Maybe DefinitionSite
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (ExtmarkStuff -> Extmark
es_mark ExtmarkStuff
es) (Map Extmark DefinitionSite -> Maybe DefinitionSite)
-> Map Extmark DefinitionSite -> Maybe DefinitionSite
forall a b. (a -> b) -> a -> b
$ BufferStuff -> Map Extmark DefinitionSite
bs_goto_sites BufferStuff
bs


doGotoDefinition :: CommandArguments -> Neovim CornelisEnv ()
doGotoDefinition :: CommandArguments -> Neovim CornelisEnv ()
doGotoDefinition CommandArguments
_ = Neovim CornelisEnv ()
gotoDefinition


gotoDefinition :: Neovim CornelisEnv ()
gotoDefinition :: Neovim CornelisEnv ()
gotoDefinition = Neovim CornelisEnv () -> Neovim CornelisEnv ()
forall a. Neovim CornelisEnv a -> Neovim CornelisEnv a
withAgda (Neovim CornelisEnv () -> Neovim CornelisEnv ())
-> Neovim CornelisEnv () -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ do
  Window
w <- Neovim CornelisEnv Window
forall env. Neovim env Window
nvim_get_current_win
  AgdaPos
rc <- Window -> Neovim CornelisEnv AgdaPos
forall env. Window -> Neovim env AgdaPos
getWindowCursor Window
w
  Buffer
b <- Window -> Neovim CornelisEnv Buffer
forall env. Window -> Neovim env Buffer
window_get_buffer Window
w
  Buffer -> AgdaPos -> Neovim CornelisEnv (First DefinitionSite)
getDefinitionSites Buffer
b AgdaPos
rc Neovim CornelisEnv (First DefinitionSite)
-> (First DefinitionSite -> Neovim CornelisEnv ())
-> Neovim CornelisEnv ()
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
    First Maybe DefinitionSite
Nothing -> Text -> Neovim CornelisEnv ()
forall env. Text -> Neovim env ()
reportInfo Text
"No syntax under cursor."
    First (Just DefinitionSite
ds) -> do
      -- TODO(sandy): escape spaces
      Text -> Neovim CornelisEnv ()
forall env. Text -> Neovim env ()
vim_command (Text -> Neovim CornelisEnv ()) -> Text -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ Text
"edit " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> DefinitionSite -> Text
ds_filepath DefinitionSite
ds
      Buffer
b' <- Window -> Neovim CornelisEnv Buffer
forall env. Window -> Neovim env Buffer
window_get_buffer Window
w
      Text
contents <- (Vector Text -> Text)
-> Neovim CornelisEnv (Vector Text) -> Neovim CornelisEnv Text
forall a b.
(a -> b) -> Neovim CornelisEnv a -> Neovim CornelisEnv b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Text] -> Text
T.unlines ([Text] -> Text) -> (Vector Text -> [Text]) -> Vector Text -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vector Text -> [Text]
forall a. Vector a -> [a]
V.toList) (Neovim CornelisEnv (Vector Text) -> Neovim CornelisEnv Text)
-> Neovim CornelisEnv (Vector Text) -> Neovim CornelisEnv Text
forall a b. (a -> b) -> a -> b
$ Buffer
-> Int64 -> Int64 -> Bool -> Neovim CornelisEnv (Vector Text)
forall env.
Buffer -> Int64 -> Int64 -> Bool -> Neovim env (Vector Text)
buffer_get_lines Buffer
b' Int64
0 (-Int64
1) Bool
False
      let buffer_idx :: Index 'Byte 'ZeroIndexed
buffer_idx = Text -> Index 'CodePoint 'ZeroIndexed -> Index 'Byte 'ZeroIndexed
toBytes Text
contents (Index 'CodePoint 'ZeroIndexed -> Index 'Byte 'ZeroIndexed)
-> Index 'CodePoint 'ZeroIndexed -> Index 'Byte 'ZeroIndexed
forall a b. (a -> b) -> a -> b
$ Index 'CodePoint 'OneIndexed -> Index 'CodePoint 'ZeroIndexed
forall (e :: Unit). Index e 'OneIndexed -> Index e 'ZeroIndexed
zeroIndex (Index 'CodePoint 'OneIndexed -> Index 'CodePoint 'ZeroIndexed)
-> Index 'CodePoint 'OneIndexed -> Index 'CodePoint 'ZeroIndexed
forall a b. (a -> b) -> a -> b
$ DefinitionSite -> Index 'CodePoint 'OneIndexed
ds_position DefinitionSite
ds
      -- TODO(sandy): use window_set_cursor instead?
      Text -> Neovim CornelisEnv ()
forall env. Text -> Neovim env ()
vim_command (Text -> Neovim CornelisEnv ()) -> Text -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ Text
"keepjumps normal! " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (Index 'Byte 'ZeroIndexed -> String
forall a. Show a => a -> String
show Index 'Byte 'ZeroIndexed
buffer_idx) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"go"


doLoad :: CommandArguments -> Neovim CornelisEnv ()
doLoad :: CommandArguments -> Neovim CornelisEnv ()
doLoad = Neovim CornelisEnv () -> CommandArguments -> Neovim CornelisEnv ()
forall a b. a -> b -> a
const Neovim CornelisEnv ()
load

atomicSwapIORef :: IORef a -> a -> IO a
atomicSwapIORef :: forall a. IORef a -> a -> IO a
atomicSwapIORef IORef a
r a
x = IORef a -> (a -> (a, a)) -> IO a
forall a b. IORef a -> (a -> (a, b)) -> IO b
atomicModifyIORef IORef a
r (a
x,)

load :: Neovim CornelisEnv ()
load :: Neovim CornelisEnv ()
load = Neovim CornelisEnv () -> Neovim CornelisEnv ()
forall a. Neovim CornelisEnv a -> Neovim CornelisEnv a
withAgda (Neovim CornelisEnv () -> Neovim CornelisEnv ())
-> Neovim CornelisEnv () -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ (Buffer -> Neovim CornelisEnv ()) -> Neovim CornelisEnv ()
forall env a. (Buffer -> Neovim env a) -> Neovim env a
withCurrentBuffer ((Buffer -> Neovim CornelisEnv ()) -> Neovim CornelisEnv ())
-> (Buffer -> Neovim CornelisEnv ()) -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ \Buffer
b -> do
  Agda
agda <- Buffer -> Neovim CornelisEnv Agda
getAgda Buffer
b
  Bool
ready <- IO Bool -> Neovim CornelisEnv Bool
forall a. IO a -> Neovim CornelisEnv a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Bool -> Neovim CornelisEnv Bool)
-> IO Bool -> Neovim CornelisEnv Bool
forall a b. (a -> b) -> a -> b
$ IORef Bool -> IO Bool
forall a. IORef a -> IO a
readIORef (IORef Bool -> IO Bool) -> IORef Bool -> IO Bool
forall a b. (a -> b) -> a -> b
$ Agda -> IORef Bool
a_ready Agda
agda
  if Bool
ready then do
    Text -> Neovim CornelisEnv ()
forall env. Text -> Neovim env ()
vim_command Text
"noautocmd w"
    Text
name <- Buffer -> Neovim CornelisEnv Text
forall env. Buffer -> Neovim env Text
buffer_get_name (Buffer -> Neovim CornelisEnv Text)
-> Buffer -> Neovim CornelisEnv Text
forall a b. (a -> b) -> a -> b
$ Agda -> Buffer
a_buffer Agda
agda
    (Interaction -> Agda -> Neovim CornelisEnv ())
-> Agda -> Interaction -> Neovim CornelisEnv ()
forall a b c. (a -> b -> c) -> b -> a -> c
flip Interaction -> Agda -> Neovim CornelisEnv ()
forall env. Interaction -> Agda -> Neovim env ()
runIOTCM Agda
agda (Interaction -> Neovim CornelisEnv ())
-> Interaction -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ Text -> [String] -> Interaction
forall range. Text -> [String] -> Interaction' range
Cmd_load Text
name []
    Buffer -> Neovim CornelisEnv Int64
forall env. Buffer -> Neovim env Int64
buffer_get_number Buffer
b Neovim CornelisEnv Int64
-> (Int64 -> Neovim CornelisEnv ()) -> Neovim CornelisEnv ()
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
>>= Int64 -> Neovim CornelisEnv ()
resetDiff
    Buffer -> Neovim CornelisEnv ()
updateLineIntervals Buffer
b
  else Text -> Neovim CornelisEnv ()
forall env. Text -> Neovim env ()
vim_report_error Text
"Agda is busy, not ready to load"

questionToMeta :: Buffer -> Neovim CornelisEnv ()
questionToMeta :: Buffer -> Neovim CornelisEnv ()
questionToMeta Buffer
b = Buffer
-> (BufferStuff -> Neovim CornelisEnv ()) -> Neovim CornelisEnv ()
forall a.
Monoid a =>
Buffer
-> (BufferStuff -> Neovim CornelisEnv a) -> Neovim CornelisEnv a
withBufferStuff Buffer
b ((BufferStuff -> Neovim CornelisEnv ()) -> Neovim CornelisEnv ())
-> (BufferStuff -> Neovim CornelisEnv ()) -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ \BufferStuff
bs -> do
  let ips :: [InteractionPoint Identity]
ips = Map InteractionId (InteractionPoint Identity)
-> [InteractionPoint Identity]
forall a. Map InteractionId a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (Map InteractionId (InteractionPoint Identity)
 -> [InteractionPoint Identity])
-> Map InteractionId (InteractionPoint Identity)
-> [InteractionPoint Identity]
forall a b. (a -> b) -> a -> b
$ BufferStuff -> Map InteractionId (InteractionPoint Identity)
bs_ips BufferStuff
bs

  Any
res <- ([Any] -> Any)
-> Neovim CornelisEnv [Any] -> Neovim CornelisEnv Any
forall a b.
(a -> b) -> Neovim CornelisEnv a -> Neovim CornelisEnv b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Any] -> Any
forall m. Monoid m => [m] -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold (Neovim CornelisEnv [Any] -> Neovim CornelisEnv Any)
-> Neovim CornelisEnv [Any] -> Neovim CornelisEnv Any
forall a b. (a -> b) -> a -> b
$ [InteractionPoint Identity]
-> (InteractionPoint Identity -> Neovim CornelisEnv Any)
-> Neovim CornelisEnv [Any]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for ((InteractionPoint Identity -> Down AgdaPos)
-> [InteractionPoint Identity] -> [InteractionPoint Identity]
forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn (AgdaPos -> Down AgdaPos
forall a. a -> Down a
Down (AgdaPos -> Down AgdaPos)
-> (InteractionPoint Identity -> AgdaPos)
-> InteractionPoint Identity
-> Down AgdaPos
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AgdaInterval -> AgdaPos
forall p. Interval p -> p
iStart (AgdaInterval -> AgdaPos)
-> (InteractionPoint Identity -> AgdaInterval)
-> InteractionPoint Identity
-> AgdaPos
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InteractionPoint Identity -> AgdaInterval
ip_interval') [InteractionPoint Identity]
ips) ((InteractionPoint Identity -> Neovim CornelisEnv Any)
 -> Neovim CornelisEnv [Any])
-> (InteractionPoint Identity -> Neovim CornelisEnv Any)
-> Neovim CornelisEnv [Any]
forall a b. (a -> b) -> a -> b
$ \InteractionPoint Identity
ip -> do
    AgdaInterval
int <- Buffer
-> InteractionPoint Identity -> Neovim CornelisEnv AgdaInterval
getIpInterval Buffer
b InteractionPoint Identity
ip
    Buffer
-> InteractionPoint Identity -> Neovim CornelisEnv (Maybe Text)
getGoalContentsMaybe Buffer
b InteractionPoint Identity
ip Neovim CornelisEnv (Maybe Text)
-> (Maybe Text -> Neovim CornelisEnv Any) -> Neovim CornelisEnv Any
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
      -- We only don't have a goal contents if we are a ? goal
      Maybe Text
Nothing -> do
        Buffer -> AgdaInterval -> Text -> Neovim CornelisEnv ()
forall env. Buffer -> AgdaInterval -> Text -> Neovim env ()
replaceInterval Buffer
b AgdaInterval
int Text
"{! !}"
        let int' :: AgdaInterval
int' = AgdaInterval
int { iEnd = iStart int `addCol` Offset 5 }
        Neovim CornelisEnv (Maybe Extmark) -> Neovim CornelisEnv ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Neovim CornelisEnv (Maybe Extmark) -> Neovim CornelisEnv ())
-> Neovim CornelisEnv (Maybe Extmark) -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ Buffer
-> AgdaInterval
-> HighlightGroup
-> Neovim CornelisEnv (Maybe Extmark)
highlightInterval Buffer
b AgdaInterval
int' HighlightGroup
CornelisHole
        Buffer -> (BufferStuff -> BufferStuff) -> Neovim CornelisEnv ()
modifyBufferStuff Buffer
b ((BufferStuff -> BufferStuff) -> Neovim CornelisEnv ())
-> (BufferStuff -> BufferStuff) -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$
          #bs_ips %~ M.insert (ip_id ip) (ip & #ip_intervalM . #_Identity .~ int')

        Any -> Neovim CornelisEnv Any
forall a. a -> Neovim CornelisEnv a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Any -> Neovim CornelisEnv Any) -> Any -> Neovim CornelisEnv Any
forall a b. (a -> b) -> a -> b
$ Bool -> Any
Any Bool
True
      Just Text
_ -> Any -> Neovim CornelisEnv Any
forall a. a -> Neovim CornelisEnv a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Any -> Neovim CornelisEnv Any) -> Any -> Neovim CornelisEnv Any
forall a b. (a -> b) -> a -> b
$ Bool -> Any
Any Bool
False

  -- Force a save if we replaced any goals
  case Any -> Bool
getAny Any
res of
    Bool
True -> Neovim CornelisEnv ()
load
    Bool
False -> () -> Neovim CornelisEnv ()
forall a. a -> Neovim CornelisEnv a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()


doAllGoals :: CommandArguments -> Neovim CornelisEnv ()
doAllGoals :: CommandArguments -> Neovim CornelisEnv ()
doAllGoals = Neovim CornelisEnv () -> CommandArguments -> Neovim CornelisEnv ()
forall a b. a -> b -> a
const Neovim CornelisEnv ()
allGoals


allGoals :: Neovim CornelisEnv ()
allGoals :: Neovim CornelisEnv ()
allGoals =
  Neovim CornelisEnv () -> Neovim CornelisEnv ()
forall a. Neovim CornelisEnv a -> Neovim CornelisEnv a
withAgda (Neovim CornelisEnv () -> Neovim CornelisEnv ())
-> Neovim CornelisEnv () -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ (Buffer -> Neovim CornelisEnv ()) -> Neovim CornelisEnv ()
forall env a. (Buffer -> Neovim env a) -> Neovim env a
withCurrentBuffer ((Buffer -> Neovim CornelisEnv ()) -> Neovim CornelisEnv ())
-> (Buffer -> Neovim CornelisEnv ()) -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ \Buffer
b ->
    Buffer
-> (BufferStuff -> Neovim CornelisEnv ()) -> Neovim CornelisEnv ()
forall a.
Monoid a =>
Buffer
-> (BufferStuff -> Neovim CornelisEnv a) -> Neovim CornelisEnv a
withBufferStuff Buffer
b ((BufferStuff -> Neovim CornelisEnv ()) -> Neovim CornelisEnv ())
-> (BufferStuff -> Neovim CornelisEnv ()) -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ \BufferStuff
bs -> do
      Buffer -> DisplayInfo -> Neovim CornelisEnv ()
goalWindow Buffer
b (DisplayInfo -> Neovim CornelisEnv ())
-> DisplayInfo -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ BufferStuff -> DisplayInfo
bs_goals BufferStuff
bs


doRestart :: CommandArguments -> Neovim CornelisEnv ()
doRestart :: CommandArguments -> Neovim CornelisEnv ()
doRestart CommandArguments
_ = do
  Map Buffer BufferStuff
bs <- (CornelisState -> Map Buffer BufferStuff)
-> Neovim CornelisEnv (Map Buffer BufferStuff)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CornelisState -> Map Buffer BufferStuff
cs_buffers
  (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 -> CornelisState -> CornelisState
forall s t a b. ASetter s t a b -> b -> s -> t
.~ Map Buffer BufferStuff
forall a. Monoid a => a
mempty
  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
$ Map Buffer BufferStuff -> (BufferStuff -> IO ()) -> IO ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ Map Buffer BufferStuff
bs ((BufferStuff -> IO ()) -> IO ())
-> (BufferStuff -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ ProcessHandle -> IO ()
terminateProcess (ProcessHandle -> IO ())
-> (BufferStuff -> ProcessHandle) -> BufferStuff -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Agda -> ProcessHandle
a_hdl (Agda -> ProcessHandle)
-> (BufferStuff -> Agda) -> BufferStuff -> ProcessHandle
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BufferStuff -> Agda
bs_agda_proc

doAbort :: CommandArguments -> Neovim CornelisEnv ()
doAbort :: CommandArguments -> Neovim CornelisEnv ()
doAbort CommandArguments
_ = Neovim CornelisEnv () -> Neovim CornelisEnv ()
forall a. Neovim CornelisEnv a -> Neovim CornelisEnv a
withAgda (Neovim CornelisEnv () -> Neovim CornelisEnv ())
-> Neovim CornelisEnv () -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ (Buffer -> Neovim CornelisEnv ()) -> Neovim CornelisEnv ()
forall env a. (Buffer -> Neovim env a) -> Neovim env a
withCurrentBuffer ((Buffer -> Neovim CornelisEnv ()) -> Neovim CornelisEnv ())
-> (Buffer -> Neovim CornelisEnv ()) -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ Buffer -> Neovim CornelisEnv Agda
getAgda (Buffer -> Neovim CornelisEnv Agda)
-> (Agda -> Neovim CornelisEnv ())
-> Buffer
-> Neovim CornelisEnv ()
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Interaction -> Agda -> Neovim CornelisEnv ()
forall env. Interaction -> Agda -> Neovim env ()
runIOTCM Interaction
forall range. Interaction' range
Cmd_abort

normalizationMode :: Neovim env Rewrite
normalizationMode :: forall env. Neovim env Rewrite
normalizationMode = Rewrite -> Neovim env Rewrite
forall a. a -> Neovim env a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Rewrite
HeadNormal

computeMode :: Neovim env ComputeMode
computeMode :: forall env. Neovim env ComputeMode
computeMode = ComputeMode -> Neovim env ComputeMode
forall a. a -> Neovim env a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ComputeMode
DefaultCompute

solveOne :: CommandArguments -> Maybe String -> Neovim CornelisEnv ()
solveOne :: CommandArguments -> Maybe String -> Neovim CornelisEnv ()
solveOne CommandArguments
_ Maybe String
ms = Maybe String
-> (Rewrite -> Neovim CornelisEnv ()) -> Neovim CornelisEnv ()
forall e. Maybe String -> (Rewrite -> Neovim e ()) -> Neovim e ()
withNormalizationMode Maybe String
ms ((Rewrite -> Neovim CornelisEnv ()) -> Neovim CornelisEnv ())
-> (Rewrite -> Neovim CornelisEnv ()) -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ \Rewrite
mode ->
  Neovim CornelisEnv () -> Neovim CornelisEnv ()
forall a. Neovim CornelisEnv a -> Neovim CornelisEnv a
withAgda (Neovim CornelisEnv () -> Neovim CornelisEnv ())
-> Neovim CornelisEnv () -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ Neovim CornelisEnv (Maybe ()) -> Neovim CornelisEnv ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Neovim CornelisEnv (Maybe ()) -> Neovim CornelisEnv ())
-> Neovim CornelisEnv (Maybe ()) -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ (Buffer -> InteractionPoint Identity -> Neovim CornelisEnv ())
-> Neovim CornelisEnv (Maybe ())
forall a.
(Buffer -> InteractionPoint Identity -> Neovim CornelisEnv a)
-> Neovim CornelisEnv (Maybe a)
withGoalAtCursor ((Buffer -> InteractionPoint Identity -> Neovim CornelisEnv ())
 -> Neovim CornelisEnv (Maybe ()))
-> (Buffer -> InteractionPoint Identity -> Neovim CornelisEnv ())
-> Neovim CornelisEnv (Maybe ())
forall a b. (a -> b) -> a -> b
$ \Buffer
b InteractionPoint Identity
ip -> do
    Agda
agda <- Buffer -> Neovim CornelisEnv Agda
getAgda Buffer
b
    Text
fp <- Buffer -> Neovim CornelisEnv Text
forall env. Buffer -> Neovim env Text
buffer_get_name Buffer
b
    (Interaction -> Agda -> Neovim CornelisEnv ())
-> Agda -> Interaction -> Neovim CornelisEnv ()
forall a b c. (a -> b -> c) -> b -> a -> c
flip Interaction -> Agda -> Neovim CornelisEnv ()
forall env. Interaction -> Agda -> Neovim env ()
runIOTCM Agda
agda (Interaction -> Neovim CornelisEnv ())
-> Interaction -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$
      Rewrite -> InteractionId -> Range -> String -> Interaction
forall range.
Rewrite -> InteractionId -> range -> String -> Interaction' range
Cmd_solveOne
        Rewrite
mode
        (InteractionPoint Identity -> InteractionId
forall (f :: * -> *). InteractionPoint f -> InteractionId
ip_id InteractionPoint Identity
ip)
        (Text -> AgdaInterval -> Range
mkAbsPathRnage Text
fp (AgdaInterval -> Range) -> AgdaInterval -> Range
forall a b. (a -> b) -> a -> b
$ InteractionPoint Identity -> AgdaInterval
ip_interval' InteractionPoint Identity
ip)
        String
""

autoOne :: CommandArguments -> Neovim CornelisEnv ()
autoOne :: CommandArguments -> Neovim CornelisEnv ()
autoOne CommandArguments
_ = Neovim CornelisEnv () -> Neovim CornelisEnv ()
forall a. Neovim CornelisEnv a -> Neovim CornelisEnv a
withAgda (Neovim CornelisEnv () -> Neovim CornelisEnv ())
-> Neovim CornelisEnv () -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ Neovim CornelisEnv (Maybe ()) -> Neovim CornelisEnv ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Neovim CornelisEnv (Maybe ()) -> Neovim CornelisEnv ())
-> Neovim CornelisEnv (Maybe ()) -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ (Buffer -> InteractionPoint Identity -> Neovim CornelisEnv ())
-> Neovim CornelisEnv (Maybe ())
forall a.
(Buffer -> InteractionPoint Identity -> Neovim CornelisEnv a)
-> Neovim CornelisEnv (Maybe a)
withGoalAtCursor ((Buffer -> InteractionPoint Identity -> Neovim CornelisEnv ())
 -> Neovim CornelisEnv (Maybe ()))
-> (Buffer -> InteractionPoint Identity -> Neovim CornelisEnv ())
-> Neovim CornelisEnv (Maybe ())
forall a b. (a -> b) -> a -> b
$ \Buffer
b InteractionPoint Identity
ip -> do
  Agda
agda <- Buffer -> Neovim CornelisEnv Agda
getAgda Buffer
b
  Text
t <- Buffer -> InteractionPoint Identity -> Neovim CornelisEnv Text
getGoalContents Buffer
b InteractionPoint Identity
ip
  Text
fp <- Buffer -> Neovim CornelisEnv Text
forall env. Buffer -> Neovim env Text
buffer_get_name Buffer
b
  (Interaction -> Agda -> Neovim CornelisEnv ())
-> Agda -> Interaction -> Neovim CornelisEnv ()
forall a b c. (a -> b -> c) -> b -> a -> c
flip Interaction -> Agda -> Neovim CornelisEnv ()
forall env. Interaction -> Agda -> Neovim env ()
runIOTCM Agda
agda (Interaction -> Neovim CornelisEnv ())
-> Interaction -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$
    InteractionId -> Range -> String -> Interaction
forall range.
InteractionId -> range -> String -> Interaction' range
Cmd_autoOne
      (InteractionPoint Identity -> InteractionId
forall (f :: * -> *). InteractionPoint f -> InteractionId
ip_id InteractionPoint Identity
ip)
      (Text -> AgdaInterval -> Range
mkAbsPathRnage Text
fp (AgdaInterval -> Range) -> AgdaInterval -> Range
forall a b. (a -> b) -> a -> b
$ InteractionPoint Identity -> AgdaInterval
ip_interval' InteractionPoint Identity
ip)
      (Text -> String
T.unpack Text
t)

withNormalizationMode :: Maybe String -> (Rewrite -> Neovim e ()) -> Neovim e ()
withNormalizationMode :: forall e. Maybe String -> (Rewrite -> Neovim e ()) -> Neovim e ()
withNormalizationMode Maybe String
Nothing Rewrite -> Neovim e ()
f = Neovim e Rewrite
forall env. Neovim env Rewrite
normalizationMode Neovim e Rewrite -> (Rewrite -> Neovim e ()) -> Neovim e ()
forall a b. Neovim e a -> (a -> Neovim e b) -> Neovim e b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Rewrite -> Neovim e ()
f
withNormalizationMode (Just String
s) Rewrite -> Neovim e ()
f =
  case String -> Maybe Rewrite
forall a. Read a => String -> Maybe a
readMaybe String
s of
    Maybe Rewrite
Nothing -> Text -> Neovim e ()
forall env. Text -> Neovim env ()
reportError (Text -> Neovim e ()) -> Text -> Neovim e ()
forall a b. (a -> b) -> a -> b
$ Text
"Invalid normalization mode: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack String
s
    Just Rewrite
nm -> Rewrite -> Neovim e ()
f Rewrite
nm

withComputeMode :: Maybe String -> (ComputeMode -> Neovim e ()) -> Neovim e ()
withComputeMode :: forall e.
Maybe String -> (ComputeMode -> Neovim e ()) -> Neovim e ()
withComputeMode Maybe String
Nothing ComputeMode -> Neovim e ()
f = Neovim e ComputeMode
forall env. Neovim env ComputeMode
computeMode Neovim e ComputeMode -> (ComputeMode -> Neovim e ()) -> Neovim e ()
forall a b. Neovim e a -> (a -> Neovim e b) -> Neovim e b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= ComputeMode -> Neovim e ()
f
withComputeMode (Just String
s) ComputeMode -> Neovim e ()
f =
  case String -> Maybe ComputeMode
forall a. Read a => String -> Maybe a
readMaybe String
s of
    Maybe ComputeMode
Nothing -> Text -> Neovim e ()
forall env. Text -> Neovim env ()
reportError (Text -> Neovim e ()) -> Text -> Neovim e ()
forall a b. (a -> b) -> a -> b
$ Text
"Invalid compute mode: "
      Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack String
s
      Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
", expected one of "
      Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack ([ComputeMode] -> String
forall a. Show a => a -> String
show [(ComputeMode
forall a. Bounded a => a
minBound :: ComputeMode) .. ])
    (Just ComputeMode
cm) -> ComputeMode -> Neovim e ()
f ComputeMode
cm

typeContext :: CommandArguments -> Maybe String -> Neovim CornelisEnv ()
typeContext :: CommandArguments -> Maybe String -> Neovim CornelisEnv ()
typeContext CommandArguments
_ Maybe String
ms = Maybe String
-> (Rewrite -> Neovim CornelisEnv ()) -> Neovim CornelisEnv ()
forall e. Maybe String -> (Rewrite -> Neovim e ()) -> Neovim e ()
withNormalizationMode Maybe String
ms ((Rewrite -> Neovim CornelisEnv ()) -> Neovim CornelisEnv ())
-> (Rewrite -> Neovim CornelisEnv ()) -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ \Rewrite
mode ->
  Neovim CornelisEnv () -> Neovim CornelisEnv ()
forall a. Neovim CornelisEnv a -> Neovim CornelisEnv a
withAgda (Neovim CornelisEnv () -> Neovim CornelisEnv ())
-> Neovim CornelisEnv () -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ Neovim CornelisEnv (Maybe ()) -> Neovim CornelisEnv ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Neovim CornelisEnv (Maybe ()) -> Neovim CornelisEnv ())
-> Neovim CornelisEnv (Maybe ()) -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ (Buffer -> InteractionPoint Identity -> Neovim CornelisEnv ())
-> Neovim CornelisEnv (Maybe ())
forall a.
(Buffer -> InteractionPoint Identity -> Neovim CornelisEnv a)
-> Neovim CornelisEnv (Maybe a)
withGoalAtCursor ((Buffer -> InteractionPoint Identity -> Neovim CornelisEnv ())
 -> Neovim CornelisEnv (Maybe ()))
-> (Buffer -> InteractionPoint Identity -> Neovim CornelisEnv ())
-> Neovim CornelisEnv (Maybe ())
forall a b. (a -> b) -> a -> b
$ \Buffer
b InteractionPoint Identity
goal -> do
    Agda
agda <- Buffer -> Neovim CornelisEnv Agda
getAgda Buffer
b
    Text
fp <- Buffer -> Neovim CornelisEnv Text
forall env. Buffer -> Neovim env Text
buffer_get_name Buffer
b
    (Interaction -> Agda -> Neovim CornelisEnv ())
-> Agda -> Interaction -> Neovim CornelisEnv ()
forall a b c. (a -> b -> c) -> b -> a -> c
flip Interaction -> Agda -> Neovim CornelisEnv ()
forall env. Interaction -> Agda -> Neovim env ()
runIOTCM Agda
agda (Interaction -> Neovim CornelisEnv ())
-> Interaction -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$
      Rewrite -> InteractionId -> Range -> String -> Interaction
forall range.
Rewrite -> InteractionId -> range -> String -> Interaction' range
Cmd_goal_type_context
        Rewrite
mode
        (InteractionPoint Identity -> InteractionId
forall (f :: * -> *). InteractionPoint f -> InteractionId
ip_id InteractionPoint Identity
goal)
        (Text -> AgdaInterval -> Range
mkAbsPathRnage Text
fp (AgdaInterval -> Range) -> AgdaInterval -> Range
forall a b. (a -> b) -> a -> b
$ InteractionPoint Identity -> AgdaInterval
ip_interval' InteractionPoint Identity
goal)
        String
""

typeContextInfer :: CommandArguments -> Maybe String -> Neovim CornelisEnv ()
typeContextInfer :: CommandArguments -> Maybe String -> Neovim CornelisEnv ()
typeContextInfer CommandArguments
_ Maybe String
ms = Maybe String
-> (Rewrite -> Neovim CornelisEnv ()) -> Neovim CornelisEnv ()
forall e. Maybe String -> (Rewrite -> Neovim e ()) -> Neovim e ()
withNormalizationMode Maybe String
ms ((Rewrite -> Neovim CornelisEnv ()) -> Neovim CornelisEnv ())
-> (Rewrite -> Neovim CornelisEnv ()) -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ \Rewrite
mode ->
  Neovim CornelisEnv () -> Neovim CornelisEnv ()
forall a. Neovim CornelisEnv a -> Neovim CornelisEnv a
withAgda (Neovim CornelisEnv () -> Neovim CornelisEnv ())
-> Neovim CornelisEnv () -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ Neovim CornelisEnv (Maybe ()) -> Neovim CornelisEnv ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Neovim CornelisEnv (Maybe ()) -> Neovim CornelisEnv ())
-> Neovim CornelisEnv (Maybe ()) -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ (Buffer -> InteractionPoint Identity -> Neovim CornelisEnv ())
-> Neovim CornelisEnv (Maybe ())
forall a.
(Buffer -> InteractionPoint Identity -> Neovim CornelisEnv a)
-> Neovim CornelisEnv (Maybe a)
withGoalAtCursor ((Buffer -> InteractionPoint Identity -> Neovim CornelisEnv ())
 -> Neovim CornelisEnv (Maybe ()))
-> (Buffer -> InteractionPoint Identity -> Neovim CornelisEnv ())
-> Neovim CornelisEnv (Maybe ())
forall a b. (a -> b) -> a -> b
$ \Buffer
b InteractionPoint Identity
ip -> do
    Agda
agda <- Buffer -> Neovim CornelisEnv Agda
getAgda Buffer
b
    Text
fp <- Buffer -> Neovim CornelisEnv Text
forall env. Buffer -> Neovim env Text
buffer_get_name Buffer
b
    Text
contents <- Buffer -> InteractionPoint Identity -> Neovim CornelisEnv Text
getGoalContents Buffer
b InteractionPoint Identity
ip
    (Interaction -> Agda -> Neovim CornelisEnv ())
-> Agda -> Interaction -> Neovim CornelisEnv ()
forall a b c. (a -> b -> c) -> b -> a -> c
flip Interaction -> Agda -> Neovim CornelisEnv ()
forall env. Interaction -> Agda -> Neovim env ()
runIOTCM Agda
agda
      (Interaction -> Neovim CornelisEnv ())
-> Interaction -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ Rewrite -> InteractionId -> Range -> String -> Interaction
forall range.
Rewrite -> InteractionId -> range -> String -> Interaction' range
Cmd_goal_type_context_infer
          Rewrite
mode
          (InteractionPoint Identity -> InteractionId
forall (f :: * -> *). InteractionPoint f -> InteractionId
ip_id InteractionPoint Identity
ip)
          (Text -> AgdaInterval -> Range
mkAbsPathRnage Text
fp (AgdaInterval -> Range) -> AgdaInterval -> Range
forall a b. (a -> b) -> a -> b
$ InteractionPoint Identity -> AgdaInterval
ip_interval' InteractionPoint Identity
ip)
      (String -> Interaction) -> String -> Interaction
forall a b. (a -> b) -> a -> b
$ Text -> String
T.unpack Text
contents

doRefine :: CommandArguments -> Neovim CornelisEnv ()
doRefine :: CommandArguments -> Neovim CornelisEnv ()
doRefine = Neovim CornelisEnv () -> CommandArguments -> Neovim CornelisEnv ()
forall a b. a -> b -> a
const Neovim CornelisEnv ()
refine

refine :: Neovim CornelisEnv ()
refine :: Neovim CornelisEnv ()
refine = Neovim CornelisEnv () -> Neovim CornelisEnv ()
forall a. Neovim CornelisEnv a -> Neovim CornelisEnv a
withAgda (Neovim CornelisEnv () -> Neovim CornelisEnv ())
-> Neovim CornelisEnv () -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ Neovim CornelisEnv (Maybe ()) -> Neovim CornelisEnv ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Neovim CornelisEnv (Maybe ()) -> Neovim CornelisEnv ())
-> Neovim CornelisEnv (Maybe ()) -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ (Buffer -> InteractionPoint Identity -> Neovim CornelisEnv ())
-> Neovim CornelisEnv (Maybe ())
forall a.
(Buffer -> InteractionPoint Identity -> Neovim CornelisEnv a)
-> Neovim CornelisEnv (Maybe a)
withGoalAtCursor ((Buffer -> InteractionPoint Identity -> Neovim CornelisEnv ())
 -> Neovim CornelisEnv (Maybe ()))
-> (Buffer -> InteractionPoint Identity -> Neovim CornelisEnv ())
-> Neovim CornelisEnv (Maybe ())
forall a b. (a -> b) -> a -> b
$ \Buffer
b InteractionPoint Identity
ip -> do
  Agda
agda <- Buffer -> Neovim CornelisEnv Agda
getAgda Buffer
b
  Text
t <- Buffer -> InteractionPoint Identity -> Neovim CornelisEnv Text
getGoalContents Buffer
b InteractionPoint Identity
ip
  (Interaction -> Agda -> Neovim CornelisEnv ())
-> Agda -> Interaction -> Neovim CornelisEnv ()
forall a b c. (a -> b -> c) -> b -> a -> c
flip Interaction -> Agda -> Neovim CornelisEnv ()
forall env. Interaction -> Agda -> Neovim env ()
runIOTCM Agda
agda
    (Interaction -> Neovim CornelisEnv ())
-> Interaction -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ Bool -> InteractionId -> Range -> String -> Interaction
forall range.
Bool -> InteractionId -> range -> String -> Interaction' range
Cmd_refine_or_intro
        Bool
True
        (InteractionPoint Identity -> InteractionId
forall (f :: * -> *). InteractionPoint f -> InteractionId
ip_id InteractionPoint Identity
ip)
        -- We intentionally don't pass the range here; since doing so changes
        -- the response from Agda and requires a different codepath to perform
        -- the necessary edits.
        Range
forall a. Range' a
noRange
    (String -> Interaction) -> String -> Interaction
forall a b. (a -> b) -> a -> b
$ Text -> String
T.unpack Text
t

doGive :: CommandArguments -> Neovim CornelisEnv ()
doGive :: CommandArguments -> Neovim CornelisEnv ()
doGive = Neovim CornelisEnv () -> CommandArguments -> Neovim CornelisEnv ()
forall a b. a -> b -> a
const Neovim CornelisEnv ()
give

give :: Neovim CornelisEnv ()
give :: Neovim CornelisEnv ()
give = Neovim CornelisEnv () -> Neovim CornelisEnv ()
forall a. Neovim CornelisEnv a -> Neovim CornelisEnv a
withAgda (Neovim CornelisEnv () -> Neovim CornelisEnv ())
-> Neovim CornelisEnv () -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ Neovim CornelisEnv (Maybe ()) -> Neovim CornelisEnv ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Neovim CornelisEnv (Maybe ()) -> Neovim CornelisEnv ())
-> Neovim CornelisEnv (Maybe ()) -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ (Buffer -> InteractionPoint Identity -> Neovim CornelisEnv ())
-> Neovim CornelisEnv (Maybe ())
forall a.
(Buffer -> InteractionPoint Identity -> Neovim CornelisEnv a)
-> Neovim CornelisEnv (Maybe a)
withGoalAtCursor ((Buffer -> InteractionPoint Identity -> Neovim CornelisEnv ())
 -> Neovim CornelisEnv (Maybe ()))
-> (Buffer -> InteractionPoint Identity -> Neovim CornelisEnv ())
-> Neovim CornelisEnv (Maybe ())
forall a b. (a -> b) -> a -> b
$ \Buffer
b InteractionPoint Identity
ip -> do
  Agda
agda <- Buffer -> Neovim CornelisEnv Agda
getAgda Buffer
b
  Text
t <- Buffer -> InteractionPoint Identity -> Neovim CornelisEnv Text
getGoalContents Buffer
b InteractionPoint Identity
ip
  (Interaction -> Agda -> Neovim CornelisEnv ())
-> Agda -> Interaction -> Neovim CornelisEnv ()
forall a b c. (a -> b -> c) -> b -> a -> c
flip Interaction -> Agda -> Neovim CornelisEnv ()
forall env. Interaction -> Agda -> Neovim env ()
runIOTCM Agda
agda
    (Interaction -> Neovim CornelisEnv ())
-> Interaction -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ UseForce -> InteractionId -> Range -> String -> Interaction
forall range.
UseForce -> InteractionId -> range -> String -> Interaction' range
Cmd_give
        UseForce
WithoutForce
        (InteractionPoint Identity -> InteractionId
forall (f :: * -> *). InteractionPoint f -> InteractionId
ip_id InteractionPoint Identity
ip)
        -- We intentionally don't pass the range here; since doing so changes
        -- the response from Agda and requires a different codepath to perform
        -- the necessary edits.
        Range
forall a. Range' a
noRange
    (String -> Interaction) -> String -> Interaction
forall a b. (a -> b) -> a -> b
$ Text -> String
T.unpack Text
t

doElaborate :: CommandArguments -> Maybe String-> Neovim CornelisEnv ()
doElaborate :: CommandArguments -> Maybe String -> Neovim CornelisEnv ()
doElaborate CommandArguments
_ Maybe String
ms = Maybe String
-> (Rewrite -> Neovim CornelisEnv ()) -> Neovim CornelisEnv ()
forall e. Maybe String -> (Rewrite -> Neovim e ()) -> Neovim e ()
withNormalizationMode Maybe String
ms Rewrite -> Neovim CornelisEnv ()
elaborate

elaborate :: Rewrite -> Neovim CornelisEnv ()
elaborate :: Rewrite -> Neovim CornelisEnv ()
elaborate Rewrite
mode = Neovim CornelisEnv () -> Neovim CornelisEnv ()
forall a. Neovim CornelisEnv a -> Neovim CornelisEnv a
withAgda (Neovim CornelisEnv () -> Neovim CornelisEnv ())
-> Neovim CornelisEnv () -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ Neovim CornelisEnv (Maybe ()) -> Neovim CornelisEnv ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Neovim CornelisEnv (Maybe ()) -> Neovim CornelisEnv ())
-> Neovim CornelisEnv (Maybe ()) -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ (Buffer -> InteractionPoint Identity -> Neovim CornelisEnv ())
-> Neovim CornelisEnv (Maybe ())
forall a.
(Buffer -> InteractionPoint Identity -> Neovim CornelisEnv a)
-> Neovim CornelisEnv (Maybe a)
withGoalAtCursor ((Buffer -> InteractionPoint Identity -> Neovim CornelisEnv ())
 -> Neovim CornelisEnv (Maybe ()))
-> (Buffer -> InteractionPoint Identity -> Neovim CornelisEnv ())
-> Neovim CornelisEnv (Maybe ())
forall a b. (a -> b) -> a -> b
$ \Buffer
b InteractionPoint Identity
ip -> do
  Agda
agda <- Buffer -> Neovim CornelisEnv Agda
getAgda Buffer
b
  Text
fp <- Buffer -> Neovim CornelisEnv Text
forall env. Buffer -> Neovim env Text
buffer_get_name Buffer
b
  Text
t <- Buffer -> InteractionPoint Identity -> Neovim CornelisEnv Text
getGoalContents Buffer
b InteractionPoint Identity
ip
  (Interaction -> Agda -> Neovim CornelisEnv ())
-> Agda -> Interaction -> Neovim CornelisEnv ()
forall a b c. (a -> b -> c) -> b -> a -> c
flip Interaction -> Agda -> Neovim CornelisEnv ()
forall env. Interaction -> Agda -> Neovim env ()
runIOTCM Agda
agda
    (Interaction -> Neovim CornelisEnv ())
-> Interaction -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ Rewrite -> InteractionId -> Range -> String -> Interaction
forall range.
Rewrite -> InteractionId -> range -> String -> Interaction' range
Cmd_elaborate_give
        Rewrite
mode
        (InteractionPoint Identity -> InteractionId
forall (f :: * -> *). InteractionPoint f -> InteractionId
ip_id InteractionPoint Identity
ip)
        (Text -> AgdaInterval -> Range
mkAbsPathRnage Text
fp (AgdaInterval -> Range) -> AgdaInterval -> Range
forall a b. (a -> b) -> a -> b
$ InteractionPoint Identity -> AgdaInterval
ip_interval' InteractionPoint Identity
ip)
    (String -> Interaction) -> String -> Interaction
forall a b. (a -> b) -> a -> b
$ Text -> String
T.unpack Text
t

doTypeInfer :: CommandArguments -> Maybe String -> Neovim CornelisEnv ()
doTypeInfer :: CommandArguments -> Maybe String -> Neovim CornelisEnv ()
doTypeInfer CommandArguments
_ Maybe String
ms = Maybe String
-> (Rewrite -> Neovim CornelisEnv ()) -> Neovim CornelisEnv ()
forall e. Maybe String -> (Rewrite -> Neovim e ()) -> Neovim e ()
withNormalizationMode Maybe String
ms Rewrite -> Neovim CornelisEnv ()
inferType

inferType :: Rewrite -> Neovim CornelisEnv ()
inferType :: Rewrite -> Neovim CornelisEnv ()
inferType Rewrite
mode = Neovim CornelisEnv () -> Neovim CornelisEnv ()
forall a. Neovim CornelisEnv a -> Neovim CornelisEnv a
withAgda (Neovim CornelisEnv () -> Neovim CornelisEnv ())
-> Neovim CornelisEnv () -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ do
    Interaction
cmd <- String
-> (InteractionPoint Identity
    -> String -> Neovim CornelisEnv Interaction)
-> (String -> Neovim CornelisEnv Interaction)
-> Neovim CornelisEnv Interaction
forall a.
String
-> (InteractionPoint Identity -> String -> Neovim CornelisEnv a)
-> (String -> Neovim CornelisEnv a)
-> Neovim CornelisEnv a
withGoalContentsOrPrompt String
"Infer type of what?"
        (\InteractionPoint Identity
goal -> Interaction -> Neovim CornelisEnv Interaction
forall a. a -> Neovim CornelisEnv a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Interaction -> Neovim CornelisEnv Interaction)
-> (String -> Interaction)
-> String
-> Neovim CornelisEnv Interaction
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rewrite -> InteractionId -> Range -> String -> Interaction
forall range.
Rewrite -> InteractionId -> range -> String -> Interaction' range
Cmd_infer Rewrite
mode (InteractionPoint Identity -> InteractionId
forall (f :: * -> *). InteractionPoint f -> InteractionId
ip_id InteractionPoint Identity
goal) Range
forall a. Range' a
NoRange)
        (Interaction -> Neovim CornelisEnv Interaction
forall a. a -> Neovim CornelisEnv a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Interaction -> Neovim CornelisEnv Interaction)
-> (String -> Interaction)
-> String
-> Neovim CornelisEnv Interaction
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rewrite -> String -> Interaction
forall range. Rewrite -> String -> Interaction' range
Cmd_infer_toplevel Rewrite
mode)
    Interaction -> Neovim CornelisEnv ()
runInteraction Interaction
cmd


doWhyInScope :: CommandArguments -> Neovim CornelisEnv ()
doWhyInScope :: CommandArguments -> Neovim CornelisEnv ()
doWhyInScope CommandArguments
_ = do
  Text
thing <- String -> Maybe String -> Maybe String -> Neovim CornelisEnv Text
forall result env.
NvimObject result =>
String -> Maybe String -> Maybe String -> Neovim env result
input String
"Why is what in scope? " Maybe String
forall a. Maybe a
Nothing Maybe String
forall a. Maybe a
Nothing
  Text -> Neovim CornelisEnv ()
whyInScope Text
thing

whyInScope :: Text -> Neovim CornelisEnv ()
whyInScope :: Text -> Neovim CornelisEnv ()
whyInScope Text
thing = do
  Neovim CornelisEnv () -> Neovim CornelisEnv ()
forall a. Neovim CornelisEnv a -> Neovim CornelisEnv a
withAgda (Neovim CornelisEnv () -> Neovim CornelisEnv ())
-> Neovim CornelisEnv () -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ Neovim CornelisEnv () -> Neovim CornelisEnv ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Neovim CornelisEnv () -> Neovim CornelisEnv ())
-> Neovim CornelisEnv () -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ (Buffer -> Neovim CornelisEnv ()) -> Neovim CornelisEnv ()
forall env a. (Buffer -> Neovim env a) -> Neovim env a
withCurrentBuffer ((Buffer -> Neovim CornelisEnv ()) -> Neovim CornelisEnv ())
-> (Buffer -> Neovim CornelisEnv ()) -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ \Buffer
b -> do
    Agda
agda <- Buffer -> Neovim CornelisEnv Agda
getAgda Buffer
b
    (Interaction -> Agda -> Neovim CornelisEnv ())
-> Agda -> Interaction -> Neovim CornelisEnv ()
forall a b c. (a -> b -> c) -> b -> a -> c
flip Interaction -> Agda -> Neovim CornelisEnv ()
forall env. Interaction -> Agda -> Neovim env ()
runIOTCM Agda
agda (Interaction -> Neovim CornelisEnv ())
-> Interaction -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ String -> Interaction
forall range. String -> Interaction' range
Cmd_why_in_scope_toplevel (String -> Interaction) -> String -> Interaction
forall a b. (a -> b) -> a -> b
$ Text -> String
T.unpack Text
thing

doNormalize :: CommandArguments -> Maybe String -> Neovim CornelisEnv ()
doNormalize :: CommandArguments -> Maybe String -> Neovim CornelisEnv ()
doNormalize CommandArguments
_ Maybe String
ms = Maybe String
-> (ComputeMode -> Neovim CornelisEnv ()) -> Neovim CornelisEnv ()
forall e.
Maybe String -> (ComputeMode -> Neovim e ()) -> Neovim e ()
withComputeMode Maybe String
ms ((ComputeMode -> Neovim CornelisEnv ()) -> Neovim CornelisEnv ())
-> (ComputeMode -> Neovim CornelisEnv ()) -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ \ComputeMode
mode ->
  Neovim CornelisEnv () -> Neovim CornelisEnv ()
forall a. Neovim CornelisEnv a -> Neovim CornelisEnv a
withAgda (Neovim CornelisEnv () -> Neovim CornelisEnv ())
-> Neovim CornelisEnv () -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ Neovim CornelisEnv () -> Neovim CornelisEnv ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Neovim CornelisEnv () -> Neovim CornelisEnv ())
-> Neovim CornelisEnv () -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ do
    (Buffer
b , Maybe (InteractionPoint Identity)
goal) <- Neovim CornelisEnv (Buffer, Maybe (InteractionPoint Identity))
getGoalAtCursor
    Agda
agda <- Buffer -> Neovim CornelisEnv Agda
getAgda Buffer
b
    Text
fp <- Buffer -> Neovim CornelisEnv Text
forall env. Buffer -> Neovim env Text
buffer_get_name Buffer
b
    case Maybe (InteractionPoint Identity)
goal of
        Maybe (InteractionPoint Identity)
Nothing -> do
            String
thing <- String -> Maybe String -> Maybe String -> Neovim CornelisEnv String
forall result env.
NvimObject result =>
String -> Maybe String -> Maybe String -> Neovim env result
input String
"Normalize what? " Maybe String
forall a. Maybe a
Nothing Maybe String
forall a. Maybe a
Nothing
            (Interaction -> Agda -> Neovim CornelisEnv ())
-> Agda -> Interaction -> Neovim CornelisEnv ()
forall a b c. (a -> b -> c) -> b -> a -> c
flip Interaction -> Agda -> Neovim CornelisEnv ()
forall env. Interaction -> Agda -> Neovim env ()
runIOTCM Agda
agda (Interaction -> Neovim CornelisEnv ())
-> Interaction -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ ComputeMode -> String -> Interaction
forall range. ComputeMode -> String -> Interaction' range
Cmd_compute_toplevel ComputeMode
mode String
thing
        Just InteractionPoint Identity
ip -> do
            Text
t <- Buffer -> InteractionPoint Identity -> Neovim CornelisEnv Text
getGoalContents Buffer
b InteractionPoint Identity
ip
            (Interaction -> Agda -> Neovim CornelisEnv ())
-> Agda -> Interaction -> Neovim CornelisEnv ()
forall a b c. (a -> b -> c) -> b -> a -> c
flip Interaction -> Agda -> Neovim CornelisEnv ()
forall env. Interaction -> Agda -> Neovim env ()
runIOTCM Agda
agda
              (Interaction -> Neovim CornelisEnv ())
-> Interaction -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ ComputeMode -> InteractionId -> Range -> String -> Interaction
forall range.
ComputeMode
-> InteractionId -> range -> String -> Interaction' range
Cmd_compute
                  ComputeMode
mode
                  (InteractionPoint Identity -> InteractionId
forall (f :: * -> *). InteractionPoint f -> InteractionId
ip_id InteractionPoint Identity
ip)
                  (Text -> AgdaInterval -> Range
mkAbsPathRnage Text
fp (AgdaInterval -> Range) -> AgdaInterval -> Range
forall a b. (a -> b) -> a -> b
$ InteractionPoint Identity -> AgdaInterval
ip_interval' InteractionPoint Identity
ip)
              (String -> Interaction) -> String -> Interaction
forall a b. (a -> b) -> a -> b
$ Text -> String
T.unpack Text
t

helperFunc :: Rewrite -> Text -> Neovim CornelisEnv ()
helperFunc :: Rewrite -> Text -> Neovim CornelisEnv ()
helperFunc Rewrite
mode Text
expr = do
  Neovim CornelisEnv () -> Neovim CornelisEnv ()
forall a. Neovim CornelisEnv a -> Neovim CornelisEnv a
withAgda (Neovim CornelisEnv () -> Neovim CornelisEnv ())
-> Neovim CornelisEnv () -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ Neovim CornelisEnv (Maybe ()) -> Neovim CornelisEnv ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Neovim CornelisEnv (Maybe ()) -> Neovim CornelisEnv ())
-> Neovim CornelisEnv (Maybe ()) -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ (Buffer -> InteractionPoint Identity -> Neovim CornelisEnv ())
-> Neovim CornelisEnv (Maybe ())
forall a.
(Buffer -> InteractionPoint Identity -> Neovim CornelisEnv a)
-> Neovim CornelisEnv (Maybe a)
withGoalAtCursor ((Buffer -> InteractionPoint Identity -> Neovim CornelisEnv ())
 -> Neovim CornelisEnv (Maybe ()))
-> (Buffer -> InteractionPoint Identity -> Neovim CornelisEnv ())
-> Neovim CornelisEnv (Maybe ())
forall a b. (a -> b) -> a -> b
$ \Buffer
b InteractionPoint Identity
ip -> do
    Agda
agda <- Buffer -> Neovim CornelisEnv Agda
getAgda Buffer
b
    Text
fp <- Buffer -> Neovim CornelisEnv Text
forall env. Buffer -> Neovim env Text
buffer_get_name Buffer
b
    (Interaction -> Agda -> Neovim CornelisEnv ())
-> Agda -> Interaction -> Neovim CornelisEnv ()
forall a b c. (a -> b -> c) -> b -> a -> c
flip Interaction -> Agda -> Neovim CornelisEnv ()
forall env. Interaction -> Agda -> Neovim env ()
runIOTCM Agda
agda
      (Interaction -> Neovim CornelisEnv ())
-> Interaction -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ Rewrite -> InteractionId -> Range -> String -> Interaction
forall range.
Rewrite -> InteractionId -> range -> String -> Interaction' range
Cmd_helper_function
          Rewrite
mode
          (InteractionPoint Identity -> InteractionId
forall (f :: * -> *). InteractionPoint f -> InteractionId
ip_id InteractionPoint Identity
ip)
          (Text -> AgdaInterval -> Range
mkAbsPathRnage Text
fp (AgdaInterval -> Range) -> AgdaInterval -> Range
forall a b. (a -> b) -> a -> b
$ InteractionPoint Identity -> AgdaInterval
ip_interval' InteractionPoint Identity
ip)
      (String -> Interaction) -> String -> Interaction
forall a b. (a -> b) -> a -> b
$ Text -> String
T.unpack Text
expr

doHelperFunc :: CommandArguments -> Maybe String -> Neovim CornelisEnv ()
doHelperFunc :: CommandArguments -> Maybe String -> Neovim CornelisEnv ()
doHelperFunc CommandArguments
_ Maybe String
ms = Maybe String
-> (Rewrite -> Neovim CornelisEnv ()) -> Neovim CornelisEnv ()
forall e. Maybe String -> (Rewrite -> Neovim e ()) -> Neovim e ()
withNormalizationMode Maybe String
ms ((Rewrite -> Neovim CornelisEnv ()) -> Neovim CornelisEnv ())
-> (Rewrite -> Neovim CornelisEnv ()) -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ \Rewrite
mode -> do
  Text
expr <- String -> Maybe String -> Maybe String -> Neovim CornelisEnv Text
forall result env.
NvimObject result =>
String -> Maybe String -> Maybe String -> Neovim env result
input String
"Expression: " Maybe String
forall a. Maybe a
Nothing Maybe String
forall a. Maybe a
Nothing
  Rewrite -> Text -> Neovim CornelisEnv ()
helperFunc Rewrite
mode Text
expr

doCaseSplit :: CommandArguments -> Neovim CornelisEnv ()
doCaseSplit :: CommandArguments -> Neovim CornelisEnv ()
doCaseSplit CommandArguments
_ = Neovim CornelisEnv () -> Neovim CornelisEnv ()
forall a. Neovim CornelisEnv a -> Neovim CornelisEnv a
withAgda (Neovim CornelisEnv () -> Neovim CornelisEnv ())
-> Neovim CornelisEnv () -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ Neovim CornelisEnv (Maybe ()) -> Neovim CornelisEnv ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Neovim CornelisEnv (Maybe ()) -> Neovim CornelisEnv ())
-> Neovim CornelisEnv (Maybe ()) -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ (Buffer -> InteractionPoint Identity -> Neovim CornelisEnv ())
-> Neovim CornelisEnv (Maybe ())
forall a.
(Buffer -> InteractionPoint Identity -> Neovim CornelisEnv a)
-> Neovim CornelisEnv (Maybe a)
withGoalAtCursor ((Buffer -> InteractionPoint Identity -> Neovim CornelisEnv ())
 -> Neovim CornelisEnv (Maybe ()))
-> (Buffer -> InteractionPoint Identity -> Neovim CornelisEnv ())
-> Neovim CornelisEnv (Maybe ())
forall a b. (a -> b) -> a -> b
$ \Buffer
b InteractionPoint Identity
ip -> do
  Text
contents <- (Text -> Text)
-> Neovim CornelisEnv Text -> Neovim CornelisEnv Text
forall a b.
(a -> b) -> Neovim CornelisEnv a -> Neovim CornelisEnv b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Text -> Text
T.strip (Neovim CornelisEnv Text -> Neovim CornelisEnv Text)
-> Neovim CornelisEnv Text -> Neovim CornelisEnv Text
forall a b. (a -> b) -> a -> b
$ Buffer -> InteractionPoint Identity -> Neovim CornelisEnv Text
getGoalContents Buffer
b InteractionPoint Identity
ip
  Text
thing <- Neovim CornelisEnv Text
-> Neovim CornelisEnv Text -> Bool -> Neovim CornelisEnv Text
forall a. a -> a -> Bool -> a
bool (Text -> Neovim CornelisEnv Text
forall a. a -> Neovim CornelisEnv a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Text
contents)
                (forall result env.
NvimObject result =>
String -> Maybe String -> Maybe String -> Neovim env result
input @Text String
"Split on what?" Maybe String
forall a. Maybe a
Nothing Maybe String
forall a. Maybe a
Nothing)
         (Bool -> Neovim CornelisEnv Text)
-> Bool -> Neovim CornelisEnv Text
forall a b. (a -> b) -> a -> b
$ Text -> Bool
T.null Text
contents
  Text -> Neovim CornelisEnv ()
caseSplit Text
thing

caseSplit :: Text -> Neovim CornelisEnv ()
caseSplit :: Text -> Neovim CornelisEnv ()
caseSplit Text
thing = Neovim CornelisEnv () -> Neovim CornelisEnv ()
forall a. Neovim CornelisEnv a -> Neovim CornelisEnv a
withAgda (Neovim CornelisEnv () -> Neovim CornelisEnv ())
-> Neovim CornelisEnv () -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ Neovim CornelisEnv (Maybe ()) -> Neovim CornelisEnv ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Neovim CornelisEnv (Maybe ()) -> Neovim CornelisEnv ())
-> Neovim CornelisEnv (Maybe ()) -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ (Buffer -> InteractionPoint Identity -> Neovim CornelisEnv ())
-> Neovim CornelisEnv (Maybe ())
forall a.
(Buffer -> InteractionPoint Identity -> Neovim CornelisEnv a)
-> Neovim CornelisEnv (Maybe a)
withGoalAtCursor ((Buffer -> InteractionPoint Identity -> Neovim CornelisEnv ())
 -> Neovim CornelisEnv (Maybe ()))
-> (Buffer -> InteractionPoint Identity -> Neovim CornelisEnv ())
-> Neovim CornelisEnv (Maybe ())
forall a b. (a -> b) -> a -> b
$ \Buffer
b InteractionPoint Identity
ip -> do
  Agda
agda <- Buffer -> Neovim CornelisEnv Agda
getAgda Buffer
b
  Text
fp <- Buffer -> Neovim CornelisEnv Text
forall env. Buffer -> Neovim env Text
buffer_get_name Buffer
b
  (Interaction -> Agda -> Neovim CornelisEnv ())
-> Agda -> Interaction -> Neovim CornelisEnv ()
forall a b c. (a -> b -> c) -> b -> a -> c
flip Interaction -> Agda -> Neovim CornelisEnv ()
forall env. Interaction -> Agda -> Neovim env ()
runIOTCM Agda
agda
    (Interaction -> Neovim CornelisEnv ())
-> Interaction -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ InteractionId -> Range -> String -> Interaction
forall range.
InteractionId -> range -> String -> Interaction' range
Cmd_make_case
        (InteractionPoint Identity -> InteractionId
forall (f :: * -> *). InteractionPoint f -> InteractionId
ip_id InteractionPoint Identity
ip)
        (Text -> AgdaInterval -> Range
mkAbsPathRnage Text
fp (AgdaInterval -> Range) -> AgdaInterval -> Range
forall a b. (a -> b) -> a -> b
$ InteractionPoint Identity -> AgdaInterval
ip_interval' InteractionPoint Identity
ip)
    (String -> Interaction) -> String -> Interaction
forall a b. (a -> b) -> a -> b
$ Text -> String
T.unpack Text
thing

doQuestionToMeta :: CommandArguments -> Neovim CornelisEnv ()
doQuestionToMeta :: CommandArguments -> Neovim CornelisEnv ()
doQuestionToMeta CommandArguments
_ = (Buffer -> Neovim CornelisEnv ()) -> Neovim CornelisEnv ()
forall env a. (Buffer -> Neovim env a) -> Neovim env a
withCurrentBuffer Buffer -> Neovim CornelisEnv ()
questionToMeta

goalWindow :: Buffer -> DisplayInfo ->  Neovim CornelisEnv ()
goalWindow :: Buffer -> DisplayInfo -> Neovim CornelisEnv ()
goalWindow Buffer
b = Buffer -> Doc HighlightGroup -> Neovim CornelisEnv ()
showInfoWindow Buffer
b (Doc HighlightGroup -> Neovim CornelisEnv ())
-> (DisplayInfo -> Doc HighlightGroup)
-> DisplayInfo
-> Neovim CornelisEnv ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DisplayInfo -> Doc HighlightGroup
prettyGoals

computeModeCompletion :: String -> String -> Int -> Neovim env String
computeModeCompletion :: forall env. String -> String -> Int -> Neovim env String
computeModeCompletion String
_ String
_ Int
_ =
  String -> Neovim env String
forall a. a -> Neovim env a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Neovim env String) -> String -> Neovim env String
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (ComputeMode -> String) -> [ComputeMode] -> [String]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ComputeMode -> String
forall a. Show a => a -> String
show ([ComputeMode] -> [String]) -> [ComputeMode] -> [String]
forall a b. (a -> b) -> a -> b
$ forall a. Enum a => a -> a -> [a]
enumFromTo @ComputeMode ComputeMode
forall a. Bounded a => a
minBound ComputeMode
forall a. Bounded a => a
maxBound

rewriteModeCompletion :: String -> String -> Int -> Neovim env String
rewriteModeCompletion :: forall env. String -> String -> Int -> Neovim env String
rewriteModeCompletion String
_ String
_ Int
_ =
  String -> Neovim env String
forall a. a -> Neovim env a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Neovim env String) -> String -> Neovim env String
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (Rewrite -> String) -> [Rewrite] -> [String]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Rewrite -> String
forall a. Show a => a -> String
show ([Rewrite] -> [String]) -> [Rewrite] -> [String]
forall a b. (a -> b) -> a -> b
$ forall a. Enum a => a -> a -> [a]
enumFromTo @Rewrite Rewrite
forall a. Bounded a => a
minBound Rewrite
forall a. Bounded a => a
maxBound

debugCommandCompletion :: String -> String -> Int -> Neovim env String
debugCommandCompletion :: forall env. String -> String -> Int -> Neovim env String
debugCommandCompletion String
_ String
_ Int
_ =
  String -> Neovim env String
forall a. a -> Neovim env a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Neovim env String) -> String -> Neovim env String
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (DebugCommand -> String) -> [DebugCommand] -> [String]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DebugCommand -> String
forall a. Show a => a -> String
show ([DebugCommand] -> [String]) -> [DebugCommand] -> [String]
forall a b. (a -> b) -> a -> b
$ forall a. Enum a => a -> a -> [a]
enumFromTo @DebugCommand DebugCommand
forall a. Bounded a => a
minBound DebugCommand
forall a. Bounded a => a
maxBound


doDebug :: CommandArguments -> String -> Neovim CornelisEnv ()
doDebug :: CommandArguments -> String -> Neovim CornelisEnv ()
doDebug CommandArguments
_ String
str =
  case String -> Maybe DebugCommand
forall a. Read a => String -> Maybe a
readMaybe String
str of
    Just DebugCommand
DumpIPs ->
      Neovim CornelisEnv () -> Neovim CornelisEnv ()
forall a. Neovim CornelisEnv a -> Neovim CornelisEnv a
withAgda (Neovim CornelisEnv () -> Neovim CornelisEnv ())
-> Neovim CornelisEnv () -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ (Buffer -> Neovim CornelisEnv ()) -> Neovim CornelisEnv ()
forall env a. (Buffer -> Neovim env a) -> Neovim env a
withCurrentBuffer ((Buffer -> Neovim CornelisEnv ()) -> Neovim CornelisEnv ())
-> (Buffer -> Neovim CornelisEnv ()) -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ \Buffer
b -> Buffer
-> (BufferStuff -> Neovim CornelisEnv ()) -> Neovim CornelisEnv ()
forall a.
Monoid a =>
Buffer
-> (BufferStuff -> Neovim CornelisEnv a) -> Neovim CornelisEnv a
withBufferStuff Buffer
b ((BufferStuff -> Neovim CornelisEnv ()) -> Neovim CornelisEnv ())
-> (BufferStuff -> Neovim CornelisEnv ()) -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ \BufferStuff
bs -> do
        String
-> Map InteractionId (InteractionPoint Identity)
-> Neovim CornelisEnv ()
forall a env. Show a => String -> a -> Neovim env ()
traceMX String
"ips" (Map InteractionId (InteractionPoint Identity)
 -> Neovim CornelisEnv ())
-> Map InteractionId (InteractionPoint Identity)
-> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ BufferStuff -> Map InteractionId (InteractionPoint Identity)
bs_ips BufferStuff
bs
        String -> Map InteractionId Extmark -> Neovim CornelisEnv ()
forall a env. Show a => String -> a -> Neovim env ()
traceMX String
"ipexts" (Map InteractionId Extmark -> Neovim CornelisEnv ())
-> Map InteractionId Extmark -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ BufferStuff -> Map InteractionId Extmark
bs_ip_exts BufferStuff
bs
    Maybe DebugCommand
Nothing ->
      Text -> Neovim CornelisEnv ()
forall env. Text -> Neovim env ()
vim_report_error (Text -> Neovim CornelisEnv ()) -> Text -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ String -> Text
T.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ String
"No matching debug command for " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String -> String
forall a. Show a => a -> String
show String
str

-- | The @on_bytes@ callback required by @nvim_buf_attach@.
notifyEdit
  :: Text -- ^ the string "bytes"
  -> BufferNum -- ^ buffer handle
  -> Bool -- ^ b:changedtick
  -> Int -- ^ start row of the changed text (zero-indexed)
  -> Int -- ^ start column of the changed text
  -> Int -- ^ byte offset of the changed text (from the start of the buffer)
  -> Int -- ^ old end row of the changed text (relative to the start row)
  -> Int -- ^ old end column of the changed text
  -> Int -- ^ old end byte length of the changed text
  -> Int -- ^ new end row of the changed text (relative to the start row)
  -> Int -- ^ new end column of the changed text
  -> Int -- ^ new end byte length of the changed text
  -> Neovim CornelisEnv Bool  -- ^ Return True to detach
notifyEdit :: Text
-> Int64
-> Bool
-> Int
-> Int
-> Int
-> Int
-> Int
-> Int
-> Int
-> Int
-> Int
-> Neovim CornelisEnv Bool
notifyEdit Text
_ Int64
buf Bool
_ Int
sr Int
sc Int
_ Int
er Int
ec Int
_ Int
fr Int
fc Int
_ = do
  Int64 -> Replace DPos -> Neovim CornelisEnv ()
recordUpdate Int64
buf (DPos -> Trans DPos -> Trans DPos -> Replace DPos
forall p. p -> Trans p -> Trans p -> Replace p
Replace (Int -> Int -> DPos
forall {a} {a} {e :: Unit} {e :: Unit}.
(Integral a, Integral a) =>
a -> a -> Colline (Index e 'ZeroIndexed) (Index e 'ZeroIndexed)
pos Int
sr Int
sc) (Int -> Int -> Vallee (Offset 'Line) (Offset 'Byte)
forall {e :: Unit} {e :: Unit}.
Int -> Int -> Vallee (Offset e) (Offset e)
range Int
er Int
ec) (Int -> Int -> Vallee (Offset 'Line) (Offset 'Byte)
forall {e :: Unit} {e :: Unit}.
Int -> Int -> Vallee (Offset e) (Offset e)
range Int
fr Int
fc))
  Bool -> Neovim CornelisEnv Bool
forall a. a -> Neovim CornelisEnv a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False
  where
    pos :: a -> a -> Colline (Index e 'ZeroIndexed) (Index e 'ZeroIndexed)
pos a
l a
c = Index e 'ZeroIndexed
-> Index e 'ZeroIndexed
-> Colline (Index e 'ZeroIndexed) (Index e 'ZeroIndexed)
forall l c. l -> c -> Colline l c
Colline (a -> Index e 'ZeroIndexed
forall a (e :: Unit). Integral a => a -> Index e 'ZeroIndexed
toZeroIndexed a
l) (a -> Index e 'ZeroIndexed
forall a (e :: Unit). Integral a => a -> Index e 'ZeroIndexed
toZeroIndexed a
c)
    range :: Int -> Int -> Vallee (Offset e) (Offset e)
range Int
l Int
c = Offset e -> Offset e -> Vallee (Offset e) (Offset e)
forall dl dc. dl -> dc -> Vallee dl dc
Vallee (Int -> Offset e
forall (e :: Unit). Int -> Offset e
Offset Int
l) (Int -> Offset e
forall (e :: Unit). Int -> Offset e
Offset Int
c)

doCloseInfoWindows :: CommandArguments -> Neovim CornelisEnv ()
doCloseInfoWindows :: CommandArguments -> Neovim CornelisEnv ()
doCloseInfoWindows = Neovim CornelisEnv () -> CommandArguments -> Neovim CornelisEnv ()
forall a b. a -> b -> a
const Neovim CornelisEnv ()
forall env. Neovim env ()
closeInfoWindows