{-# 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 Data.Text qualified as Text

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)
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  ( treeToTextNoAnn, 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 -> String -> 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 String -> IO ()) -> Lisp String -> TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> IO ()
putStrLn (String -> IO ())
-> (Lisp String -> String) -> Lisp String -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lisp String -> String
forall a. Pretty a => a -> String
prettyShow (Lisp String -> TCM ())
-> (Response_boot TCErr TCWarning WarningsAndNonFatalErrors
    -> TCMT IO (Lisp String))
-> 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 String)
lispifyResponse) String
"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 String)
lispifyResponse = \case

  Resp_HighlightingInfo HighlightingInfo
info RemoveTokenBasedHighlighting
remove HighlightingMethod
method ModuleToSource
modFile ->
    IO (Lisp String) -> TCMT IO (Lisp String)
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (HighlightingInfo
-> RemoveTokenBasedHighlighting
-> HighlightingMethod
-> ModuleToSource
-> IO (Lisp String)
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 String)
lispifyDisplayInfo DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
info

  Resp_ClearHighlighting TokenBased
tokenBased ->
    Lisp String -> TCMT IO (Lisp String)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Lisp String -> TCMT IO (Lisp String))
-> Lisp String -> TCMT IO (Lisp String)
forall a b. (a -> b) -> a -> b
$ [Lisp String] -> Lisp String
forall a. [Lisp a] -> Lisp a
L ([Lisp String] -> Lisp String) -> [Lisp String] -> Lisp String
forall a b. (a -> b) -> a -> b
$
      String -> Lisp String
forall a. a -> Lisp a
A String
"agda2-highlight-clear" Lisp String -> [Lisp String] -> [Lisp String]
forall a. a -> [a] -> [a]
:
      case TokenBased
tokenBased of
        TokenBased
TokenBased -> [ Lisp String -> Lisp String
forall a. Lisp a -> Lisp a
Q (TokenBased -> Lisp String
lispifyTokenBased TokenBased
tokenBased) ]
        TokenBased
NotOnlyTokenBased -> []

  Response_boot TCErr TCWarning WarningsAndNonFatalErrors
Resp_DoneAborting ->
    Lisp String -> TCMT IO (Lisp String)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Lisp String -> TCMT IO (Lisp String))
-> Lisp String -> TCMT IO (Lisp String)
forall a b. (a -> b) -> a -> b
$ [Lisp String] -> Lisp String
forall a. [Lisp a] -> Lisp a
L [ String -> Lisp String
forall a. a -> Lisp a
A String
"agda2-abort-done" ]

  Response_boot TCErr TCWarning WarningsAndNonFatalErrors
Resp_DoneExiting ->
    Lisp String -> TCMT IO (Lisp String)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Lisp String -> TCMT IO (Lisp String))
-> Lisp String -> TCMT IO (Lisp String)
forall a b. (a -> b) -> a -> b
$ [Lisp String] -> Lisp String
forall a. [Lisp a] -> Lisp a
L [ String -> Lisp String
forall a. a -> Lisp a
A String
"agda2-exit-done" ]

  Response_boot TCErr TCWarning WarningsAndNonFatalErrors
Resp_ClearRunningInfo ->
    Lisp String -> TCMT IO (Lisp String)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Lisp String
clearRunningInfo

  Resp_RunningInfo Nat
n DocTree
docTree
    | Nat
n Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
<= Nat
1 -> do
        DocTree -> Maybe ModuleToSource -> Lisp String
displayRunningInfo DocTree
docTree (Maybe ModuleToSource -> Lisp String)
-> TCMT IO (Maybe ModuleToSource) -> TCMT IO (Lisp String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO (Maybe ModuleToSource)
wantBufferHighlighting
    | Bool
otherwise ->
        Lisp String -> TCMT IO (Lisp String)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Lisp String -> TCMT IO (Lisp String))
