content: {-# LANGUAGE CPP #-}
  
  module Agda.Convert where
  
  import Agda.IR (FromAgda (..))
  import qualified Agda.IR as IR
  import Agda.Interaction.Base
  import Agda.Interaction.BasicOps as B
  import Agda.Interaction.EmacsCommand (Lisp)
  import Agda.Interaction.EmacsTop (showInfoError)
  import Agda.Interaction.Highlighting.Common (chooseHighlightingMethod, toAtoms)
  import Agda.Interaction.Highlighting.Precise (Aspects (..), DefinitionSite (..), HighlightingInfo, TokenBased (..))
  import qualified Agda.Interaction.Highlighting.Range as Highlighting
  #if MIN_VERSION_Agda(2,8,0)
  import Agda.Interaction.Command (localStateCommandM)
  import Agda.TypeChecking.Monad.Base (topLevelModuleFilePath)
  #else
  import Agda.Interaction.InteractionTop (localStateCommandM)
  #endif
  #if MIN_VERSION_Agda(2,7,0)
  import Agda.Interaction.Output ( OutputConstraint )
  #endif
  import Agda.Interaction.Response as R
  import Agda.Syntax.Abstract as A
  import Agda.Syntax.Abstract.Pretty (prettyATop)
  import Agda.Syntax.Common
  import Agda.Syntax.Concrete as C
  import Agda.Syntax.Internal (alwaysUnblock)
  import Agda.Syntax.Position (HasRange (getRange), Range, noRange)
  import Agda.Syntax.Scope.Base
  import Agda.TypeChecking.Errors (explainWhyInScope, getAllWarningsOfTCErr, prettyError)
  import Agda.TypeChecking.Monad hiding (Function)
  import Agda.TypeChecking.Monad.MetaVars (withInteractionId)
  import Agda.TypeChecking.Pretty (prettyTCM)
  import qualified Agda.TypeChecking.Pretty as TCP
  import Agda.TypeChecking.Pretty.Warning (filterTCWarnings, prettyTCWarnings, prettyTCWarnings')
  import Agda.TypeChecking.Warnings (WarningsAndNonFatalErrors (..))
  import Agda.Utils.FileName (filePath)
  import Agda.Utils.Function (applyWhen)
  import Agda.Utils.IO.TempFile (writeToTempFile)
  import Agda.Utils.Impossible (__IMPOSSIBLE__)
  import Agda.Utils.Maybe (catMaybes)
  import Agda.Utils.Null (empty)
  import Agda.Utils.RangeMap (IsBasicRangeMap (toList))
  import Agda.Utils.String (delimiter)
  import Agda.Utils.Time (CPUTime)
  import Agda.VersionCommit (versionWithCommitInfo)
  import Control.Monad
  import Control.Monad.State hiding (state)
  import qualified Data.Aeson as JSON
  import qualified Data.ByteString.Lazy.Char8 as BS8
  import qualified Data.List as List
  import qualified Data.Map as Map
  import Data.String (IsString)
  import Render (Block (..), Inlines, Render (..), renderATop)
  import qualified Render
  
  import Agda.Syntax.Common.Pretty hiding (render)
  import qualified Prettyprinter
  
  responseAbbr :: (IsString a) => Response -> a
  responseAbbr res = case res of
    Resp_HighlightingInfo {} -> "Resp_HighlightingInfo"
    Resp_Status {} -> "Resp_Status"
    Resp_JumpToError {} -> "Resp_JumpToError"
    Resp_InteractionPoints {} -> "Resp_InteractionPoints"
    Resp_GiveAction {} -> "Resp_GiveAction"
    Resp_MakeCase {} -> "Resp_MakeCase"
    Resp_SolveAll {} -> "Resp_SolveAll"
  #if MIN_VERSION_Agda(2,7,0)
    Resp_Mimer {} -> "Resp_Mimer"
  #endif
    Resp_DisplayInfo {} -> "Resp_DisplayInfo"
    Resp_RunningInfo {} -> "Resp_RunningInfo"
    Resp_ClearRunningInfo {} -> "Resp_ClearRunningInfo"
    Resp_ClearHighlighting {} -> "Resp_ClearHighlighting"
    Resp_DoneAborting {} -> "Resp_DoneAborting"
    Resp_DoneExiting {} -> "Resp_DoneExiting"
  
  ----------------------------------
  
  serialize :: Lisp String -> String
  serialize = show . pretty
  
  fromResponse :: Response -> TCM IR.Response
  fromResponse (Resp_HighlightingInfo info remove method modFile) =
    fromHighlightingInfo info remove method modFile
  fromResponse (Resp_DisplayInfo info) = IR.ResponseDisplayInfo <$> fromDisplayInfo info
  fromResponse (Resp_ClearHighlighting TokenBased) = return IR.ResponseClearHighlightingTokenBased
  fromResponse (Resp_ClearHighlighting NotOnlyTokenBased) = return IR.ResponseClearHighlightingNotOnlyTokenBased
  fromResponse Resp_DoneAborting = return IR.ResponseDoneAborting
  fromResponse Resp_DoneExiting = return IR.ResponseDoneExiting
  fromResponse Resp_ClearRunningInfo = return IR.ResponseClearRunningInfo
  fromResponse (Resp_RunningInfo n s) = return $ IR.ResponseRunningInfo n s
  fromResponse (Resp_Status s) = return $ IR.ResponseStatus (sChecked s) (sShowImplicitArguments s)
  fromResponse (Resp_JumpToError f p) = return $ IR.ResponseJumpToError f (fromIntegral p)
  fromResponse (Resp_InteractionPoints is) =
    return $ IR.ResponseInteractionPoints (fmap interactionId is)
  fromResponse (Resp_GiveAction (InteractionId i) giveAction) =
    return $ IR.ResponseGiveAction i (fromAgda giveAction)
  fromResponse (Resp_MakeCase _ Function pcs) = return $ IR.ResponseMakeCaseFunction pcs
  fromResponse (Resp_MakeCase _ ExtendedLambda pcs) = return $ IR.ResponseMakeCaseExtendedLambda pcs
  #if MIN_VERSION_Agda(2,7,0)
  fromResponse (Resp_Mimer (InteractionId i) s) = return $ IR.ResponseMimer i s
  #endif
  fromResponse (Resp_SolveAll ps) = return $ IR.ResponseSolveAll (fmap prn ps)
    where
      prn (InteractionId i, e) = (i, prettyShow e)
  
  fromHighlightingInfo ::
    HighlightingInfo ->
    RemoveTokenBasedHighlighting ->
    HighlightingMethod ->
    ModuleToSource ->
    TCM IR.Response
  fromHighlightingInfo h remove method modFile =
    case chooseHighlightingMethod h method of
      Direct -> return $ IR.ResponseHighlightingInfoDirect info
      Indirect -> IR.ResponseHighlightingInfoIndirect <$> indirect
    where
      fromAspects ::
        (Highlighting.Range, Aspects) ->
        IR.HighlightingInfo
      fromAspects (range, aspects) =
        IR.HighlightingInfo
          (Highlighting.from range)
          (Highlighting.to range)
          (toAtoms aspects)
          (tokenBased aspects == TokenBased)
          (note aspects)
          (defSite <$> definitionSite aspects)
        where
          defSite (DefinitionSite moduleName offset _ _) =
  #if MIN_VERSION_Agda(2,8,0)
            (filePath (topLevelModuleFilePath modFile moduleName), offset)
  #else
            (filePath (Map.findWithDefault __IMPOSSIBLE__ moduleName modFile), offset)
  #endif
  
      infos :: [IR.HighlightingInfo]
      infos = fmap fromAspects (toList h)
  
      keepHighlighting :: Bool
      keepHighlighting =
        case remove of
          RemoveHighlighting -> False
          KeepHighlighting -> True
  
      info :: IR.HighlightingInfos
      info = IR.HighlightingInfos keepHighlighting infos
  
      indirect :: TCM FilePath
      indirect = liftIO $ writeToTempFile (BS8.unpack (JSON.encode info))
  
  fromDisplayInfo :: DisplayInfo -> TCM IR.DisplayInfo
  fromDisplayInfo = \case
    Info_CompilationOk _ ws -> do
      -- filter
  #if MIN_VERSION_Agda(2,8,0)
      filteredWarnings <- filterTCWarnings (tcWarnings ws)
      filteredErrors <- filterTCWarnings (nonFatalErrors ws)
  #else
      let filteredWarnings = filterTCWarnings (tcWarnings ws)
      let filteredErrors = filterTCWarnings (nonFatalErrors ws)
  #endif
      -- serializes
      warnings <- mapM prettyTCM filteredWarnings
      errors <- mapM prettyTCM filteredErrors
      return $ IR.DisplayInfoCompilationOk (fmap show warnings) (fmap show errors)
    Info_Constraints s -> do
      -- constraints <- forM s $ \e -> do
      --   rendered <- renderTCM e
      --   let raw = show (pretty e)
      --   return $ Unlabeled rendered (Just raw)
      -- return $ IR.DisplayInfoGeneric "Constraints" constraints
      return $ IR.DisplayInfoGeneric "Constraints" [Unlabeled (Render.text $ show $ vcat $ fmap pretty s) Nothing Nothing]
    Info_AllGoalsWarnings (ims, hms) ws -> do
      -- visible metas (goals)
      goals <- mapM convertGoal ims
      -- hidden (unsolved) metas
      metas <- mapM convertHiddenMeta hms
  
      -- errors / warnings
      -- filter
  #if MIN_VERSION_Agda(2,8,0)
      filteredWarnings <- filterTCWarnings (tcWarnings ws)
      filteredErrors <- filterTCWarnings (nonFatalErrors ws)
  #else
      let filteredWarnings = filterTCWarnings (tcWarnings ws)
      let filteredErrors = filterTCWarnings (nonFatalErrors ws)
  #endif
      -- serializes
      warnings <- mapM prettyTCM filteredWarnings
      errors <- mapM prettyTCM filteredErrors
  
      let isG = not (null goals && null metas)
      let isW = not $ null warnings
      let isE = not $ null errors
      let title =
            List.intercalate "," $
              catMaybes
                [ " Goals" <$ guard isG,
                  " Errors" <$ guard isE,
                  " Warnings" <$ guard isW,
                  " Done" <$ guard (not (isG || isW || isE))
                ]
  
      return $ IR.DisplayInfoAllGoalsWarnings ("*All" ++ title ++ "*") goals metas (fmap show warnings) (fmap show errors)
      where
        convertHiddenMeta :: OutputConstraint A.Expr NamedMeta -> TCM Block
        convertHiddenMeta m = do
          let i = nmid $ namedMetaOf m
          -- output constrain
          meta <- withMetaId i $ renderATop m
          serialized <- show <$> withMetaId i (prettyATop m)
          -- range
          range <- getMetaRange i
  
          return $ Unlabeled meta (Just serialized) (Just range)
  
        convertGoal :: OutputConstraint A.Expr InteractionId -> TCM Block
        convertGoal i = do
          -- output constrain
          goal <-
            withInteractionId (outputFormId $ OutputForm noRange [] alwaysUnblock i) $
              renderATop i
  
          serialized <-
            withInteractionId (outputFormId $ OutputForm noRange [] alwaysUnblock i) $
              prettyATop i
          return $ Unlabeled goal (Just $ show serialized) Nothing
    Info_Auto s -> return $ IR.DisplayInfoAuto s
    Info_Error err -> do
      s <- showInfoError err
      return $ IR.DisplayInfoError s
    Info_Time s ->
      return $ IR.DisplayInfoTime (show (prettyTimed s))
    Info_NormalForm state cmode time expr -> do
      exprDoc <- evalStateT prettyExpr state
      let doc = maybe empty prettyTimed time $$ exprDoc
      return $ IR.DisplayInfoNormalForm (show doc)
      where
        prettyExpr =
          localStateCommandM $
            lift $
              B.atTopLevel $
                allowNonTerminatingReductions $
                  (if computeIgnoreAbstract cmode then ignoreAbstractMode else inConcreteMode) $
                    B.showComputed cmode expr
    Info_InferredType state time expr -> do
      renderedExpr <-
        flip evalStateT state $
          localStateCommandM $
            lift $
              B.atTopLevel $
                Render.renderA expr
      let rendered = case time of
            Nothing -> renderedExpr
            -- TODO: handle this newline
            Just t -> "Time:" Render.<+> Render.render t Render.<+> "\n" Render.<+> renderedExpr
      exprDoc <-
        flip evalStateT state $
          localStateCommandM $
            lift $
              B.atTopLevel $
                TCP.prettyA expr
      let raw = show $ maybe empty prettyTimed time $$ exprDoc
      return $ IR.DisplayInfoGeneric "Inferred Type" [Unlabeled rendered (Just raw) Nothing]
    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 $ fmap pretty modules,
              "Names",
              nest 2 $ align 10 typeDocs
            ]
      return $ IR.DisplayInfoGeneric "Module contents" [Unlabeled (Render.text $ show doc) Nothing Nothing]
    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)
      return $ IR.DisplayInfoGeneric "Search About" [Unlabeled (Render.text $ show doc) Nothing Nothing]
    Info_WhyInScope why -> do
      doc <- explainWhyInScope why
      return $ IR.DisplayInfoGeneric "Scope Info" [Unlabeled (Render.text $ show doc) Nothing Nothing]
    Info_Context ii ctx -> do
      doc <- localTCState (prettyResponseContexts ii False ctx)
      return $ IR.DisplayInfoGeneric "Context" [Unlabeled (Render.text $ show doc) Nothing Nothing]
    Info_Intro_NotFound ->
      return $ IR.DisplayInfoGeneric "Intro" [Unlabeled (Render.text "No introduction forms found.") Nothing Nothing]
    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)
              ]
      return $ IR.DisplayInfoGeneric "Intro" [Unlabeled (Render.text $ show doc) Nothing Nothing]
    Info_Version ->
      return $ IR.DisplayInfoGeneric "Agda Version" [Unlabeled (Render.text $ "Agda version " ++ versionWithCommitInfo) Nothing Nothing]
    Info_GoalSpecific ii kind -> lispifyGoalSpecificDisplayInfo ii kind
  
  lispifyGoalSpecificDisplayInfo :: InteractionId -> GoalDisplayInfo -> TCM IR.DisplayInfo
  lispifyGoalSpecificDisplayInfo ii kind = localTCState $
    withInteractionId ii $
      case kind of
        Goal_HelperFunction helperType -> do
          doc <- inTopContext $ prettyATop helperType
          return $ IR.DisplayInfoGeneric "Helper function" [Unlabeled (Render.text $ show doc ++ "\n") Nothing Nothing]
        Goal_NormalForm cmode expr -> do
          doc <- showComputed cmode expr
          return $ IR.DisplayInfoGeneric "Normal Form" [Unlabeled (Render.text $ show doc) Nothing Nothing]
        Goal_GoalType norm aux resCtxs boundaries constraints -> do
          goalSect <- do
            (rendered, raw) <- prettyTypeOfMeta norm ii
            return [Labeled rendered (Just raw) Nothing "Goal" "special"]
  
          auxSect <- case aux of
            GoalOnly -> return []
            GoalAndHave expr bndry -> do
              -- TODO: render bndry
              rendered <- renderATop expr
              raw <- show <$> prettyATop expr
              return [Labeled rendered (Just raw) Nothing "Have" "special"]
            GoalAndElaboration expr -> do
  #if MIN_VERSION_Agda(2,8,0)
              rendered <- renderATop expr
  #else
              let rendered = render expr
  #endif
              raw <- show <$> TCP.prettyTCM expr
              return [Labeled rendered (Just raw) Nothing "Elaborates to" "special"]
          let boundarySect =
                if null boundaries
                  then []
                  else
                    Header "Boundary"
                      : fmap (\boundary -> Unlabeled (render boundary) (Just $ show $ pretty boundary) Nothing) boundaries
          contextSect <- reverse . concat <$> mapM (renderResponseContext ii) resCtxs
          let constraintSect =
                if null constraints
                  then []
                  else
                    Header "Constraints"
                      : fmap (\constraint -> Unlabeled (render constraint) (Just $ show $ pretty constraint) Nothing) constraints
  
          return $
            IR.DisplayInfoGeneric "Goal type etc" $
              goalSect ++ auxSect ++ boundarySect ++ contextSect ++ constraintSect
        Goal_CurrentGoal norm -> do
          (rendered, raw) <- prettyTypeOfMeta norm ii
          return $ IR.DisplayInfoCurrentGoal (Unlabeled rendered (Just raw) Nothing)
        Goal_InferredType expr -> do
          rendered <- renderATop expr
          raw <- show <$> prettyATop expr
          return $ IR.DisplayInfoInferredType (Unlabeled rendered (Just raw) Nothing)
  
  -- -- | Format responses of DisplayInfo
  -- formatPrim :: Bool -> [Block] -> String -> TCM IR.DisplayInfo
  -- formatPrim _copy items header = return $ IR.DisplayInfoGeneric header items
  
  -- -- | Format responses of DisplayInfo ("agda2-info-action")
  -- format :: [Block] -> String -> TCM IR.DisplayInfo
  -- format = formatPrim False
  
  -- -- | Format responses of DisplayInfo ("agda2-info-action-copy")
  -- formatAndCopy :: [Block] -> String -> TCM IR.DisplayInfo
  -- formatAndCopy = formatPrim True
  
  --------------------------------------------------------------------------------
  
  -- | Pretty-prints the context of the given meta-variable.
  prettyResponseContexts ::
    -- | Context of this meta-variable.
    InteractionId ->
    -- | Print the elements in reverse order?
    Bool ->
    [ResponseContextEntry] ->
    TCM Doc
  prettyResponseContexts ii rev ctxs = do
    rows <- mapM (prettyResponseContext ii) ctxs
    return $ align 10 $ concat $ applyWhen rev reverse rows
  
  -- | Pretty-prints the context of the given meta-variable.
  prettyResponseContext ::
    -- | Context of this meta-variable.
    InteractionId ->
    ResponseContextEntry ->
    TCM [(String, Doc)]
  prettyResponseContext ii (ResponseContextEntry n x (Arg ai expr) letv nis) = withInteractionId ii $ do
    modality <- currentModality
    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)
  
          extras :: [Doc]
          extras =
            concat
              [ ["not in scope" | isInScope nis == C.NotInScope],
                -- Print erased if hypothesis is erased by goal is non-erased.
                ["erased" | not $ getQuantity ai `moreQuantity` getQuantity modality],
                -- Print irrelevant if hypothesis is strictly less relevant than goal.
                ["irrelevant" | not $ getRelevance ai `moreRelevant` getRelevance modality],
                -- Print instance if variable is considered by instance search
                ["instance" | isInstance ai]
              ]
      ty <- prettyATop expr
  
      letv' <- case letv of
        Nothing -> return []
        Just val -> do
          val' <- prettyATop val
          return [(prettyShow x, "=" <+> val')]
  
      return $
        (attribute ++ prettyCtxName, ":" <+> ty <+> parenSep extras) : letv'
    where
      parenSep :: [Doc] -> Doc
      parenSep docs
        | null docs = empty
        | otherwise = (" " <+>) $ parens $ fsep $ punctuate comma docs
  
  -- | Render the context of the given meta-variable.
  renderResponseContext ::
    -- | Context of this meta-variable.
    InteractionId ->
    ResponseContextEntry ->
    TCM [Block]
  renderResponseContext ii (ResponseContextEntry n x (Arg ai expr) letv nis) = withInteractionId ii $ do
    modality <- currentModality
    do
      let rawCtxName :: String
          rawCtxName
            | n == x = prettyShow x
            | isInScope n == InScope = prettyShow n ++ " = " ++ prettyShow x
            | otherwise = prettyShow x
  
          renderedCtxName :: Inlines
          renderedCtxName
            | n == x = render x
            | isInScope n == InScope = render n Render.<+> "=" Render.<+> render x
            | otherwise = render x
  
          -- Some attributes are useful to report whenever they are not
          -- in the default state.
          rawAttribute :: String
          rawAttribute = c ++ if null c then "" else " "
            where
              c = prettyShow (getCohesion ai)
  
          renderedAttribute :: Inlines
          renderedAttribute = c <> if null (show c) then "" else " "
            where
              c = render (getCohesion ai)
  
          extras :: (IsString a) => [a]
          extras =
            concat
              [ ["not in scope" | isInScope nis == C.NotInScope],
                -- Print erased if hypothesis is erased by goal is non-erased.
                ["erased" | not $ getQuantity ai `moreQuantity` getQuantity modality],
                -- Print irrelevant if hypothesis is strictly less relevant than goal.
                ["irrelevant" | not $ getRelevance ai `moreRelevant` getRelevance modality],
                -- Print instance if variable is considered by instance search
                ["instance" | isInstance ai]
              ]
  
          extras2 :: [Inlines]
          extras2 =
            concat
              [ ["not in scope" | isInScope nis == C.NotInScope],
                -- Print erased if hypothesis is erased by goal is non-erased.
                ["erased" | not $ getQuantity ai `moreQuantity` getQuantity modality],
                -- Print irrelevant if hypothesis is strictly less relevant than goal.
                ["irrelevant" | not $ getRelevance ai `moreRelevant` getRelevance modality],
                -- Print instance if variable is considered by instance search
                ["instance" | isInstance ai]
              ]
  
      -- raw
      rawExpr <- prettyATop expr
      let rawType = show $ align 10 [(rawAttribute ++ rawCtxName, ":" <+> rawExpr <+> parenSep extras)]
      -- rendered
      renderedExpr <- renderATop expr
      let renderedType = (renderedCtxName <> renderedAttribute) Render.<+> ":" Render.<+> renderedExpr Render.<+> parenSep2 extras2
      -- (Render.fsep $ Render.punctuate "," extras)
  
      -- result
      let typeItem = Unlabeled renderedType (Just rawType) Nothing
  
      valueItem <- case letv of
        Nothing -> return []
        Just val -> do
          valText <- renderATop val
          valString <- prettyATop val
          let renderedValue = Render.render x Render.<+> "=" Render.<+> valText
          let rawValue = show $ align 10 [(prettyShow x, "=" <+> valString)]
          return
            [ Unlabeled renderedValue (Just rawValue) Nothing
            ]
  
      return $ typeItem : valueItem
    where
      parenSep :: [Doc] -> Doc
      parenSep docs
        | null docs = empty
        | otherwise = (" " <+>) $ parens $ fsep $ punctuate comma docs
  
      parenSep2 :: [Inlines] -> Inlines
      parenSep2 docs
        | null docs = mempty
        | otherwise = (" " Render.<+>) $ Render.parens $ Render.fsep $ Render.punctuate "," docs
  
  -- | Pretty-prints the type of the meta-variable.
  prettyTypeOfMeta :: Rewrite -> InteractionId -> TCM (Inlines, String)
  prettyTypeOfMeta norm ii = do
    form <- B.typeOfMeta norm ii
    case form of
      OfType _ e -> do
        rendered <- renderATop e
        raw <- show <$> prettyATop e
        return (rendered, raw)
      _ -> do
        rendered <- renderATop form
        raw <- show <$> prettyATop form
        return (rendered, raw)
  
  -- | Prefix prettified CPUTime with "Time:"
  prettyTimed :: CPUTime -> Doc
  prettyTimed time = "Time:" <+> pretty time
  