{-# LANGUAGE NumDecimals       #-}
{-# LANGUAGE OverloadedLabels  #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TemplateHaskell   #-}
{-# LANGUAGE ViewPatterns      #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}

module Lib where

import           Control.Arrow ((&&&))
import           Control.Concurrent.Chan.Unagi
import           Control.Lens
import           Control.Monad (forever, when)
import           Control.Monad.State.Class (gets)
import           Cornelis.Config (getConfig)
import           Cornelis.Debug (reportExceptions)
import           Cornelis.Goals
import           Cornelis.Highlighting (highlightBuffer, getLineIntervals, lookupPoint)
import           Cornelis.InfoWin
import           Cornelis.Offsets
import           Cornelis.Subscripts (incNextDigitSeq, decNextDigitSeq)
import           Cornelis.Types
import           Cornelis.Utils
import           Cornelis.Vim
import           Data.Foldable (for_)
import           Data.IORef (newIORef)
import qualified Data.Map as M
import           Data.Maybe
import qualified Data.Text as T
import           Neovim
import           Neovim.API.Text
import           Neovim.Plugin (CommandOption(CmdComplete))
import           Plugin


getInteractionPoint
    :: Buffer
    -> InteractionId
    -> Neovim CornelisEnv (Maybe (InteractionPoint Identity))
getInteractionPoint :: Buffer
-> InteractionId
-> Neovim CornelisEnv (Maybe (InteractionPoint Identity))
getInteractionPoint Buffer
b InteractionId
i = (CornelisState -> Maybe (InteractionPoint Identity))
-> Neovim CornelisEnv (Maybe (InteractionPoint Identity))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ((CornelisState -> Maybe (InteractionPoint Identity))
 -> Neovim CornelisEnv (Maybe (InteractionPoint Identity)))
-> (CornelisState -> Maybe (InteractionPoint Identity))
-> Neovim CornelisEnv (Maybe (InteractionPoint Identity))
forall a b. (a -> b) -> a -> b
$ Getting
  (First (InteractionPoint Identity))
  CornelisState
  (InteractionPoint Identity)
-> CornelisState -> Maybe (InteractionPoint Identity)
forall s (m :: * -> *) a.
MonadReader s m =>
Getting (First a) s a -> m (Maybe a)
preview (Getting
   (First (InteractionPoint Identity))
   CornelisState
   (InteractionPoint Identity)
 -> CornelisState -> Maybe (InteractionPoint Identity))
-> Getting
     (First (InteractionPoint Identity))
     CornelisState
     (InteractionPoint Identity)
-> CornelisState
-> Maybe (InteractionPoint Identity)
forall a b. (a -> b) -> a -> b
$ (Map Buffer BufferStuff
 -> Const
      (First (InteractionPoint Identity)) (Map Buffer BufferStuff))
-> CornelisState
-> Const (First (InteractionPoint Identity)) CornelisState
#cs_buffers ((Map Buffer BufferStuff
  -> Const
       (First (InteractionPoint Identity)) (Map Buffer BufferStuff))
 -> CornelisState
 -> Const (First (InteractionPoint Identity)) CornelisState)
-> ((InteractionPoint Identity
     -> Const
          (First (InteractionPoint Identity)) (InteractionPoint Identity))
    -> Map Buffer BufferStuff
    -> Const
         (First (InteractionPoint Identity)) (Map Buffer BufferStuff))
-> Getting
     (First (InteractionPoint Identity))
     CornelisState
     (InteractionPoint Identity)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index (Map Buffer BufferStuff)
-> Traversal'
     (Map Buffer BufferStuff) (IxValue (Map Buffer BufferStuff))
forall m. Ixed m => Index m -> Traversal' m (IxValue m)
ix Index (Map Buffer BufferStuff)
Buffer
b ((IxValue (Map Buffer BufferStuff)
  -> Const
       (First (InteractionPoint Identity))
       (IxValue (Map Buffer BufferStuff)))
 -> Map Buffer BufferStuff
 -> Const
      (First (InteractionPoint Identity)) (Map Buffer BufferStuff))
-> ((InteractionPoint Identity
     -> Const
          (First (InteractionPoint Identity)) (InteractionPoint Identity))
    -> IxValue (Map Buffer BufferStuff)
    -> Const
         (First (InteractionPoint Identity))
         (IxValue (Map Buffer BufferStuff)))
-> (InteractionPoint Identity
    -> Const
         (First (InteractionPoint Identity)) (InteractionPoint Identity))
-> Map Buffer BufferStuff
-> Const
     (First (InteractionPoint Identity)) (Map Buffer BufferStuff)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map InteractionId (InteractionPoint Identity)
 -> Const
      (First (InteractionPoint Identity))
      (Map InteractionId (InteractionPoint Identity)))
-> IxValue (Map Buffer BufferStuff)
-> Const
     (First (InteractionPoint Identity))
     (IxValue (Map Buffer BufferStuff))
#bs_ips ((Map InteractionId (InteractionPoint Identity)
  -> Const
       (First (InteractionPoint Identity))
       (Map InteractionId (InteractionPoint Identity)))
 -> IxValue (Map Buffer BufferStuff)
 -> Const
      (First (InteractionPoint Identity))
      (IxValue (Map Buffer BufferStuff)))
-> ((InteractionPoint Identity
     -> Const
          (First (InteractionPoint Identity)) (InteractionPoint Identity))
    -> Map InteractionId (InteractionPoint Identity)
    -> Const
         (First (InteractionPoint Identity))
         (Map InteractionId (InteractionPoint Identity)))
-> (InteractionPoint Identity
    -> Const
         (First (InteractionPoint Identity)) (InteractionPoint Identity))
-> IxValue (Map Buffer BufferStuff)
-> Const
     (First (InteractionPoint Identity))
     (IxValue (Map Buffer BufferStuff))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index (Map InteractionId (InteractionPoint Identity))
-> Traversal'
     (Map InteractionId (InteractionPoint Identity))
     (IxValue (Map InteractionId (InteractionPoint Identity)))
