{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE DeriveAnyClass        #-}
{-# LANGUAGE DeriveGeneric         #-}
{-# LANGUAGE DerivingStrategies    #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings     #-}
{-# LANGUAGE StandaloneDeriving    #-}
{-# LANGUAGE UndecidableInstances  #-}

{-# OPTIONS_GHC -Wno-orphans #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
{-# HLINT ignore "Use camelCase" #-}

module Cornelis.Types
  ( module Cornelis.Types
  , InteractionId
  , Buffer
  , Window
  , Text
  , traceMX
  , HasCallStack
  ) where

import Control.Concurrent.Chan.Unagi (InChan)
import Control.Monad.State.Class
import Cornelis.Debug
import Cornelis.Offsets (Pos(..), Interval(..), AgdaIndex, AgdaPos, AgdaInterval, VimIndex, LineNumber, Indexing(..))
import Cornelis.Types.Agda (InteractionId)
import Data.Aeson hiding (Error)
import Data.Char (toLower)
import Data.Functor.Identity
import Data.Generics.Labels ()
import Data.IORef
import Data.IntervalMap.FingerTree (IntervalMap)
import Data.Map (Map)
import Data.Maybe (listToMaybe)
import Data.Text (Text)
import DiffLoc (Diff, Colline)
import GHC.Generics
import GHC.Stack
import Neovim hiding (err)
import Neovim.API.Text (Buffer(..), Window)
import System.Process (ProcessHandle)

deriving stock instance Ord Buffer

data Agda = Agda
  { a_buffer :: Buffer
  , a_ready  :: IORef Bool
  , a_req    :: InChan String
  , a_hdl    :: ProcessHandle
  }
  deriving Generic

data BufferStuff = BufferStuff
  { bs_agda_proc  :: Agda
  , bs_ips        :: Map InteractionId (InteractionPoint Identity)
  , bs_ip_exts    :: Map InteractionId Extmark
  , bs_goto_sites :: Map Extmark DefinitionSite
  , bs_goals      :: DisplayInfo
  , bs_info_win   :: InfoBuffer
  , bs_code_map   :: LineIntervals
  }
  deriving Generic

newtype InfoBuffer = InfoBuffer
  { iw_buffer :: Buffer
  }
  deriving Generic

data CornelisState = CornelisState
  { cs_buffers :: Map Buffer BufferStuff
  , cs_diff :: Map BufferNum Diff0
  }
  deriving Generic

data SplitLocation
  = Vertical
  | Horizontal
  | OnLeft
  | OnRight
  | OnTop
  | OnBottom
  deriving (Eq, Ord, Enum, Bounded)

instance Show SplitLocation where
  show Vertical   = "vertical"
  show Horizontal = "horizontal"
  show OnLeft     = "left"
  show OnRight    = "right"
  show OnTop      = "top"
  show OnBottom   = "bottom"

readSplitLocation :: String -> Maybe SplitLocation
readSplitLocation s = case fmap toLower s of
  "vertical"   -> Just Vertical
  "horizontal" -> Just Horizontal
  "left"       -> Just OnLeft
  "right"      -> Just OnRight
  "top"        -> Just OnTop
  "bottom"     -> Just OnBottom
  _            -> Nothing


data CornelisConfig = CornelisConfig
  { cc_max_height :: Int64
  , cc_max_width :: Int64
  , cc_split_location :: SplitLocation
  }
  deriving (Show, Generic)

data CornelisEnv = CornelisEnv
  { ce_state :: IORef CornelisState
  , ce_stream :: InChan AgdaResp
  , ce_namespace :: Int64
  , ce_config :: CornelisConfig
  }
  deriving Generic

data AgdaResp = AgdaResp
  { ar_buffer :: Buffer
  , ar_message :: Response
  }
  deriving Generic

instance MonadState CornelisState (Neovim CornelisEnv) where
  get = do
    mv <- asks ce_state
    liftIO $ readIORef mv
  put a = do
    mv <- asks ce_state
    liftIO $ writeIORef mv a

data Response
  = DisplayInfo DisplayInfo
  | ClearHighlighting -- TokenBased
  | HighlightingInfo Bool [Highlight]
  | ClearRunningInfo
  | RunningInfo Int Text
  | Status
    { status_checked :: Bool
    , status_showIrrelevant :: Bool
    , status_showImplicits :: Bool
    }
  | JumpToError FilePath AgdaIndex
  | InteractionPoints [InteractionPoint Maybe]
  | GiveAction Text (InteractionPoint (Const ()))
  | MakeCase MakeCase
  | SolveAll [Solution]
  | Unknown Text Value
  deriving (Eq, Ord, Show)

data DefinitionSite = DefinitionSite
  { ds_filepath :: Text
  , ds_position :: AgdaIndex
  }
  deriving (Eq, Ord, Show)

instance FromJSON DefinitionSite where
  parseJSON = withObject "DefinitionSite" $ \obj ->
    DefinitionSite <$> obj .: "filepath" <*> obj .: "position"

data Highlight = Highlight
  { hl_atoms          :: [Text]
  , hl_definitionSite :: Maybe DefinitionSite
  , hl_start          :: AgdaIndex
  , hl_end            :: AgdaIndex
  }
  deriving (Eq, Ord, Show)

instance FromJSON Highlight where
  parseJSON = withObject "Highlight" $ \obj ->
    Highlight
      <$> obj .: "atoms"
      <*> obj .:? "definitionSite"
      <*> fmap (!! 0) (obj .: "range")
      <*> fmap (!! 1) (obj .: "range")

data MakeCase
  = RegularCase MakeCaseVariant [Text] (InteractionPoint Identity)
  deriving (Eq, Ord, Show, Generic)

data MakeCaseVariant = Function | ExtendedLambda
  deriving stock (Eq, Ord, Show, Generic)
  deriving anyclass (FromJSON)

instance FromJSON MakeCase where
  parseJSON = withObject "MakeCase" $ \obj ->
    RegularCase <$> obj .: "variant" <*> obj .: "clauses" <*> obj .: "interactionPoint"


data Solution = Solution
  { s_ip :: InteractionId
  , s_expression :: Text
  }
  deriving (Eq, Ord, Show)

data InteractionPoint f = InteractionPoint
  { ip_id :: InteractionId
  , ip_intervalM :: f AgdaInterval
  } deriving Generic

deriving instance Eq (f AgdaInterval) => Eq (InteractionPoint f)
deriving instance Ord (f AgdaInterval) => Ord (InteractionPoint f)
deriving instance Show (f AgdaInterval) => Show (InteractionPoint f)

ip_interval' :: InteractionPoint Identity -> AgdaInterval
ip_interval' (InteractionPoint _ (Identity i)) = i

sequenceInteractionPoint :: Applicative f => InteractionPoint f -> f (InteractionPoint Identity)
sequenceInteractionPoint (InteractionPoint n f) = pure (InteractionPoint n) <*> fmap Identity f


data NamedPoint = NamedPoint
  { np_name :: Text
  , np_interval :: Maybe AgdaInterval
  }
  deriving (Eq, Ord, Show)

instance FromJSON AgdaInterval where
  parseJSON = withObject "IntervalWithoutFile" $ \obj -> do
    mkInterval <$> obj .: "start" <*> obj .: "end"
    where
      mkInterval (AgdaPos p) (AgdaPos q) = Interval p q

newtype AgdaPos' = AgdaPos AgdaPos

instance FromJSON AgdaPos' where
  parseJSON = withObject "Position" $ \obj -> do
    AgdaPos <$> (Pos <$> obj .: "line" <*> obj .: "col")

instance FromJSON (InteractionPoint Maybe) where
  parseJSON = withObject "InteractionPoint" $ \obj -> do
    InteractionPoint <$> obj .: "id" <*> fmap listToMaybe (obj .: "range")

instance FromJSON (InteractionPoint Identity) where
  parseJSON = withObject "InteractionPoint" $ \obj -> do
    InteractionPoint <$> obj .: "id" <*> fmap head (obj .: "range")

instance FromJSON (InteractionPoint (Const ())) where
  parseJSON = withObject "InteractionPoint" $ \obj -> do
    InteractionPoint <$> obj .: "id" <*> pure (Const ())

instance FromJSON NamedPoint where
  parseJSON = withObject "InteractionPoint" $ \obj -> do
    NamedPoint <$> obj .: "name" <*> fmap listToMaybe (obj .: "range")

instance FromJSON Solution where
  parseJSON = withObject "Solution" $ \obj ->
    Solution <$> obj .: "interactionPoint" <*> obj .: "expression"

data GoalInfo a = GoalInfo
  { gi_ip :: a
  , gi_type :: Type
  }
  deriving (Eq, Ord, Show, Functor)

instance FromJSON a => FromJSON (GoalInfo a) where
  parseJSON = withObject "GoalInfo" $ \obj ->
    (obj .: "kind") >>= \case
      "OfType" -> GoalInfo <$> obj .: "constraintObj" <*> obj .: "type"
      "JustSort" -> GoalInfo <$> obj .: "constraintObj" <*> pure (Type "Sort")
      (_ :: Text) -> empty

newtype Type = Type Text
  deriving newtype (Eq, Ord, Show, FromJSON)

data InScope = InScope
  { is_refied_name :: Text
  , is_original_name :: Text
  , is_in_scope :: Bool
  , is_type :: Type
  }
  deriving (Eq, Ord, Show)

instance FromJSON InScope where
  parseJSON = withObject "InScope" $ \obj ->
    InScope <$> obj .: "reifiedName" <*> obj .: "originalName" <*> obj .: "inScope" <*> obj .: "binding"

newtype Message = Message { getMessage :: Text }
  deriving (Eq, Ord, Show)

instance FromJSON Message where
  parseJSON = withObject "Message" $ \obj ->
    Message <$> obj .: "message"


data DisplayInfo
  = AllGoalsWarnings
      { di_all_visible :: [GoalInfo (InteractionPoint Identity)]
      , di_all_invisible :: [GoalInfo NamedPoint]
      , di_errors :: [Message]
      , di_warnings :: [Message]
      }
  | GoalSpecific
      { di_ips :: InteractionPoint Identity
      , di_in_scope :: [InScope]
      , di_type :: Type
      , di_type_aux :: Maybe Type
      , di_boundary :: Maybe [Text]
      , di_output_forms :: Maybe [Text]
      }
  | HelperFunction Text
  | InferredType Type
  | DisplayError Text
  | WhyInScope Text
  | NormalForm Text
  | UnknownDisplayInfo Value
  deriving (Eq, Ord, Show, Generic)

newtype TypeAux = TypeAux
  { ta_expr :: Type
  }

instance FromJSON TypeAux where
  parseJSON = withObject "TypeAux" $ \obj ->
    TypeAux . Type <$> obj .: "expr"

instance FromJSON DisplayInfo where
  parseJSON v = flip (withObject "DisplayInfo") v $ \obj ->
    obj .: "kind" >>= \case
      "AllGoalsWarnings" ->
        AllGoalsWarnings
          <$> obj .: "visibleGoals"
          <*> obj .: "invisibleGoals"
          <*> (obj .: "errors"   <|> fmap pure (obj .: "errors"))
          <*> (obj .: "warnings" <|> fmap pure (obj .: "warnings"))
      "Error" ->
        obj .: "error" >>= \err ->
          DisplayError <$> err .: "message"
      "InferredType" ->
        InferredType <$> obj .: "expr"
      "WhyInScope" ->
        WhyInScope <$> obj .: "message"
      "NormalForm" ->
        NormalForm <$> obj .: "expr"
      "GoalSpecific" ->
        (obj .: "goalInfo") >>= \info ->
          (info .: "kind") >>= \case
            "HelperFunction" ->
              HelperFunction <$> info .: "signature"
            "GoalType" ->
              GoalSpecific
                <$> obj .: "interactionPoint"
                <*> info .: "entries"
                <*> info .: "type"
                <*> (fmap (fmap ta_expr) (info .: "typeAux") <|> pure Nothing)
                <*> info .:? "boundary"
                <*> info .:? "outputForms"
            "NormalForm" -> NormalForm <$> info .: "expr"
            "InferredType" ->
              InferredType <$> info .: "expr"
            (_ :: Text) ->
              pure $ UnknownDisplayInfo v
      (_ :: Text) -> pure $ UnknownDisplayInfo v

instance FromJSON Response where
  parseJSON v = flip (withObject "Response") v $ \obj -> do
    obj .: "kind" >>= \case
      "MakeCase" ->
        MakeCase <$> parseJSON v
      "ClearRunningInfo" ->
        pure ClearRunningInfo
      "HighlightingInfo" ->
        (obj .: "info") >>= \info ->
          HighlightingInfo <$> info .: "remove" <*> info .: "payload"
      "ClearHighlighting" ->
        pure ClearHighlighting
      "RunningInfo" ->
        RunningInfo <$> obj .: "debugLevel" <*> obj .: "message"
      "InteractionPoints" ->
        InteractionPoints <$> obj .: "interactionPoints"
      "SolveAll" ->
        SolveAll <$> obj .: "solutions"
      "GiveAction" ->
        (obj .: "giveResult") >>= \result ->
          GiveAction <$> result .: "str" <*> obj .: "interactionPoint"
      "DisplayInfo" ->
        DisplayInfo <$> obj .: "info"
      "JumpToError" ->
        JumpToError <$> obj .: "filepath" <*> obj .: "position"
      "Status" -> do
        (obj .: "status" >>=) $ withObject "Status" $ \s ->
          Status <$> s .: "checked"
                  <*> (s .: "showIrrelevantArguments"<|> pure False)
                  <*> s .: "showImplicitArguments"
      (_ :: Text) -> Unknown <$> obj .: "kind" <*> pure v

newtype Extmark = Extmark Int64
  deriving (Eq, Ord, Show)

data ExtmarkStuff = ExtmarkStuff
  { es_mark     :: Extmark
  , es_hlgroup  :: Text
  , es_interval :: AgdaInterval
  }
  deriving (Eq, Ord, Show)


data DebugCommand
  = DumpIPs
  deriving (Eq, Ord, Show, Read, Enum, Bounded)

-- * Translating Agda indices to Vim indices
--
-- Agda sometimes takes a while to process. We want to be able to modify the
-- buffer in the meantime. But then, Agda's highlighting instructions
-- will be out of sync.
--
-- We record the LineIntervals mapping (in field 'bs_code_map') at the time
-- when we reloaded, to translate old AgdaIndex to old VimPos, and then use the
-- 'Diff0' data structure (in field 'cs_diff') to translate (intervals of) old
-- VimPos to new VimPos.

-- | Data for mapping code point indices to byte indices
newtype LineIntervals = LineIntervals
  { li_intervalMap :: IntervalMap AgdaIndex (LineNumber 'ZeroIndexed, Text)
    -- ^ Mapping from positions to line numbers
  } deriving newtype (Semigroup, Monoid)

-- | Buffer update events give us this instead of a proper Buffer
-- There is  buffer_get_number :: Buffer -> Neovim env BufferNum
-- but nothing the other way???
type BufferNum = Int64

-- Data structures from the diff-loc library
type DPos = Colline (LineNumber 'ZeroIndexed) VimIndex
type Diff0 = Diff DPos