{-# LANGUAGE OverloadedStrings #-}

module Cornelis.Goals where

import           Control.Arrow ((&&&))
import           Control.Lens
import           Cornelis.Agda (withAgda)
import           Cornelis.Offsets
import           Cornelis.Types
import           Cornelis.Utils
import           Cornelis.Vim
import           Data.Foldable (toList, fold)
import           Data.List
import qualified Data.Map as M
import           Data.Maybe
import           Data.Ord
import qualified Data.Text as T
import           Data.Traversable (for)
import           Neovim
import           Neovim.API.Text
import           Neovim.User.Input (input)


------------------------------------------------------------------------------
-- | Get the spanning interval of an interaction point. If we already have
-- highlighting information from vim, use the extmark for this goal, otherwise
-- using the interval that Agda knows about.
getIpInterval :: Buffer -> InteractionPoint Identity -> Neovim CornelisEnv AgdaInterval
getIpInterval :: Buffer
-> InteractionPoint Identity -> Neovim CornelisEnv AgdaInterval
getIpInterval Buffer
b InteractionPoint Identity
ip = do
  Int64
ns <- (CornelisEnv -> Int64) -> Neovim CornelisEnv Int64
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks CornelisEnv -> Int64
ce_namespace
  Map InteractionId Extmark
extmap <- Buffer
-> (BufferStuff -> Neovim CornelisEnv (Map InteractionId Extmark))
-> Neovim CornelisEnv (Map InteractionId Extmark)
forall a.
Monoid a =>
Buffer
-> (BufferStuff -> Neovim CornelisEnv a) -> Neovim CornelisEnv a
withBufferStuff Buffer
b ((BufferStuff -> Neovim CornelisEnv (Map InteractionId Extmark))
 -> Neovim CornelisEnv (Map InteractionId Extmark))
-> (BufferStuff -> Neovim CornelisEnv (Map InteractionId Extmark))
-> Neovim CornelisEnv (Map InteractionId Extmark)
forall a b. (a -> b) -> a -> b
$ Map InteractionId Extmark
-> Neovim CornelisEnv (Map InteractionId Extmark)
forall a. a -> Neovim CornelisEnv a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map InteractionId Extmark
 -> Neovim CornelisEnv (Map InteractionId Extmark))
-> (BufferStuff -> Map InteractionId Extmark)
-> BufferStuff
-> Neovim CornelisEnv (Map InteractionId Extmark)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BufferStuff -> Map InteractionId Extmark
bs_ip_exts
  (Maybe AgdaInterval -> AgdaInterval)
-> Neovim CornelisEnv (Maybe AgdaInterval)
-> Neovim CornelisEnv AgdaInterval
forall a b.
(a -> b) -> Neovim CornelisEnv a -> Neovim CornelisEnv b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (AgdaInterval -> Maybe AgdaInterval -> AgdaInterval
forall a. a -> Maybe a -> a
fromMaybe (InteractionPoint Identity -> AgdaInterval
ip_interval' InteractionPoint Identity
ip)) (Neovim CornelisEnv (Maybe AgdaInterval)
 -> Neovim CornelisEnv AgdaInterval)
-> Neovim CornelisEnv (Maybe AgdaInterval)
-> Neovim CornelisEnv AgdaInterval
forall a b. (a -> b) -> a -> b
$
    case (InteractionId -> Map InteractionId Extmark -> Maybe Extmark)
-> Map InteractionId Extmark -> InteractionId -> Maybe Extmark
forall a b c. (a -> b -> c) -> b -> a -> c
flip InteractionId -> Map InteractionId Extmark -> Maybe Extmark
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Map InteractionId Extmark
extmap (InteractionId -> Maybe Extmark) -> InteractionId -> Maybe Extmark
forall a b. (a -> b) -> a -> b
$ InteractionPoint Identity -> InteractionId
forall (f :: * -> *). InteractionPoint f -> InteractionId
ip_id InteractionPoint Identity
ip of
      Just Extmark
i -> Int64
-> Buffer -> Extmark -> Neovim CornelisEnv (Maybe AgdaInterval)
forall env.
Int64 -> Buffer -> Extmark -> Neovim env (Maybe AgdaInterval)
getExtmarkIntervalById Int64
ns Buffer
b Extmark
i
      Maybe Extmark
