    {-# OPTIONS_GHC -Wunused-imports #-}

    module Agda.Interaction.EmacsTop
        ( mimicGHCi
        , namedMetaOf
        , showGoals
        , showInfoError
        , explainWhyInScope
        , prettyResponseContext
        , prettyTypeOfMeta
        ) where

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

    import qualified Data.List as List

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

    import Agda.TypeChecking.Errors ( explainWhyInScope, getAllWarningsOfTCErr, renderError, verbalize )
    import qualified Agda.TypeChecking.Pretty 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.EmacsCommand hiding (putResponse)
    import Agda.Interaction.Highlighting.Emacs
    import Agda.Interaction.Highlighting.Precise (TokenBased(..))
    import Agda.Interaction.Command (localStateCommandM)
    import Agda.Utils.Function (applyWhen)
    import Agda.Utils.Null (empty)
    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 :: TCM () -> TCM ()
    mimicGHCi = InteractionOutputCallback -> [Char] -> TCM () -> TCM ()
    repl (IO () -> TCM ()
    forall a. IO a -> TCMT IO a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO () -> TCM ())
    -> ([Lisp [Char]] -> IO ()) -> [Lisp [Char]] -> TCM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Lisp [Char] -> IO ()) -> [Lisp [Char]] -> IO ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ ([Char] -> IO ()
    putStrLn ([Char] -> IO ())
    -> (Lisp [Char] -> [Char]) -> Lisp [Char] -> IO ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Lisp [Char] -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow) ([Lisp [Char]] -> TCM ())
    -> (Response_boot TCErr TCWarning WarningsAndNonFatalErrors
        -> TCMT IO [Lisp [Char]])
    -> InteractionOutputCallback
    forall (m :: * -> *) b c a.
    Monad m =>
    (b -> m c) -> (a -> m b) -> a -> m c
    <=< Response_boot TCErr TCWarning WarningsAndNonFatalErrors
    -> TCMT IO [Lisp [Char]]
    lispifyResponse) [Char]
    "Agda2> "

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

    lispifyResponse :: Response -> TCM [Lisp String]
    lispifyResponse :: Response_boot TCErr TCWarning WarningsAndNonFatalErrors
    -> TCMT IO [Lisp [Char]]
    lispifyResponse (Resp_HighlightingInfo HighlightingInfo
    info RemoveTokenBasedHighlighting
    remove HighlightingMethod
    method ModuleToSource
    modFile) =
      (Lisp [Char] -> [Lisp [Char]] -> [Lisp [Char]]
    forall a. a -> [a] -> [a]
    :[]) (Lisp [Char] -> [Lisp [Char]])
    -> TCMT IO (Lisp [Char]) -> TCMT IO [Lisp [Char]]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> IO (Lisp [Char]) -> TCMT IO (Lisp [Char])
    forall a. IO a -> TCMT IO a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (HighlightingInfo
    -> RemoveTokenBasedHighlighting
    -> HighlightingMethod
    -> ModuleToSource
    -> IO (Lisp [Char])
    lispifyHighlightingInfo HighlightingInfo
    info RemoveTokenBasedHighlighting
    remove HighlightingMethod
    method ModuleToSource
    modFile)
    lispifyResponse (Resp_DisplayInfo DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
    info) = DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
    -> TCMT IO [Lisp [Char]]
    lispifyDisplayInfo DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
    info
    lispifyResponse (Resp_ClearHighlighting TokenBased
    tokenBased) =
      [Lisp [Char]] -> TCMT IO [Lisp [Char]]
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [ [Lisp [Char]] -> Lisp [Char]
    forall a. [Lisp a] -> Lisp a
    L ([Lisp [Char]] -> Lisp [Char]) -> [Lisp [Char]] -> Lisp [Char]
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Lisp [Char]
    forall a. a -> Lisp a
    A [Char]
    "agda2-highlight-clear" Lisp [Char] -> [Lisp [Char]] -> [Lisp [Char]]
    forall a. a -> [a] -> [a]
    :
                   case TokenBased
    tokenBased of
                     TokenBased
    NotOnlyTokenBased -> []
                     TokenBased
    TokenBased        ->
                       [ Lisp [Char] -> Lisp [Char]
    forall a. Lisp a -> Lisp a
    Q (TokenBased -> Lisp [Char]
    lispifyTokenBased TokenBased
    tokenBased) ]
             ]
    lispifyResponse Response_boot TCErr TCWarning WarningsAndNonFatalErrors
    Resp_DoneAborting = [Lisp [Char]] -> TCMT IO [Lisp [Char]]
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [ [Lisp [Char]] -> Lisp [Char]
    forall a. [Lisp a] -> Lisp a
    L [ [Char] -> Lisp [Char]
    forall a. a -> Lisp a
    A [Char]
    "agda2-abort-done" ] ]
    lispifyResponse Response_boot TCErr TCWarning WarningsAndNonFatalErrors
    Resp_DoneExiting  = [Lisp [Char]] -> TCMT IO [Lisp [Char]]
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [ [Lisp [Char]] -> Lisp [Char]
    forall a. [Lisp a] -> Lisp a
    L [ [Char] -> Lisp [Char]
    forall a. a -> Lisp a
    A [Char]
    "agda2-exit-done"  ] ]
    lispifyResponse Response_boot TCErr TCWarning WarningsAndNonFatalErrors
    Resp_ClearRunningInfo = [Lisp [Char]] -> TCMT IO [Lisp [Char]]
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [ Lisp [Char]
    clearRunningInfo ]
    lispifyResponse (Resp_RunningInfo Nat
    n [Char]
    s)
      | Nat
    n Nat -> Nat -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Nat
    1    = [Lisp [Char]] -> TCMT IO [Lisp [Char]]
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [ [Char] -> Lisp [Char]
    displayRunningInfo [Char]
    s ]
      | Bool
    otherwise = [Lisp [Char]] -> TCMT IO [Lisp [Char]]
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [ [Lisp [Char]] -> Lisp [Char]
    forall a. [Lisp a] -> Lisp a
    L [[Char] -> Lisp [Char]
    forall a. a -> Lisp a
    A [Char]
    "agda2-verbose", [Char] -> Lisp [Char]
    forall a. a -> Lisp a
    A ([Char] -> [Char]
    quote [Char]
    s)] ]
    lispifyResponse (Resp_Status Status
    s)
        = [Lisp [Char]] -> TCMT IO [Lisp [Char]]
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [ [Lisp [Char]] -> Lisp [Char]
    forall a. [Lisp a] -> Lisp a
    L [ [Char] -> Lisp [Char]
    forall a. a -> Lisp a
    A [Char]
    "agda2-status-action"
                     , [Char] -> Lisp [Char]
    forall a. a -> Lisp a
    A ([Char] -> [Char]
    quote ([Char] -> [Char]) -> [Char] -> [Char]
    forall a b. (a -> b) -> a -> b
    $ [Char] -> [[Char]] -> [Char]
    forall a. [a] -> [[a]] -> [a]
    List.intercalate [Char]
    "," ([[Char]] -> [Char]) -> [[Char]] -> [Char]
    forall a b. (a -> b) -> a -> b
    $ [Maybe [Char]] -> [[Char]]
    forall a. [Maybe a] -> [a]
    catMaybes [Maybe [Char]
    checked, Maybe [Char]
    showImpl, Maybe [Char]
    showIrr])
                     ]
                 ]
      where
        checked :: Maybe [Char]
    checked  = Bool -> [Char] -> Maybe [Char]
    forall a. Bool -> a -> Maybe a
    boolToMaybe (Status -> Bool
    sChecked                 Status
    s) [Char]
    "Checked"
        showImpl :: Maybe [Char]
    showImpl = Bool -> [Char] -> Maybe [Char]
    forall a. Bool -> a -> Maybe a
    boolToMaybe (Status -> Bool
    sShowImplicitArguments   Status
    s) [Char]
    "ShowImplicit"
        showIrr :: Maybe [Char]
    showIrr  = Bool -> [Char] -> Maybe [Char]
    forall a. Bool -> a -> Maybe a
    boolToMaybe (Status -> Bool
    sShowIrrelevantArguments Status
    s) [Char]
    "ShowIrrelevant"

    lispifyResponse (Resp_JumpToError [Char]
    f Word32
    p) = [Lisp [Char]] -> TCMT IO [Lisp [Char]]
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return
      [ Integer -> Lisp [Char] -> Lisp [Char]
    lastTag Integer
    3 (Lisp [Char] -> Lisp [Char]) -> Lisp [Char] -> Lisp [Char]
    forall a b. (a -> b) -> a -> b
    $
          [Lisp [Char]] -> Lisp [Char]
    forall a. [Lisp a] -> Lisp a
    L [ [Char] -> Lisp [Char]
    forall a. a -> Lisp a
    A [Char]
    "agda2-maybe-goto", Lisp [Char] -> Lisp [Char]
    forall a. Lisp a -> Lisp a
    Q (Lisp [Char] -> Lisp [Char]) -> Lisp [Char] -> Lisp [Char]
    forall a b. (a -> b) -> a -> b
    $ [Lisp [Char]] -> Lisp [Char]
    forall a. [Lisp a] -> Lisp a
    L [[Char] -> Lisp [Char]
    forall a. a -> Lisp a
    A ([Char] -> [Char]
    quote [Char]
    f), [Char] -> Lisp [Char]
    forall a. a -> Lisp a
    A [Char]
    ".", [Char] -> Lisp [Char]
    forall a. a -> Lisp a
    A (Word32 -> [Char]
    forall a. Show a => a -> [Char]
    show Word32
    p)] ]
      ]
    lispifyResponse (Resp_InteractionPoints [InteractionId]
    is) = [Lisp [Char]] -> TCMT IO [Lisp [Char]]
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return
      [ Integer -> Lisp [Char] -> Lisp [Char]
    lastTag Integer
    1 (Lisp [Char] -> Lisp [Char]) -> Lisp [Char] -> Lisp [Char]
    forall a b. (a -> b) -> a -> b
    $
          [Lisp [Char]] -> Lisp [Char]
    forall a. [Lisp a] -> Lisp a
    L [[Char] -> Lisp [Char]
    forall a. a -> Lisp a
    A [Char]
    "agda2-goals-action", Lisp [Char] -> Lisp [Char]
    forall a. Lisp a -> Lisp a
    Q (Lisp [Char] -> Lisp [Char]) -> Lisp [Char] -> Lisp [Char]
    forall a b. (a -> b) -> a -> b
    $ [Lisp [Char]] -> Lisp [Char]
    forall a. [Lisp a] -> Lisp a
    L ([Lisp [Char]] -> Lisp [Char]) -> [Lisp [Char]] -> Lisp [Char]
    forall a b. (a -> b) -> a -> b
    $ (InteractionId -> Lisp [Char]) -> [InteractionId] -> [Lisp [Char]]
    forall a b. (a -> b) -> [a] -> [b]
    map InteractionId -> Lisp [Char]
    showNumIId [InteractionId]
    is]
      ]
    lispifyResponse (Resp_GiveAction InteractionId
    ii GiveResult
    s)
        = [Lisp [Char]] -> TCMT IO [Lisp [Char]]
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [ [Lisp [Char]] -> Lisp [Char]
    forall a. [Lisp a] -> Lisp a
    L [ [Char] -> Lisp [Char]
    forall a. a -> Lisp a
    A [Char]
    "agda2-give-action", InteractionId -> Lisp [Char]
    showNumIId InteractionId
    ii, [Char] -> Lisp [Char]
    forall a. a -> Lisp a
    A [Char]
    s' ] ]
      where
        s' :: [Char]
    s' = case GiveResult
    s of
            Give_String [Char]
    str -> [Char] -> [Char]
    quote [Char]
    str
            GiveResult
    Give_Paren      -> [Char]
    "'paren"
            GiveResult
    Give_NoParen    -> [Char]
    "'no-paren"
    lispifyResponse (Resp_MakeCase InteractionId
    ii MakeCaseVariant
    variant [[Char]]
    pcs) = [Lisp [Char]] -> TCMT IO [Lisp [Char]]
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return
      [ Integer -> Lisp [Char] -> Lisp [Char]
    lastTag Integer
    2 (Lisp [Char] -> Lisp [Char]) -> Lisp [Char] -> Lisp [Char]
    forall a b. (a -> b) -> a -> b
    $ [Lisp [Char]] -> Lisp [Char]
    forall a. [Lisp a] -> Lisp a
    L [ [Char] -> Lisp [Char]
    forall a. a -> Lisp a
    A [Char]
    cmd, Lisp [Char] -> Lisp [Char]
    forall a. Lisp a -> Lisp a
    Q (Lisp [Char] -> Lisp [Char]) -> Lisp [Char] -> Lisp [Char]
    forall a b. (a -> b) -> a -> b
    $ [Lisp [Char]] -> Lisp [Char]
    forall a. [Lisp a] -> Lisp a
    L ([Lisp [Char]] -> Lisp [Char]) -> [Lisp [Char]] -> Lisp [Char]
    forall a b. (a -> b) -> a -> b
    $ ([Char] -> Lisp [Char]) -> [[Char]] -> [Lisp [Char]]
    forall a b. (a -> b) -> [a] -> [b]
    map ([Char] -> Lisp [Char]
    forall a. a -> Lisp a
    A ([Char] -> Lisp [Char])
    -> ([Char] -> [Char]) -> [Char] -> Lisp [Char]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Char] -> [Char]
    quote) [[Char]]
    pcs ] ]
      where
      cmd :: [Char]
    cmd = case MakeCaseVariant
    variant of
        MakeCaseVariant
    R.Function       -> [Char]
    "agda2-make-case-action"
        MakeCaseVariant
    R.ExtendedLambda -> [Char]
    "agda2-make-case-action-extendlam"
    lispifyResponse (Resp_SolveAll [(InteractionId, Expr)]
    ps) = [Lisp [Char]] -> TCMT IO [Lisp [Char]]
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return
      [ Integer -> Lisp [Char] -> Lisp [Char]
    lastTag Integer
    2 (Lisp [Char] -> Lisp [Char]) -> Lisp [Char] -> Lisp [Char]
    forall a b. (a -> b) -> a -> b
    $
          [Lisp [Char]] -> Lisp [Char]
    forall a. [Lisp a] -> Lisp a
    L [ [Char] -> Lisp [Char]
    forall a. a -> Lisp a
    A [Char]
    "agda2-solveAll-action", Lisp [Char] -> Lisp [Char]
    forall a. Lisp a -> Lisp a
    Q (Lisp [Char] -> Lisp [Char])
    -> ([Lisp [Char]] -> Lisp [Char]) -> [Lisp [Char]] -> Lisp [Char]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Lisp [Char]] -> Lisp [Char]
    forall a. [Lisp a] -> Lisp a
    L ([Lisp [Char]] -> Lisp [Char]) -> [Lisp [Char]] -> Lisp [Char]
    forall a b. (a -> b) -> a -> b
    $ ((InteractionId, Expr) -> [Lisp [Char]])
    -> [(InteractionId, Expr)] -> [Lisp [Char]]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap (InteractionId, Expr) -> [Lisp [Char]]
    forall {a}. Pretty a => (InteractionId, a) -> [Lisp [Char]]
    prn [(InteractionId, Expr)]
    ps ]
      ]
      where
        prn :: (InteractionId, a) -> [Lisp [Char]]
    prn (InteractionId
    ii,a
    e)= [InteractionId -> Lisp [Char]
    showNumIId InteractionId
    ii, [Char] -> Lisp [Char]
    forall a. a -> Lisp a
    A ([Char] -> Lisp [Char]) -> [Char] -> Lisp [Char]
    forall a b. (a -> b) -> a -> b
    $ [Char] -> [Char]
    quote ([Char] -> [Char]) -> [Char] -> [Char]
    forall a b. (a -> b) -> a -> b
    $ a -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow a
    e]
    -- TODO: For now, I piggy-back on the Resp_SolveAll implementation
    lispifyResponse (Resp_Mimer InteractionId
    ii Maybe [Char]
    msol) = [Lisp [Char]] -> TCMT IO [Lisp [Char]]
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Lisp [Char]] -> TCMT IO [Lisp [Char]])
    -> [Lisp [Char]] -> TCMT IO [Lisp [Char]]
    forall a b. (a -> b) -> a -> b
    $ case Maybe [Char]
    msol of
      Maybe [Char]
    Nothing ->
        [ Integer -> Lisp [Char] -> Lisp [Char]
    lastTag Integer
    1 (Lisp [Char] -> Lisp [Char]) -> Lisp [Char] -> Lisp [Char]
    forall a b. (a -> b) -> a -> b
    $ -- TODO: What is this lastTag used for?
            [Lisp [Char]] -> Lisp [Char]
    forall a. [Lisp a] -> Lisp a
    L [ [Char] -> Lisp [Char]
    forall a. a -> Lisp a
    A [Char]
    "agda2-info-action", [Char] -> Lisp [Char]
    forall a. a -> Lisp a
    A ([Char] -> Lisp [Char]) -> [Char] -> Lisp [Char]
    forall a b. (a -> b) -> a -> b
    $ [Char] -> [Char]
    quote [Char]
    "*Mimer*", [Char] -> Lisp [Char]
    forall a. a -> Lisp a
    A ([Char] -> Lisp [Char]) -> [Char] -> Lisp [Char]
    forall a b. (a -> b) -> a -> b
    $ [Char] -> [Char]
    quote [Char]
    "No solution found" ]
        ]
      Just [Char]
    str ->
        [ Integer -> Lisp [Char] -> Lisp [Char]
    lastTag Integer
    1 (Lisp [Char] -> Lisp [Char]) -> Lisp [Char] -> Lisp [Char]
    forall a b. (a -> b) -> a -> b
    $ -- TODO: What is this lastTag used for?
            [Lisp [Char]] -> Lisp [Char]
    forall a. [Lisp a] -> Lisp a
    L [ [Char] -> Lisp [Char]
    forall a. a -> Lisp a
    A [Char]
    "agda2-solve-action", InteractionId -> Lisp [Char]
    showNumIId InteractionId
    ii, [Char] -> Lisp [Char]
    forall a. a -> Lisp a
    A ([Char] -> Lisp [Char]) -> [Char] -> Lisp [Char]
    forall a b. (a -> b) -> a -> b
    $ [Char] -> [Char]
    quote [Char]
    str ]
        ]

    lispifyDisplayInfo :: DisplayInfo -> TCM [Lisp String]
    lispifyDisplayInfo :: DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
    -> TCMT IO [Lisp [Char]]
    lispifyDisplayInfo DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
    info = case DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
    info of
        Info_CompilationOk CompilerBackend
    backend WarningsAndNonFatalErrors
    ws -> do
          warnings <- Set TCWarning -> TCM [Char]
    prettyTCWarnings (WarningsAndNonFatalErrors -> Set TCWarning
    tcWarnings WarningsAndNonFatalErrors
    ws)
          errors <- prettyTCWarnings (nonFatalErrors ws)
          let
            msg = [[Char]] -> [Char]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat
              [ [Char]
    "The module was successfully compiled with backend "
              , CompilerBackend -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow CompilerBackend
    backend
              , [Char]
    ".\n"
              ]
          -- abusing the goals field since we ignore the title
            (body, _) = formatWarningsAndErrors msg warnings errors
          format body "*Compilation result*"
        Info_Constraints [OutputForm_boot TCErr Expr Expr]
    s -> do
          doc <- [TCMT IO (Doc Aspects)] -> TCMT IO (Doc Aspects)
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m (Doc Aspects)) -> m (Doc Aspects)
    TCP.vcat ([TCMT IO (Doc Aspects)] -> TCMT IO (Doc Aspects))
    -> [TCMT IO (Doc Aspects)] -> TCMT IO (Doc Aspects)
    forall a b. (a -> b) -> a -> b
    $ (OutputForm_boot TCErr Expr Expr -> TCMT IO (Doc Aspects))
    -> [OutputForm_boot TCErr Expr Expr] -> [TCMT IO (Doc Aspects)]
    forall a b. (a -> b) -> [a] -> [b]
    map OutputForm_boot TCErr Expr Expr -> TCMT IO (Doc Aspects)
    forall a (m :: * -> *).
    (PrettyTCM a, MonadPretty m) =>
    a -> m (Doc Aspects)
    forall (m :: * -> *).
    MonadPretty m =>
    OutputForm_boot TCErr Expr Expr -> m (Doc Aspects)
    prettyTCM [OutputForm_boot TCErr Expr Expr]
    s
          format (render doc) "*Constraints*"
        Info_AllGoalsWarnings Goals_boot TCErr
    ms WarningsAndNonFatalErrors
    ws -> do
          goals <- Goals_boot TCErr -> TCM [Char]
    showGoals Goals_boot TCErr
    ms
          warnings <- prettyTCWarnings (tcWarnings ws)
          errors <- prettyTCWarnings (nonFatalErrors ws)
          let (body, title) = formatWarningsAndErrors goals warnings errors
          format body ("*All" ++ title ++ "*")
        Info_Auto [Char]
    s -> [Char] -> [Char] -> TCMT IO [Lisp [Char]]
    format [Char]
    s [Char]
    "*Auto*"
        Info_Error Info_Error_boot TCErr TCWarning
    err -> do
          s <- Info_Error_boot TCErr TCWarning -> TCM [Char]
    showInfoError Info_Error_boot TCErr TCWarning
    err
          format s "*Error*"
        Info_Time CPUTime
    s -> [Char] -> [Char] -> TCMT IO [Lisp [Char]]
    format (Doc Aspects -> [Char]
    forall a. Doc a -> [Char]
    render (Doc Aspects -> [Char]) -> Doc Aspects -> [Char]
    forall a b. (a -> b) -> a -> b
    $ CPUTime -> Doc Aspects
    prettyTimed CPUTime
    s) [Char]
    "*Time*"
        Info_NormalForm CommandState
    state ComputeMode
    cmode Maybe CPUTime
    time Expr
    expr -> do
          exprDoc <- StateT CommandState (TCMT IO) (Doc Aspects)
    -> CommandState -> TCMT IO (Doc Aspects)
    forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
    evalStateT StateT CommandState (TCMT IO) (Doc Aspects)
    prettyExpr CommandState
    state
          let doc = Doc Aspects
    -> (CPUTime -> Doc Aspects) -> Maybe CPUTime -> Doc Aspects
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Doc Aspects
    forall a. Null a => a
    empty CPUTime -> Doc Aspects
    prettyTimed Maybe CPUTime
    time Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    $$ Doc Aspects
    exprDoc
              lbl | ComputeMode
    cmode ComputeMode -> ComputeMode -> Bool
    forall a. Eq a => a -> a -> Bool
    == ComputeMode
    HeadCompute = [Char]
    "*Head Normal Form*"
                  | Bool
    otherwise            = [Char]
    "*Normal Form*"
          format (render doc) lbl
          where
            prettyExpr :: StateT CommandState (TCMT IO) (Doc Aspects)
    prettyExpr = StateT CommandState (TCMT IO) (Doc Aspects)
    -> StateT CommandState (TCMT IO) (Doc Aspects)
    forall a. CommandM a -> CommandM a
    localStateCommandM
                (StateT CommandState (TCMT IO) (Doc Aspects)
     -> StateT CommandState (TCMT IO) (Doc Aspects))
    -> StateT CommandState (TCMT IO) (Doc Aspects)
    -> StateT CommandState (TCMT IO) (Doc Aspects)
    forall a b. (a -> b) -> a -> b
    $ TCMT IO (Doc Aspects)
    -> StateT CommandState (TCMT IO) (Doc Aspects)
    forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift
                (TCMT IO (Doc Aspects)
     -> StateT CommandState (TCMT IO) (Doc Aspects))
    -> TCMT IO (Doc Aspects)
    -> StateT CommandState (TCMT IO) (Doc Aspects)
    forall a b. (a -> b) -> a -> b
    $ TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects)
    forall a. TCM a -> TCM a
    B.atTopLevel
                (TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects))
    -> TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects)
    forall a b. (a -> b) -> a -> b
    $ TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects)
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    allowNonTerminatingReductions
                (TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects))
    -> TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects)
    forall a b. (a -> b) -> a -> b
    $ (if ComputeMode -> Bool
    computeIgnoreAbstract ComputeMode
    cmode then TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects)
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    ignoreAbstractMode else TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects)
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    inConcreteMode)
                (TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects))
    -> TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects)
    forall a b. (a -> b) -> a -> b
    $ (ComputeMode -> Expr -> TCMT IO (Doc Aspects)
    B.showComputed ComputeMode
    cmode)
                (Expr -> TCMT IO (Doc Aspects)) -> Expr -> TCMT IO (Doc Aspects)
    forall a b. (a -> b) -> a -> b
    $ Expr
    expr
        Info_InferredType CommandState
    state Maybe CPUTime
    time Expr
    expr -> do
          exprDoc <- StateT CommandState (TCMT IO) (Doc Aspects)
    -> CommandState -> TCMT IO (Doc Aspects)
    forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
    evalStateT StateT CommandState (TCMT IO) (Doc Aspects)
    prettyExpr CommandState
    state
          let doc = Doc Aspects
    -> (CPUTime -> Doc Aspects) -> Maybe CPUTime -> Doc Aspects
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Doc Aspects
    forall a. Null a => a
    empty CPUTime -> Doc Aspects
    prettyTimed Maybe CPUTime
    time Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    $$ Doc Aspects
    exprDoc
          format (render doc) "*Inferred Type*"
          where
            prettyExpr :: StateT CommandState (TCMT IO) (Doc Aspects)
    prettyExpr = StateT CommandState (TCMT IO) (Doc Aspects)
    -> StateT CommandState (TCMT IO) (Doc Aspects)
    forall a. CommandM a -> CommandM a
    localStateCommandM
                (StateT CommandState (TCMT IO) (Doc Aspects)
     -> StateT CommandState (TCMT IO) (Doc Aspects))
    -> StateT CommandState (TCMT IO) (Doc Aspects)
    -> StateT CommandState (TCMT IO) (Doc Aspects)
    forall a b. (a -> b) -> a -> b
    $ TCMT IO (Doc Aspects)
    -> StateT CommandState (TCMT IO) (Doc Aspects)
    forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift
                (TCMT IO (Doc Aspects)
     -> StateT CommandState (TCMT IO) (Doc Aspects))
    -> TCMT IO (Doc Aspects)
    -> StateT CommandState (TCMT IO) (Doc Aspects)
    forall a b. (a -> b) -> a -> b
    $ TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects)
    forall a. TCM a -> TCM a
    B.atTopLevel
                (TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects))
    -> TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects)
    forall a b. (a -> b) -> a -> b
    $ Expr -> TCMT IO (Doc Aspects)
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m (Doc Aspects)
    TCP.prettyA
                (Expr -> TCMT IO (Doc Aspects)) -> Expr -> TCMT IO (Doc Aspects)
    forall a b. (a -> b) -> a -> b
    $ Expr
    expr
        Info_ModuleContents [Name]
    modules Telescope
    tel [(Name, Type)]
    types -> do
          doc <- TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects)
    forall a. TCM a -> TCM a
    localTCState (TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects))
    -> TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects)
    forall a b. (a -> b) -> a -> b
    $ do
            typeDocs <- Telescope
    -> TCMT IO [([Char], Doc Aspects)]
    -> TCMT IO [([Char], Doc Aspects)]
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Telescope -> m a -> m a
    addContext Telescope
    tel (TCMT IO [([Char], Doc Aspects)]
     -> TCMT IO [([Char], Doc Aspects)])
    -> TCMT IO [([Char], Doc Aspects)]
    -> TCMT IO [([Char], Doc Aspects)]
    forall a b. (a -> b) -> a -> b
    $ [(Name, Type)]
    -> ((Name, Type) -> TCMT IO ([Char], Doc Aspects))
    -> TCMT IO [([Char], Doc Aspects)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM [(Name, Type)]
    types (((Name, Type) -> TCMT IO ([Char], Doc Aspects))
     -> TCMT IO [([Char], Doc Aspects)])
    -> ((Name, Type) -> TCMT IO ([Char], Doc Aspects))
    -> TCMT IO [([Char], Doc Aspects)]
    forall a b. (a -> b) -> a -> b
    $ \ (Name
    x, Type
    t) -> do
              doc <- Type -> TCMT IO (Doc Aspects)
    forall a (m :: * -> *).
    (PrettyTCM a, MonadPretty m) =>
    a -> m (Doc Aspects)
    forall (m :: * -> *). MonadPretty m => Type -> m (Doc Aspects)
    prettyTCM Type
    t
              return (prettyShow x, ":" <+> doc)
            return $ vcat
              [ "Modules"
              , nest 2 $ vcat $ map pretty modules
              , "Names"
              , nest 2 $ align 10 typeDocs
              ]
          format (render doc) "*Module contents*"
        Info_SearchAbout [(Name, Type)]
    hits [Char]
    names -> do
          hitDocs <- [(Name, Type)]
    -> ((Name, Type) -> TCMT IO ([Char], Doc Aspects))
    -> TCMT IO [([Char], Doc Aspects)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM [(Name, Type)]
    hits (((Name, Type) -> TCMT IO ([Char], Doc Aspects))
     -> TCMT IO [([Char], Doc Aspects)])
    -> ((Name, Type) -> TCMT IO ([Char], Doc Aspects))
    -> TCMT IO [([Char], Doc Aspects)]
    forall a b. (a -> b) -> a -> b
    $ \ (Name
    x, Type
    t) -> do
            doc <- Type -> TCMT IO (Doc Aspects)
    forall a (m :: * -> *).
    (PrettyTCM a, MonadPretty m) =>
    a -> m (Doc Aspects)
    forall (m :: * -> *). MonadPretty m => Type -> m (Doc Aspects)
    prettyTCM Type
    t
            return (prettyShow x, ":" <+> doc)
          let doc = Doc Aspects
    "Definitions about" Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+>
                    [Char] -> Doc Aspects
    forall a. [Char] -> Doc a
    text ([Char] -> [[Char]] -> [Char]
    forall a. [a] -> [[a]] -> [a]
    List.intercalate [Char]
    ", " ([[Char]] -> [Char]) -> [[Char]] -> [Char]
    forall a b. (a -> b) -> a -> b
    $ [Char] -> [[Char]]
    words [Char]
    names) Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    $$ Nat -> Doc Aspects -> Doc Aspects
    forall a. Nat -> Doc a -> Doc a
    nest Nat
    2 (Nat -> [([Char], Doc Aspects)] -> Doc Aspects
    align Nat
    10 [([Char], Doc Aspects)]
    hitDocs)
          format (render doc) "*Search About*"
        Info_WhyInScope WhyInScopeData
    why -> do
          doc <- WhyInScopeData -> TCMT IO (Doc Aspects)
    forall (m :: * -> *).
    MonadPretty m =>
    WhyInScopeData -> m (Doc Aspects)
    explainWhyInScope WhyInScopeData
    why
          format (render doc) "*Scope Info*"
        Info_Context InteractionId
    ii [ResponseContextEntry]
    ctx -> do
          doc <- TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects)
    forall a. TCM a -> TCM a
    localTCState (InteractionId
    -> Bool -> [ResponseContextEntry] -> TCMT IO (Doc Aspects)
    prettyResponseContext InteractionId
    ii Bool
    False [ResponseContextEntry]
    ctx)
          format (render doc) "*Context*"
        DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
    Info_Intro_NotFound -> [Char] -> [Char] -> TCMT IO [Lisp [Char]]
    format [Char]
    "No introduction forms found." [Char]
    "*Intro*"
        Info_Intro_ConstructorUnknown [[Char]]
    ss -> do
          let doc :: Doc Aspects
    doc = [Doc Aspects] -> Doc Aspects
    forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
    sep [ Doc Aspects
    "Don't know which constructor to introduce of"
                        , let mkOr :: [[Char]] -> [Doc a]
    mkOr []     = []
                              mkOr [[Char]
    x, [Char]
    y] = [[Char] -> Doc a
    forall a. [Char] -> Doc a
    text [Char]
    x Doc a -> Doc a -> Doc a
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc a
    "or" Doc a -> Doc a -> Doc a
    forall a. Doc a -> Doc a -> Doc a
    <+> [Char] -> Doc a
    forall a. [Char] -> Doc a
    text [Char]
    y]
                              mkOr ([Char]
    x:[[Char]]
    xs) = [Char] -> Doc a
    forall a. [Char] -> Doc a
    text [Char]
    x Doc a -> [Doc a] -> [Doc a]
    forall a. a -> [a] -> [a]
    : [[Char]] -> [Doc a]
    mkOr [[Char]]
    xs
                          in Nat -> Doc Aspects -> Doc Aspects
    forall a. Nat -> Doc a -> Doc a
    nest Nat
    2 (Doc Aspects -> Doc Aspects) -> Doc Aspects -> Doc Aspects
    forall a b. (a -> b) -> a -> b
    $ [Doc Aspects] -> Doc Aspects
    forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
    fsep ([Doc Aspects] -> Doc Aspects) -> [Doc Aspects] -> Doc Aspects
    forall a b. (a -> b) -> a -> b
    $ Doc Aspects -> [Doc Aspects] -> [Doc Aspects]
    forall (t :: * -> *).
    Foldable t =>
    Doc Aspects -> t (Doc Aspects) -> [Doc Aspects]
    punctuate Doc Aspects
    comma ([[Char]] -> [Doc Aspects]
    forall {a}. [[Char]] -> [Doc a]
    mkOr [[Char]]
    ss)
                        ]
          [Char] -> [Char] -> TCMT IO [Lisp [Char]]
    format (Doc Aspects -> [Char]
    forall a. Doc a -> [Char]
    render Doc Aspects
    doc) [Char]
    "*Intro*"
        DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
    Info_Version -> [Char] -> [Char] -> TCMT IO [Lisp [Char]]
    format ([Char]
    "Agda version " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    versionWithCommitInfo) [Char]
    "*Agda Version*"
        Info_GoalSpecific InteractionId
    ii GoalDisplayInfo_boot TCErr
    kind -> InteractionId
    -> GoalDisplayInfo_boot TCErr -> TCMT IO [Lisp [Char]]
    lispifyGoalSpecificDisplayInfo InteractionId
    ii GoalDisplayInfo_boot TCErr
    kind

    lispifyGoalSpecificDisplayInfo :: InteractionId -> GoalDisplayInfo -> TCM [Lisp String]
    lispifyGoalSpecificDisplayInfo :: InteractionId
    -> GoalDisplayInfo_boot TCErr -> TCMT IO [Lisp [Char]]
    lispifyGoalSpecificDisplayInfo InteractionId
    ii GoalDisplayInfo_boot TCErr
    kind = TCMT IO [Lisp [Char]] -> TCMT IO [Lisp [Char]]
    forall a. TCM a -> TCM a
    localTCState (TCMT IO [Lisp [Char]] -> TCMT IO [Lisp [Char]])
    -> TCMT IO [Lisp [Char]] -> TCMT IO [Lisp [Char]]
    forall a b. (a -> b) -> a -> b
    $ InteractionId -> TCMT IO [Lisp [Char]] -> TCMT IO [Lisp [Char]]
    forall (m :: * -> *) a.
    (MonadDebug m, ReadTCState m, MonadError TCErr m, MonadTCEnv m,
     MonadTrace m) =>
    InteractionId -> m a -> m a
    withInteractionId InteractionId
    ii (TCMT IO [Lisp [Char]] -> TCMT IO [Lisp [Char]])
    -> TCMT IO [Lisp [Char]] -> TCMT IO [Lisp [Char]]
    forall a b. (a -> b) -> a -> b
    $
      case GoalDisplayInfo_boot TCErr
    kind of
        Goal_HelperFunction OutputConstraint' Expr Expr
    helperType -> do
          doc <- TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects)
    forall (tcm :: * -> *) a.
    (MonadTCEnv tcm, ReadTCState tcm) =>
    tcm a -> tcm a
    inTopContext (TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects))
    -> TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects)
    forall a b. (a -> b) -> a -> b
    $ OutputConstraint' Expr Expr -> TCMT IO (Doc Aspects)
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m (Doc Aspects)
    prettyATop OutputConstraint' Expr Expr
    helperType
          return [ L [ A "agda2-info-action-and-copy"
                     , A $ quote "*Helper function*"
                     , A $ quote (render doc ++ "\n")
                     , A "nil"
                     ]
                 ]
        Goal_NormalForm ComputeMode
    cmode Expr
    expr -> do
          doc <- ComputeMode -> Expr -> TCMT IO (Doc Aspects)
    showComputed ComputeMode
    cmode Expr
    expr
          format (render doc) "*Normal Form*"   -- show?
        Goal_GoalType Rewrite
    norm GoalTypeAux
    aux [ResponseContextEntry]
    ctx [IPFace' Expr]
    bndry [OutputForm_boot TCErr Expr Expr]
    constraints -> do
          ctxDoc <- InteractionId
    -> Bool -> [ResponseContextEntry] -> TCMT IO (Doc Aspects)
    prettyResponseContext InteractionId
    ii Bool
    True [ResponseContextEntry]
    ctx
          goalDoc <- prettyTypeOfMeta norm ii
          let boundaryDoc [Char]
    hd [a]
    bndry
                | [a] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [a]
    bndry = []
                | Bool
    otherwise  = [ [Char] -> Doc Aspects
    forall a. [Char] -> Doc a
    text ([Char] -> Doc Aspects) -> [Char] -> Doc Aspects
    forall a b. (a -> b) -> a -> b
    $ [Char] -> [Char]
    delimiter [Char]
    hd
                               , [Doc Aspects] -> Doc Aspects
    forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
    vcat ([Doc Aspects] -> Doc Aspects) -> [Doc Aspects] -> Doc Aspects
    forall a b. (a -> b) -> a -> b
    $ (a -> Doc Aspects) -> [a] -> [Doc Aspects]
    forall a b. (a -> b) -> [a] -> [b]
    map a -> Doc Aspects
    forall a. Pretty a => a -> Doc Aspects
    pretty [a]
    bndry
                               ]
          auxDoc <- case aux of
                GoalTypeAux
    GoalOnly -> Doc Aspects -> TCMT IO (Doc Aspects)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Doc Aspects
    forall a. Null a => a
    empty
                GoalAndHave Expr
    expr [IPFace' Expr]
    bndry -> do
                  doc <- Expr -> TCMT IO (Doc Aspects)
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m (Doc Aspects)
    prettyATop Expr
    expr
                  return $ ("Have:" <+> doc) $$ vcat (boundaryDoc ("Boundary (actual)") bndry)
                GoalAndElaboration Expr
    expr -> do
                  doc <- Expr -> TCMT IO (Doc Aspects)
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m (Doc Aspects)
    prettyATop Expr
    expr
                  return $ "Elaborates to:" <+> doc
          let constraintsDoc
                | [OutputForm_boot TCErr Expr Expr] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [OutputForm_boot TCErr Expr Expr]
    constraints = []
                | Bool
    otherwise        =
                  [ [Char] -> TCMT IO (Doc Aspects)
    forall (m :: * -> *). Applicative m => [Char] -> m (Doc Aspects)
    TCP.text ([Char] -> TCMT IO (Doc Aspects))
    -> [Char] -> TCMT IO (Doc Aspects)
    forall a b. (a -> b) -> a -> b
    $ [Char] -> [Char]
    delimiter [Char]
    "Constraints"
                  , [TCMT IO (Doc Aspects)] -> TCMT IO (Doc Aspects)
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m (Doc Aspects)) -> m (Doc Aspects)
    TCP.vcat ([TCMT IO (Doc Aspects)] -> TCMT IO (Doc Aspects))
    -> [TCMT IO (Doc Aspects)] -> TCMT IO (Doc Aspects)
    forall a b. (a -> b) -> a -> b
    $ (OutputForm_boot TCErr Expr Expr -> TCMT IO (Doc Aspects))
    -> [OutputForm_boot TCErr Expr Expr] -> [TCMT IO (Doc Aspects)]
    forall a b. (a -> b) -> [a] -> [b]
    map OutputForm_boot TCErr Expr Expr -> TCMT IO (Doc Aspects)
    forall a (m :: * -> *).
    (PrettyTCM a, MonadPretty m) =>
    a -> m (Doc Aspects)
    forall (m :: * -> *).
    MonadPretty m =>
    OutputForm_boot TCErr Expr Expr -> m (Doc Aspects)
    prettyTCM [OutputForm_boot TCErr Expr Expr]
    constraints
                  ]
          doc <- TCP.vcat $
            [ "Goal:" TCP.<+> return goalDoc
            , return (vcat (boundaryDoc "Boundary (wanted)" bndry))
            , return auxDoc
            , TCP.text (replicate 60 '\x2014')
            , return ctxDoc
            ] ++ constraintsDoc
          format (render doc) "*Goal type etc.*"
        Goal_CurrentGoal Rewrite
    norm -> do
          doc <- Rewrite -> InteractionId -> TCMT IO (Doc Aspects)
    prettyTypeOfMeta Rewrite
    norm InteractionId
    ii
          format (render doc) "*Current Goal*"
        Goal_InferredType Expr
    expr -> do
          doc <- Expr -> TCMT IO (Doc Aspects)
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m (Doc Aspects)
    prettyATop Expr
    expr
          format (render doc) "*Inferred Type*"

    -- | Format responses of DisplayInfo

    format :: String -> String -> TCM [Lisp String]
    format :: [Char] -> [Char] -> TCMT IO [Lisp [Char]]
    format [Char]
    content [Char]
    bufname = [Lisp [Char]] -> TCMT IO [Lisp [Char]]
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [ Bool -> [Char] -> [Char] -> Lisp [Char]
    display_info' Bool
    False [Char]
    bufname [Char]
    content ]

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

    lastTag :: Integer -> Lisp String -> Lisp String
    lastTag :: Integer -> Lisp [Char] -> Lisp [Char]
    lastTag Integer
    n Lisp [Char]
    r = Lisp [Char] -> Lisp [Char] -> Lisp [Char]
    forall a. Lisp a -> Lisp a -> Lisp a
    Cons (Lisp [Char] -> Lisp [Char] -> Lisp [Char]
    forall a. Lisp a -> Lisp a -> Lisp a
    Cons ([Char] -> Lisp [Char]
    forall a. a -> Lisp a
    A [Char]
    "last") ([Char] -> Lisp [Char]
    forall a. a -> Lisp a
    A ([Char] -> Lisp [Char]) -> [Char] -> Lisp [Char]
    forall a b. (a -> b) -> a -> b
    $ Integer -> [Char]
    forall a. Show a => a -> [Char]
    show Integer
    n)) Lisp [Char]
    r

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

    showNumIId :: InteractionId -> Lisp String
    showNumIId :: InteractionId -> Lisp [Char]
    showNumIId = [Char] -> Lisp [Char]
    forall a. a -> Lisp a
    A ([Char] -> Lisp [Char])
    -> (InteractionId -> [Char]) -> InteractionId -> Lisp [Char]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Nat -> [Char]
    forall a. Show a => a -> [Char]
    show (Nat -> [Char])
    -> (InteractionId -> Nat) -> InteractionId -> [Char]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . InteractionId -> Nat
    interactionId

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

    -- | Given strings of goals, warnings and errors, return a pair of the
    --   body and the title for the info buffer
    formatWarningsAndErrors :: String -> String -> String -> (String, String)
    formatWarningsAndErrors :: [Char] -> [Char] -> [Char] -> ([Char], [Char])
    formatWarningsAndErrors [Char]
    g [Char]
    w [Char]
    e = ([Char]
    body, [Char]
    title)
      where
        isG :: Bool
    isG = Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [Char]
    g
        isW :: Bool
    isW = Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [Char]
    w
        isE :: Bool
    isE = Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [Char]
    e
        title :: [Char]
    title = [Char] -> [[Char]] -> [Char]
    forall a. [a] -> [[a]] -> [a]
    List.intercalate [Char]
    "," ([[Char]] -> [Char]) -> [[Char]] -> [Char]
    forall a b. (a -> b) -> a -> b
    $ [Maybe [Char]] -> [[Char]]
    forall a. [Maybe a] -> [a]
    catMaybes
                  [ [Char]
    " Goals"    [Char] -> Maybe () -> Maybe [Char]
    forall a b. a -> Maybe b -> Maybe a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Bool -> Maybe ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard Bool
    isG
                  , [Char]
    " Errors"   [Char] -> Maybe () -> Maybe [Char]
    forall a b. a -> Maybe b -> Maybe a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Bool -> Maybe ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard Bool
    isE
                  , [Char]
    " Warnings" [Char] -> Maybe () -> Maybe [Char]
    forall a b. a -> Maybe b -> Maybe a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Bool -> Maybe ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard Bool
    isW
                  , [Char]
    " Done"     [Char] -> Maybe () -> Maybe [Char]
    forall a b. a -> Maybe b -> Maybe a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Bool -> Maybe ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Bool -> Bool
    not (Bool
    isG Bool -> Bool -> Bool
    || Bool
    isW Bool -> Bool -> Bool
    || Bool
    isE))
                  ]

        body :: [Char]
    body = [Char] -> [[Char]] -> [Char]
    forall a. [a] -> [[a]] -> [a]
    List.intercalate [Char]
    "\n" ([[Char]] -> [Char]) -> [[Char]] -> [Char]
    forall a b. (a -> b) -> a -> b
    $ [Maybe [Char]] -> [[Char]]
    forall a. [Maybe a] -> [a]
    catMaybes
                 [ [Char]
    g                    [Char] -> Maybe () -> Maybe [Char]
    forall a b. a -> Maybe b -> Maybe a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Bool -> Maybe ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard Bool
    isG
                 , [Char] -> [Char]
    delimiter [Char]
    "Error"    [Char] -> Maybe () -> Maybe [Char]
    forall a b. a -> Maybe b -> Maybe a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Bool -> Maybe ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Bool
    isE Bool -> Bool -> Bool
    && (Bool
    isG Bool -> Bool -> Bool
    || Bool
    isW))
                 , [Char]
    e                    [Char] -> Maybe () -> Maybe [Char]
    forall a b. a -> Maybe b -> Maybe a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Bool -> Maybe ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard Bool
    isE
                 , [Char] -> [Char]
    delimiter [Char]
    "Warnings" [Char] -> Maybe () -> Maybe [Char]
    forall a b. a -> Maybe b -> Maybe a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Bool -> Maybe ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Bool
    isW Bool -> Bool -> Bool
    && (Bool
    isG Bool -> Bool -> Bool
    || Bool
    isE))
                 , [Char]
    w                    [Char] -> Maybe () -> Maybe [Char]
    forall a b. a -> Maybe b -> Maybe a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Bool -> Maybe ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard Bool
    isW
                 ]

    -- | Serializing Info_Error
    showInfoError :: Info_Error -> TCM String
    showInfoError :: Info_Error_boot TCErr TCWarning -> TCM [Char]
    showInfoError (Info_GenericError TCErr
    err) = do
      e <- TCErr -> TCM [Char]
    forall (tcm :: * -> *). MonadTCM tcm => TCErr -> tcm [Char]
    renderError TCErr
    err
      w <- prettyTCWarnings =<< getAllWarningsOfTCErr err
      let (body, _) = formatWarningsAndErrors "" w e
      return body
    showInfoError (Info_CompilationError Set TCWarning
    warnings) = do
      s <- Set TCWarning -> TCM [Char]
    prettyTCWarnings Set TCWarning
    warnings
      return $ unlines
        [ "You need to fix the following errors before you can compile the module:"
        , ""
        , s
        ]
    showInfoError (Info_HighlightingParseError InteractionId
    ii) =
      [Char] -> TCM [Char]
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Char] -> TCM [Char]) -> [Char] -> TCM [Char]
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Highlighting failed to parse expression in " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ InteractionId -> [Char]
    forall a. Show a => a -> [Char]
    show InteractionId
    ii
    showInfoError (Info_HighlightingScopeCheckError InteractionId
    ii) =
      [Char] -> TCM [Char]
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Char] -> TCM [Char]) -> [Char] -> TCM [Char]
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Highlighting failed to scope check expression in " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ InteractionId -> [Char]
    forall a. Show a => a -> [Char]
    show InteractionId
    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 :: InteractionId
    -> Bool -> [ResponseContextEntry] -> TCMT IO (Doc Aspects)
    prettyResponseContext InteractionId
    ii Bool
    rev [ResponseContextEntry]
    ctx = InteractionId -> TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects)
    forall (m :: * -> *) a.
    (MonadDebug m, ReadTCState m, MonadError TCErr m, MonadTCEnv m,
     MonadTrace m) =>
    InteractionId -> m a -> m a
    withInteractionId InteractionId
    ii (TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects))
    -> TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects)
    forall a b. (a -> b) -> a -> b
    $ do
      mod <- TCMT IO Modality
    forall (m :: * -> *). MonadTCEnv m => m Modality
    currentModality
      align 10 . concat . applyWhen rev reverse <$> do
        forM ctx $ \ (ResponseContextEntry Name
    n Name
    x (Arg ArgInfo
    ai Expr
    expr) Maybe Expr
    letv NameInScope
    nis) -> do
          let
            prettyCtxName :: String
            prettyCtxName :: [Char]
    prettyCtxName
              | Name
    n Name -> Name -> Bool
    forall a. Eq a => a -> a -> Bool
    == Name
    x                 = Name -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow Name
    x
              | Name -> NameInScope
    forall a. LensInScope a => a -> NameInScope
    isInScope Name
    n NameInScope -> NameInScope -> Bool
    forall a. Eq a => a -> a -> Bool
    == NameInScope
    InScope = Name -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow Name
    n [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " = " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Name -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow Name
    x
              | Bool
    otherwise              = Name -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow Name
    x

            -- Some attributes are useful to report whenever they are not
            -- in the default state.
            attribute :: String
            attribute :: [Char]
    attribute = [Char]
    c [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ if [Char] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [Char]
    c then [Char]
    "" else [Char]
    " "
              where c :: [Char]
    c = Cohesion -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow (ArgInfo -> Cohesion
    forall a. LensCohesion a => a -> Cohesion
    getCohesion ArgInfo
    ai)

            pol :: ModalPolarity
            pol :: ModalPolarity
    pol = PolarityModality -> ModalPolarity
    modPolarityAnn (PolarityModality -> ModalPolarity)
    -> PolarityModality -> ModalPolarity
    forall a b. (a -> b) -> a -> b
    $ ArgInfo -> PolarityModality
    forall a. LensModalPolarity a => a -> PolarityModality
    getModalPolarity ArgInfo
    ai

            extras :: [Doc]
            extras :: [Doc Aspects]
    extras = [[Doc Aspects]] -> [Doc Aspects]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat ([[Doc Aspects]] -> [Doc Aspects])
    -> [[Doc Aspects]] -> [Doc Aspects]
    forall a b. (a -> b) -> a -> b
    $
              [ [ Doc Aspects
    "not in scope" | NameInScope -> NameInScope
    forall a. LensInScope a => a -> NameInScope
    isInScope NameInScope
    nis NameInScope -> NameInScope -> Bool
    forall a. Eq a => a -> a -> Bool
    == NameInScope
    C.NotInScope ]
                -- Print "erased" if hypothesis is erased but goal is non-erased.
              , [ Doc Aspects
    "erased"       | Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ ArgInfo -> Quantity
    forall a. LensQuantity a => a -> Quantity
    getQuantity  ArgInfo
    ai Quantity -> Quantity -> Bool
    `moreQuantity` Modality -> Quantity
    forall a. LensQuantity a => a -> Quantity
    getQuantity  Modality
    mod ]
                -- Print relevance of hypothesis relative to relevance of the goal. (Issue #6706.)
              , [ [Char] -> Doc Aspects
    forall a. [Char] -> Doc a
    text ([Char] -> Doc Aspects) -> [Char] -> Doc Aspects
    forall a b. (a -> b) -> a -> b
    $ Relevance -> [Char]
    forall a. Verbalize a => a -> [Char]
    verbalize Relevance
    r
                                 | let r :: Relevance
    r = Modality -> Relevance
    forall a. LensRelevance a => a -> Relevance
    getRelevance Modality
    mod Relevance -> Relevance -> Relevance
    `inverseComposeRelevance` ArgInfo -> Relevance
    forall a. LensRelevance a => a -> Relevance
    getRelevance ArgInfo
    ai
                                 , Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ Relevance -> Bool
    forall a. LensRelevance a => a -> Bool
    isRelevant Relevance
    r ]
              , [ [Char] -> Doc Aspects
    forall a. [Char] -> Doc a
    text ([Char] -> Doc Aspects) -> [Char] -> Doc Aspects
    forall a b. (a -> b) -> a -> b
    $ ModalPolarity -> [Char]
    forall a. Verbalize a => a -> [Char]
    verbalize ModalPolarity
    pol | Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ ModalPolarity
    pol ModalPolarity -> ModalPolarity -> Bool
    forall a. Eq a => a -> a -> Bool
    == ModalPolarity
    MixedPolarity ]
                -- Print "instance" if variable is considered by instance search.
              , [ Doc Aspects
    "instance"     | ArgInfo -> Bool
    forall a. LensHiding a => a -> Bool
    isInstance ArgInfo
    ai ]
              ]
          ty <- Expr -> TCMT IO (Doc Aspects)
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m (Doc Aspects)
    prettyATop Expr
    expr
          maybeVal <- traverse prettyATop letv

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

      where
        parenSep :: [Doc] -> Doc
        parenSep :: [Doc Aspects] -> Doc Aspects
    parenSep [Doc Aspects]
    docs
          | [Doc Aspects] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [Doc Aspects]
    docs = Doc Aspects
    forall a. Null a => a
    empty
          | Bool
    otherwise = (Doc Aspects
    " " Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+>) (Doc Aspects -> Doc Aspects) -> Doc Aspects -> Doc Aspects
    forall a b. (a -> b) -> a -> b
    $ Doc Aspects -> Doc Aspects
    parens (Doc Aspects -> Doc Aspects) -> Doc Aspects -> Doc Aspects
    forall a b. (a -> b) -> a -> b
    $ [Doc Aspects] -> Doc Aspects
    forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
    fsep ([Doc Aspects] -> Doc Aspects) -> [Doc Aspects] -> Doc Aspects
    forall a b. (a -> b) -> a -> b
    $ Doc Aspects -> [Doc Aspects] -> [Doc Aspects]
    forall (t :: * -> *).
    Foldable t =>
    Doc Aspects -> t (Doc Aspects) -> [Doc Aspects]
    punctuate Doc Aspects
    comma [Doc Aspects]
    docs

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

    prettyTypeOfMeta :: Rewrite -> InteractionId -> TCM Doc
    prettyTypeOfMeta :: Rewrite -> InteractionId -> TCMT IO (Doc Aspects)
    prettyTypeOfMeta Rewrite
    norm InteractionId
    ii = do
      form <- Rewrite
    -> InteractionId -> TCM (OutputConstraint Expr InteractionId)
    B.typeOfMeta Rewrite
    norm InteractionId
    ii
      case form of
        OfType InteractionId
    _ Expr
    e -> Expr -> TCMT IO (Doc Aspects)
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m (Doc Aspects)
    prettyATop Expr
    e
        OutputConstraint Expr InteractionId
    _            -> OutputConstraint Expr InteractionId -> TCMT IO (Doc Aspects)
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m (Doc Aspects)
    prettyATop OutputConstraint Expr InteractionId
    form

    -- | Prefix prettified CPUTime with "Time:"
    prettyTimed :: CPUTime -> Doc
    prettyTimed :: CPUTime -> Doc Aspects
    prettyTimed CPUTime
    time = Doc Aspects
    "Time:" Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> CPUTime -> Doc Aspects
    forall a. Pretty a => a -> Doc Aspects
    pretty CPUTime
    time