{-# OPTIONS_GHC -Wunused-imports #-}

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

import Prelude hiding (null)

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

import Data.List qualified as List

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

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

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

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

import Agda.VersionCommit

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

-- | 'mimicGHCi' is a fake ghci interpreter for the Emacs frontend
--   and for interaction tests.
--
--   'mimicGHCi' reads the Emacs frontend commands from stdin,
--   interprets them and print the result into stdout.
mimicGHCi :: TCM () -> TCM ()
mimicGHCi :: 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
. [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 = \case

  Resp_HighlightingInfo HighlightingInfo
info RemoveTokenBasedHighlighting
remove HighlightingMethod
method ModuleToSource
modFile ->
    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)

  Resp_DisplayInfo DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
info ->
    DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
-> TCMT IO (Lisp [Char])
lispifyDisplayInfo DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
info

  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] -> TCMT IO (Lisp [Char]))
-> Lisp [Char] -> TCMT IO (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]
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
TokenBased -> [ Lisp [Char] -> Lisp [Char]
forall a. Lisp a -> Lisp a
Q (TokenBased -> Lisp [Char]
lispifyTokenBased TokenBased
tokenBased) ]
        TokenBased
NotOnlyTokenBased -> []

  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] -> TCMT IO (Lisp [Char]))
-> Lisp [Char] -> TCMT IO (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-abort-done" ]

  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] -> TCMT IO (Lisp [Char]))
-> Lisp [Char] -> TCMT IO (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-exit-done" ]

  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

  Resp_RunningInfo Int
n DocTree
docTree
    | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
1 -> DocTree -> Maybe ModuleToSource -> Lisp [Char]
displayRunningInfo DocTree
docTree (Maybe ModuleToSource -> Lisp [Char])
-> TCMT IO (Maybe ModuleToSource) -> TCMT IO (Lisp [Char])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO (Maybe ModuleToSource)
wantBufferHighlighting
    | Bool
otherwise -> DocTree -> Maybe ModuleToSource -> Lisp [Char]
displayVerboseInfo DocTree
docTree (Maybe ModuleToSource -> Lisp [Char])
-> TCMT IO (Maybe ModuleToSource) -> TCMT IO (Lisp [Char])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO (Maybe ModuleToSource)
wantBufferHighlighting

  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] -> TCMT IO (Lisp [Char]))
-> Lisp [Char] -> TCMT IO (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-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"

  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 (Lisp [Char] -> TCMT IO (Lisp [Char]))
-> Lisp [Char] -> TCMT IO (Lisp [Char])
forall a b. (a -> b) -> a -> b
$ 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) ]
      ]

  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 (Lisp [Char] -> TCMT IO (Lisp [Char]))
-> Lisp [Char] -> TCMT IO (Lisp [Char])
forall a b. (a -> b) -> a -> b
$ 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
      ]

  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] -> TCMT IO (Lisp [Char]))
-> Lisp [Char] -> TCMT IO (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-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"

  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 (Lisp [Char] -> TCMT IO (Lisp [Char]))
-> Lisp [Char] -> TCMT IO (Lisp [Char])
forall a b. (a -> b) -> a -> b
$ 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"

  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 (Lisp [Char] -> TCMT IO (Lisp [Char]))
-> Lisp [Char] -> TCMT IO (Lisp [Char])
forall a b. (a -> b) -> a -> b
$ 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]
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, 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]

  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
$ 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 ([Lisp [Char]] -> Lisp [Char]) -> [Lisp [Char]] -> Lisp [Char]
forall a b. (a -> b) -> a -> b
$ case Maybe [Char]
msol of
      Maybe [Char]