-> Lisp String -> TCMT IO (Lisp String)
forall a b. (a -> b) -> a -> b
$ [Lisp String] -> Lisp String
forall a. [Lisp a] -> Lisp a
L [ String -> Lisp String
forall a. a -> Lisp a
A String
"agda2-verbose", String -> Lisp String
forall a. a -> Lisp a
A (String -> String
quote (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ Text -> String
Text.unpack (Text -> String) -> Text -> String
forall a b. (a -> b) -> a -> b
$ DocTree -> Text
forall ann. DocTree ann -> Text
treeToTextNoAnn DocTree
docTree) ]
        -- TODO: do we want colored debug-printout?

  Resp_Status Status
s ->
    Lisp String -> TCMT IO (Lisp String)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Lisp String -> TCMT IO (Lisp String))
-> Lisp String -> TCMT IO (Lisp String)
forall a b. (a -> b) -> a -> b
$ [Lisp String] -> Lisp String
forall a. [Lisp a] -> Lisp a
L
      [ String -> Lisp String
forall a. a -> Lisp a
A String
"agda2-status-action"
      , String -> Lisp String
forall a. a -> Lisp a
A (String -> String
quote (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
List.intercalate String
"," ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [Maybe String] -> [String]
forall a. [Maybe a] -> [a]
catMaybes [Maybe String
checked, Maybe String
showImpl, Maybe String
showIrr])
      ]
    where
      checked :: Maybe String
checked  = Bool -> String -> Maybe String
forall a. Bool -> a -> Maybe a
boolToMaybe (Status -> Bool
sChecked                 Status
s) String
"Checked"
      showImpl :: Maybe String
showImpl = Bool -> String -> Maybe String
forall a. Bool -> a -> Maybe a
boolToMaybe (Status -> Bool
sShowImplicitArguments   Status
s) String
"ShowImplicit"
      showIrr :: Maybe String
showIrr  = Bool -> String -> Maybe String
forall a. Bool -> a -> Maybe a
boolToMaybe (Status -> Bool
sShowIrrelevantArguments Status
s) String
"ShowIrrelevant"

  Resp_JumpToError String
f Word32
p ->
    Lisp String -> TCMT IO (Lisp String)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Lisp String -> TCMT IO (Lisp String))
-> Lisp String -> TCMT IO (Lisp String)
forall a b. (a -> b) -> a -> b
$ Integer -> Lisp String -> Lisp String
lastTag Integer
3 (Lisp String -> Lisp String) -> Lisp String -> Lisp String
forall a b. (a -> b) -> a -> b
$ [Lisp String] -> Lisp String
forall a. [Lisp a] -> Lisp a
L
      [ String -> Lisp String
forall a. a -> Lisp a
A String
"agda2-maybe-goto"
      , Lisp String -> Lisp String
forall a. Lisp a -> Lisp a
Q (Lisp String -> Lisp String) -> Lisp String -> Lisp String
forall a b. (a -> b) -> a -> b
$ [Lisp String] -> Lisp String
forall a. [Lisp a] -> Lisp a
L [ String -> Lisp String
forall a. a -> Lisp a
A (String -> String
quote String
f), String -> Lisp String
forall a. a -> Lisp a
A String
".", String -> Lisp String
forall a. a -> Lisp a
A (Word32 -> String
forall a. Show a => a -> String
show Word32
p) ]
      ]

  Resp_InteractionPoints [InteractionId]
is ->
    Lisp String -> TCMT IO (Lisp String)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Lisp String -> TCMT IO (Lisp String))
-> Lisp String -> TCMT IO (Lisp String)
forall a b. (a -> b) -> a -> b
$ Integer -> Lisp String -> Lisp String
lastTag Integer
1 (Lisp String -> Lisp String) -> Lisp String -> Lisp String
forall a b. (a -> b) -> a -> b
$ [Lisp String] -> Lisp String
forall a. [Lisp a] -> Lisp a
L
      [ String -> Lisp String
forall a. a -> Lisp a
A String
"agda2-goals-action"
      , Lisp String -> Lisp String
forall a. Lisp a -> Lisp a
Q (Lisp String -> Lisp String) -> Lisp String -> Lisp String
forall a b. (a -> b) -> a -> b
$ [Lisp String] -> Lisp String
forall a. [Lisp a] -> Lisp a
L ([Lisp String] -> Lisp String) -> [Lisp String] -> Lisp String
forall a b. (a -> b) -> a -> b
$ (InteractionId -> Lisp String) -> [InteractionId] -> [Lisp String]
forall a b. (a -> b) -> [a] -> [b]
map InteractionId -> Lisp String
showNumIId [InteractionId]
is
      ]

  Resp_GiveAction InteractionId