Nothing -> Maybe AgdaInterval -> Neovim CornelisEnv (Maybe AgdaInterval)
forall a. a -> Neovim CornelisEnv a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe AgdaInterval
forall a. Maybe a
Nothing


--------------------------------------------------------------------------------
-- | Move the vim cursor to a goal in the current window
findGoal :: Ord a => (AgdaPos -> AgdaPos -> Maybe a) -> Neovim CornelisEnv ()
findGoal :: forall a.
Ord a =>
(AgdaPos -> AgdaPos -> Maybe a) -> Neovim CornelisEnv ()
findGoal AgdaPos -> AgdaPos -> Maybe a
hunt = 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
vim_get_current_window
  Buffer
b <- Window -> Neovim CornelisEnv Buffer
forall env. Window -> Neovim env Buffer
window_get_buffer Window
w
  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
    AgdaPos
pos <- Window -> Neovim CornelisEnv AgdaPos
forall env. Window -> Neovim env AgdaPos
getWindowCursor Window
w
    let goals :: [InteractionPoint Identity]
goals = 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
    [(AgdaPos, a)]
judged_goals <- ([Maybe (AgdaPos, a)] -> [(AgdaPos, a)])
-> Neovim CornelisEnv [Maybe (AgdaPos, a)]
-> Neovim CornelisEnv [(AgdaPos, a)]
forall a b.
(a -> b) -> Neovim CornelisEnv a -> Neovim CornelisEnv b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Maybe (AgdaPos, a)] -> [(AgdaPos, a)]
forall a. [Maybe a] -> [a]
catMaybes (Neovim CornelisEnv [Maybe (AgdaPos, a)]
 -> Neovim CornelisEnv [(AgdaPos, a)])
-> Neovim CornelisEnv [Maybe (AgdaPos, a)]
-> Neovim CornelisEnv [(AgdaPos, a)]
forall a b. (a -> b) -> a -> b
$ [InteractionPoint Identity]
-> (InteractionPoint Identity
    -> Neovim CornelisEnv (Maybe (AgdaPos, a)))