forall m. Ixed m => Index m -> Traversal' m (IxValue m)
ix Index (Map InteractionId (InteractionPoint Identity))
InteractionId
i


respondToHelperFunction :: DisplayInfo -> Neovim env ()
respondToHelperFunction :: forall env. DisplayInfo -> Neovim env ()
respondToHelperFunction (HelperFunction Text
sig) = Text -> Text -> Neovim env ()
forall env. Text -> Text -> Neovim env ()
setreg Text
"\"" Text
sig
respondToHelperFunction DisplayInfo
_ = () -> Neovim env ()
forall a. a -> Neovim env a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()


respond :: Buffer -> Response -> Neovim CornelisEnv ()
-- Update the buffer's goal map
respond :: Buffer -> Response -> Neovim CornelisEnv ()
respond Buffer
b (DisplayInfo DisplayInfo
dp) = do
  DisplayInfo -> Neovim CornelisEnv ()
forall env. DisplayInfo -> Neovim env ()
respondToHelperFunction DisplayInfo
dp
  Bool -> Neovim CornelisEnv () -> Neovim CornelisEnv ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (DisplayInfo
dp DisplayInfo -> (DisplayInfo -> Bool) -> Bool
forall a b. a -> (a -> b) -> b
& Getting
  All
  DisplayInfo
  (InteractionPoint Identity, [InScope], Type, Maybe Type,
   Maybe [Text], Maybe [Text])
-> DisplayInfo -> Bool
forall s a. Getting All s a -> s -> Bool
hasn't Getting
  All
  DisplayInfo
  (InteractionPoint Identity, [InScope], Type, Maybe Type,
   Maybe [Text], Maybe [Text])
#_GoalSpecific) (Neovim CornelisEnv () -> Neovim CornelisEnv ())
-> Neovim CornelisEnv () -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$
    Buffer -> (BufferStuff -> BufferStuff) -> Neovim CornelisEnv ()
modifyBufferStuff Buffer
b ((BufferStuff -> BufferStuff) -> Neovim CornelisEnv ())
-> (BufferStuff -> BufferStuff) -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ ASetter BufferStuff BufferStuff DisplayInfo DisplayInfo
#bs_goals ASetter BufferStuff BufferStuff DisplayInfo DisplayInfo
-> DisplayInfo -> BufferStuff -> BufferStuff
forall s t a b. ASetter s t a b -> b -> s -> t
.~ DisplayInfo
dp
  Buffer -> DisplayInfo -> Neovim CornelisEnv ()
goalWindow Buffer
b DisplayInfo
dp
-- Update the buffer's interaction points map
respond Buffer
b (InteractionPoints [InteractionPoint Maybe]
ips) = do
  let ips' :: [InteractionPoint Identity]
ips' = (InteractionPoint Maybe -> Maybe (InteractionPoint Identity))
-> [InteractionPoint Maybe] -> [InteractionPoint Identity]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe InteractionPoint Maybe -> Maybe (InteractionPoint Identity)
forall (f :: * -> *).
Applicative f =>
InteractionPoint f -> f (InteractionPoint Identity)
sequenceInteractionPoint [InteractionPoint Maybe]
ips
  Buffer -> (BufferStuff -> BufferStuff) -> Neovim CornelisEnv ()
modifyBufferStuff Buffer
b ((BufferStuff -> BufferStuff) -> Neovim CornelisEnv ())
-> (BufferStuff -> BufferStuff) -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ ASetter
  BufferStuff
  BufferStuff
  (Map InteractionId (InteractionPoint Identity))
  (Map InteractionId (InteractionPoint Identity))
#bs_ips ASetter
  BufferStuff
  BufferStuff
  (Map InteractionId (InteractionPoint Identity))
  (Map InteractionId (InteractionPoint Identity))
-> Map InteractionId (InteractionPoint Identity)
-> BufferStuff
-> BufferStuff
forall s t a b. ASetter s t a b -> b -> s -> t
.~ [(InteractionId, InteractionPoint Identity)]
-> Map InteractionId (InteractionPoint Identity)
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ((InteractionPoint Identity
 -> (InteractionId, InteractionPoint Identity))
-> [InteractionPoint Identity]
-> [(InteractionId, InteractionPoint Identity)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (InteractionPoint Identity -> InteractionId
forall (f :: * -> *). InteractionPoint f -> InteractionId
ip_id (InteractionPoint Identity -> InteractionId)
-> (InteractionPoint Identity -> InteractionPoint Identity)
-> InteractionPoint Identity
-> (InteractionId, InteractionPoint Identity)
forall b c c'. (b -> c) -> (b -> c') -> b -> (c, c')
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& InteractionPoint Identity -> InteractionPoint Identity
forall a. a -> a
id) [InteractionPoint Identity]
ips')
-- Replace a function clause
respond Buffer
b (MakeCase MakeCase
mkcase) = do
  Buffer -> MakeCase -> Neovim CornelisEnv ()
doMakeCase Buffer
b MakeCase
mkcase
  Neovim CornelisEnv ()
load
-- Replace the interaction point with a result
respond Buffer
b (GiveAction Text
result InteractionPoint (Const ())
ip) = do
  let i :: InteractionId
i = InteractionPoint (Const ()) -> InteractionId
forall (f :: * -> *). InteractionPoint f -> InteractionId
ip_id InteractionPoint (Const ())
ip
  Buffer
-> InteractionId
-> Neovim CornelisEnv (Maybe (InteractionPoint Identity))
getInteractionPoint Buffer
b InteractionId
i Neovim CornelisEnv (Maybe (InteractionPoint Identity))
-> (Maybe (InteractionPoint Identity) -> 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
    Maybe (InteractionPoint Identity)
Nothing -> Text -> Neovim CornelisEnv ()
forall env. Text -> Neovim env ()
reportError (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
"Can't find interaction point " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> InteractionId -> String
forall a. Show a => a -> String
show InteractionId
i
    Just InteractionPoint Identity
ip' -> do
      AgdaInterval
int <- Buffer
-> InteractionPoint Identity -> Neovim CornelisEnv AgdaInterval
getIpInterval Buffer
b InteractionPoint Identity
ip'
      Buffer -> AgdaInterval -> Text -> Neovim CornelisEnv ()
forall env. Buffer -> AgdaInterval -> Text -> Neovim env ()
replaceInterval Buffer
b AgdaInterval
int (Text -> Neovim CornelisEnv ()) -> Text -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ Text -> Text
replaceQuestion Text
result
  Neovim CornelisEnv ()
load
-- Replace the interaction point with a result
respond Buffer
b (SolveAll [Solution]
solutions) = do
  [Solution]
-> (Solution -> Neovim CornelisEnv ()) -> Neovim CornelisEnv ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ [Solution]
solutions ((Solution -> Neovim CornelisEnv ()) -> Neovim CornelisEnv ())
-> (Solution -> Neovim CornelisEnv ()) -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ \(Solution InteractionId
i Text
ex) ->
    Buffer
-> InteractionId
-> Neovim CornelisEnv (Maybe (InteractionPoint Identity))
getInteractionPoint Buffer
b InteractionId
i Neovim CornelisEnv (Maybe (InteractionPoint Identity))
-> (Maybe (InteractionPoint Identity) -> 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
      Maybe (InteractionPoint Identity)
Nothing -> Text -> Neovim CornelisEnv ()
forall env. Text -> Neovim env ()
reportError (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
"Can't find interaction point " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> InteractionId -> String
forall a. Show a => a -> String
show InteractionId
i
      Just InteractionPoint Identity
ip -> do
        AgdaInterval
int <- Buffer
-> InteractionPoint Identity -> Neovim CornelisEnv AgdaInterval
getIpInterval Buffer
b InteractionPoint Identity
ip
        Buffer -> AgdaInterval -> Text -> Neovim CornelisEnv ()
forall env. Buffer -> AgdaInterval -> Text -> Neovim env ()
replaceInterval Buffer
b AgdaInterval
int (Text -> Neovim CornelisEnv ()) -> Text -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ Text -> Text
replaceQuestion Text
ex
  Neovim CornelisEnv ()
load
respond Buffer
b Response
ClearHighlighting = do
  -- delete what we know about goto positions and stored extmarks
  Buffer -> (BufferStuff -> BufferStuff) -> Neovim CornelisEnv ()
modifyBufferStuff Buffer
b ((BufferStuff -> BufferStuff) -> Neovim CornelisEnv ())
-> (BufferStuff -> BufferStuff) -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ \BufferStuff
bs -> BufferStuff
bs
    BufferStuff -> (BufferStuff -> BufferStuff) -> BufferStuff
forall a b. a -> (a -> b) -> b
& ASetter
  BufferStuff
  BufferStuff
  (Map Extmark DefinitionSite)
  (Map Extmark DefinitionSite)
#bs_goto_sites ASetter
  BufferStuff
  BufferStuff
  (Map Extmark DefinitionSite)
  (Map Extmark DefinitionSite)
-> Map Extmark DefinitionSite -> BufferStuff -> BufferStuff
forall s t a b. ASetter s t a b -> b -> s -> t
.~ Map Extmark DefinitionSite
forall a. Monoid a => a
mempty
    BufferStuff -> (BufferStuff -> BufferStuff) -> BufferStuff
forall a b. a -> (a -> b) -> b
& ASetter
  BufferStuff
  BufferStuff
  (Map InteractionId Extmark)
  (Map InteractionId Extmark)
#bs_ip_exts ASetter
  BufferStuff
  BufferStuff
  (Map InteractionId Extmark)
  (Map InteractionId Extmark)
-> Map InteractionId Extmark -> BufferStuff -> BufferStuff
forall s t a b. ASetter s t a b -> b -> s -> t
.~ Map InteractionId Extmark
forall a. Monoid a => a
mempty
  -- remove the extmarks and highlighting
  Int64
ns <- (CornelisEnv -> Int64) -> Neovim CornelisEnv Int64
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks CornelisEnv -> Int64
ce_namespace
  Buffer -> Int64 -> Int64 -> Int64 -> Neovim CornelisEnv ()
forall env. Buffer -> Int64 -> Int64 -> Int64 -> Neovim env ()
nvim_buf_clear_namespace Buffer
b Int64
ns Int64
0 (-Int64
1)
respond Buffer
b (HighlightingInfo Bool
_remove [Highlight]
hl) = do
  Map AgdaInterval Extmark
extmap <- Buffer
-> [Highlight] -> Neovim CornelisEnv (Map AgdaInterval Extmark)
highlightBuffer Buffer
b [Highlight]
hl
  Buffer -> (BufferStuff -> BufferStuff) -> Neovim CornelisEnv ()
modifyBufferStuff Buffer
b ((BufferStuff -> BufferStuff) -> Neovim CornelisEnv ())
-> (BufferStuff -> BufferStuff) -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ \BufferStuff
bs -> BufferStuff
bs
    BufferStuff -> (BufferStuff -> BufferStuff) -> BufferStuff
forall a b. a -> (a -> b) -> b
& ASetter
  BufferStuff
  BufferStuff
  (Map InteractionId Extmark)
  (Map InteractionId Extmark)
#bs_ip_exts ASetter
  BufferStuff
  BufferStuff
  (Map InteractionId Extmark)
  (Map InteractionId Extmark)
-> Map InteractionId Extmark -> BufferStuff -> BufferStuff
forall a s t. Semigroup a => ASetter s t a a -> a -> s -> t
<>~ Map AgdaInterval Extmark
-> Map InteractionId AgdaInterval -> Map InteractionId Extmark
forall b c a. Ord b => Map b c -> Map a b -> Map a c
M.compose Map AgdaInterval Extmark
extmap ((InteractionPoint Identity -> AgdaInterval)
-> Map InteractionId (InteractionPoint Identity)
-> Map InteractionId AgdaInterval
forall a b. (a -> b) -> Map InteractionId a -> Map InteractionId b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap InteractionPoint Identity -> AgdaInterval
ip_interval' (Map InteractionId (InteractionPoint Identity)
 -> Map InteractionId AgdaInterval)
-> Map InteractionId (InteractionPoint Identity)
-> Map InteractionId AgdaInterval
forall a b. (a -> b) -> a -> b
$ BufferStuff -> Map InteractionId (InteractionPoint Identity)
bs_ips BufferStuff
bs)
respond Buffer
_ (RunningInfo Int
_ Text
x) = Text -> Neovim CornelisEnv ()
forall env. Text -> Neovim env ()
reportInfo Text
x
respond Buffer
_ Response
ClearRunningInfo = Text -> Neovim CornelisEnv ()
forall env. Text -> Neovim env ()
reportInfo Text
""
respond Buffer
b (JumpToError String
_ Index 'CodePoint 'OneIndexed
pos) = do
  -- HACK(sandy): See #113. Agda reports error positions in sent messages
  -- relative to the *bytes* attached to the sent interval. But we can't easily
  -- get this when we send intervals. So instead, we just don't jump backwards
  -- if the absolute position is small, because this is indicative that it is
  -- actually a relative position.
  Bool -> Neovim CornelisEnv () -> Neovim CornelisEnv ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall a (e :: Unit). Num a => Index e 'OneIndexed -> a
fromOneIndexed @Int Index 'CodePoint 'OneIndexed
pos Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
50) (Neovim CornelisEnv () -> Neovim CornelisEnv ())
-> Neovim CornelisEnv () -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ do
    Vector Text
buf_lines <- Buffer
-> Int64 -> Int64 -> Bool -> Neovim CornelisEnv (Vector Text)
forall env.
Buffer -> Int64 -> Int64 -> Bool -> Neovim env (Vector Text)
nvim_buf_get_lines Buffer
b Int64
0 (-Int64
1) Bool
True
    let li :: LineIntervals
li = Vector Text -> LineIntervals
getLineIntervals Vector Text
buf_lines
    case LineIntervals -> Index 'CodePoint 'OneIndexed -> Maybe VimPos
lookupPoint LineIntervals
li Index 'CodePoint 'OneIndexed
pos of
      Maybe VimPos
Nothing -> Text -> Neovim CornelisEnv ()
forall env. Text -> Neovim env ()
reportError Text
"invalid error report from Agda"
      Just (Pos Index 'Line 'ZeroIndexed
l Index 'Byte 'ZeroIndexed
c) -> do
        Maybe Window
ws <- ([Window] -> Maybe Window)
-> Neovim CornelisEnv [Window] -> Neovim CornelisEnv (Maybe Window)
forall a b.
(a -> b) -> Neovim CornelisEnv a -> Neovim CornelisEnv b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Window] -> Maybe Window
forall a. [a] -> Maybe a
listToMaybe (Neovim CornelisEnv [Window] -> Neovim CornelisEnv (Maybe Window))
-> Neovim CornelisEnv [Window] -> Neovim CornelisEnv (Maybe Window)
forall a b. (a -> b) -> a -> b
$ Buffer -> Neovim CornelisEnv [Window]
forall env. Buffer -> Neovim env [Window]
windowsForBuffer Buffer
b
        Maybe Window
-> (Window -> Neovim CornelisEnv ()) -> Neovim CornelisEnv ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ Maybe Window
ws ((Window -> Neovim CornelisEnv ()) -> Neovim CornelisEnv ())
-> (Window -> Neovim CornelisEnv ()) -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ (Window -> (Int64, Int64) -> Neovim CornelisEnv ())
-> (Int64, Int64) -> Window -> Neovim CornelisEnv ()
forall a b c. (a -> b -> c) -> b -> a -> c
flip Window -> (Int64, Int64) -> Neovim CornelisEnv ()
forall env. Window -> (Int64, Int64) -> Neovim env ()
window_set_cursor (Index 'Line 'OneIndexed -> Int64
forall a (e :: Unit). Num a => Index e 'OneIndexed -> a
fromOneIndexed (Index 'Line 'ZeroIndexed -> Index 'Line 'OneIndexed
forall (e :: Unit). Index e 'ZeroIndexed -> Index e 'OneIndexed
oneIndex Index 'Line 'ZeroIndexed
l), Index 'Byte 'ZeroIndexed -> Int64
forall a (e :: Unit). Num a => Index e 'ZeroIndexed -> a
fromZeroIndexed Index 'Byte 'ZeroIndexed
c)
respond Buffer
_ Status{} = () -> Neovim CornelisEnv ()
forall a. a -> Neovim CornelisEnv a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
respond Buffer
_ (Unknown Text
k Value
_) = Text -> Neovim CornelisEnv ()
forall env. Text -> Neovim env ()
reportError Text
k

{-# HLINT ignore doMakeCase "Functor law" #-}
doMakeCase :: Buffer -> MakeCase -> Neovim CornelisEnv ()
doMakeCase :: Buffer -> MakeCase -> Neovim CornelisEnv ()
doMakeCase Buffer
b (RegularCase MakeCaseVariant
Function [Text]
clauses InteractionPoint Identity
ip) = do
  AgdaInterval
int' <- Buffer
-> InteractionPoint Identity -> Neovim CornelisEnv AgdaInterval
getIpInterval Buffer
b InteractionPoint Identity
ip
  let int :: AgdaInterval
int = AgdaInterval
int' AgdaInterval -> (AgdaInterval -> AgdaInterval) -> AgdaInterval
forall a b. a -> (a -> b) -> b
& (Pos 'CodePoint 'OneIndexed 'OneIndexed
 -> Identity (Pos 'CodePoint 'OneIndexed 'OneIndexed))
-> AgdaInterval -> Identity AgdaInterval
#iStart ((Pos 'CodePoint 'OneIndexed 'OneIndexed
  -> Identity (Pos 'CodePoint 'OneIndexed 'OneIndexed))
 -> AgdaInterval -> Identity AgdaInterval)
-> ((Index 'CodePoint 'OneIndexed
     -> Identity (Index 'CodePoint 'OneIndexed))
    -> Pos 'CodePoint 'OneIndexed 'OneIndexed
    -> Identity (Pos 'CodePoint 'OneIndexed 'OneIndexed))
-> (Index 'CodePoint 'OneIndexed
    -> Identity (Index 'CodePoint 'OneIndexed))
-> AgdaInterval
-> Identity AgdaInterval
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Index 'CodePoint 'OneIndexed
 -> Identity (Index 'CodePoint 'OneIndexed))
-> Pos 'CodePoint 'OneIndexed 'OneIndexed
-> Identity (Pos 'CodePoint 'OneIndexed 'OneIndexed)
#p_col ((Index 'CodePoint 'OneIndexed
  -> Identity (Index 'CodePoint 'OneIndexed))
 -> AgdaInterval -> Identity AgdaInterval)
-> Index 'CodePoint 'OneIndexed -> AgdaInterval -> AgdaInterval
forall s t a b. ASetter s t a b -> b -> s -> t
.~ forall a (e :: Unit). Integral a => a -> Index e 'OneIndexed
toOneIndexed @Int Int
1
  Int
ins <- Buffer -> Index 'Line 'ZeroIndexed -> Neovim CornelisEnv Int
forall env. Buffer -> Index 'Line 'ZeroIndexed -> Neovim env Int
getIndent Buffer
b (Index 'Line 'OneIndexed -> Index 'Line 'ZeroIndexed
forall (e :: Unit). Index e 'OneIndexed -> Index e 'ZeroIndexed
zeroIndex (Pos 'CodePoint 'OneIndexed 'OneIndexed -> Index 'Line 'OneIndexed
forall (e :: Unit) (i :: Indexing) (j :: Indexing).
Pos e i j -> Index 'Line i
p_line (AgdaInterval -> Pos 'CodePoint 'OneIndexed 'OneIndexed
forall p. Interval p -> p
iStart AgdaInterval
int)))
  Buffer -> AgdaInterval -> Text -> Neovim CornelisEnv ()
forall env. Buffer -> AgdaInterval -> Text -> Neovim env ()
replaceInterval Buffer
b AgdaInterval
int
    (Text -> Neovim CornelisEnv ()) -> Text -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ [Text] -> Text
T.unlines
    ([Text] -> Text) -> [Text] -> Text
forall a b. (a -> b) -> a -> b
$ (Text -> Text) -> [Text] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Int -> Text -> Text
T.replicate Int
ins Text
" " <>)
    ([Text] -> [Text]) -> [Text] -> [Text]
forall a b. (a -> b) -> a -> b
$ (Text -> Text) -> [Text] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Text -> Text
replaceQuestion [Text]
clauses
-- TODO(sandy): It would be nice if Agda just gave us the bounds we're supposed to replace...
doMakeCase Buffer
b (RegularCase MakeCaseVariant
ExtendedLambda [Text]
clauses InteractionPoint Identity
ip) = do
  [Window]
ws <- Buffer -> Neovim CornelisEnv [Window]
forall env. Buffer -> Neovim env [Window]
windowsForBuffer Buffer
b
  case [Window] -> Maybe Window
forall a. [a] -> Maybe a
listToMaybe [Window]
ws of
    Maybe Window
Nothing ->
      Text -> Neovim CornelisEnv ()
forall env. Text -> Neovim env ()
reportError
        Text
"Unable to extend a lambda without having a window that contains the modified buffer. This is a limitation in cornelis."
    Just Window
w -> do
      AgdaInterval
int' <- Buffer
-> InteractionPoint Identity -> Neovim CornelisEnv AgdaInterval
getIpInterval Buffer
b InteractionPoint Identity
ip
      Interval Pos 'CodePoint 'OneIndexed 'OneIndexed
start Pos 'CodePoint 'OneIndexed 'OneIndexed
end
        <- Window -> Buffer -> AgdaInterval -> Neovim CornelisEnv AgdaInterval
forall env.
Window -> Buffer -> AgdaInterval -> Neovim env AgdaInterval
getLambdaClause Window
w Buffer
b (AgdaInterval
int' AgdaInterval -> (AgdaInterval -> AgdaInterval) -> AgdaInterval
forall a b. a -> (a -> b) -> b
& (Pos 'CodePoint 'OneIndexed 'OneIndexed
 -> Identity (Pos 'CodePoint 'OneIndexed 'OneIndexed))
-> AgdaInterval -> Identity AgdaInterval
#iStart ((Pos 'CodePoint 'OneIndexed 'OneIndexed
  -> Identity (Pos 'CodePoint 'OneIndexed 'OneIndexed))
 -> AgdaInterval -> Identity AgdaInterval)
-> ((Index 'CodePoint 'OneIndexed
     -> Identity (Index 'CodePoint 'OneIndexed))
    -> Pos 'CodePoint 'OneIndexed 'OneIndexed
    -> Identity (Pos 'CodePoint 'OneIndexed 'OneIndexed))
-> (Index 'CodePoint 'OneIndexed
    -> Identity (Index 'CodePoint 'OneIndexed))
-> AgdaInterval
-> Identity AgdaInterval
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Index 'CodePoint 'OneIndexed
 -> Identity (Index 'CodePoint 'OneIndexed))
-> Pos 'CodePoint 'OneIndexed 'OneIndexed
-> Identity (Pos 'CodePoint 'OneIndexed 'OneIndexed)
#p_col ((Index 'CodePoint 'OneIndexed
  -> Identity (Index 'CodePoint 'OneIndexed))
 -> AgdaInterval -> Identity AgdaInterval)
-> (Index 'CodePoint 'OneIndexed -> Index 'CodePoint 'OneIndexed)
-> AgdaInterval
-> AgdaInterval
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (Index 'CodePoint 'OneIndexed
-> Offset 'CodePoint -> Index 'CodePoint 'OneIndexed
forall (e :: Unit) (i :: Indexing).
Index e i -> Offset e -> Index e i
.+ Int -> Offset 'CodePoint
forall (e :: Unit). Int -> Offset e
Offset (- Int
1)))
           -- Subtract one so we are outside of a {! !} goal and the i} movement
           -- works correctly
      -- Add an extra character to the start so we leave a space after the
      -- opening brace, and subtract two characters from the end for the space and the }
      Buffer -> AgdaInterval -> Text -> Neovim CornelisEnv ()
forall env. Buffer -> AgdaInterval -> Text -> Neovim env ()
replaceInterval Buffer
b (Pos 'CodePoint 'OneIndexed 'OneIndexed
-> Pos 'CodePoint 'OneIndexed 'OneIndexed -> AgdaInterval
forall p. p -> p -> Interval p
Interval (Pos 'CodePoint 'OneIndexed 'OneIndexed
start Pos 'CodePoint 'OneIndexed 'OneIndexed
-> (Pos 'CodePoint 'OneIndexed 'OneIndexed
    -> Pos 'CodePoint 'OneIndexed 'OneIndexed)
-> Pos 'CodePoint 'OneIndexed 'OneIndexed
forall a b. a -> (a -> b) -> b
& (Index 'CodePoint 'OneIndexed
 -> Identity (Index 'CodePoint 'OneIndexed))
-> Pos 'CodePoint 'OneIndexed 'OneIndexed
-> Identity (Pos 'CodePoint 'OneIndexed 'OneIndexed)
#p_col ((Index 'CodePoint 'OneIndexed
  -> Identity (Index 'CodePoint 'OneIndexed))
 -> Pos 'CodePoint 'OneIndexed 'OneIndexed
 -> Identity (Pos 'CodePoint 'OneIndexed 'OneIndexed))
-> (Index 'CodePoint 'OneIndexed -> Index 'CodePoint 'OneIndexed)
-> Pos 'CodePoint 'OneIndexed 'OneIndexed
-> Pos 'CodePoint 'OneIndexed 'OneIndexed
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (Index 'CodePoint 'OneIndexed
-> Offset 'CodePoint -> Index 'CodePoint 'OneIndexed
forall (e :: Unit) (i :: Indexing).
Index e i -> Offset e -> Index e i
.+ Int -> Offset 'CodePoint
forall (e :: Unit). Int -> Offset e
Offset Int
1)) (Pos 'CodePoint 'OneIndexed 'OneIndexed
end Pos 'CodePoint 'OneIndexed 'OneIndexed
-> (Pos 'CodePoint 'OneIndexed 'OneIndexed
    -> Pos 'CodePoint 'OneIndexed 'OneIndexed)
-> Pos 'CodePoint 'OneIndexed 'OneIndexed
forall a b. a -> (a -> b) -> b
& (Index 'CodePoint 'OneIndexed
 -> Identity (Index 'CodePoint 'OneIndexed))
-> Pos 'CodePoint 'OneIndexed 'OneIndexed
-> Identity (Pos 'CodePoint 'OneIndexed 'OneIndexed)
#p_col ((Index 'CodePoint 'OneIndexed
  -> Identity (Index 'CodePoint 'OneIndexed))
 -> Pos 'CodePoint 'OneIndexed 'OneIndexed
 -> Identity (Pos 'CodePoint 'OneIndexed 'OneIndexed))
-> (Index 'CodePoint 'OneIndexed -> Index 'CodePoint 'OneIndexed)
-> Pos 'CodePoint 'OneIndexed 'OneIndexed
-> Pos 'CodePoint 'OneIndexed 'OneIndexed
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (Index 'CodePoint 'OneIndexed
-> Offset 'CodePoint -> Index 'CodePoint 'OneIndexed
forall (e :: Unit) (i :: Indexing).
Index e i -> Offset e -> Index e i
.+ Int -> Offset 'CodePoint
forall (e :: Unit). Int -> Offset e
Offset (- Int
2))))
        (Text -> Neovim CornelisEnv ()) -> Text -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ [Text] -> Text
T.unlines
        ([Text] -> Text) -> [Text] -> Text
forall a b. (a -> b) -> a -> b
$ (Text -> Text) -> [Text] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Text -> Text
replaceQuestion [Text]
clauses [Text] -> ([Text] -> [Text]) -> [Text]
forall a b. a -> (a -> b) -> b
& ([Text] -> Identity [Text]) -> [Text] -> Identity [Text]
forall s a. Cons s s a a => Traversal' s s
Traversal' [Text] [Text]
_tail (([Text] -> Identity [Text]) -> [Text] -> Identity [Text])
-> ([Text] -> [Text]) -> [Text] -> [Text]
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (Text -> Text) -> [Text] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Pos 'CodePoint 'OneIndexed 'OneIndexed -> Text -> Text
indent Pos 'CodePoint 'OneIndexed 'OneIndexed
start)


------------------------------------------------------------------------------
-- | Indent a string with the given offset.
indent :: AgdaPos -> Text -> Text
indent :: Pos 'CodePoint 'OneIndexed 'OneIndexed -> Text -> Text
indent (Pos Index 'Line 'OneIndexed
_ Index 'CodePoint 'OneIndexed
c) Text
s = [Text] -> Text
forall a. Monoid a => [a] -> a
mconcat
  [ (Int -> Text -> Text) -> Text -> Int -> Text
forall a b c. (a -> b -> c) -> b -> a -> c
flip Int -> Text -> Text
T.replicate Text
" " (Int -> Text) -> Int -> Text
forall a b. (a -> b) -> a -> b
$ Index 'CodePoint 'ZeroIndexed -> Int
forall a (e :: Unit). Num a => Index e 'ZeroIndexed -> a
fromZeroIndexed (Index 'CodePoint 'OneIndexed -> Index 'CodePoint 'ZeroIndexed
forall (e :: Unit). Index e 'OneIndexed -> Index e 'ZeroIndexed
zeroIndex Index 'CodePoint 'OneIndexed
c) Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1
  , Text
"; "
  , Text
s
  ]


doPrevGoal :: CommandArguments -> Neovim CornelisEnv ()
doPrevGoal :: CommandArguments -> Neovim CornelisEnv ()
doPrevGoal = Neovim CornelisEnv () -> CommandArguments -> Neovim CornelisEnv ()
forall a b. a -> b -> a
const Neovim CornelisEnv ()
prevGoal

doNextGoal :: CommandArguments -> Neovim CornelisEnv ()
doNextGoal :: CommandArguments -> Neovim CornelisEnv ()
doNextGoal = Neovim CornelisEnv () -> CommandArguments -> Neovim CornelisEnv ()
forall a b. a -> b -> a
const Neovim CornelisEnv ()
nextGoal


doIncNextDigitSeq :: CommandArguments -> Neovim CornelisEnv ()
doIncNextDigitSeq :: CommandArguments -> Neovim CornelisEnv ()
doIncNextDigitSeq = Neovim CornelisEnv () -> CommandArguments -> Neovim CornelisEnv ()
forall a b. a -> b -> a
const Neovim CornelisEnv ()
forall env. Neovim env ()
incNextDigitSeq

doDecNextDigitSeq :: CommandArguments -> Neovim CornelisEnv ()
doDecNextDigitSeq :: CommandArguments -> Neovim CornelisEnv ()
doDecNextDigitSeq = Neovim CornelisEnv () -> CommandArguments -> Neovim CornelisEnv ()
forall a b. a -> b -> a
const Neovim CornelisEnv ()
forall env. Neovim env ()
decNextDigitSeq


cornelisInit :: Neovim env CornelisEnv
cornelisInit :: forall env. Neovim env CornelisEnv
cornelisInit = do
  (InChan AgdaResp
inchan, OutChan AgdaResp
outchan) <- IO (InChan AgdaResp, OutChan AgdaResp)
-> Neovim env (InChan AgdaResp, OutChan AgdaResp)
forall a. IO a -> Neovim env a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO (InChan AgdaResp, OutChan AgdaResp)
forall a. IO (InChan a, OutChan a)
newChan
  Int64
ns <- Text -> Neovim env Int64
forall env. Text -> Neovim env Int64
nvim_create_namespace Text
"cornelis"
  IORef CornelisState
mvar <- IO (IORef CornelisState) -> Neovim env (IORef CornelisState)
forall a. IO a -> Neovim env a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (IORef CornelisState) -> Neovim env (IORef CornelisState))
-> IO (IORef CornelisState) -> Neovim env (IORef CornelisState)
forall a b. (a -> b) -> a -> b
$ CornelisState -> IO (IORef CornelisState)
forall a. a -> IO (IORef a)
newIORef (CornelisState -> IO (IORef CornelisState))
-> CornelisState -> IO (IORef CornelisState)
forall a b. (a -> b) -> a -> b
$ Map Buffer BufferStuff -> Map Int64 Diff0 -> CornelisState
CornelisState Map Buffer BufferStuff
forall a. Monoid a => a
mempty Map Int64 Diff0
forall a. Monoid a => a
mempty

  CornelisConfig
cfg <- Neovim env CornelisConfig
forall env. Neovim env CornelisConfig
getConfig

  let env :: CornelisEnv
env = IORef CornelisState
-> InChan AgdaResp -> Int64 -> CornelisConfig -> CornelisEnv
CornelisEnv IORef CornelisState
mvar InChan AgdaResp
inchan Int64
ns CornelisConfig
cfg
  Neovim env (Async Any) -> Neovim env ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Neovim env (Async Any) -> Neovim env ())
-> Neovim env (Async Any) -> Neovim env ()
forall a b. (a -> b) -> a -> b
$ CornelisEnv
-> Neovim CornelisEnv (Async Any) -> Neovim env (Async Any)
forall env a env'. env -> Neovim env a -> Neovim env' a
withLocalEnv CornelisEnv
env (Neovim CornelisEnv (Async Any) -> Neovim env (Async Any))
-> Neovim CornelisEnv (Async Any) -> Neovim env (Async Any)
forall a b. (a -> b) -> a -> b
$
    Neovim CornelisEnv Any -> Neovim CornelisEnv (Async Any)
forall (m :: * -> *) a. MonadUnliftIO m => m a -> m (Async a)
neovimAsync (Neovim CornelisEnv Any -> Neovim CornelisEnv (Async Any))
-> Neovim CornelisEnv Any -> Neovim CornelisEnv (Async Any)
forall a b. (a -> b) -> a -> b
$ do
      Neovim CornelisEnv () -> Neovim CornelisEnv Any
forall (f :: * -> *) a b. Applicative f => f a -> f b
forever (Neovim CornelisEnv () -> Neovim CornelisEnv Any)
-> Neovim CornelisEnv () -> Neovim CornelisEnv Any
forall a b. (a -> b) -> a -> b
$ Neovim CornelisEnv () -> Neovim CornelisEnv ()
forall env. Neovim env () -> Neovim env ()
reportExceptions (Neovim CornelisEnv () -> Neovim CornelisEnv ())
-> Neovim CornelisEnv () -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ do
        AgdaResp Buffer
buffer Response
next <- IO AgdaResp -> Neovim CornelisEnv AgdaResp
forall a. IO a -> Neovim CornelisEnv a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO AgdaResp -> Neovim CornelisEnv AgdaResp)
-> IO AgdaResp -> Neovim CornelisEnv AgdaResp
forall a b. (a -> b) -> a -> b
$ OutChan AgdaResp -> IO AgdaResp
forall a. OutChan a -> IO a
readChan OutChan AgdaResp
outchan
        Neovim CornelisEnv (Async ()) -> Neovim CornelisEnv ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Neovim CornelisEnv (Async ()) -> Neovim CornelisEnv ())
-> Neovim CornelisEnv (Async ()) -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ Neovim CornelisEnv () -> Neovim CornelisEnv (Async ())
forall (m :: * -> *) a. MonadUnliftIO m => m a -> m (Async a)
neovimAsync (Neovim CornelisEnv () -> Neovim CornelisEnv (Async ()))
-> Neovim CornelisEnv () -> Neovim CornelisEnv (Async ())
forall a b. (a -> b) -> a -> b
$ Neovim CornelisEnv () -> Neovim CornelisEnv ()
forall env. Neovim env () -> Neovim env ()
reportExceptions (Neovim CornelisEnv () -> Neovim CornelisEnv ())
-> Neovim CornelisEnv () -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ Buffer -> Response -> Neovim CornelisEnv ()
respond Buffer
buffer Response
next
  CornelisEnv -> Neovim env CornelisEnv
forall a. a -> Neovim env a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CornelisEnv
env


-- Flush the TH environment
$(pure [])


main :: IO ()
main :: IO ()
main = NeovimConfig -> IO ()
neovim NeovimConfig
defaultConfig { plugins = [cornelis] }


cornelis :: Neovim () NeovimPlugin
cornelis :: Neovim () NeovimPlugin
cornelis = do
  CornelisEnv
env <- Neovim () CornelisEnv
forall env. Neovim env CornelisEnv
cornelisInit
  Neovim () ()
forall env. Neovim env ()
closeInfoWindows

  let rw_complete :: CommandOption
rw_complete = String -> CommandOption
CmdComplete String
"custom,InternalCornelisRewriteModeCompletion"
      cm_complete :: CommandOption
cm_complete = String -> CommandOption
CmdComplete String
"custom,InternalCornelisComputeModeCompletion"
      debug_complete :: CommandOption
debug_complete = String -> CommandOption
CmdComplete String
"custom,InternalCornelisDebugCommandCompletion"

  Plugin CornelisEnv -> Neovim () NeovimPlugin
forall (m :: * -> *) env.
Applicative m =>
Plugin env -> m NeovimPlugin
wrapPlugin (Plugin CornelisEnv -> Neovim () NeovimPlugin)
-> Plugin CornelisEnv -> Neovim () NeovimPlugin
forall a b. (a -> b) -> a -> b
$ Plugin
    { environment :: CornelisEnv
environment = CornelisEnv
env
    , exports :: [ExportedFunctionality CornelisEnv]
exports =
        [ $(command "CornelisRestart"          'doRestart)          [Synchronous -> CommandOption
CmdSync Synchronous
Async]
        , $(command "CornelisAbort"            'doAbort)            [Synchronous -> CommandOption
CmdSync Synchronous
Async]
        , $(command "CornelisLoad"             'doLoad)             [Synchronous -> CommandOption
CmdSync Synchronous
Async]
        , $(command "CornelisGoals"            'doAllGoals)         [Synchronous -> CommandOption
CmdSync Synchronous
Async]
        , $(command "CornelisSolve"            'solveOne)           [Synchronous -> CommandOption
CmdSync Synchronous
Async, CommandOption
rw_complete]
        , $(command "CornelisAuto"             'autoOne)            [Synchronous -> CommandOption
CmdSync Synchronous
Async]
        , $(command "CornelisTypeInfer"        'doTypeInfer)        [Synchronous -> CommandOption
CmdSync Synchronous
Async]
        , $(command "CornelisTypeContext"      'typeContext)        [Synchronous -> CommandOption
CmdSync Synchronous
Async, CommandOption
rw_complete]
        , $(command "CornelisTypeContextInfer" 'typeContextInfer)   [Synchronous -> CommandOption
CmdSync Synchronous
Async, CommandOption
rw_complete]
        , $(command "CornelisMakeCase"         'doCaseSplit)        [Synchronous -> CommandOption
CmdSync Synchronous
Async]
        , $(command "CornelisRefine"           'doRefine)           [Synchronous -> CommandOption
CmdSync Synchronous
Async]
        , $(command "CornelisGive"             'doGive)             [Synchronous -> CommandOption
CmdSync Synchronous
Async]
        , $(command "CornelisElaborate"        'doElaborate)        [Synchronous -> CommandOption
CmdSync Synchronous
Async, CommandOption
rw_complete]
        , $(command "CornelisPrevGoal"         'doPrevGoal)         [Synchronous -> CommandOption
CmdSync Synchronous
Async]
        , $(command "CornelisNextGoal"         'doNextGoal)         [Synchronous -> CommandOption
CmdSync Synchronous
Async]
        , $(command "CornelisGoToDefinition"   'doGotoDefinition)   [Synchronous -> CommandOption
CmdSync Synchronous
Async]
        , $(command "CornelisWhyInScope"       'doWhyInScope)       [Synchronous -> CommandOption
CmdSync Synchronous
Async]
        , $(command "CornelisNormalize"        'doNormalize)        [Synchronous -> CommandOption
CmdSync Synchronous
Async, CommandOption
cm_complete]
        , $(command "CornelisHelperFunc"       'doHelperFunc)       [Synchronous -> CommandOption
CmdSync Synchronous
Async, CommandOption
rw_complete]
        , $(command "CornelisQuestionToMeta"   'doQuestionToMeta)   [Synchronous -> CommandOption
CmdSync Synchronous
Async]
        , $(command "CornelisInc"              'doIncNextDigitSeq)  [Synchronous -> CommandOption
CmdSync Synchronous
Async]
        , $(command "CornelisDec"              'doDecNextDigitSeq)  [Synchronous -> CommandOption
CmdSync Synchronous
Async]
        , $(command "CornelisDebug"            'doDebug)            [Synchronous -> CommandOption
CmdSync Synchronous
Async, CommandOption
debug_complete]
        , $(command "CornelisCloseInfoWindows" 'doCloseInfoWindows) [Synchronous -> CommandOption
CmdSync Synchronous
Sync]
        , $(function "InternalCornelisRewriteModeCompletion" 'rewriteModeCompletion) Synchronous
Sync
        , $(function "InternalCornelisComputeModeCompletion" 'computeModeCompletion) Synchronous
Sync
        , $(function "InternalCornelisDebugCommandCompletion" 'debugCommandCompletion) Synchronous
Sync
        , $(function "InternalCornelisNotifyEdit" 'notifyEdit) Synchronous
Async
        ]
    }