ii GiveResult
s ->
    Lisp String -> TCMT IO (Lisp String)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Lisp String -> TCMT IO (Lisp String))
-> Lisp String -> TCMT IO (Lisp String)
forall a b. (a -> b) -> a -> b
$ [Lisp String] -> Lisp String
forall a. [Lisp a] -> Lisp a
L
      [ String -> Lisp String
forall a. a -> Lisp a
A String
"agda2-give-action"
      , InteractionId -> Lisp String
showNumIId InteractionId
ii
      , String -> Lisp String
forall a. a -> Lisp a
A String
s'
      ]
    where
      s' :: String
s' = case GiveResult
s of
          Give_String String
str -> String -> String
quote String
str
          GiveResult
Give_Paren      -> String
"'paren"
          GiveResult
Give_NoParen    -> String
"'no-paren"

  Resp_MakeCase InteractionId
ii MakeCaseVariant
variant [String]
pcs ->
    Lisp String -> TCMT IO (Lisp String)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Lisp String -> TCMT IO (Lisp String))
-> Lisp String -> TCMT IO (Lisp String)
forall a b. (a -> b) -> a -> b
$ Integer -> Lisp String -> Lisp String
lastTag Integer
2 (Lisp String -> Lisp String) -> Lisp String -> Lisp String
forall a b. (a -> b) -> a -> b
$ [Lisp String] -> Lisp String
forall a. [Lisp a] -> Lisp a
L
      [ String -> Lisp String
forall a. a -> Lisp a
A String
cmd
      , Lisp String -> Lisp String
forall a. Lisp a -> Lisp a
Q (Lisp String -> Lisp String) -> Lisp String -> Lisp String
forall a b. (a -> b) -> a -> b
$ [Lisp String] -> Lisp String
forall a. [Lisp a] -> Lisp a
L ([Lisp String] -> Lisp String) -> [Lisp String] -> Lisp String
forall a b. (a -> b) -> a -> b
$ (String -> Lisp String) -> [String] -> [Lisp String]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Lisp String
forall a. a -> Lisp a
A (String -> Lisp String)
-> (String -> String) -> String -> Lisp String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
quote) [String]
pcs
      ]
    where
    cmd :: String
cmd = case MakeCaseVariant
variant of
      MakeCaseVariant
R.Function       -> String
"agda2-make-case-action"
      MakeCaseVariant
R.ExtendedLambda -> String
"agda2-make-case-action-extendlam"

  Resp_SolveAll [(InteractionId, Expr)]
ps ->
    Lisp String -> TCMT IO (Lisp String)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Lisp String -> TCMT IO (Lisp String))
