Plugin.hs

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

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)
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 = withCurrentBuffer $ \b -> do
    agda <- getAgda b
    runIOTCM interaction agda


getDefinitionSites :: Buffer -> AgdaPos -> Neovim CornelisEnv (First DefinitionSite)
getDefinitionSites b p = withBufferStuff b $ \bs -> do
  marks <- getExtmarks b p
  pure $ flip foldMap marks $ \es ->
    First $ M.lookup (es_mark es) $ bs_goto_sites bs


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


gotoDefinition :: Neovim CornelisEnv ()
gotoDefinition = withAgda $ do
  w <- nvim_get_current_win
  rc <- getWindowCursor w
  b <- window_get_buffer w
  getDefinitionSites b rc >>= \case
    First Nothing -> reportInfo "No syntax under cursor."
    First (Just ds) -> do
      -- TODO(sandy): escape spaces
      vim_command $ "edit " <> ds_filepath ds
      b' <- window_get_buffer w
      contents <- fmap (T.unlines . V.toList) $ buffer_get_lines b' 0 (-1) False
      let buffer_idx = toBytes contents $ zeroIndex $ ds_position ds
      -- TODO(sandy): use window_set_cursor instead?
      vim_command $ "keepjumps normal! " <> T.pack (show buffer_idx) <> "go"


doLoad :: CommandArguments -> Neovim CornelisEnv ()
doLoad = const load

atomicSwapIORef :: IORef a -> a -> IO a
atomicSwapIORef r x = atomicModifyIORef r (\y -> (x , y))

load :: Neovim CornelisEnv ()
load = withAgda $ withCurrentBuffer $ \b -> do
  agda <- getAgda b
  ready <- liftIO $ readIORef $ a_ready agda
  if ready then do
    vim_command "noautocmd w"
    name <- buffer_get_name $ a_buffer agda
    flip runIOTCM agda $ Cmd_load name []
    buffer_get_number b >>= resetDiff
    updateLineIntervals b
  else vim_report_error "Agda is busy, not ready to load"

