{-# 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 b i = gets $ preview $ #cs_buffers . ix b . #bs_ips . ix i


respondToHelperFunction :: DisplayInfo -> Neovim env ()
respondToHelperFunction (HelperFunction sig) = setreg "\"" sig
respondToHelperFunction _ = pure ()


respond :: Buffer -> Response -> Neovim CornelisEnv ()
-- Update the buffer's goal map
respond b (DisplayInfo dp) = do
  respondToHelperFunction dp
  when (dp & hasn't #_GoalSpecific) $
    modifyBufferStuff b $ #bs_goals .~ dp
  goalWindow b dp
-- Update the buffer's interaction points map
respond b (InteractionPoints ips) = do
  let ips' = mapMaybe sequenceInteractionPoint ips
  modifyBufferStuff b $ #bs_ips .~ M.fromList (fmap (ip_id &&& id) ips')
-- Replace a function clause
respond b (MakeCase mkcase) = do
  doMakeCase b mkcase
  load
-- Replace the interaction point with a result
respond b (GiveAction result ip) = do
  let i = ip_id ip
  getInteractionPoint b i >>= \case
    Nothing -> reportError $ T.pack $ "Can't find interaction point " <> show i
    Just ip' -> do
      int <- getIpInterval b ip'
      replaceInterval b int $ replaceQuestion result
  load
-- Replace the interaction point with a result
respond b (SolveAll solutions) = do
  for_ solutions $ \(Solution i ex) ->
    getInteractionPoint b i >>= \case
      Nothing -> reportError $ T.pack $ "Can't find interaction point " <> show i
      Just ip -> do
        int <- getIpInterval b ip
        replaceInterval b int $ replaceQuestion ex
  load
respond b ClearHighlighting = do
  -- delete what we know about goto positions and stored extmarks
  modifyBufferStuff b $ \bs -> bs
    & #bs_goto_sites .~ mempty
    & #bs_ip_exts .~ mempty
  -- remove the extmarks and highlighting
  ns <- asks ce_namespace
  nvim_buf_clear_namespace b ns 0 (-1)
respond b (HighlightingInfo _remove hl) = do
  extmap <- highlightBuffer b hl
  modifyBufferStuff b $ \bs -> bs
    & #bs_ip_exts <>~ M.compose extmap (fmap ip_interval' $ bs_ips bs)
respond _ (RunningInfo _ x) = reportInfo x
respond _ ClearRunningInfo = reportInfo ""
respond b (JumpToError _ 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.
  when (fromOneIndexed @Int pos >= 50) $ do
    buf_lines <- nvim_buf_get_lines b 0 (-1) True
    let li = getLineIntervals buf_lines
    case lookupPoint li pos of
      Nothing -> reportError "invalid error report from Agda"
      Just (Pos l c) -> do
        ws <- fmap listToMaybe $ windowsForBuffer b
        for_ ws $ flip window_set_cursor (fromOneIndexed (oneIndex l), fromZeroIndexed c)
respond _ Status{} = pure ()
respond _ (Unknown k _) = reportError k

{-# HLINT ignore doMakeCase "Functor law" #-}
doMakeCase :: Buffer -> MakeCase -> Neovim CornelisEnv ()
doMakeCase b (RegularCase Function clauses ip) = do
  int' <- getIpInterval b ip
  let int = int' & #iStart . #p_col .~ toOneIndexed @Int 1
  ins <- getIndent b (zeroIndex (p_line (iStart int)))
  replaceInterval b int
    $ T.unlines
    $ fmap (T.replicate ins " " <>)
    $ fmap replaceQuestion clauses
-- TODO(sandy): It would be nice if Agda just gave us the bounds we're supposed to replace...
doMakeCase b (RegularCase ExtendedLambda clauses ip) = do
  ws <- windowsForBuffer b
  case listToMaybe ws of
    Nothing ->
      reportError
        "Unable to extend a lambda without having a window that contains the modified buffer. This is a limitation in cornelis."
    Just w -> do
      int' <- getIpInterval b ip
      Interval start end
        <- getLambdaClause w b (int' & #iStart . #p_col %~ (.+ Offset (- 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 }
      replaceInterval b (Interval (start & #p_col %~ (.+ Offset 1)) (end & #p_col %~ (.+ Offset (- 2))))
        $ T.unlines
        $ fmap replaceQuestion clauses & _tail %~ fmap (indent start)


------------------------------------------------------------------------------
-- | Indent a string with the given offset.
indent :: AgdaPos -> Text -> Text
indent (Pos _ c) s = mconcat
  [ flip T.replicate " " $ fromZeroIndexed (zeroIndex c) - 1
  , "; "
  , s
  ]


doPrevGoal :: CommandArguments -> Neovim CornelisEnv ()
doPrevGoal = const prevGoal

doNextGoal :: CommandArguments -> Neovim CornelisEnv ()
doNextGoal = const nextGoal


doIncNextDigitSeq :: CommandArguments -> Neovim CornelisEnv ()
doIncNextDigitSeq = const incNextDigitSeq

doDecNextDigitSeq :: CommandArguments -> Neovim CornelisEnv ()
doDecNextDigitSeq = const decNextDigitSeq


cornelisInit :: Neovim env CornelisEnv
cornelisInit = do
  (inchan, outchan) <- liftIO newChan
  ns <- nvim_create_namespace "cornelis"
  mvar <- liftIO $ newIORef $ CornelisState mempty mempty

  cfg <- getConfig

  let env = CornelisEnv mvar inchan ns cfg
  void $ withLocalEnv env $
    neovimAsync $ do
      forever $ reportExceptions $ do
        AgdaResp buffer next <- liftIO $ readChan outchan
        void $ neovimAsync $ reportExceptions $ respond buffer next
  pure env


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


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


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

  let rw_complete = CmdComplete "custom,InternalCornelisRewriteModeCompletion"
      cm_complete = CmdComplete "custom,InternalCornelisComputeModeCompletion"
      debug_complete = CmdComplete "custom,InternalCornelisDebugCommandCompletion"

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