-> Neovim CornelisEnv [Maybe (AgdaPos, a)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [InteractionPoint Identity]
goals ((InteractionPoint Identity
  -> Neovim CornelisEnv (Maybe (AgdaPos, a)))
 -> Neovim CornelisEnv [Maybe (AgdaPos, a)])
-> (InteractionPoint Identity
    -> Neovim CornelisEnv (Maybe (AgdaPos, a)))
-> Neovim CornelisEnv [Maybe (AgdaPos, a)]
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
      Maybe (AgdaPos, a) -> Neovim CornelisEnv (Maybe (AgdaPos, a))
forall a. a -> Neovim CornelisEnv a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
        (Maybe (AgdaPos, a) -> Neovim CornelisEnv (Maybe (AgdaPos, a)))
-> (AgdaPos -> Maybe (AgdaPos, a))
-> AgdaPos
-> Neovim CornelisEnv (Maybe (AgdaPos, a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (AgdaPos, Maybe a) -> Maybe (AgdaPos, a)
forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
forall (f :: * -> *) a.
Applicative f =>
(AgdaPos, f a) -> f (AgdaPos, a)
sequenceA
        ((AgdaPos, Maybe a) -> Maybe (AgdaPos, a))
-> (AgdaPos -> (AgdaPos, Maybe a)) -> AgdaPos -> Maybe (AgdaPos, a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (AgdaPos -> AgdaPos
forall a. a -> a
id (AgdaPos -> AgdaPos)
-> (AgdaPos -> Maybe a) -> AgdaPos -> (AgdaPos, Maybe a)
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')
&&& AgdaPos -> AgdaPos -> Maybe a
hunt AgdaPos
pos)
        (AgdaPos -> Neovim CornelisEnv (Maybe (AgdaPos, a)))
-> AgdaPos -> Neovim CornelisEnv (Maybe (AgdaPos, a))
forall a b. (a -> b) -> a -> b
$ AgdaInterval -> AgdaPos
forall p. Interval p -> p
iStart AgdaInterval
int
    case [(AgdaPos, a)]
judged_goals of
      [] -> Text -> Neovim CornelisEnv ()
forall env. Text -> Neovim env ()
reportInfo Text
"No hole matching predicate"
      [(AgdaPos, a)]
_ -> do
        let pos' :: AgdaPos
pos' = (AgdaPos, a) -> AgdaPos
forall a b. (a, b) -> a
fst ((AgdaPos, a) -> AgdaPos) -> (AgdaPos, a) -> AgdaPos
forall a b. (a -> b) -> a -> b
$ ((AgdaPos, a) -> (AgdaPos, a) -> Ordering)
-> [(AgdaPos, a)] -> (AgdaPos, a)
forall (t :: * -> *) a.
Foldable t =>
(a -> a -> Ordering) -> t a -> a
maximumBy (((AgdaPos, a) -> a) -> (AgdaPos, a) -> (AgdaPos, a) -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing (AgdaPos, a) -> a
forall a b. (a, b) -> b
snd) [(AgdaPos, a)]
judged_goals
        Window -> AgdaPos -> Neovim CornelisEnv ()
forall env. Window -> AgdaPos -> Neovim env ()
setWindowCursor Window
w AgdaPos
pos'


------------------------------------------------------------------------------
-- | Move the vim cursor to the previous interaction point.
prevGoal :: Neovim CornelisEnv ()
prevGoal :: Neovim CornelisEnv ()
prevGoal =
  (AgdaPos -> AgdaPos -> Maybe (Offset 'Line, Offset 'CodePoint))
-> Neovim CornelisEnv ()
forall a.
Ord a =>
(AgdaPos -> AgdaPos -> Maybe a) -> Neovim CornelisEnv ()
findGoal ((AgdaPos -> AgdaPos -> Maybe (Offset 'Line, Offset 'CodePoint))
 -> Neovim CornelisEnv ())
-> (AgdaPos -> AgdaPos -> Maybe (Offset 'Line, Offset 'CodePoint))
-> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ \AgdaPos
pos AgdaPos
goal ->
    case AgdaPos
pos AgdaPos -> AgdaPos -> Bool
forall a. Ord a => a -> a -> Bool
> AgdaPos
goal of
      Bool
False -> Maybe (Offset 'Line, Offset 'CodePoint)
forall a. Maybe a
Nothing
      Bool
True -> (Offset 'Line, Offset 'CodePoint)
-> Maybe (Offset 'Line, Offset 'CodePoint)
forall a. a -> Maybe a
Just ( AgdaPos -> Index 'Line 'OneIndexed
forall (e :: Unit) (i :: Indexing) (j :: Indexing).
Pos e i j -> Index 'Line i
p_line AgdaPos
goal Index 'Line 'OneIndexed -> Index 'Line 'OneIndexed -> Offset 'Line
forall (e :: Unit) (i :: Indexing).
Index e i -> Index e i -> Offset e
.-. AgdaPos -> Index 'Line 'OneIndexed
forall (e :: Unit) (i :: Indexing) (j :: Indexing).
Pos e i j -> Index 'Line i
p_line AgdaPos
pos
                   , AgdaPos -> Index 'CodePoint 'OneIndexed
forall (e :: Unit) (i :: Indexing) (j :: Indexing).
Pos e i j -> Index e j
p_col AgdaPos
goal Index 'CodePoint 'OneIndexed
-> Index 'CodePoint 'OneIndexed -> Offset 'CodePoint
forall (e :: Unit) (i :: Indexing).
Index e i -> Index e i -> Offset e
.-. AgdaPos -> Index 'CodePoint 'OneIndexed
forall (e :: Unit) (i :: Indexing) (j :: Indexing).
Pos e i j -> Index e j
p_col AgdaPos
pos  -- TODO: This formula looks fishy
                   )


------------------------------------------------------------------------------
-- | Move the vim cursor to the next interaction point.
nextGoal :: Neovim CornelisEnv ()
nextGoal :: Neovim CornelisEnv ()
nextGoal =
  (AgdaPos
 -> AgdaPos -> Maybe (Down (Offset 'Line, Offset 'CodePoint)))
-> Neovim CornelisEnv ()
forall a.
Ord a =>
(AgdaPos -> AgdaPos -> Maybe a) -> Neovim CornelisEnv ()
findGoal ((AgdaPos
  -> AgdaPos -> Maybe (Down (Offset 'Line, Offset 'CodePoint)))
 -> Neovim CornelisEnv ())
-> (AgdaPos
    -> AgdaPos -> Maybe (Down (Offset 'Line, Offset 'CodePoint)))
-> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ \AgdaPos
pos AgdaPos
goal ->
    case AgdaPos
pos AgdaPos -> AgdaPos -> Bool
forall a. Ord a => a -> a -> Bool
< AgdaPos
goal of
      Bool
False -> Maybe (Down (Offset 'Line, Offset 'CodePoint))
forall a. Maybe a
Nothing
      Bool
True -> Down (Offset 'Line, Offset 'CodePoint)
-> Maybe (Down (Offset 'Line, Offset 'CodePoint))
forall a. a -> Maybe a
Just (Down (Offset 'Line, Offset 'CodePoint)
 -> Maybe (Down (Offset 'Line, Offset 'CodePoint)))
-> Down (Offset 'Line, Offset 'CodePoint)
-> Maybe (Down (Offset 'Line, Offset 'CodePoint))
forall a b. (a -> b) -> a -> b
$ (Offset 'Line, Offset 'CodePoint)
-> Down (Offset 'Line, Offset 'CodePoint)
forall a. a -> Down a
Down ( AgdaPos -> Index 'Line 'OneIndexed
forall (e :: Unit) (i :: Indexing) (j :: Indexing).
Pos e i j -> Index 'Line i
p_line AgdaPos
goal Index 'Line 'OneIndexed -> Index 'Line 'OneIndexed -> Offset 'Line
forall (e :: Unit) (i :: Indexing).
Index e i -> Index e i -> Offset e
.-. AgdaPos -> Index 'Line 'OneIndexed
forall (e :: Unit) (i :: Indexing) (j :: Indexing).
Pos e i j -> Index 'Line i
p_line AgdaPos
pos
                          , AgdaPos -> Index 'CodePoint 'OneIndexed
forall (e :: Unit) (i :: Indexing) (j :: Indexing).
Pos e i j -> Index e j
p_col AgdaPos
goal Index 'CodePoint 'OneIndexed
-> Index 'CodePoint 'OneIndexed -> Offset 'CodePoint
forall (e :: Unit) (i :: Indexing).
Index e i -> Index e i -> Offset e
.-. AgdaPos -> Index 'CodePoint 'OneIndexed
forall (e :: Unit) (i :: Indexing) (j :: Indexing).
Pos e i j -> Index e j
p_col AgdaPos
pos
                          )

------------------------------------------------------------------------------
-- | Uses highlighting extmarks to determine what a hole is; since the user
-- might have typed inside of a {! !} goal since they last saved.
getGoalAtCursor :: Neovim CornelisEnv (Buffer, Maybe (InteractionPoint Identity))
getGoalAtCursor :: Neovim CornelisEnv (Buffer, Maybe (InteractionPoint Identity))
getGoalAtCursor = do
  Window
w <- Neovim CornelisEnv Window
forall env. Neovim env Window
nvim_get_current_win
  Buffer
b <- Window -> Neovim CornelisEnv Buffer
forall env. Window -> Neovim env Buffer
window_get_buffer Window
w
  AgdaPos
p <- Window -> Neovim CornelisEnv AgdaPos
forall env. Window -> Neovim env AgdaPos
getWindowCursor Window
w
  (Maybe (InteractionPoint Identity)
 -> (Buffer, Maybe (InteractionPoint Identity)))
-> Neovim CornelisEnv (Maybe (InteractionPoint Identity))
-> Neovim CornelisEnv (Buffer, Maybe (InteractionPoint Identity))
forall a b.
(a -> b) -> Neovim CornelisEnv a -> Neovim CornelisEnv b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Buffer
b, ) (Neovim CornelisEnv (Maybe (InteractionPoint Identity))
 -> Neovim CornelisEnv (Buffer, Maybe (InteractionPoint Identity)))
-> Neovim CornelisEnv (Maybe (InteractionPoint Identity))
-> Neovim CornelisEnv (Buffer, Maybe (InteractionPoint Identity))
forall a b. (a -> b) -> a -> b
$ Buffer
-> AgdaPos
-> Neovim CornelisEnv (Maybe (InteractionPoint Identity))
getGoalAtPos Buffer
b AgdaPos
p


getGoalAtPos
    :: Buffer
    -> AgdaPos
    -> Neovim CornelisEnv (Maybe (InteractionPoint Identity))
getGoalAtPos :: Buffer
-> AgdaPos
-> Neovim CornelisEnv (Maybe (InteractionPoint Identity))
getGoalAtPos Buffer
b AgdaPos
p = do
  (Map InteractionId (First (InteractionPoint Identity))
 -> Maybe (InteractionPoint Identity))
-> Neovim
     CornelisEnv (Map InteractionId (First (InteractionPoint Identity)))
-> Neovim CornelisEnv (Maybe (InteractionPoint Identity))
forall a b.
(a -> b) -> Neovim CornelisEnv a -> Neovim CornelisEnv b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (First (InteractionPoint Identity)
-> Maybe (InteractionPoint Identity)
forall a. First a -> Maybe a
getFirst (First (InteractionPoint Identity)
 -> Maybe (InteractionPoint Identity))
-> (Map InteractionId (First (InteractionPoint Identity))
    -> First (InteractionPoint Identity))
-> Map InteractionId (First (InteractionPoint Identity))
-> Maybe (InteractionPoint Identity)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map InteractionId (First (InteractionPoint Identity))
-> First (InteractionPoint Identity)
forall m. Monoid m => Map InteractionId m -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold) (Neovim
   CornelisEnv (Map InteractionId (First (InteractionPoint Identity)))
 -> Neovim CornelisEnv (Maybe (InteractionPoint Identity)))
-> Neovim
     CornelisEnv (Map InteractionId (First (InteractionPoint Identity)))
-> Neovim CornelisEnv (Maybe (InteractionPoint Identity))
forall a b. (a -> b) -> a -> b
$ Buffer
-> (BufferStuff
    -> Neovim
         CornelisEnv
         (Map InteractionId (First (InteractionPoint Identity))))
-> Neovim
     CornelisEnv (Map InteractionId (First (InteractionPoint Identity)))
forall a.
Monoid a =>
Buffer
-> (BufferStuff -> Neovim CornelisEnv a) -> Neovim CornelisEnv a
withBufferStuff Buffer
b ((BufferStuff
  -> Neovim
       CornelisEnv
       (Map InteractionId (First (InteractionPoint Identity))))
 -> Neovim
      CornelisEnv
      (Map InteractionId (First (InteractionPoint Identity))))
-> (BufferStuff
    -> Neovim
         CornelisEnv
         (Map InteractionId (First (InteractionPoint Identity))))
-> Neovim
     CornelisEnv (Map InteractionId (First (InteractionPoint Identity)))
forall a b. (a -> b) -> a -> b
$ \BufferStuff
bs -> do
    Map InteractionId (InteractionPoint Identity)
-> (InteractionPoint Identity
    -> Neovim CornelisEnv (First (InteractionPoint Identity)))
-> Neovim
     CornelisEnv (Map InteractionId (First (InteractionPoint Identity)))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for (BufferStuff -> Map InteractionId (InteractionPoint Identity)
bs_ips BufferStuff
bs) ((InteractionPoint Identity
  -> Neovim CornelisEnv (First (InteractionPoint Identity)))
 -> Neovim
      CornelisEnv
      (Map InteractionId (First (InteractionPoint Identity))))
-> (InteractionPoint Identity
    -> Neovim CornelisEnv (First (InteractionPoint Identity)))
-> Neovim
     CornelisEnv (Map InteractionId (First (InteractionPoint Identity)))
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
      First (InteractionPoint Identity)
-> Neovim CornelisEnv (First (InteractionPoint Identity))
forall a. a -> Neovim CornelisEnv a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (First (InteractionPoint Identity)
 -> Neovim CornelisEnv (First (InteractionPoint Identity)))
-> First (InteractionPoint Identity)
-> Neovim CornelisEnv (First (InteractionPoint Identity))
forall a b. (a -> b) -> a -> b
$ case AgdaInterval -> AgdaPos -> Bool
forall p. Ord p => Interval p -> p -> Bool
containsPoint AgdaInterval
int AgdaPos
p of
        Bool
False -> First (InteractionPoint Identity)
forall a. Monoid a => a
mempty
        Bool
True -> InteractionPoint Identity -> First (InteractionPoint Identity)
forall a. a -> First a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (InteractionPoint Identity -> First (InteractionPoint Identity))
-> InteractionPoint Identity -> First (InteractionPoint Identity)
forall a b. (a -> b) -> a -> b
$ InteractionPoint Identity
ip { ip_intervalM = Identity int }

------------------------------------------------------------------------------
-- | Run a continuation on a goal at the current position in the current
-- buffer, if it exists.
withGoalAtCursor
    :: (Buffer -> InteractionPoint Identity -> Neovim CornelisEnv a)
    -> Neovim CornelisEnv (Maybe a)
withGoalAtCursor :: forall a.
(Buffer -> InteractionPoint Identity -> Neovim CornelisEnv a)
-> Neovim CornelisEnv (Maybe a)
withGoalAtCursor Buffer -> InteractionPoint Identity -> Neovim CornelisEnv a
f = Neovim CornelisEnv (Buffer, Maybe (InteractionPoint Identity))
getGoalAtCursor Neovim CornelisEnv (Buffer, Maybe (InteractionPoint Identity))
-> ((Buffer, Maybe (InteractionPoint Identity))
    -> Neovim CornelisEnv (Maybe a))
-> Neovim CornelisEnv (Maybe a)
forall a b.
Neovim CornelisEnv a
-> (a -> Neovim CornelisEnv b) -> Neovim CornelisEnv b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
   (Buffer
_, Maybe (InteractionPoint Identity)
Nothing) -> do
     Text -> Neovim CornelisEnv ()
forall env. Text -> Neovim env ()
reportInfo Text
"No goal at cursor"
     Maybe a -> Neovim CornelisEnv (Maybe a)
forall a. a -> Neovim CornelisEnv a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe a
forall a. Maybe a
Nothing
   (Buffer
b, Just InteractionPoint Identity
ip) -> (a -> Maybe a)
-> Neovim CornelisEnv a -> Neovim CornelisEnv (Maybe a)
forall a b.
(a -> b) -> Neovim CornelisEnv a -> Neovim CornelisEnv b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Maybe a
forall a. a -> Maybe a
Just (Neovim CornelisEnv a -> Neovim CornelisEnv (Maybe a))
-> Neovim CornelisEnv a -> Neovim CornelisEnv (Maybe a)
forall a b. (a -> b) -> a -> b
$ Buffer -> InteractionPoint Identity -> Neovim CornelisEnv a
f Buffer
b InteractionPoint Identity
ip

------------------------------------------------------------------------------
-- | Run the first continuation on the goal at the current position,
-- otherwise run the second continuation.
--
-- If there is a non-empty hole, provide its content to the first continuation.
-- If the hole is empty, prompt for input and provide that.
--
-- If there is no goal, prompt the user for input and run the second continuation.
withGoalContentsOrPrompt
    :: String
    -- ^ Text to print when prompting the user for input
    -> (InteractionPoint Identity -> String -> Neovim CornelisEnv a)
    -- ^ Continuation to run on goal, with hole contents
    -> (String -> Neovim CornelisEnv a)
    -- ^ Continuation to run on user input if there's no goal here
    -> Neovim CornelisEnv a
withGoalContentsOrPrompt :: forall a.
String
-> (InteractionPoint Identity -> String -> Neovim CornelisEnv a)
-> (String -> Neovim CornelisEnv a)
-> Neovim CornelisEnv a
withGoalContentsOrPrompt String
prompt_str InteractionPoint Identity -> String -> Neovim CornelisEnv a
on_goal String -> Neovim CornelisEnv a
on_no_goal = Neovim CornelisEnv (Buffer, Maybe (InteractionPoint Identity))
getGoalAtCursor Neovim CornelisEnv (Buffer, Maybe (InteractionPoint Identity))
-> ((Buffer, Maybe (InteractionPoint Identity))
    -> Neovim CornelisEnv a)
-> Neovim CornelisEnv a
forall a b.
Neovim CornelisEnv a
-> (a -> Neovim CornelisEnv b) -> Neovim CornelisEnv b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    (Buffer
_, Maybe (InteractionPoint Identity)
Nothing) ->
        -- If there's no goal here, run `on_no_goal` on user input.
        Neovim CornelisEnv String
forall {env}. Neovim env String
prompt Neovim CornelisEnv String
-> (String -> Neovim CornelisEnv a) -> Neovim CornelisEnv a
forall a b.
Neovim CornelisEnv a
-> (a -> Neovim CornelisEnv b) -> Neovim CornelisEnv b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= String -> Neovim CornelisEnv a
on_no_goal
    (Buffer
b, Just InteractionPoint Identity
ip) -> do
        Text
content <- Buffer -> InteractionPoint Identity -> Neovim CornelisEnv Text
getGoalContents Buffer
b InteractionPoint Identity
ip
        -- If there is a goal under the cursor, but it's contents
        -- are empty, prompt the user for input.  Otherwise, unpack
        -- the hole contents are provide that.
        if Text -> Bool
T.null Text
content
            then Neovim CornelisEnv String
forall {env}. Neovim env String
prompt Neovim CornelisEnv String
-> (String -> Neovim CornelisEnv a) -> Neovim CornelisEnv a
forall a b.
Neovim CornelisEnv a
-> (a -> Neovim CornelisEnv b) -> Neovim CornelisEnv b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= InteractionPoint Identity -> String -> Neovim CornelisEnv a
on_goal InteractionPoint Identity
ip
            else InteractionPoint Identity -> String -> Neovim CornelisEnv a
on_goal InteractionPoint Identity
ip (Text -> String
T.unpack Text
content)
    where
        prompt :: Neovim env String
prompt = String -> Maybe String -> Maybe String -> Neovim env String
forall result env.
NvimObject result =>
String -> Maybe String -> Maybe String -> Neovim env result
input String
prompt_str Maybe String
forall a. Maybe a
Nothing Maybe String
forall a. Maybe a
Nothing


------------------------------------------------------------------------------
-- | Get the contents of a goal.
getGoalContentsMaybe :: Buffer -> InteractionPoint Identity -> Neovim CornelisEnv (Maybe Text)
getGoalContentsMaybe :: Buffer
-> InteractionPoint Identity -> Neovim CornelisEnv (Maybe Text)
getGoalContentsMaybe Buffer
b InteractionPoint Identity
ip = do
  AgdaInterval
int <- Buffer
-> InteractionPoint Identity -> Neovim CornelisEnv AgdaInterval
getIpInterval Buffer
b InteractionPoint Identity
ip
  Text
iv <- (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 -> AgdaInterval -> Neovim CornelisEnv Text
forall env. Buffer -> AgdaInterval -> Neovim env Text
getBufferInterval Buffer
b AgdaInterval
int
  Maybe Text -> Neovim CornelisEnv (Maybe Text)
forall a. a -> Neovim CornelisEnv a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe Text -> Neovim CornelisEnv (Maybe Text))
-> Maybe Text -> Neovim CornelisEnv (Maybe Text)
forall a b. (a -> b) -> a -> b
$ case Text
iv of
    Text
"?" -> Maybe Text
forall a. Maybe a
Nothing
         -- Chop off {!, !} and trim any spaces.
    Text
_ -> Text -> Maybe Text
forall a. a -> Maybe a
Just (Text -> Maybe Text) -> Text -> Maybe Text
forall a b. (a -> b) -> a -> b
$ Text -> Text
T.strip (Text -> Text) -> Text -> Text
forall a b. (a -> b) -> a -> b
$ Int -> Text -> Text
T.dropEnd Int
2 (Text -> Text) -> Text -> Text
forall a b. (a -> b) -> a -> b
$ Int -> Text -> Text
T.drop Int
2 Text
iv


------------------------------------------------------------------------------
-- | Like 'getGoalContents_maybe'.
getGoalContents :: Buffer -> InteractionPoint Identity -> Neovim CornelisEnv Text
getGoalContents :: Buffer -> InteractionPoint Identity -> Neovim CornelisEnv Text
getGoalContents Buffer
b InteractionPoint Identity
ip = Text -> Maybe Text -> Text
forall a. a -> Maybe a -> a
fromMaybe Text
"" (Maybe Text -> Text)
-> Neovim CornelisEnv (Maybe Text) -> Neovim CornelisEnv Text
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Buffer
-> InteractionPoint Identity -> Neovim CornelisEnv (Maybe Text)
getGoalContentsMaybe Buffer
b InteractionPoint Identity
ip


------------------------------------------------------------------------------
-- | Replace all single @?@ tokens with interaction holes.
replaceQuestion :: Text -> Text
replaceQuestion :: Text -> Text
replaceQuestion = [Text] -> Text
T.unwords ([Text] -> Text) -> (Text -> [Text]) -> Text -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (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
go ([Text] -> [Text]) -> (Text -> [Text]) -> Text -> [Text]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> [Text]
T.words
  where
    go :: Text -> Text
go Text
"(?" = Text
"({! !}"
    go Text
"?" = Text
"{! !}"
    go Text
x   =
      case (Char -> Bool) -> Text -> Text
T.dropWhileEnd (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
')') Text
x of
        Text
"?" -> Text
"{! !}" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text -> Text
T.drop Int
1 Text
x
        Text
_ -> Text
x