-> Lisp String -> TCMT IO (Lisp String)
forall a b. (a -> b) -> a -> b
$ Integer -> Lisp String -> Lisp String
lastTag Integer
2 (Lisp String -> Lisp String) -> Lisp String -> Lisp String
forall a b. (a -> b) -> a -> b
$ [Lisp String] -> Lisp String
forall a. [Lisp a] -> Lisp a
L
      [ String -> Lisp String
forall a. a -> Lisp a
A String
"agda2-solveAll-action"
      , Lisp String -> Lisp String
forall a. Lisp a -> Lisp a
Q (Lisp String -> Lisp String) -> Lisp String -> Lisp String
forall a b. (a -> b) -> a -> b
$ [Lisp String] -> Lisp String
forall a. [Lisp a] -> Lisp a
L ([Lisp String] -> Lisp String) -> [Lisp String] -> Lisp String
forall a b. (a -> b) -> a -> b
$ ((InteractionId, Expr) -> [Lisp String])
-> [(InteractionId, Expr)] -> [Lisp String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (InteractionId, Expr) -> [Lisp String]
forall {a}. Pretty a => (InteractionId, a) -> [Lisp String]
prn [(InteractionId, Expr)]
ps
      ]
    where
      prn :: (InteractionId, a) -> [Lisp String]
prn (InteractionId
ii,a
e)= [InteractionId -> Lisp String
showNumIId InteractionId
ii, String -> Lisp String
forall a. a -> Lisp a
A (String -> Lisp String) -> String -> Lisp String
forall a b. (a -> b) -> a -> b
$ String -> String
quote (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ a -> String
forall a. Pretty a => a -> String
prettyShow a
e]

  Resp_Mimer InteractionId
ii Maybe String
msol ->
    Lisp String -> TCMT IO (Lisp String)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Lisp String -> TCMT IO (Lisp String))
-> Lisp String -> TCMT IO (Lisp String)
forall a b. (a -> b) -> a -> b
$ Integer -> Lisp String -> Lisp String
lastTag Integer
1 (Lisp String -> Lisp String) -> Lisp String -> Lisp String
forall a b. (a -> b) -> a -> b
$ [Lisp String] -> Lisp String
forall a. [Lisp a] -> Lisp a
L ([Lisp String] -> Lisp String) -> [Lisp String] -> Lisp String
forall a b. (a -> b) -> a -> b
$ case Maybe String
msol of
      Maybe String
Nothing ->
        [ String -> Lisp String
forall a. a -> Lisp a
A String
"agda2-info-action"
        , String -> Lisp String
forall a. a -> Lisp a
A (String -> Lisp String) -> String -> Lisp String
forall a b. (a -> b) -> a -> b
$ String -> String
quote String
"*Mimer*"
        , String -> Lisp String
forall a. a -> Lisp a
A (String -> Lisp String) -> String -> Lisp String
forall a b. (a -> b) -> a -> b
$ String -> String
quote String
"No solution found"
        ]
      Just String
str ->
        [ String -> Lisp String
forall a. a -> Lisp a
A String
"agda2-solve-action"
        , InteractionId -> Lisp String
showNumIId InteractionId
ii
        , String -> Lisp String
forall a. a -> Lisp a
A (String -> Lisp String) -> String -> Lisp String
forall a b. (a -> b) -> a -> b
$ String -> String
quote String
str
        ]

lispifyDisplayInfo :: DisplayInfo -> TCM (Lisp String)
lispifyDisplayInfo :: DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
-> TCMT IO (Lisp String)
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 String
s ->
      String -> Doc Aspects -> TCMT IO (Lisp String)
format String
"*Auto*" (Doc Aspects -> TCMT IO (Lisp String))
-> Doc Aspects -> TCMT IO (Lisp String)
forall a b. (a -> b) -> a -> b
$ String -> Doc Aspects
forall a. String -> Doc a
P.text String
s

    Info_Error Info_Error_boot TCErr TCWarning
err -> do
      String -> Doc Aspects -> TCMT IO (Lisp String)
format String
"*Error*" (Doc Aspects -> TCMT IO (Lisp String))
-> TCMT IO (Doc Aspects) -> TCMT IO (Lisp String)
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 ->
      String -> Doc Aspects -> TCMT IO (Lisp String)
format String
"*Time*" (Doc Aspects -> TCMT IO (Lisp String))
-> Doc Aspects -> TCMT IO (Lisp String)
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 = String
"*Head Normal Form*"
              | Bool
otherwise            = String
"*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
$ TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects)
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
allowNonTerminatingReductions
            (TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects))
-> TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects)
forall a b. (a -> b) -> a -> b
$ (if ComputeMode -> Bool
computeIgnoreAbstract ComputeMode
cmode then TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects)
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
ignoreAbstractMode else TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects)
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
inConcreteMode)
            (TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects))
-> TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects)
forall a b. (a -> b) -> a -> b
$ (ComputeMode -> Expr -> TCMT IO (Doc Aspects)
B.showComputed ComputeMode
cmode)
            (Expr -> TCMT IO (Doc Aspects)) -> Expr -> TCMT IO (Doc Aspects)
forall a b. (a -> b) -> a -> b
$ Expr
expr

    Info_InferredType CommandState
state Maybe CPUTime
time Expr
expr -> do
      exprDoc <- StateT CommandState (TCMT IO) (Doc Aspects)
-> CommandState -> TCMT IO (Doc Aspects)
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT StateT CommandState (TCMT IO) (Doc Aspects)
prettyExpr CommandState
state
      let doc = Doc Aspects
-> (CPUTime -> Doc Aspects) -> Maybe CPUTime -> Doc Aspects
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc Aspects
forall a. Null a => a
empty CPUTime -> Doc Aspects
prettyTimed Maybe CPUTime
time Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
$$ Doc Aspects
exprDoc
      format "*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 Telescope
tel [(Name, Type)]
types -> do
      doc <- TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects)
forall a. TCM a -> TCM a
localTCState (TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects))
-> TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects)
forall a b. (a -> b) -> a -> b
$ do
        typeDocs <- Telescope
-> TCMT IO [(String, Doc Aspects)]
-> TCMT IO [(String, Doc Aspects)]
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
tel (TCMT IO [(String, Doc Aspects)]
 -> TCMT IO [(String, Doc Aspects)])
-> TCMT IO [(String, Doc Aspects)]
-> TCMT IO [(String, Doc Aspects)]
forall a b. (a -> b) -> a -> b
$ [(Name, Type)]
-> ((Name, Type) -> TCMT IO (String, Doc Aspects))
-> TCMT IO [(String, 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 (String, Doc Aspects))
 -> TCMT IO [(String, Doc Aspects)])
