module Agda.Convert where

import Render ( Block(..), Inlines, renderATop, Render(..) )

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.Highlighting.Common (chooseHighlightingMethod, toAtoms)
import Agda.Interaction.Highlighting.Precise (Aspects (..), DefinitionSite (..), HighlightingInfo, TokenBased (..))
import qualified Agda.Interaction.Highlighting.Range as Highlighting
import Agda.Interaction.InteractionTop (localStateCommandM)
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 (getAllWarningsOfTCErr, prettyError)
import Agda.TypeChecking.Monad hiding (Function)
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.Pretty hiding (render)
import Agda.Utils.RangeMap ( IsBasicRangeMap(toList) ) 
import Agda.Utils.String (delimiter)
import Agda.Utils.Time (CPUTime)
import Agda.VersionCommit (versionWithCommitInfo)
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 qualified Render

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"
  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
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 _ _) =
          (filePath (Map.findWithDefault __IMPOSSIBLE__ moduleName modFile), offset)

    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 info = case info of
  Info_CompilationOk ws -> do
    -- filter
    let filteredWarnings = filterTCWarnings (tcWarnings ws)
    let filteredErrors = filterTCWarnings (nonFatalErrors ws)
    -- 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
    let filteredWarnings = filterTCWarnings (tcWarnings ws)
    let filteredErrors = filterTCWarnings (nonFatalErrors ws)
    -- 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 s cwd v xs ms -> do
    doc <- explainWhyInScope s cwd v xs ms
    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 $
  B.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 -> do
            rendered <- renderATop expr
            raw <- show <$> prettyATop expr
            return [Labeled rendered (Just raw) Nothing "Have" "special"]
          GoalAndElaboration term -> do
            let rendered = render term
            raw <- show <$> TCP.prettyTCM term
            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

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

-- | Serializing Info_Error
showInfoError :: Info_Error -> TCM String
showInfoError (Info_GenericError err) = do
  e <- prettyError err
  w <- prettyTCWarnings' =<< getAllWarningsOfTCErr err

  let errorMsg =
        if null w
          then e
          else delimiter "Error" ++ "\n" ++ e
  let warningMsg =
        List.intercalate "\n" $
          delimiter "Warning(s)" :
          filter (not . null) w
  return $
    if null w
      then errorMsg
      else errorMsg ++ "\n\n" ++ warningMsg
showInfoError (Info_CompilationError warnings) = do
  s <- prettyTCWarnings warnings
  return $
    unlines
      [ "You need to fix the following errors before you can compile",
        "the module:",
        "",
        s
      ]
showInfoError (Info_HighlightingParseError ii) =
  return $ "Highlighting failed to parse expression in " ++ show ii
showInfoError (Info_HighlightingScopeCheckError ii) =
  return $ "Highlighting failed to scope check expression in " ++ show ii

explainWhyInScope ::
  FilePath ->
  String ->
  Maybe LocalVar ->
  [AbstractName] ->
  [AbstractModule] ->
  TCM Doc
explainWhyInScope s _ Nothing [] [] = TCP.text (s ++ " is not in scope.")
explainWhyInScope s _ v xs ms =
  TCP.vcat
    [ TCP.text (s ++ " is in scope as"),
      TCP.nest 2 $ TCP.vcat [variable v xs, modules ms]
    ]
  where
    -- variable :: Maybe _ -> [_] -> TCM Doc
    variable Nothing vs = names vs
    variable (Just x) vs
      | null vs = asVar
      | otherwise =
        TCP.vcat
          [ TCP.sep [asVar, TCP.nest 2 $ shadowing x],
            TCP.nest 2 $ names vs
          ]
      where
        asVar :: TCM Doc
        asVar =
          "* a variable bound at" TCP.<+> TCP.prettyTCM (nameBindingSite $ localVar x)
        shadowing :: LocalVar -> TCM Doc
        shadowing (LocalVar _ _ []) = "shadowing"
        shadowing _ = "in conflict with"
    names = TCP.vcat . fmap pName
    modules = TCP.vcat . fmap pMod

    pKind = \case
      AxiomName                -> "postulate"
      ConName                  -> "constructor"
      CoConName                -> "coinductive constructor"
      DataName                 -> "data type"
      DisallowedGeneralizeName -> "generalizable variable from let open"
      FldName                  -> "record field"
      FunName                  -> "defined name"
      GeneralizeName           -> "generalizable variable"
      MacroName                -> "macro name"
      PatternSynName           -> "pattern synonym"
      PrimName                 -> "primitive function"
      QuotableName             -> "quotable name"
      -- previously DefName:
      RecName                  -> "record type"
      OtherDefName             -> "defined name"

    pName :: AbstractName -> TCM Doc
    pName a =
      TCP.sep
        [ "* a"
            TCP.<+> pKind (anameKind a)
            TCP.<+> TCP.text (prettyShow $ anameName a),
          TCP.nest 2 "brought into scope by"
        ]
        TCP.$$ TCP.nest 2 (pWhy (nameBindingSite $ qnameName $ anameName a) (anameLineage a))
    pMod :: AbstractModule -> TCM Doc
    pMod a =
      TCP.sep
        [ "* a module" TCP.<+> TCP.text (prettyShow $ amodName a),
          TCP.nest 2 "brought into scope by"
        ]
        TCP.$$ TCP.nest 2 (pWhy (nameBindingSite $ qnameName $ mnameToQName $ amodName a) (amodLineage a))

    pWhy :: Range -> WhyInScope -> TCM Doc
    pWhy r Defined = "- its definition at" TCP.<+> TCP.prettyTCM r
    pWhy r (Opened (C.QName x) w) | isNoName x = pWhy r w
    pWhy r (Opened m w) =
      "- the opening of"
        TCP.<+> TCP.prettyTCM m
        TCP.<+> "at"
        TCP.<+> TCP.prettyTCM (getRange m)
        TCP.$$ pWhy r w
    pWhy r (Applied m w) =
      "- the application of"
        TCP.<+> TCP.prettyTCM m
        TCP.<+> "at"
        TCP.<+> TCP.prettyTCM (getRange m)
        TCP.$$ pWhy r w

-- | 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 <- asksTC getModality
  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 <- asksTC getModality
  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