    module Agda.Interaction.EmacsTop
        ( mimicGHCi
        , namedMetaOf
        , showGoals
        , showInfoError
        , explainWhyInScope
        , 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.Position
    import Agda.Syntax.Scope.Base
    import Agda.Syntax.Abstract.Pretty (prettyATop)
    import Agda.Syntax.Abstract as A
    import Agda.Syntax.Concrete as C

    import Agda.TypeChecking.Errors (prettyError, getAllWarningsOfTCErr)
    import qualified Agda.TypeChecking.Pretty as TCP
    import Agda.TypeChecking.Pretty (prettyTCM)
    import Agda.TypeChecking.Pretty.Warning (prettyTCWarnings, prettyTCWarnings')
    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Warnings (WarningsAndNonFatalErrors(..))
    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.InteractionTop (localStateCommandM)
    import Agda.Utils.Function (applyWhen)
    import Agda.Utils.Null (empty)
    import Agda.Utils.Maybe
    import Agda.Utils.Pretty
    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 (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 -> TCMT IO [Lisp [Char]]) -> InteractionOutputCallback
    forall (m :: * -> *) b c a.
    Monad m =>
    (b -> m c) -> (a -> m b) -> a -> m c
    <=< Response -> 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 -> 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 (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
    info) = DisplayInfo -> TCMT IO [Lisp [Char]]
    lispifyDisplayInfo DisplayInfo
    info
    lispifyResponse (Resp_ClearHighlighting TokenBased
    tokenBased) =
      [Lisp [Char]] -> TCMT IO [Lisp [Char]]
    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
    Resp_DoneAborting = [Lisp [Char]] -> TCMT IO [Lisp [Char]]
    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
    Resp_DoneExiting  = [Lisp [Char]] -> TCMT IO [Lisp [Char]]
    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
    Resp_ClearRunningInfo = [Lisp [Char]] -> TCMT IO [Lisp [Char]]
    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 (m :: * -> *) a. Monad m => a -> m a
    return [ [Char] -> Lisp [Char]
    displayRunningInfo [Char]
    s ]
      | Bool
    otherwise = [Lisp [Char]] -> TCMT IO [Lisp [Char]]
    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 (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 Int32
    p) = [Lisp [Char]] -> TCMT IO [Lisp [Char]]
    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 (Int32 -> [Char]
    forall a. Show a => a -> [Char]
    show Int32
    p)] ]
      ]
    lispifyResponse (Resp_InteractionPoints [InteractionId]
    is) = [Lisp [Char]] -> TCMT IO [Lisp [Char]]
    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 (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 (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 (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]

    lispifyDisplayInfo :: DisplayInfo -> TCM [Lisp String]
    lispifyDisplayInfo :: DisplayInfo -> TCMT IO [Lisp [Char]]
    lispifyDisplayInfo DisplayInfo
    info = case DisplayInfo
    info of
        Info_CompilationOk CompilerBackend
    backend WarningsAndNonFatalErrors
    ws -> do
          [Char]
    warnings <- [TCWarning] -> TCM [Char]
    prettyTCWarnings (WarningsAndNonFatalErrors -> [TCWarning]
    tcWarnings WarningsAndNonFatalErrors
    ws)
          [Char]
    errors <- [TCWarning] -> TCM [Char]
    prettyTCWarnings (WarningsAndNonFatalErrors -> [TCWarning]
    nonFatalErrors WarningsAndNonFatalErrors
    ws)
          let
            msg :: [Char]
    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
            ([Char]
    body, [Char]
    _) = [Char] -> [Char] -> [Char] -> ([Char], [Char])
    formatWarningsAndErrors [Char]
    msg [Char]
    warnings [Char]
    errors
          [Char] -> [Char] -> TCMT IO [Lisp [Char]]
    format [Char]
    body [Char]
    "*Compilation result*"
        Info_Constraints [OutputForm Expr Expr]
    s -> [Char] -> [Char] -> TCMT IO [Lisp [Char]]
    format (Doc -> [Char]
    forall a. Show a => a -> [Char]
    show (Doc -> [Char]) -> Doc -> [Char]
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ (OutputForm Expr Expr -> Doc) -> [OutputForm Expr Expr] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map OutputForm Expr Expr -> Doc
    forall a. Pretty a => a -> Doc
    pretty [OutputForm Expr Expr]
    s) [Char]
    "*Constraints*"
        Info_AllGoalsWarnings Goals
    ms WarningsAndNonFatalErrors
    ws -> do
          [Char]
    goals <- Goals -> TCM [Char]
    showGoals Goals
    ms
          [Char]
    warnings <- [TCWarning] -> TCM [Char]
    prettyTCWarnings (WarningsAndNonFatalErrors -> [TCWarning]
    tcWarnings WarningsAndNonFatalErrors
    ws)
          [Char]
    errors <- [TCWarning] -> TCM [Char]
    prettyTCWarnings (WarningsAndNonFatalErrors -> [TCWarning]
    nonFatalErrors WarningsAndNonFatalErrors
    ws)
          let ([Char]
    body, [Char]
    title) = [Char] -> [Char] -> [Char] -> ([Char], [Char])
    formatWarningsAndErrors [Char]
    goals [Char]
    warnings [Char]
    errors
          [Char] -> [Char] -> TCMT IO [Lisp [Char]]
    format [Char]
    body ([Char]
    "*All" [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    title [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "*")
        Info_Auto [Char]
    s -> [Char] -> [Char] -> TCMT IO [Lisp [Char]]
    format [Char]
    s [Char]
    "*Auto*"
        Info_Error Info_Error
    err -> do
          [Char]
    s <- Info_Error -> TCM [Char]
    showInfoError Info_Error
    err
          [Char] -> [Char] -> TCMT IO [Lisp [Char]]
    format [Char]
    s [Char]
    "*Error*"
        Info_Time CPUTime
    s -> [Char] -> [Char] -> TCMT IO [Lisp [Char]]
    format (Doc -> [Char]
    render (Doc -> [Char]) -> Doc -> [Char]
    forall a b. (a -> b) -> a -> b
    $ CPUTime -> Doc
    prettyTimed CPUTime
    s) [Char]
    "*Time*"
        Info_NormalForm CommandState
    state ComputeMode
    cmode Maybe CPUTime
    time Expr
    expr -> do
          Doc
    exprDoc <- StateT CommandState (TCMT IO) Doc -> CommandState -> TCMT IO Doc
    forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
    evalStateT StateT CommandState (TCMT IO) Doc
    prettyExpr CommandState
    state
          let doc :: Doc
    doc = Doc -> (CPUTime -> Doc) -> Maybe CPUTime -> Doc
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Doc
    forall a. Null a => a
    empty CPUTime -> Doc
    prettyTimed Maybe CPUTime
    time Doc -> Doc -> Doc
    $$ Doc
    exprDoc
              lbl :: [Char]
    lbl | ComputeMode
    cmode ComputeMode -> ComputeMode -> Bool
    forall a. Eq a => a -> a -> Bool
    == ComputeMode
    HeadCompute = [Char]
    "*Head Normal Form*"
                  | Bool
    otherwise            = [Char]
    "*Normal Form*"
          [Char] -> [Char] -> TCMT IO [Lisp [Char]]
    format (Doc -> [Char]
    render Doc
    doc) [Char]
    lbl
          where
            prettyExpr :: StateT CommandState (TCMT IO) Doc
    prettyExpr = StateT CommandState (TCMT IO) Doc
    -> StateT CommandState (TCMT IO) Doc
    forall a. CommandM a -> CommandM a
    localStateCommandM
                (StateT CommandState (TCMT IO) Doc
     -> StateT CommandState (TCMT IO) Doc)
    -> StateT CommandState (TCMT IO) Doc
    -> StateT CommandState (TCMT IO) Doc
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc -> StateT CommandState (TCMT IO) Doc
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift
                (TCMT IO Doc -> StateT CommandState (TCMT IO) Doc)
    -> TCMT IO Doc -> StateT CommandState (TCMT IO) Doc
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc -> TCMT IO Doc
    forall a. TCM a -> TCM a
    B.atTopLevel
                (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    allowNonTerminatingReductions
                (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ (if ComputeMode -> Bool
    computeIgnoreAbstract ComputeMode
    cmode then TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    ignoreAbstractMode else TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    inConcreteMode)
                (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ (ComputeMode -> Expr -> TCMT IO Doc
    B.showComputed ComputeMode
    cmode)
                (Expr -> TCMT IO Doc) -> Expr -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Expr
    expr
        Info_InferredType CommandState
    state Maybe CPUTime
    time Expr
    expr -> do
          Doc
    exprDoc <- StateT CommandState (TCMT IO) Doc -> CommandState -> TCMT IO Doc
    forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
    evalStateT StateT CommandState (TCMT IO) Doc
    prettyExpr CommandState
    state
          let doc :: Doc
    doc = Doc -> (CPUTime -> Doc) -> Maybe CPUTime -> Doc
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Doc
    forall a. Null a => a
    empty CPUTime -> Doc
    prettyTimed Maybe CPUTime
    time Doc -> Doc -> Doc
    $$ Doc
    exprDoc
          [Char] -> [Char] -> TCMT IO [Lisp [Char]]
    format (Doc -> [Char]
    render Doc
    doc) [Char]
    "*Inferred Type*"
          where
            prettyExpr :: StateT CommandState (TCMT IO) Doc
    prettyExpr = StateT CommandState (TCMT IO) Doc
    -> StateT CommandState (TCMT IO) Doc
    forall a. CommandM a -> CommandM a
    localStateCommandM
                (StateT CommandState (TCMT IO) Doc
     -> StateT CommandState (TCMT IO) Doc)
    -> StateT CommandState (TCMT IO) Doc
    -> StateT CommandState (TCMT IO) Doc
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc -> StateT CommandState (TCMT IO) Doc
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift
                (TCMT IO Doc -> StateT CommandState (TCMT IO) Doc)
    -> TCMT IO Doc -> StateT CommandState (TCMT IO) Doc
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc -> TCMT IO Doc
    forall a. TCM a -> TCM a
    B.atTopLevel
                (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Expr -> TCMT IO Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    TCP.prettyA
                (Expr -> TCMT IO Doc) -> Expr -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Expr
    expr
        Info_ModuleContents [Name]
    modules Telescope
    tel [(Name, Type)]
    types -> do
          Doc
    doc <- TCMT IO Doc -> TCMT IO Doc
    forall a. TCM a -> TCM a
    localTCState (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ do
            [([Char], Doc)]
    typeDocs <- Telescope -> TCMT IO [([Char], Doc)] -> TCMT IO [([Char], Doc)]
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    tel (TCMT IO [([Char], Doc)] -> TCMT IO [([Char], Doc)])
    -> TCMT IO [([Char], Doc)] -> TCMT IO [([Char], Doc)]
    forall a b. (a -> b) -> a -> b
    $ [(Name, Type)]
    -> ((Name, Type) -> TCMT IO ([Char], Doc))
    -> TCMT IO [([Char], Doc)]
    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))
     -> TCMT IO [([Char], Doc)])
    -> ((Name, Type) -> TCMT IO ([Char], Doc))
    -> TCMT IO [([Char], Doc)]
    forall a b. (a -> b) -> a -> b
    $ \ (Name
    x, Type
    t) -> do
              Doc
    doc <- Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    t
              ([Char], Doc) -> TCMT IO ([Char], Doc)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Name -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow Name
    x, Doc
    ":" Doc -> Doc -> Doc
    <+> Doc
    doc)
            Doc -> TCMT IO Doc
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Doc -> TCMT IO Doc) -> Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat
              [ Doc
    "Modules"
              , Nat -> Doc -> Doc
    nest Nat
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ (Name -> Doc) -> [Name] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty [Name]
    modules
              , Doc
    "Names"
              , Nat -> Doc -> Doc
    nest Nat
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Nat -> [([Char], Doc)] -> Doc
    align Nat
    10 [([Char], Doc)]
    typeDocs
              ]
          [Char] -> [Char] -> TCMT IO [Lisp [Char]]
    format (Doc -> [Char]
    render Doc
    doc) [Char]
    "*Module contents*"
        Info_SearchAbout [(Name, Type)]
    hits [Char]
    names -> do
          [([Char], Doc)]
    hitDocs <- [(Name, Type)]
    -> ((Name, Type) -> TCMT IO ([Char], Doc))
    -> TCMT IO [([Char], Doc)]
    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))
     -> TCMT IO [([Char], Doc)])
    -> ((Name, Type) -> TCMT IO ([Char], Doc))
    -> TCMT IO [([Char], Doc)]
    forall a b. (a -> b) -> a -> b
    $ \ (Name
    x, Type
    t) -> do
            Doc
    doc <- Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    t
            ([Char], Doc) -> TCMT IO ([Char], Doc)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Name -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow Name
    x, Doc
    ":" Doc -> Doc -> Doc
    <+> Doc
    doc)
          let doc :: Doc
    doc = Doc
    "Definitions about" Doc -> Doc -> Doc
    <+>
                    [Char] -> Doc
    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 -> Doc -> Doc
    $$ Nat -> Doc -> Doc
    nest Nat
    2 (Nat -> [([Char], Doc)] -> Doc
    align Nat
    10 [([Char], Doc)]
    hitDocs)
          [Char] -> [Char] -> TCMT IO [Lisp [Char]]
    format (Doc -> [Char]
    render Doc
    doc) [Char]
    "*Search About*"
        Info_WhyInScope [Char]
    s [Char]
    cwd Maybe LocalVar
    v [AbstractName]
    xs [AbstractModule]
    ms -> do
          Doc
    doc <- [Char]
    -> [Char]
    -> Maybe LocalVar
    -> [AbstractName]
    -> [AbstractModule]
    -> TCMT IO Doc
    explainWhyInScope [Char]
    s [Char]
    cwd Maybe LocalVar
    v [AbstractName]
    xs [AbstractModule]
    ms
          [Char] -> [Char] -> TCMT IO [Lisp [Char]]
    format (Doc -> [Char]
    render Doc
    doc) [Char]
    "*Scope Info*"
        Info_Context InteractionId
    ii [ResponseContextEntry]
    ctx -> do
          Doc
    doc <- TCMT IO Doc -> TCMT IO Doc
    forall a. TCM a -> TCM a
    localTCState (InteractionId -> Bool -> [ResponseContextEntry] -> TCMT IO Doc
    prettyResponseContext InteractionId
    ii Bool
    False [ResponseContextEntry]
    ctx)
          [Char] -> [Char] -> TCMT IO [Lisp [Char]]
    format (Doc -> [Char]
    render Doc
    doc) [Char]
    "*Context*"
        DisplayInfo
    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
    doc = [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep [ Doc
    "Don't know which constructor to introduce of"
                        , let mkOr :: [[Char]] -> [Doc]
    mkOr []     = []
                              mkOr [[Char]
    x, [Char]
    y] = [[Char] -> Doc
    text [Char]
    x Doc -> Doc -> Doc
    <+> Doc
    "or" Doc -> Doc -> Doc
    <+> [Char] -> Doc
    text [Char]
    y]
                              mkOr ([Char]
    x:[[Char]]
    xs) = [Char] -> Doc
    text [Char]
    x Doc -> [Doc] -> [Doc]
    forall a. a -> [a] -> [a]
    : [[Char]] -> [Doc]
    mkOr [[Char]]
    xs
                          in Nat -> Doc -> Doc
    nest Nat
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ Doc -> [Doc] -> [Doc]
    forall (t :: * -> *). Foldable t => Doc -> t Doc -> [Doc]
    punctuate Doc
    comma ([[Char]] -> [Doc]
    mkOr [[Char]]
    ss)
                        ]
          [Char] -> [Char] -> TCMT IO [Lisp [Char]]
    format (Doc -> [Char]
    render Doc
    doc) [Char]
    "*Intro*"
        DisplayInfo
    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
    kind -> InteractionId -> GoalDisplayInfo -> TCMT IO [Lisp [Char]]
    lispifyGoalSpecificDisplayInfo InteractionId
    ii GoalDisplayInfo
    kind

    lispifyGoalSpecificDisplayInfo :: InteractionId -> GoalDisplayInfo -> TCM [Lisp String]
    lispifyGoalSpecificDisplayInfo :: InteractionId -> GoalDisplayInfo -> TCMT IO [Lisp [Char]]
    lispifyGoalSpecificDisplayInfo InteractionId
    ii GoalDisplayInfo
    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.
    (MonadFail 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
    kind of
        Goal_HelperFunction OutputConstraint' Expr Expr
    helperType -> do
          Doc
    doc <- TCMT IO Doc -> TCMT IO Doc
    forall (tcm :: * -> *) a.
    (MonadTCEnv tcm, ReadTCState tcm) =>
    tcm a -> tcm a
    inTopContext (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ OutputConstraint' Expr Expr -> TCMT IO Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyATop OutputConstraint' Expr Expr
    helperType
          [Lisp [Char]] -> TCMT IO [Lisp [Char]]
    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-info-action-and-copy"
                     , [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]
    "*Helper function*"
                     , [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 (Doc -> [Char]
    render Doc
    doc [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "\n")
                     , [Char] -> Lisp [Char]
    forall a. a -> Lisp a
    A [Char]
    "nil"
                     ]
                 ]
        Goal_NormalForm ComputeMode
    cmode Expr
    expr -> do
          Doc
    doc <- ComputeMode -> Expr -> TCMT IO Doc
    showComputed ComputeMode
    cmode Expr
    expr
          [Char] -> [Char] -> TCMT IO [Lisp [Char]]
    format (Doc -> [Char]
    render Doc
    doc) [Char]
    "*Normal Form*"   -- show?
        Goal_GoalType Rewrite
    norm GoalTypeAux
    aux [ResponseContextEntry]
    ctx [IPBoundary' Expr]
    bndry [OutputForm Expr Expr]
    constraints -> do
          Doc
    ctxDoc <- InteractionId -> Bool -> [ResponseContextEntry] -> TCMT IO Doc
    prettyResponseContext InteractionId
    ii Bool
    True [ResponseContextEntry]
    ctx
          Doc
    goalDoc <- Rewrite -> InteractionId -> TCMT IO Doc
    prettyTypeOfMeta Rewrite
    norm InteractionId
    ii
          Doc
    auxDoc <- case GoalTypeAux
    aux of
                GoalTypeAux
    GoalOnly -> Doc -> TCMT IO Doc
    forall (m :: * -> *) a. Monad m => a -> m a
    return Doc
    forall a. Null a => a
    empty
                GoalAndHave Expr
    expr -> do
                  Doc
    doc <- Expr -> TCMT IO Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyATop Expr
    expr
                  Doc -> TCMT IO Doc
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Doc -> TCMT IO Doc) -> Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Doc
    "Have:" Doc -> Doc -> Doc
    <+> Doc
    doc
                GoalAndElaboration Term
    term -> do
                  Doc
    doc <- Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    TCP.prettyTCM Term
    term
                  Doc -> TCMT IO Doc
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Doc -> TCMT IO Doc) -> Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Doc
    "Elaborates to:" Doc -> Doc -> Doc
    <+> Doc
    doc
          let boundaryDoc :: [Doc]
    boundaryDoc
                | [IPBoundary' Expr] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [IPBoundary' Expr]
    bndry = []
                | Bool
    otherwise  = [ [Char] -> Doc
    text ([Char] -> Doc) -> [Char] -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Char] -> [Char]
    delimiter [Char]
    "Boundary"
                               , [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ (IPBoundary' Expr -> Doc) -> [IPBoundary' Expr] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map IPBoundary' Expr -> Doc
    forall a. Pretty a => a -> Doc
    pretty [IPBoundary' Expr]
    bndry
                               ]
          let constraintsDoc :: [Doc]
    constraintsDoc = if ([OutputForm Expr Expr] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [OutputForm Expr Expr]
    constraints)
                then  []
                else  [ [Char] -> Doc
    text ([Char] -> Doc) -> [Char] -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Char] -> [Char]
    delimiter [Char]
    "Constraints"
                      , [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ (OutputForm Expr Expr -> Doc) -> [OutputForm Expr Expr] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map OutputForm Expr Expr -> Doc
    forall a. Pretty a => a -> Doc
    pretty [OutputForm Expr Expr]
    constraints
                      ]
          let doc :: Doc
    doc = [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $
                [ Doc
    "Goal:" Doc -> Doc -> Doc
    <+> Doc
    goalDoc
                , Doc
    auxDoc
                , [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat [Doc]
    boundaryDoc
                , [Char] -> Doc
    text (Nat -> Char -> [Char]
    forall a. Nat -> a -> [a]
    replicate Nat
    60 Char
    '\x2014')
                , Doc
    ctxDoc
                ] [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ [Doc]
    constraintsDoc
          [Char] -> [Char] -> TCMT IO [Lisp [Char]]
    format (Doc -> [Char]
    render Doc
    doc) [Char]
    "*Goal type etc.*"
        Goal_CurrentGoal Rewrite
    norm -> do
          Doc
    doc <- Rewrite -> InteractionId -> TCMT IO Doc
    prettyTypeOfMeta Rewrite
    norm InteractionId
    ii
          [Char] -> [Char] -> TCMT IO [Lisp [Char]]
    format (Doc -> [Char]
    render Doc
    doc) [Char]
    "*Current Goal*"
        Goal_InferredType Expr
    expr -> do
          Doc
    doc <- Expr -> TCMT IO Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyATop Expr
    expr
          [Char] -> [Char] -> TCMT IO [Lisp [Char]]
    format (Doc -> [Char]
    render Doc
    doc) [Char]
    "*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 (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 (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 (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 (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 (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 (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 (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 (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 (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]
    "Errors"   [Char] -> Maybe () -> Maybe [Char]
    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 (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 (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 (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 -> TCM [Char]
    showInfoError (Info_GenericError TCErr
    err) = do
      [Char]
    e <- TCErr -> TCM [Char]
    forall (tcm :: * -> *). MonadTCM tcm => TCErr -> tcm [Char]
    prettyError TCErr
    err
      [[Char]]
    w <- [TCWarning] -> TCM [[Char]]
    prettyTCWarnings' ([TCWarning] -> TCM [[Char]])
    -> TCMT IO [TCWarning] -> TCM [[Char]]
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TCErr -> TCMT IO [TCWarning]
    getAllWarningsOfTCErr TCErr
    err

      let errorMsg :: [Char]
    errorMsg  = if [[Char]] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [[Char]]
    w
                          then [Char]
    e
                          else [Char] -> [Char]
    delimiter [Char]
    "Error" [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "\n" [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    e
      let warningMsg :: [Char]
    warningMsg = [Char] -> [[Char]] -> [Char]
    forall a. [a] -> [[a]] -> [a]
    List.intercalate [Char]
    "\n" ([[Char]] -> [Char]) -> [[Char]] -> [Char]
    forall a b. (a -> b) -> a -> b
    $ [Char] -> [Char]
    delimiter [Char]
    "Warning(s)"
                                          [Char] -> [[Char]] -> [[Char]]
    forall a. a -> [a] -> [a]
    : ([Char] -> Bool) -> [[Char]] -> [[Char]]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (Bool -> Bool
    not (Bool -> Bool) -> ([Char] -> Bool) -> [Char] -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Char] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null) [[Char]]
    w
      [Char] -> TCM [Char]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Char] -> TCM [Char]) -> [Char] -> TCM [Char]
    forall a b. (a -> b) -> a -> b
    $ if [[Char]] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [[Char]]
    w
                then [Char]
    errorMsg
                else [Char]
    errorMsg [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "\n\n" [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    warningMsg
    showInfoError (Info_CompilationError [TCWarning]
    warnings) = do
      [Char]
    s <- [TCWarning] -> TCM [Char]
    prettyTCWarnings [TCWarning]
    warnings
      [Char] -> TCM [Char]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Char] -> TCM [Char]) -> [Char] -> TCM [Char]
    forall a b. (a -> b) -> a -> b
    $ [[Char]] -> [Char]
    unlines
                [ [Char]
    "You need to fix the following errors before you can compile"
                , [Char]
    "the module:"
                , [Char]
    ""
                , [Char]
    s
                ]
    showInfoError (Info_HighlightingParseError InteractionId
    ii) =
      [Char] -> TCM [Char]
    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 (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

    explainWhyInScope :: FilePath
                      -> String
                      -> (Maybe LocalVar)
                      -> [AbstractName]
                      -> [AbstractModule]
                      -> TCM Doc
    explainWhyInScope :: [Char]
    -> [Char]
    -> Maybe LocalVar
    -> [AbstractName]
    -> [AbstractModule]
    -> TCMT IO Doc
    explainWhyInScope [Char]
    s [Char]
    _ Maybe LocalVar
    Nothing [] [] = [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    TCP.text ([Char]
    s [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " is not in scope.")
    explainWhyInScope [Char]
    s [Char]
    _ Maybe LocalVar
    v [AbstractName]
    xs [AbstractModule]
    ms = [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    TCP.vcat
      [ [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    TCP.text ([Char]
    s [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " is in scope as")
      , Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    TCP.nest Nat
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    TCP.vcat [Maybe LocalVar -> [AbstractName] -> TCMT IO Doc
    variable Maybe LocalVar
    v [AbstractName]
    xs, [AbstractModule] -> TCMT IO Doc
    modules [AbstractModule]
    ms]
      ]
      where
        -- variable :: Maybe _ -> [_] -> TCM Doc
        variable :: Maybe LocalVar -> [AbstractName] -> TCMT IO Doc
    variable Maybe LocalVar
    Nothing [AbstractName]
    vs = [AbstractName] -> TCMT IO Doc
    names [AbstractName]
    vs
        variable (Just LocalVar
    x) [AbstractName]
    vs
          | [AbstractName] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [AbstractName]
    vs   = TCMT IO Doc
    asVar
          | Bool
    otherwise = [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    TCP.vcat
             [ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    TCP.sep [ TCMT IO Doc
    asVar, Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    TCP.nest Nat
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ LocalVar -> TCMT IO Doc
    shadowing LocalVar
    x]
             , Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    TCP.nest Nat
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [AbstractName] -> TCMT IO Doc
    names [AbstractName]
    vs
             ]
          where
            asVar :: TCM Doc
            asVar :: TCMT IO Doc
    asVar = do
              TCMT IO Doc
    "* a variable bound at" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    TCP.<+> Range -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    TCP.prettyTCM (Name -> Range
    nameBindingSite (Name -> Range) -> Name -> Range
    forall a b. (a -> b) -> a -> b
    $ LocalVar -> Name
    localVar LocalVar
    x)
            shadowing :: LocalVar -> TCM Doc
            shadowing :: LocalVar -> TCMT IO Doc
    shadowing (LocalVar Name
    _ BindingSource
    _ [])    = TCMT IO Doc
    "shadowing"
            shadowing LocalVar
    _ = TCMT IO Doc
    "in conflict with"
        names :: [AbstractName] -> TCMT IO Doc
    names   = [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    TCP.vcat ([TCMT IO Doc] -> TCMT IO Doc)
    -> ([AbstractName] -> [TCMT IO Doc])
    -> [AbstractName]
    -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (AbstractName -> TCMT IO Doc) -> [AbstractName] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map AbstractName -> TCMT IO Doc
    pName
        modules :: [AbstractModule] -> TCMT IO Doc
    modules = [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    TCP.vcat ([TCMT IO Doc] -> TCMT IO Doc)
    -> ([AbstractModule] -> [TCMT IO Doc])
    -> [AbstractModule]
    -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (AbstractModule -> TCMT IO Doc)
    -> [AbstractModule] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map AbstractModule -> TCMT IO Doc
    pMod

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

        pName :: AbstractName -> TCM Doc
        pName :: AbstractName -> TCMT IO Doc
    pName AbstractName
    a = [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    TCP.sep
          [ TCMT IO Doc
    "* a"
            TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    TCP.<+> KindOfName -> TCMT IO Doc
    pKind (AbstractName -> KindOfName
    anameKind AbstractName
    a)
            TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    TCP.<+> [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    TCP.text (QName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow (QName -> [Char]) -> QName -> [Char]
    forall a b. (a -> b) -> a -> b
    $ AbstractName -> QName
    anameName AbstractName
    a)
          , Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    TCP.nest Nat
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "brought into scope by"
          ] TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    TCP.$$
          Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    TCP.nest Nat
    2 (Range -> WhyInScope -> TCMT IO Doc
    pWhy (Name -> Range
    nameBindingSite (Name -> Range) -> Name -> Range
    forall a b. (a -> b) -> a -> b
    $ QName -> Name
    qnameName (QName -> Name) -> QName -> Name
    forall a b. (a -> b) -> a -> b
    $ AbstractName -> QName
    anameName AbstractName
    a) (AbstractName -> WhyInScope
    anameLineage AbstractName
    a))
        pMod :: AbstractModule -> TCM Doc
        pMod :: AbstractModule -> TCMT IO Doc
    pMod  AbstractModule
    a = [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    TCP.sep
          [ TCMT IO Doc
    "* a module" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    TCP.<+> [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    TCP.text (ModuleName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow (ModuleName -> [Char]) -> ModuleName -> [Char]
    forall a b. (a -> b) -> a -> b
    $ AbstractModule -> ModuleName
    amodName AbstractModule
    a)
          , Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    TCP.nest Nat
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "brought into scope by"
          ] TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    TCP.$$
          Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    TCP.nest Nat
    2 (Range -> WhyInScope -> TCMT IO Doc
    pWhy (Name -> Range
    nameBindingSite (Name -> Range) -> Name -> Range
    forall a b. (a -> b) -> a -> b
    $ QName -> Name
    qnameName (QName -> Name) -> QName -> Name
    forall a b. (a -> b) -> a -> b
    $ ModuleName -> QName
    mnameToQName (ModuleName -> QName) -> ModuleName -> QName
    forall a b. (a -> b) -> a -> b
    $ AbstractModule -> ModuleName
    amodName AbstractModule
    a) (AbstractModule -> WhyInScope
    amodLineage AbstractModule
    a))

        pWhy :: Range -> WhyInScope -> TCM Doc
        pWhy :: Range -> WhyInScope -> TCMT IO Doc
    pWhy Range
    r WhyInScope
    Defined = TCMT IO Doc
    "- its definition at" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    TCP.<+> Range -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    TCP.prettyTCM Range
    r
        pWhy Range
    r (Opened (C.QName Name
    x) WhyInScope
    w) | Name -> Bool
    forall a. IsNoName a => a -> Bool
    isNoName Name
    x = Range -> WhyInScope -> TCMT IO Doc
    pWhy Range
    r WhyInScope
    w
        pWhy Range
    r (Opened QName
    m WhyInScope
    w) =
          TCMT IO Doc
    "- the opening of"
          TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    TCP.<+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    TCP.prettyTCM QName
    m
          TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    TCP.<+> TCMT IO Doc
    "at"
          TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    TCP.<+> Range -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    TCP.prettyTCM (QName -> Range
    forall a. HasRange a => a -> Range
    getRange QName
    m)
          TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    TCP.$$
          Range -> WhyInScope -> TCMT IO Doc
    pWhy Range
    r WhyInScope
    w
        pWhy Range
    r (Applied QName
    m WhyInScope
    w) =
          TCMT IO Doc
    "- the application of"
          TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    TCP.<+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    TCP.prettyTCM QName
    m
          TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    TCP.<+> TCMT IO Doc
    "at"
          TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    TCP.<+> Range -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    TCP.prettyTCM (QName -> Range
    forall a. HasRange a => a -> Range
    getRange QName
    m)
          TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    TCP.$$
          Range -> WhyInScope -> TCMT IO Doc
    pWhy Range
    r WhyInScope
    w

    -- | 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
    prettyResponseContext InteractionId
    ii Bool
    rev [ResponseContextEntry]
    ctx = InteractionId -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *) a.
    (MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m,
     MonadTrace m) =>
    InteractionId -> m a -> m a
    withInteractionId InteractionId
    ii (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ do
      Modality
    mod   <- (TCEnv -> Modality) -> TCMT IO Modality
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> Modality
    forall a. LensModality a => a -> Modality
    getModality
      Nat -> [([Char], Doc)] -> Doc
    align Nat
    10 ([([Char], Doc)] -> Doc)
    -> ([[([Char], Doc)]] -> [([Char], Doc)])
    -> [[([Char], Doc)]]
    -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [[([Char], Doc)]] -> [([Char], Doc)]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat ([[([Char], Doc)]] -> [([Char], Doc)])
    -> ([[([Char], Doc)]] -> [[([Char], Doc)]])
    -> [[([Char], Doc)]]
    -> [([Char], Doc)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Bool
    -> ([[([Char], Doc)]] -> [[([Char], Doc)]])
    -> [[([Char], Doc)]]
    -> [[([Char], Doc)]]
    forall a. Bool -> (a -> a) -> a -> a
    applyWhen Bool
    rev [[([Char], Doc)]] -> [[([Char], Doc)]]
    forall a. [a] -> [a]
    reverse ([[([Char], Doc)]] -> Doc)
    -> TCMT IO [[([Char], Doc)]] -> TCMT IO Doc
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do
        [ResponseContextEntry]
    -> (ResponseContextEntry -> TCMT IO [([Char], Doc)])
    -> TCMT IO [[([Char], Doc)]]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM [ResponseContextEntry]
    ctx ((ResponseContextEntry -> TCMT IO [([Char], Doc)])
     -> TCMT IO [[([Char], Doc)]])
    -> (ResponseContextEntry -> TCMT IO [([Char], Doc)])
    -> TCMT IO [[([Char], Doc)]]
    forall a b. (a -> b) -> a -> b
    $ \ (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 (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)

            extras :: [Doc]
            extras :: [Doc]
    extras = [[Doc]] -> [Doc]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat ([[Doc]] -> [Doc]) -> [[Doc]] -> [Doc]
    forall a b. (a -> b) -> a -> b
    $
              [ [ Doc
    "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 by goal is non-erased.
              , [ Doc
    "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 irrelevant if hypothesis is strictly less relevant than goal.
              , [ Doc
    "irrelevant"   | Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ ArgInfo -> Relevance
    forall a. LensRelevance a => a -> Relevance
    getRelevance ArgInfo
    ai Relevance -> Relevance -> Bool
    `moreRelevant` Modality -> Relevance
    forall a. LensRelevance a => a -> Relevance
    getRelevance Modality
    mod ]
                -- Print instance if variable is considered by instance search
              , [ Doc
    "instance"     | ArgInfo -> Bool
    forall a. LensHiding a => a -> Bool
    isInstance ArgInfo
    ai ]
              ]
          Doc
    ty <- Expr -> TCMT IO Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyATop Expr
    expr
          Maybe Doc
    maybeVal <- (Expr -> TCMT IO Doc) -> Maybe Expr -> TCMT IO (Maybe Doc)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse Expr -> TCMT IO Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyATop Maybe Expr
    letv

          [([Char], Doc)] -> TCMT IO [([Char], Doc)]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([([Char], Doc)] -> TCMT IO [([Char], Doc)])
    -> [([Char], Doc)] -> TCMT IO [([Char], Doc)]
    forall a b. (a -> b) -> a -> b
    $
            ([Char]
    attribute [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    prettyCtxName, Doc
    ":" Doc -> Doc -> Doc
    <+> Doc
    ty Doc -> Doc -> Doc
    <+> ([Doc] -> Doc
    parenSep [Doc]
    extras)) ([Char], Doc) -> [([Char], Doc)] -> [([Char], Doc)]
    forall a. a -> [a] -> [a]
    :
            [ (Name -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow Name
    x, Doc
    "=" Doc -> Doc -> Doc
    <+> Doc
    val) | Doc
    val <- Maybe Doc -> [Doc]
    forall a. Maybe a -> [a]
    maybeToList Maybe Doc
    maybeVal ]

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

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

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

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