{-# 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
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
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
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
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)
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)
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
notifyEdit
:: Text
-> BufferNum
-> Bool
-> Int
-> Int
-> Int
-> Int
-> Int
-> Int
-> Int
-> Int
-> Int
-> Neovim CornelisEnv Bool
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