questionToMeta :: Buffer -> Neovim CornelisEnv ()
questionToMeta b = withBufferStuff b $ \bs -> do
  let ips = toList $ bs_ips bs

  res <- fmap fold $ for (sortOn (Down . iStart . ip_interval') ips) $ \ip -> do
    int <- getIpInterval b ip
    getGoalContents_maybe b ip >>= \case
      -- We only don't have a goal contents if we are a ? goal
      Nothing -> do
        replaceInterval b int "{! !}"
        let int' = int { iEnd = (iStart int) `addCol` Offset 5 }
        void $ highlightInterval b int' CornelisHole
        modifyBufferStuff b $
          #bs_ips %~ M.insert (ip_id ip) (ip & #ip_intervalM . #_Identity .~ int')

        pure $ Any True
      Just _ -> pure $ Any False

  -- Force a save if we replaced any goals
  case getAny res of
    True -> load
    False -> pure ()


doAllGoals :: CommandArguments -> Neovim CornelisEnv ()
doAllGoals = const allGoals


allGoals :: Neovim CornelisEnv ()
allGoals =
  withAgda $ withCurrentBuffer $ \b ->
    withBufferStuff b $ \bs -> do
      goalWindow b $ bs_goals bs


doRestart :: CommandArguments -> Neovim CornelisEnv ()
doRestart _ = do
  bs <- gets cs_buffers
  modify $ #cs_buffers .~ mempty
  liftIO $ for_ bs $ terminateProcess . a_hdl . bs_agda_proc

doAbort :: CommandArguments -> Neovim CornelisEnv ()
doAbort _ = withAgda $ withCurrentBuffer $ getAgda >=> runIOTCM Cmd_abort

normalizationMode :: Neovim env Rewrite
normalizationMode = pure HeadNormal

computeMode :: Neovim env ComputeMode
computeMode = pure DefaultCompute

solveOne :: CommandArguments -> Maybe String -> Neovim CornelisEnv ()
solveOne _ ms = withNormalizationMode ms $ \mode ->
  withAgda $ void $ withGoalAtCursor $ \b ip -> do
    agda <- getAgda b
    fp <- buffer_get_name b
    flip runIOTCM agda $
      Cmd_solveOne
        mode
        (ip_id ip)
        (mkAbsPathRnage fp $ ip_interval' ip)
        ""

autoOne :: CommandArguments -> Neovim CornelisEnv ()
autoOne _ = withAgda $ void $ withGoalAtCursor $ \b ip -> do
  agda <- getAgda b
  t <- getGoalContents b ip
  fp <- buffer_get_name b
  flip runIOTCM agda $
    Cmd_autoOne
      (ip_id ip)
      (mkAbsPathRnage fp $ ip_interval' ip)
      (T.unpack t)

withNormalizationMode :: Maybe String -> (Rewrite -> Neovim e ()) -> Neovim e ()
withNormalizationMode Nothing f = normalizationMode >>= f
withNormalizationMode (Just s) f =
  case readMaybe s of
    Nothing -> reportError $ "Invalid normalization mode: " <> T.pack s
    Just nm -> f nm

withComputeMode :: Maybe String -> (ComputeMode -> Neovim e ()) -> Neovim e ()
withComputeMode Nothing f = computeMode >>= f
withComputeMode (Just s) f =
  case readMaybe s of
    Nothing -> reportError $ "Invalid compute mode: "
      <> T.pack s
      <> ", expected one of "
      <> T.pack (show [(minBound :: ComputeMode) .. ])
    (Just cm) -> f cm

typeContext :: CommandArguments -> Maybe String -> Neovim CornelisEnv ()
typeContext _ ms = withNormalizationMode ms $ \mode ->
  withAgda $ void $ withGoalAtCursor $ \b goal -> do
    agda <- getAgda b
    fp <- buffer_get_name b
    flip runIOTCM agda $
      Cmd_goal_type_context
        mode
        (ip_id goal)
        (mkAbsPathRnage fp $ ip_interval' goal)
        ""

typeContextInfer :: CommandArguments -> Maybe String -> Neovim CornelisEnv ()
typeContextInfer _ ms = withNormalizationMode ms $ \mode ->
  withAgda $ void $ withGoalAtCursor $ \b ip -> do
    agda <- getAgda b
    fp <- buffer_get_name b
    contents <- getGoalContents b ip
    flip runIOTCM agda
      $ Cmd_goal_type_context_infer
          mode
          (ip_id ip)
          (mkAbsPathRnage fp $ ip_interval' ip)
      $ T.unpack contents

doRefine :: CommandArguments -> Neovim CornelisEnv ()
doRefine = const refine

refine :: Neovim CornelisEnv ()
refine = withAgda $ void $ withGoalAtCursor $ \b ip -> do
  agda <- getAgda b
  t <- getGoalContents b ip
  flip runIOTCM agda
    $ Cmd_refine_or_intro
        True
        (ip_id ip)
        -- We intentionally don't pass the range here; since doing so changes
        -- the response from Agda and requires a different codepath to perform
        -- the necessary edits.
        noRange
    $ T.unpack t

doGive :: CommandArguments -> Neovim CornelisEnv ()
doGive = const give

give :: Neovim CornelisEnv ()
give = withAgda $ void $ withGoalAtCursor $ \b ip -> do
  agda <- getAgda b
  t <- getGoalContents b ip
  flip runIOTCM agda
    $ Cmd_give
        WithoutForce
        (ip_id ip)
        -- We intentionally don't pass the range here; since doing so changes
        -- the response from Agda and requires a different codepath to perform
        -- the necessary edits.
        noRange
    $ T.unpack t

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

elaborate :: Rewrite -> Neovim CornelisEnv ()
elaborate mode = withAgda $ void $ withGoalAtCursor $ \b ip -> do
  agda <- getAgda b
  fp <- buffer_get_name b
  t <- getGoalContents b ip
  flip runIOTCM agda
    $ Cmd_elaborate_give
        mode
        (ip_id ip)
        (mkAbsPathRnage fp $ ip_interval' ip)
    $ T.unpack t

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

inferType :: Rewrite -> Neovim CornelisEnv ()
inferType mode = withAgda $ do
    cmd <- withGoalContentsOrPrompt "Infer type of what?"
        (\goal -> pure . Cmd_infer mode (ip_id goal) NoRange)
        (\input -> pure $ Cmd_infer_toplevel mode input)
    runInteraction cmd


doWhyInScope :: CommandArguments -> Neovim CornelisEnv ()
doWhyInScope _ = do
  thing <- input "Why is what in scope? " Nothing Nothing
  whyInScope thing

whyInScope :: Text -> Neovim CornelisEnv ()
whyInScope thing = do
  withAgda $ void $ withCurrentBuffer $ \b -> do
    agda <- getAgda b
    flip runIOTCM agda $ Cmd_why_in_scope_toplevel $ T.unpack thing

doNormalize :: CommandArguments -> Maybe String -> Neovim CornelisEnv ()
doNormalize _ ms = withComputeMode ms $ \mode ->
  withAgda $ void $ do
    (b , goal) <- getGoalAtCursor
    agda <- getAgda b
    fp <- buffer_get_name b
    case goal of
        Nothing -> do
            thing <- input "Normalize what? " Nothing Nothing
            flip runIOTCM agda $ Cmd_compute_toplevel mode thing
        Just ip -> do
            t <- getGoalContents b ip
            flip runIOTCM agda
              $ Cmd_compute
                  mode
                  (ip_id ip)
                  (mkAbsPathRnage fp $ ip_interval' ip)
              $ T.unpack t

helperFunc :: Rewrite -> Text -> Neovim CornelisEnv ()
helperFunc mode expr = do
  withAgda $ void $ withGoalAtCursor $ \b ip -> do
    agda <- getAgda b
    fp <- buffer_get_name b
    flip runIOTCM agda
      $ Cmd_helper_function
          mode
          (ip_id ip)
          (mkAbsPathRnage fp $ ip_interval' ip)
      $ T.unpack expr

doHelperFunc :: CommandArguments -> Maybe String -> Neovim CornelisEnv ()
doHelperFunc _ ms = withNormalizationMode ms $ \mode -> do
  expr <- input "Expression: " Nothing Nothing
  helperFunc mode expr

doCaseSplit :: CommandArguments -> Neovim CornelisEnv ()
doCaseSplit _ = withAgda $ void $ withGoalAtCursor $ \b ip -> do
  contents <- fmap T.strip $ getGoalContents b ip
  thing <- bool (pure contents)
                (input @Text "Split on what?" Nothing Nothing)
         $ T.null contents
  caseSplit thing

caseSplit :: Text -> Neovim CornelisEnv ()
caseSplit thing = withAgda $ void $ withGoalAtCursor $ \b ip -> do
  agda <- getAgda b
  fp <- buffer_get_name b
  flip runIOTCM agda
    $ Cmd_make_case
        (ip_id ip)
        (mkAbsPathRnage fp $ ip_interval' ip)
    $ T.unpack thing

doQuestionToMeta :: CommandArguments -> Neovim CornelisEnv ()
doQuestionToMeta _ = withCurrentBuffer questionToMeta

goalWindow :: Buffer -> DisplayInfo ->  Neovim CornelisEnv ()
goalWindow b = showInfoWindow b . prettyGoals

computeModeCompletion :: String -> String -> Int -> Neovim env String
computeModeCompletion _ _ _ =
  pure $ unlines $ fmap show $ enumFromTo @ComputeMode minBound maxBound

rewriteModeCompletion :: String -> String -> Int -> Neovim env String
rewriteModeCompletion _ _ _ =
  pure $ unlines $ fmap show $ enumFromTo @Rewrite minBound maxBound

debugCommandCompletion :: String -> String -> Int -> Neovim env String
debugCommandCompletion _ _ _ =
  pure $ unlines $ fmap show $ enumFromTo @DebugCommand minBound maxBound


doDebug :: CommandArguments -> String -> Neovim CornelisEnv ()
doDebug _ str =
  case readMaybe str of
    Just DumpIPs ->
      withAgda $ withCurrentBuffer $ \b -> withBufferStuff b $ \bs -> do
        traceMX "ips" $ bs_ips bs
        traceMX "ipexts" $ bs_ip_exts bs
    Nothing ->
      vim_report_error $ T.pack $ "No matching debug command for " <> show str

-- | The @on_bytes@ callback required by @nvim_buf_attach@.
notifyEdit
  :: Text -- ^ the string "bytes"
  -> BufferNum -- ^ buffer handle
  -> Bool -- ^ b:changedtick
  -> Int -- ^ start row of the changed text (zero-indexed)
  -> Int -- ^ start column of the changed text
  -> Int -- ^ byte offset of the changed text (from the start of the buffer)
  -> Int -- ^ old end row of the changed text (relative to the start row)
  -> Int -- ^ old end column of the changed text
  -> Int -- ^ old end byte length of the changed text
  -> Int -- ^ new end row of the changed text (relative to the start row)
  -> Int -- ^ new end column of the changed text
  -> Int -- ^ new end byte length of the changed text
  -> Neovim CornelisEnv Bool  -- ^ Return True to detach
notifyEdit _ buf _ sr sc _ er ec _ fr fc _ = do
  recordUpdate buf (Replace (pos sr sc) (range er ec) (range fr fc))
  pure False
  where
    pos l c = Colline (toZeroIndexed l) (toZeroIndexed c)
    range l c = Vallee (Offset l) (Offset c)