Goals.hs

{-# 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 b ip = do
  ns <- asks ce_namespace
  extmap <- withBufferStuff b $ pure . bs_ip_exts
  fmap (fromMaybe (ip_interval' ip)) $
    case flip M.lookup extmap $ ip_id ip of
      Just i -> getExtmarkIntervalById ns b i
      Nothing -> pure Nothing


--------------------------------------------------------------------------------
-- | Move the vim cursor to a goal in the current window
findGoal :: Ord a => (AgdaPos -> AgdaPos -> Maybe a) -> Neovim CornelisEnv ()
findGoal hunt = withAgda $ do
  w <- vim_get_current_window
  b <- window_get_buffer w
  withBufferStuff b $ \bs -> do
    pos <- getWindowCursor w
    let goals = toList $ bs_ips bs
    judged_goals <- fmap catMaybes $ for goals $ \ip -> do
      int <- getIpInterval b ip
      pure
        . sequenceA
        . (id &&& hunt pos)
        $ iStart int
    case judged_goals of
      [] -> reportInfo "No hole matching predicate"
      _ -> do
        let pos' = fst $ maximumBy (comparing snd) judged_goals
        setWindowCursor w pos'


------------------------------------------------------------------------------
-- | Move the vim cursor to the previous interaction point.
prevGoal :: Neovim CornelisEnv ()
prevGoal =
  findGoal $ \pos goal ->
    case pos > goal of
      False -> Nothing
      True -> Just ( p_line goal .-. p_line pos
                   , p_col goal .-. p_col pos  -- TODO: This formula looks fishy
                   )


------------------------------------------------------------------------------
-- | Move the vim cursor to the next interaction point.
nextGoal :: Neovim CornelisEnv ()
nextGoal =
  findGoal $ \pos goal ->
    case pos < goal of
      False -> Nothing
      True -> Just $ Down ( p_line goal .-. p_line pos
                          , p_col goal .-. p_col 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 = do
  w <- nvim_get_current_win
  b <- window_get_buffer w
  p <- getWindowCursor w
  fmap (b, ) $ getGoalAtPos b p


getGoalAtPos
    :: Buffer
    -> AgdaPos
    -> Neovim CornelisEnv (Maybe (InteractionPoint Identity))
getGoalAtPos b p = do
  fmap (getFirst . fold) $ withBufferStuff b $ \bs -> do
    for (bs_ips bs) $ \ip -> do
      int <- getIpInterval b ip
      pure $ case containsPoint int p of
        False -> mempty
        True -> pure $ 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 f = getGoalAtCursor >>= \case
   (_, Nothing) -> do
     reportInfo "No goal at cursor"
     pure Nothing
   (b, Just ip) -> fmap Just $ f b 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 prompt_str on_goal on_no_goal = getGoalAtCursor >>= \case
    (_, Nothing) ->
        -- If there's no goal here, run `on_no_goal` on user input.
        prompt >>= on_no_goal
    (b, Just ip) -> do
        content <- getGoalContents b 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 T.null content
            then prompt >>= on_goal ip
            else on_goal ip (T.unpack content)
    where
        prompt = input prompt_str Nothing Nothing


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


------------------------------------------------------------------------------
-- | Like 'getGoalContents_maybe'.
getGoalContents :: Buffer -> InteractionPoint Identity -> Neovim CornelisEnv Text
getGoalContents b ip = fromMaybe "" <$> getGoalContentsMaybe b ip


------------------------------------------------------------------------------
-- | Replace all single @?@ tokens with interaction holes.
replaceQuestion :: Text -> Text
replaceQuestion = T.unwords . fmap go . T.words
  where
    go "(?" = "({! !}"
    go "?" = "{! !}"
    go x   =
      case T.dropWhileEnd (== ')') x of
        "?" -> "{! !}" <> T.drop 1 x
        _ -> x