{-# OPTIONS_GHC -Wunused-imports #-}

module Agda.Interaction.EmacsTop
    ( mimicGHCi
    , namedMetaOf
    , showInfoError
    , prettyGoals
    , prettyInfoError
    , explainWhyInScope
    , prettyResponseContext
    , prettyTypeOfMeta
    , prettyNormalForm
    , prettyInferredType
    ) where

import Prelude hiding (null)

import Control.Monad
import Control.Monad.IO.Class ( MonadIO(..) )
import Control.Monad.State    ( evalStateT )
import Control.Monad.Trans    ( lift )

import Data.List qualified as List

import Agda.Syntax.Common
import Agda.Syntax.Common.Pretty as P
import Agda.Syntax.Abstract qualified as A
import Agda.Syntax.Abstract.Pretty (prettyATop)
import Agda.Syntax.Concrete as C

import Agda.TypeChecking.Errors ( explainWhyInScope, getAllWarningsOfTCErr, verbalize, prettyError )
import Agda.TypeChecking.Pretty qualified as TCP
import Agda.TypeChecking.Pretty (prettyTCM)
import Agda.TypeChecking.Pretty.Warning (prettyTCWarnings')
import Agda.TypeChecking.Monad

import Agda.Interaction.AgdaTop
import Agda.Interaction.Base
import Agda.Interaction.BasicOps as B
import Agda.Interaction.Response as R
import Agda.Interaction.Emacs.Lisp
import Agda.Interaction.EmacsCommand ( displayInfo, clearRunningInfo, displayRunningInfo, displayVerboseInfo)
import Agda.Interaction.Highlighting.Emacs
import Agda.Interaction.Highlighting.Precise (TokenBased(..))
import Agda.Interaction.Command (localStateCommandM)
import Agda.Interaction.Options ( DiagnosticsColours(..), optDiagnosticsColour )

import Agda.Utils.DocTree  ( renderToTree )
import Agda.Utils.Function ( applyWhen )
import Agda.Utils.Functor  ( (<.>) )
import Agda.Utils.Null
import Agda.Utils.Maybe
import Agda.Utils.String
import Agda.Utils.Time (CPUTime)

import Agda.VersionCommit

----------------------------------

-- | 'mimicGHCi' is a fake ghci interpreter for the Emacs frontend
--   and for interaction tests.
--
--   'mimicGHCi' reads the Emacs frontend commands from stdin,
--   interprets them and print the result into stdout.
mimicGHCi :: TCM () -> TCM ()
mimicGHCi = repl (liftIO . putStrLn . prettyShow <=< lispifyResponse) "Agda2> "

-- | Convert Response to an elisp value for the interactive emacs frontend.

lispifyResponse :: Response -> TCM (Lisp String)
lispifyResponse = \case

  Resp_HighlightingInfo info remove method modFile file ->
    liftIO (lispifyHighlightingInfo info remove method modFile file)

  Resp_DisplayInfo info ->
    lispifyDisplayInfo info

  Resp_ClearHighlighting tokenBased ->
    return $ L $
      A "agda2-highlight-clear" :
      case tokenBased of
        TokenBased -> [ Q (lispifyTokenBased tokenBased) ]
        NotOnlyTokenBased -> []

  Resp_DoneAborting ->
    return $ L [ A "agda2-abort-done" ]

  Resp_DoneExiting ->
    return $ L [ A "agda2-exit-done" ]

  Resp_ClearRunningInfo ->
    return clearRunningInfo

  Resp_RunningInfo n docTree
    | n <= 1 -> displayRunningInfo docTree <$> wantBufferHighlighting
    | otherwise -> displayVerboseInfo docTree <$> wantBufferHighlighting

  Resp_Status s ->
    return $ L
      [ A "agda2-status-action"
      , A (quote $ List.intercalate "," $ catMaybes [checked, showImpl, showIrr])
      ]
    where
      checked  = boolToMaybe (sChecked                 s) "Checked"
      showImpl = boolToMaybe (sShowImplicitArguments   s) "ShowImplicit"
      showIrr  = boolToMaybe (sShowIrrelevantArguments s) "ShowIrrelevant"

  Resp_JumpToError f p ->
    return $ lastTag 3 $ L
      [ A "agda2-maybe-goto"
      , Q $ L [ A (quote f), A ".", A (show p) ]
      ]

  Resp_InteractionPoints is ->
    return $ lastTag 1 $ L
      [ A "agda2-goals-action"
      , Q $ L $ map showNumIId is
      ]

  Resp_GiveAction ii s ->
    return $ L
      [ A "agda2-give-action"
      , showNumIId ii
      , A s'
      ]
    where
      s' = case s of
          Give_String str -> quote str
          Give_Paren      -> "'paren"
          Give_NoParen    -> "'no-paren"

  Resp_MakeCase ii variant pcs ->
    return $ lastTag 2 $ L
      [ A cmd
      , Q $ L $ map (A . quote) pcs
      ]
    where
    cmd = case variant of
      R.Function       -> "agda2-make-case-action"
      R.ExtendedLambda -> "agda2-make-case-action-extendlam"

  Resp_SolveAll ps ->
    return $ lastTag 2 $ L
      [ A "agda2-solveAll-action"
      , Q $ L $ concatMap prn ps
      ]
    where
      prn (ii,e)= [showNumIId ii, A $ quote $ prettyShow e]

  Resp_Mimer ii msol ->
    return $ lastTag 1 $ L $ case msol of
      Nothing ->
        [ A "agda2-info-action"
        , A $ quote "*Mimer*"
        , A $ quote "No solution found"
        ]
      Just str ->
        [ A "agda2-solve-action"
        , showNumIId ii
        , A $ quote str
        ]

lispifyDisplayInfo :: DisplayInfo -> TCM (Lisp String)
lispifyDisplayInfo = \case

    Info_CompilationOk backend ws -> do
      warnings <- prettyTCWarnings' (tcWarnings ws)
      errors   <- prettyTCWarnings' (nonFatalErrors ws)
      let
        msg = hcat
          [ "The module was successfully compiled with backend "
          , pretty backend
          , ".\n"
          ]
      -- abusing the goals field since we ignore the title
        (_title, body) = formatWarningsAndErrors msg warnings errors
      format "*Compilation result*" body

    Info_Constraints s -> do
      doc <- TCP.vcat $ map prettyTCM s
      format "*Constraints*" doc

    Info_AllGoalsWarnings ms ws -> do
      goals    <- prettyGoals ms
      warnings <- prettyTCWarnings' (tcWarnings ws)
      errors   <- prettyTCWarnings' (nonFatalErrors ws)
      let (title, body) = formatWarningsAndErrors goals warnings errors
      format ("*All" ++ title ++ "*") body

    Info_Auto s ->
      format "*Auto*" $ P.text s

    Info_Error err -> format' "*Error*" =<< prettyInfoError err

    Info_Time time ->
      format "*Time*" $ prettyTimed time

    Info_NormalForm state cmode time expr -> do
      exprDoc <- prettyNormalForm state cmode expr
      let doc = maybe empty prettyTimed time $$ exprDoc
          lbl | cmode == HeadCompute = "*Head Normal Form*"
              | otherwise            = "*Normal Form*"
      format lbl doc

    Info_InferredType state time expr -> do
      exprDoc <- prettyInferredType state expr
      let doc = maybe empty prettyTimed time $$ exprDoc
      format "*Inferred Type*" doc

    Info_ModuleContents modules tel types -> do
      doc <- localTCState $ do
        typeDocs <- addContext tel $ forM types $ \ (x, t) -> do
          doc <- prettyTCM t
          return (prettyShow x, ":" <+> doc)
        return $ vcat
          [ "Modules"
          , nest 2 $ vcat $ map pretty modules
          , "Names"
          , nest 2 $ align 10 typeDocs
          ]
      format "*Module contents*" doc

    Info_SearchAbout hits names -> do
      hitDocs <- forM hits $ \ (x, t) -> do
        doc <- prettyTCM t
        return (prettyShow x, ":" <+> doc)
      let doc = "Definitions about" <+>
                text (List.intercalate ", " $ words names) $$ nest 2 (align 10 hitDocs)
      format "*Search About*" doc

    Info_WhyInScope why -> do
      doc <- explainWhyInScope why
      format "*Scope Info*" doc

    Info_Context ii ctx -> do
      doc <- localTCState (prettyResponseContext ii False ctx)
      format "*Context*" doc

    Info_Intro_NotFound ->
      format "*Intro*" "No introduction forms found."

    Info_Intro_ConstructorUnknown ss -> do
      let doc = sep [ "Don't know which constructor to introduce of"
                    , let mkOr []     = []
                          mkOr [x, y] = [text x <+> "or" <+> text y]
                          mkOr (x:xs) = text x : mkOr xs
                      in nest 2 $ fsep $ punctuate comma (mkOr ss)
                    ]
      format "*Intro*" doc

    Info_Version ->
      format "*Agda Version*" ("Agda version" <+> text versionWithCommitInfo)

    Info_GoalSpecific ii kind ->
      lispifyGoalSpecificDisplayInfo ii kind

lispifyGoalSpecificDisplayInfo :: InteractionId -> GoalDisplayInfo -> TCM (Lisp String)
lispifyGoalSpecificDisplayInfo ii kind = localTCState $ withInteractionId ii $
  case kind of

    Goal_HelperFunction helperType -> do
      doc <- inTopContext $ prettyATop helperType
      return $ L
        [ A "agda2-info-action-and-copy"
        , A $ quote "*Helper function*"
        , A $ quote (render doc ++ "\n")
        , A "nil"
        ]

    Goal_NormalForm cmode expr -> do
      doc <- showComputed cmode expr
      format "*Normal Form*" doc

    Goal_GoalType norm aux ctx bndry constraints -> do
      ctxDoc <- prettyResponseContext ii True ctx
      goalDoc <- prettyTypeOfMeta norm ii
      let boundaryDoc hd bndry
            | null bndry = []
            | otherwise  = [ text $ delimiter hd
                           , vcat $ map pretty bndry
                           ]
      auxDoc <- case aux of
            GoalOnly -> return empty
            GoalAndHave expr bndry -> do
              doc <- prettyATop expr
              return $ ("Have:" <+> doc) $$ vcat (boundaryDoc ("Boundary (actual)") bndry)
            GoalAndElaboration expr -> do
              doc <- prettyATop expr
              return $ "Elaborates to:" <+> doc
      let constraintsDoc
            | null constraints = []
            | otherwise        =
              [ TCP.text $ delimiter "Constraints"
              , TCP.vcat $ map prettyTCM constraints
              ]
      doc <- TCP.vcat $ concat
        [ [ "Goal:" TCP.<+> return goalDoc
          , return (vcat (boundaryDoc "Boundary (wanted)" bndry))
          , return auxDoc
          ]
        , [ TCP.text (delimiter "Context") | not $ null ctxDoc ]
        , [ return ctxDoc ]
        , constraintsDoc
        ]
      format "*Goal type etc.*" doc

    Goal_CurrentGoal norm -> do
      doc <- prettyTypeOfMeta norm ii
      format "*Current Goal*" doc

    Goal_InferredType expr -> do
      doc <- prettyATop expr
      format "*Inferred Type*" doc

format :: String -> Doc -> TCM (Lisp String)
format header = format' header

-- | Format responses of 'DisplayInfo'.
format'
  :: String
  -- ^ String to use as a header.
  -> Doc
  -- ^ The document to print.
  -> TCM (Lisp String)
format' header content = displayInfo header (renderToTree content) False <$>
  wantBufferHighlighting

-- | Do we want highlighting in the Agda information buffer?
--   'Nothing' with option @--color=never@.
wantBufferHighlighting :: TCM (Maybe ModuleToSource)
wantBufferHighlighting = do
  col <- commandLineOptions <&> optDiagnosticsColour <&> \case
    AutoColour   -> True
    AlwaysColour -> True
    NeverColour  -> False
  if col
    then Just <$> useSession lensModuleToSource
    else return Nothing

-- | Adds a \"last\" tag to a response.

lastTag :: Integer -> Lisp String -> Lisp String
lastTag n r = Cons (Cons (A "last") (A $ show n)) r

-- | Show an iteraction point identifier as an elisp expression.

showNumIId :: InteractionId -> Lisp String
showNumIId = A . show . interactionId

--------------------------------------------------------------------------------

-- | Given goals, warnings and errors, return a pair of the
--   title and the body for the info buffer.
formatWarningsAndErrors :: Doc -> [Doc] -> [Doc] -> (String, Doc)
formatWarningsAndErrors g ws es = (title, body)
  where
    isG = not $ null g
    isW = not $ null ws
    isE = not $ null es
    title = List.intercalate "," $ concat
      [ [ " Goals"    | isG ]
      , [ " Errors"   | isE ]
      , [ " Warnings" | isW ]
      , [ " Done"     | not (isG || isW || isE) ]
      ]
    body = vcat $ concat
      [ [ g ]
      , [ text $ delimiter "Error"    | isE && (isG || isW) ]
      , es
      , [ text $ delimiter "Warnings" | isW && (isG || isE) ]
      , ws
      ]

-- | Serializing 'Info_Error'.
showInfoError :: Info_Error -> TCM String
showInfoError = render <.> prettyInfoError

-- | Turn an 'Info_Error' into a 'Doc'.
prettyInfoError :: Info_Error -> TCM Doc
prettyInfoError = \case
  Info_GenericError err -> do
    e  <- prettyError err
    ws <- prettyTCWarnings' =<< getAllWarningsOfTCErr err
    let (_title, body) = formatWarningsAndErrors empty ws [e]
    return body

  Info_CompilationError warnings -> do
    docs <- prettyTCWarnings' warnings
    return $ vcat $
      "You need to fix the following errors before you can compile the module:" :
      "" :
      docs

  Info_HighlightingParseError ii ->
    return $ "Highlighting failed to parse expression in" <+> pretty ii

  Info_HighlightingScopeCheckError ii ->
    return $ "Highlighting failed to scope check expression in" <+> pretty ii

-- | Pretty-prints the context of the given meta-variable.

prettyResponseContext
  :: InteractionId  -- ^ Context of this meta-variable.
  -> Bool           -- ^ Print the elements in reverse order?
  -> [ResponseContextEntry]
  -> TCM Doc
prettyResponseContext ii rev ctx = withInteractionId ii $ do
  mod <- currentModality
  align 10 . concat . applyWhen rev reverse <$> do
    forM ctx $ \ (ResponseContextEntry n x (Arg ai expr) letv nis) -> do
      let
        prettyCtxName :: String
        prettyCtxName
          | n == x                 = prettyShow x
          | isInScope n == InScope = prettyShow n ++ " = " ++ prettyShow x
          | otherwise              = prettyShow x

        -- Some attributes are useful to report whenever they are not
        -- in the default state.
        attribute :: String
        attribute = c ++ if null c then "" else " "
          where c = prettyShow (getCohesion ai)

        pol :: ModalPolarity
        pol = modPolarityAnn $ getModalPolarity ai

        extras :: [Doc]
        extras = concat $
          [ [ "not in scope" | isInScope nis == C.NotInScope ]
            -- Print "erased" if hypothesis is erased but goal is non-erased.
          , [ "erased"       | not $ getQuantity  ai `moreQuantity` getQuantity  mod ]
            -- Print relevance of hypothesis relative to relevance of the goal. (Issue #6706.)
          , [ text $ verbalize r
                             | let r = getRelevance mod `inverseComposeRelevance` getRelevance ai
                             , not $ isRelevant r ]
          , [ text $ verbalize pol | not $ pol == MixedPolarity ]
            -- Print "instance" if variable is considered by instance search.
          , [ "instance"     | isInstance ai ]
          ]
      ty <- prettyATop expr
      maybeVal <- traverse prettyATop letv

      return $
        (attribute ++ prettyCtxName, ":" <+> ty <+> (parenSep extras)) :
        [ (prettyShow x, "=" <+> val) | val <- maybeToList maybeVal ]

  where
    parenSep :: [Doc] -> Doc
    parenSep docs
      | null docs = empty
      | otherwise = (" " <+>) $ parens $ fsep $ punctuate comma docs


-- | Pretty-prints the type of the meta-variable.

prettyTypeOfMeta :: Rewrite -> InteractionId -> TCM Doc
prettyTypeOfMeta norm ii = do
  B.typeOfMeta norm ii >>= \case
    OfType _ e -> prettyATop e
    form       -> prettyATop form

-- | Pretty-print the result of a compute command in the command state
--   captured when the command completed.  Shared with the JSON frontend
--   ("Agda.Interaction.JSONTop") so that both frontends render the
--   expression identically.
prettyNormalForm :: CommandState -> ComputeMode -> A.Expr -> TCM Doc
prettyNormalForm state cmode expr = evalStateT prettyExpr state
  where
    prettyExpr = localStateCommandM
        $ lift
        $ B.atTopLevel
        $ (B.withComputeIgnoreAbstract cmode)
        $ (B.showComputed cmode)
        $ expr

-- | Pretty-print an inferred type in the command state captured when the
--   inference command completed.  Shared with the JSON frontend.
prettyInferredType :: CommandState -> A.Expr -> TCM Doc
prettyInferredType state expr = evalStateT prettyExpr state
  where
    prettyExpr = localStateCommandM
        $ lift
        $ B.atTopLevel
        $ TCP.prettyA
        $ expr

-- | Prefix prettified CPUTime with "Time:"
prettyTimed :: CPUTime -> Doc
prettyTimed time = "Time:" <+> pretty time