-> ((Name, Type) -> TCMT IO (String, Doc Aspects))
-> TCMT IO [(String, 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 String
names -> do
      hitDocs <- [(Name, Type)]
-> ((Name, Type) -> TCMT IO (String, Doc Aspects))
-> TCMT IO [(String, 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 (String, Doc Aspects))
 -> TCMT IO [(String, Doc Aspects)])
-> ((Name, Type) -> TCMT IO (String, Doc Aspects))
-> TCMT IO [(String, 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
<+>
                String -> Doc Aspects
forall a. String -> Doc a
text (String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
List.intercalate String
", " ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ String -> [String]
words String
names) Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
$$ Nat -> Doc Aspects -> Doc Aspects
forall a. Nat -> Doc a -> Doc a
nest Nat
2 (Nat -> [(String, Doc Aspects)] -> Doc Aspects
align Nat
10 [(String, 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 ->
      String -> Doc Aspects -> TCMT IO (Lisp String)
format String
"*Intro*" Doc Aspects
"No introduction forms found."

    Info_Intro_ConstructorUnknown [String]
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 :: [String] -> [Doc a]
mkOr []     = []
                          mkOr [String
x, String
y] = [String -> Doc a
forall a. String -> Doc a
text String
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
<+> String -> Doc a
forall a. String -> Doc a
text String
y]
                          mkOr (String
x:[String]
xs) = String -> Doc a
forall a. String -> Doc a
text String
x Doc a -> [Doc a] -> [Doc a]
forall a. a -> [a] -> [a]
: [String] -> [Doc a]
mkOr [String]
xs
                      in Nat -> Doc Aspects -> Doc Aspects
forall a. Nat -> Doc a -> Doc a
nest Nat
2 (Doc Aspects -> Doc Aspects) -> Doc Aspects -> Doc Aspects
forall a b. (a -> b) -> a -> b
$ [Doc Aspects] -> Doc Aspects
forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
fsep ([Doc Aspects] -> Doc Aspects) -> [Doc Aspects] -> Doc Aspects
forall a b. (a -> b) -> a -> b
$ Doc Aspects -> [Doc Aspects] -> [Doc Aspects]
forall (t :: * -> *).
Foldable t =>
Doc Aspects -> t (Doc Aspects) -> [Doc Aspects]
punctuate Doc Aspects
comma ([String] -> [Doc Aspects]
forall {a}. [String] -> [Doc a]
mkOr [String]
ss)
                    ]
      String -> Doc Aspects -> TCMT IO (Lisp String)
format String
"*Intro*" Doc Aspects
doc

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

    Info_GoalSpecific InteractionId
ii GoalDisplayInfo_boot TCErr
kind ->
      InteractionId
-> GoalDisplayInfo_boot TCErr -> TCMT IO (Lisp String)
lispifyGoalSpecificDisplayInfo InteractionId
ii GoalDisplayInfo_boot TCErr
kind

lispifyGoalSpecificDisplayInfo :: InteractionId -> GoalDisplayInfo -> TCM (Lisp String)
lispifyGoalSpecificDisplayInfo :: InteractionId
-> GoalDisplayInfo_boot TCErr -> TCMT IO (Lisp String)
lispifyGoalSpecificDisplayInfo InteractionId
ii GoalDisplayInfo_boot TCErr
kind = TCMT IO (Lisp String) -> TCMT IO (Lisp String)
forall a. TCM a -> TCM a
localTCState (TCMT IO (Lisp String) -> TCMT IO (Lisp String))
-> TCMT IO (Lisp String) -> TCMT IO (Lisp String)
forall a b. (a -> b) -> a -> b
$ InteractionId -> TCMT IO (Lisp String) -> TCMT IO (Lisp String)
forall (m :: * -> *) a.
(MonadDebug m, ReadTCState m, MonadError TCErr m, MonadTCEnv m,
 MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
ii (TCMT IO (Lisp String) -> TCMT IO (Lisp String))
-> TCMT IO (Lisp String) -> TCMT IO (Lisp String)
forall a b. (a -> b) -> a -> b
$
  case GoalDisplayInfo_boot TCErr
kind of

    Goal_HelperFunction OutputConstraint' Expr Expr
helperType -> do
      doc <- TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects)
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects))
-> TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects)
forall a b. (a -> b) -> a -> b
$ OutputConstraint' Expr Expr -> TCMT IO (Doc Aspects)
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m (Doc Aspects)
prettyATop OutputConstraint' Expr Expr
helperType
      return $ L
        [ A "agda2-info-action-and-copy"
        , A $ quote "*Helper function*"
        , A $ quote (render doc ++ "\n")
        , A "nil"
        ]

    Goal_NormalForm ComputeMode
cmode Expr
expr -> do
      doc <- ComputeMode -> Expr -> TCMT IO (Doc Aspects)
showComputed ComputeMode
cmode Expr
expr
      format "*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 String
hd [a]
bndry
            | [a] -> Bool
forall a. Null a => a -> Bool
null [a]
bndry = []
            | Bool
otherwise  = [ String -> Doc Aspects
forall a. String -> Doc a
text (String -> Doc Aspects) -> String -> Doc Aspects
forall a b. (a -> b) -> a -> b
$ String -> String
delimiter String
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        =
              [ String -> TCMT IO (Doc Aspects)
forall (m :: * -> *). Applicative m => String -> m (Doc Aspects)
TCP.text (String -> TCMT IO (Doc Aspects))
-> String -> TCMT IO (Doc Aspects)
forall a b. (a -> b) -> a -> b
$ String -> String
delimiter String
"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 responses of DisplayInfo

format :: String -> Doc -> TCM (Lisp String)
format :: String -> Doc Aspects -> TCMT IO (Lisp String)
format String
header Doc Aspects
content = do
  String -> DocTree -> Bool -> Maybe ModuleToSource -> Lisp String
displayInfo String
header (Doc Aspects -> DocTree
forall ann. Null ann => Doc ann -> DocTree ann
renderToTree Doc Aspects
content) Bool
False (Maybe ModuleToSource -> Lisp String)
-> TCMT IO (Maybe ModuleToSource) -> TCMT IO (Lisp String)
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 <$> useTC stModuleToSource else return Nothing

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

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

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

showNumIId :: InteractionId -> Lisp String
showNumIId :: InteractionId -> Lisp String
showNumIId = String -> Lisp String
forall a. a -> Lisp a
A (String -> Lisp String)
-> (InteractionId -> String) -> InteractionId -> Lisp String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat -> String
forall a. Show a => a -> String
show (Nat -> String)
-> (InteractionId -> Nat) -> InteractionId -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InteractionId -> Nat
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] -> (String, Doc Aspects)
formatWarningsAndErrors Doc Aspects
g [Doc Aspects]
ws [Doc Aspects]
es = (String
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 :: String
title = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
List.intercalate String
"," ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [[String]] -> [String]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
      [ [ String
" Goals"    | Bool
isG ]
      , [ String
" Errors"   | Bool
isE ]
      , [ String
" Warnings" | Bool
isW ]
      , [ String
" 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 ]
      , [ String -> Doc Aspects
forall a. String -> Doc a
text (String -> Doc Aspects) -> String -> Doc Aspects
forall a b. (a -> b) -> a -> b
$ String -> String
delimiter String
"Error"    | Bool
isE Bool -> Bool -> Bool
&& (Bool
isG Bool -> Bool -> Bool
|| Bool
isW) ]
      , [Doc Aspects]
es
      , [ String -> Doc Aspects
forall a. String -> Doc a
text (String -> Doc Aspects) -> String -> Doc Aspects
forall a b. (a -> b) -> a -> b
$ String -> String
delimiter String
"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 String
showInfoError = Doc Aspects -> String
forall a. Doc a -> String
render (Doc Aspects -> String)
-> (Info_Error_boot TCErr TCWarning -> TCMT IO (Doc Aspects))
-> Info_Error_boot TCErr TCWarning
-> TCM String
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

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, ReadTCState m, MonadError TCErr m, MonadTCEnv m,
 MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
ii (TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects))
-> TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects)
forall a b. (a -> b) -> a -> b
$ do
  mod <- TCMT IO Modality
forall (m :: * -> *). MonadTCEnv m => m Modality
currentModality
  align 10 . concat . applyWhen rev reverse <$> do
    forM ctx $ \ (ResponseContextEntry Name
n Name
x (Arg ArgInfo
ai Expr
expr) Maybe Expr
letv NameInScope
nis) -> do
      let
        prettyCtxName :: String
        prettyCtxName :: String
prettyCtxName
          | Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
x                 = Name -> String
forall a. Pretty a => a -> String
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 -> String
forall a. Pretty a => a -> String
prettyShow Name
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Pretty a => a -> String
prettyShow Name
x
          | Bool
otherwise              = Name -> String
forall a. Pretty a => a -> String
prettyShow Name
x

        -- Some attributes are useful to report whenever they are not
        -- in the default state.
        attribute :: String
        attribute :: String
attribute = String
c String -> String -> String
forall a. [a] -> [a] -> [a]
++ if String -> Bool
forall a. Null a => a -> Bool
null String
c then String
"" else String
" "
          where c :: String
c = Cohesion -> String
forall a. Pretty a => a -> String
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.)
          , [ String -> Doc Aspects
forall a. String -> Doc a
text (String -> Doc Aspects) -> String -> Doc Aspects
forall a b. (a -> b) -> a -> b
$ Relevance -> String
forall a. Verbalize a => a -> String
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 ]
          , [ String -> Doc Aspects
forall a. String -> Doc a
text (String -> Doc Aspects) -> String -> Doc Aspects
forall a b. (a -> b) -> a -> b
$ ModalPolarity -> String
forall a. Verbalize a => a -> String
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 Expr InteractionId)
B.typeOfMeta Rewrite
norm InteractionId
ii TCM (OutputConstraint Expr InteractionId)
-> (OutputConstraint 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 Expr InteractionId
form       -> OutputConstraint Expr InteractionId -> TCMT IO (Doc Aspects)
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m (Doc Aspects)
prettyATop OutputConstraint Expr InteractionId
form

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