Nothing ->
        [ [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 ->
        [ [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 = \case

    Info_CompilationOk CompilerBackend
backend WarningsAndNonFatalErrors
ws -> do
      warnings <- Set TCWarning -> TCM [Doc Aspects]
prettyTCWarnings' (WarningsAndNonFatalErrors -> Set TCWarning
tcWarnings WarningsAndNonFatalErrors
ws)
      errors   <- prettyTCWarnings' (nonFatalErrors ws)
      let
        msg = [Doc Aspects] -> Doc Aspects
forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
hcat
          [ Doc Aspects
"The module was successfully compiled with backend "
          , CompilerBackend -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty CompilerBackend
backend
          , Doc Aspects
".\n"
          ]
      -- abusing the goals field since we ignore the title
        (_title, body) = formatWarningsAndErrors msg warnings errors
      format "*Compilation result*" body

    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 "*Constraints*" doc

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

    Info_Auto [Char]
s ->
      [Char] -> Doc Aspects -> TCMT IO (Lisp [Char])
format [Char]
"*Auto*" (Doc Aspects -> TCMT IO (Lisp [Char]))
-> Doc Aspects -> TCMT IO (Lisp [Char])
forall a b. (a -> b) -> a -> b
$ [Char] -> Doc Aspects
forall a. [Char] -> Doc a
P.text [Char]
s

    Info_Error Info_Error_boot TCErr TCWarning
err -> [Char] -> Doc Aspects -> TCMT IO (Lisp [Char])
format' [Char]
"*Error*" (Doc Aspects -> TCMT IO (Lisp [Char]))
-> TCMT IO (Doc Aspects) -> TCMT IO (Lisp [Char])
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Info_Error_boot TCErr TCWarning -> TCMT IO (Doc Aspects)
prettyInfoError Info_Error_boot TCErr TCWarning
err

    Info_Time CPUTime
time ->
      [Char] -> Doc Aspects -> TCMT IO (Lisp [Char])
format [Char]
"*Time*" (Doc Aspects -> TCMT IO (Lisp [Char]))
-> Doc Aspects -> TCMT IO (Lisp [Char])
forall a b. (a -> b) -> a -> b
$ CPUTime -> Doc Aspects
prettyTimed CPUTime
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 lbl doc
      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
$ (ComputeMode -> TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects)
forall (m :: * -> *) a. MonadTCEnv m => ComputeMode -> m a -> m a
B.withComputeIgnoreAbstract ComputeMode
cmode)
            (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 "*Inferred Type*" doc
      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 Tele (Dom Type)
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 <- Tele (Dom Type)
-> 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 =>
Tele (Dom Type) -> m a -> m a
addContext Tele (Dom Type)
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 "*Module contents*" doc

    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
$$ Int -> Doc Aspects -> Doc Aspects
forall a. Int -> Doc a -> Doc a
nest Int
2 (Int -> [([Char], Doc Aspects)] -> Doc Aspects
align Int
10 [([Char], Doc Aspects)]
hitDocs)
      format "*Search About*" doc

    Info_WhyInScope WhyInScopeData
why -> do
      doc <- WhyInScopeData -> TCMT IO (Doc Aspects)
forall (m :: * -> *).
MonadPretty m =>
WhyInScopeData -> m (Doc Aspects)
explainWhyInScope WhyInScopeData
why
      format "*Scope Info*" doc

    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 "*Context*" doc

    DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
Info_Intro_NotFound ->
      [Char] -> Doc Aspects -> TCMT IO (Lisp [Char])
format [Char]
"*Intro*" Doc Aspects
"No introduction forms found."

    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 Int -> Doc Aspects -> Doc Aspects
forall a. Int -> Doc a -> Doc a
nest Int
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] -> Doc Aspects -> TCMT IO (Lisp [Char])
format [Char]
"*Intro*" Doc Aspects
doc

    DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
Info_Version ->
      [Char] -> Doc Aspects -> TCMT IO (Lisp [Char])
format [Char]
"*Agda Version*" (Doc Aspects
"Agda version" Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> [Char] -> Doc Aspects
forall a. [Char] -> Doc a
text [Char]
versionWithCommitInfo)

    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, MonadError TCErr 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 Name
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 Name -> TCMT IO (Doc Aspects)
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m (Doc Aspects)
prettyATop OutputConstraint' Expr Name
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 "*Normal Form*" doc

    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. Null a => 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. Null a => 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 $ concat
        [ [ "Goal:" TCP.<+> return goalDoc
          , return (vcat (boundaryDoc "Boundary (wanted)" bndry))
          , return auxDoc
          ]
        , [ TCP.text (delimiter "Context") | not $ null ctxDoc ]
        , [ return ctxDoc ]
        , constraintsDoc
        ]
      format "*Goal type etc.*" doc

    Goal_CurrentGoal Rewrite
norm -> do
      doc <- Rewrite -> InteractionId -> TCMT IO (Doc Aspects)
prettyTypeOfMeta Rewrite
norm InteractionId
ii
      format "*Current Goal*" doc

    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 "*Inferred Type*" doc

format :: String -> Doc -> TCM (Lisp String)
format :: [Char] -> Doc Aspects -> TCMT IO (Lisp [Char])
format [Char]
header = [Char] -> Doc Aspects -> TCMT IO (Lisp [Char])
format' [Char]
header

-- | Format responses of 'DisplayInfo'.
format'
  :: String
  -- ^ String to use as a header.
  -> Doc
  -- ^ The document to print.
  -> TCM (Lisp String)
format' :: [Char] -> Doc Aspects -> TCMT IO (Lisp [Char])
format' [Char]
header Doc Aspects
content = [Char] -> DocTree -> Bool -> Maybe ModuleToSource -> Lisp [Char]
displayInfo [Char]
header (Doc Aspects -> DocTree
forall ann. Null ann => Doc ann -> DocTree ann
renderToTree Doc Aspects
content) Bool
False (Maybe ModuleToSource -> Lisp [Char])
-> TCMT IO (Maybe ModuleToSource) -> TCMT IO (Lisp [Char])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
  TCMT IO (Maybe ModuleToSource)
wantBufferHighlighting

-- | Do we want highlighting in the Agda information buffer?
--   'Nothing' with option @--color=never@.
wantBufferHighlighting :: TCM (Maybe ModuleToSource)
wantBufferHighlighting :: TCMT IO (Maybe ModuleToSource)
wantBufferHighlighting = do
  col <- TCMT IO CommandLineOptions
forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions TCMT IO CommandLineOptions
-> (CommandLineOptions -> DiagnosticsColours)
-> TCMT IO DiagnosticsColours
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> CommandLineOptions -> DiagnosticsColours
optDiagnosticsColour TCMT IO DiagnosticsColours
-> (DiagnosticsColours -> Bool) -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
    DiagnosticsColours
AutoColour   -> Bool
True
    DiagnosticsColours
AlwaysColour -> Bool
True
    DiagnosticsColours
NeverColour  -> Bool
False
  if col
    then Just <$> useSession lensModuleToSource
    else return Nothing

-- | 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
. Int -> [Char]
forall a. Show a => a -> [Char]
show (Int -> [Char])
-> (InteractionId -> Int) -> InteractionId -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InteractionId -> Int
interactionId

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

-- | Given goals, warnings and errors, return a pair of the
--   title and the body for the info buffer.
formatWarningsAndErrors :: Doc -> [Doc] -> [Doc] -> (String, Doc)
formatWarningsAndErrors :: Doc Aspects
-> [Doc Aspects] -> [Doc Aspects] -> ([Char], Doc Aspects)
formatWarningsAndErrors Doc Aspects
g [Doc Aspects]
ws [Doc Aspects]
es = ([Char]
title, Doc Aspects
body)
  where
    isG :: Bool
isG = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Doc Aspects -> Bool
forall a. Null a => a -> Bool
null Doc Aspects
g
    isW :: Bool
isW = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [Doc Aspects] -> Bool
forall a. Null a => a -> Bool
null [Doc Aspects]
ws
    isE :: Bool
isE = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [Doc Aspects] -> Bool
forall a. Null a => a -> Bool
null [Doc Aspects]
es
    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
$ [[[Char]]] -> [[Char]]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
      [ [ [Char]
" Goals"    | Bool
isG ]
      , [ [Char]
" Errors"   | Bool
isE ]
      , [ [Char]
" Warnings" | Bool
isW ]
      , [ [Char]
" Done"     | Bool -> Bool
not (Bool
isG Bool -> Bool -> Bool
|| Bool
isW Bool -> Bool -> Bool
|| Bool
isE) ]
      ]
    body :: Doc Aspects
body = [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
$ [[Doc Aspects]] -> [Doc Aspects]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
      [ [ Doc Aspects
g ]
      , [ [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]
"Error"    | Bool
isE Bool -> Bool -> Bool
&& (Bool
isG Bool -> Bool -> Bool
|| Bool
isW) ]
      , [Doc Aspects]
es
      , [ [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]
"Warnings" | Bool
isW Bool -> Bool -> Bool
&& (Bool
isG Bool -> Bool -> Bool
|| Bool
isE) ]
      , [Doc Aspects]
ws
      ]

-- | Serializing 'Info_Error'.
showInfoError :: Info_Error -> TCM String
showInfoError :: Info_Error_boot TCErr TCWarning -> TCM [Char]
showInfoError = Doc Aspects -> [Char]
forall a. Doc a -> [Char]
render (Doc Aspects -> [Char])
-> (Info_Error_boot TCErr TCWarning -> TCMT IO (Doc Aspects))
-> Info_Error_boot TCErr TCWarning
-> TCM [Char]
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> Info_Error_boot TCErr TCWarning -> TCMT IO (Doc Aspects)
prettyInfoError

-- | Turn an 'Info_Error' into a 'Doc'.
prettyInfoError :: Info_Error -> TCM Doc
prettyInfoError :: Info_Error_boot TCErr TCWarning -> TCMT IO (Doc Aspects)
prettyInfoError = \case
  Info_GenericError TCErr
err -> do
    e  <- TCErr -> TCMT IO (Doc Aspects)
forall (tcm :: * -> *). MonadTCM tcm => TCErr -> tcm (Doc Aspects)
prettyError TCErr
err
    ws <- prettyTCWarnings' =<< getAllWarningsOfTCErr err
    let (_title, body) = formatWarningsAndErrors empty ws [e]
    return body

  Info_CompilationError Set TCWarning
warnings -> do
    docs <- Set TCWarning -> TCM [Doc Aspects]
prettyTCWarnings' Set TCWarning
warnings
    return $ vcat $
      "You need to fix the following errors before you can compile the module:" :
      "" :
      docs

  Info_HighlightingParseError InteractionId
ii ->
    Doc Aspects -> TCMT IO (Doc Aspects)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc Aspects -> TCMT IO (Doc Aspects))
-> Doc Aspects -> TCMT IO (Doc Aspects)
forall a b. (a -> b) -> a -> b
$ Doc Aspects
"Highlighting failed to parse expression in" Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> InteractionId -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty InteractionId
ii

  Info_HighlightingScopeCheckError InteractionId
ii ->
    Doc Aspects -> TCMT IO (Doc Aspects)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc Aspects -> TCMT IO (Doc Aspects))
-> Doc Aspects -> TCMT IO (Doc Aspects)
forall a b. (a -> b) -> a -> b
$ Doc Aspects
"Highlighting failed to scope check expression in" Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> InteractionId -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty 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, MonadError TCErr 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. Null a => 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. Null a => 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
  Rewrite
-> InteractionId
-> TCM (OutputConstraint_boot TCErr Expr InteractionId)
B.typeOfMeta Rewrite
norm InteractionId
ii TCM (OutputConstraint_boot TCErr Expr InteractionId)
-> (OutputConstraint_boot TCErr Expr InteractionId
    -> TCMT IO (Doc Aspects))
-> TCMT IO (Doc Aspects)
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    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_boot TCErr Expr InteractionId
form       -> OutputConstraint_boot TCErr Expr InteractionId
-> TCMT IO (Doc Aspects)
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m (Doc Aspects)
prettyATop OutputConstraint_boot TCErr 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