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

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

import qualified Data.List as List

import Agda.Syntax.Common
import Agda.Syntax.Position
import Agda.Syntax.Scope.Base
import Agda.Syntax.Abstract.Pretty (prettyATop)
import Agda.Syntax.Abstract as A
import Agda.Syntax.Concrete as C

import Agda.TypeChecking.Errors ( explainWhyInScope, getAllWarningsOfTCErr, prettyError )
import qualified Agda.TypeChecking.Pretty as TCP
import Agda.TypeChecking.Pretty (prettyTCM)
import Agda.TypeChecking.Pretty.Warning (prettyTCWarnings, prettyTCWarnings')
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Warnings (WarningsAndNonFatalErrors(..))
import Agda.Interaction.AgdaTop
import Agda.Interaction.Base
import Agda.Interaction.BasicOps as B
import Agda.Interaction.Response as R
import Agda.Interaction.EmacsCommand hiding (putResponse)
import Agda.Interaction.Highlighting.Emacs
import Agda.Interaction.Highlighting.Precise (TokenBased(..))
import Agda.Interaction.InteractionTop (localStateCommandM)
import Agda.Utils.Function (applyWhen)
import Agda.Utils.Null (empty)
import Agda.Utils.Maybe
import Agda.Utils.Pretty
import Agda.Utils.String
import Agda.Utils.Time (CPUTime)
import Agda.VersionCommit

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

-- | 'mimicGHCi' is a fake ghci interpreter for the Emacs frontend
--   and for interaction tests.
--
--   'mimicGHCi' reads the Emacs frontend commands from stdin,
--   interprets them and print the result into stdout.
mimicGHCi :: TCM () -> TCM ()
mimicGHCi :: TCM () -> TCM ()
mimicGHCi = InteractionOutputCallback -> [Char] -> TCM () -> TCM ()
repl (IO () -> TCM ()
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> TCM ())
-> ([Lisp [Char]] -> IO ()) -> [Lisp [Char]] -> TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Lisp [Char] -> IO ()) -> [Lisp [Char]] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ([Char] -> IO ()
putStrLn ([Char] -> IO ())
-> (Lisp [Char] -> [Char]) -> Lisp [Char] -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lisp [Char] -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow) ([Lisp [Char]] -> TCM ())
-> (Response -> TCMT IO [Lisp [Char]]) -> InteractionOutputCallback
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Response -> TCMT IO [Lisp [Char]]
lispifyResponse) [Char]
"Agda2> "

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

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

lispifyResponse (Resp_JumpToError [Char]
f Int32
p) = [Lisp [Char]] -> TCMT IO [Lisp [Char]]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return
  [ Integer -> Lisp [Char] -> Lisp [Char]
lastTag Integer
3 (Lisp [Char] -> Lisp [Char]) -> Lisp [Char] -> Lisp [Char]
forall a b. (a -> b) -> a -> b
$
      [Lisp [Char]] -> Lisp [Char]
forall a. [Lisp a] -> Lisp a
L [ [Char] -> Lisp [Char]
forall a. a -> Lisp a
A [Char]
"agda2-maybe-goto", Lisp [Char] -> Lisp [Char]
forall a. Lisp a -> Lisp a
Q (Lisp [Char] -> Lisp [Char]) -> Lisp [Char] -> Lisp [Char]
forall a b. (a -> b) -> a -> b
$ [Lisp [Char]] -> Lisp [Char]
forall a. [Lisp a] -> Lisp a
L [[Char] -> Lisp [Char]
forall a. a -> Lisp a
A ([Char] -> [Char]
quote [Char]
f), [Char] -> Lisp [Char]
forall a. a -> Lisp a
A [Char]
".", [Char] -> Lisp [Char]
forall a. a -> Lisp a
A (Int32 -> [Char]
forall a. Show a => a -> [Char]
show Int32
p)] ]
  ]
lispifyResponse (Resp_InteractionPoints [InteractionId]
is) = [Lisp [Char]] -> TCMT IO [Lisp [Char]]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return
  [ Integer -> Lisp [Char] -> Lisp [Char]
lastTag Integer
1 (Lisp [Char] -> Lisp [Char]) -> Lisp [Char] -> Lisp [Char]
forall a b. (a -> b) -> a -> b
$
      [Lisp [Char]] -> Lisp [Char]
forall a. [Lisp a] -> Lisp a
L [[Char] -> Lisp [Char]
forall a. a -> Lisp a
A [Char]
"agda2-goals-action", Lisp [Char] -> Lisp [Char]
forall a. Lisp a -> Lisp a
Q (Lisp [Char] -> Lisp [Char]) -> Lisp [Char] -> Lisp [Char]
forall a b. (a -> b) -> a -> b
$ [Lisp [Char]] -> Lisp [Char]
forall a. [Lisp a] -> Lisp a
L ([Lisp [Char]] -> Lisp [Char]) -> [Lisp [Char]] -> Lisp [Char]
forall a b. (a -> b) -> a -> b
$ (InteractionId -> Lisp [Char]) -> [InteractionId] -> [Lisp [Char]]
forall a b. (a -> b) -> [a] -> [b]
map InteractionId -> Lisp [Char]
showNumIId [InteractionId]
is]
  ]
lispifyResponse (Resp_GiveAction InteractionId
ii GiveResult
s)
    = [Lisp [Char]] -> TCMT IO [Lisp [Char]]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [ [Lisp [Char]] -> Lisp [Char]
forall a. [Lisp a] -> Lisp a
L [ [Char] -> Lisp [Char]
forall a. a -> Lisp a
A [Char]
"agda2-give-action", InteractionId -> Lisp [Char]
showNumIId InteractionId
ii, [Char] -> Lisp [Char]
forall a. a -> Lisp a
A [Char]
s' ] ]
  where
    s' :: [Char]
s' = case GiveResult
s of
        Give_String [Char]
str -> [Char] -> [Char]
quote [Char]
str
        GiveResult
Give_Paren      -> [Char]
"'paren"
        GiveResult
Give_NoParen    -> [Char]
"'no-paren"
lispifyResponse (Resp_MakeCase InteractionId
ii MakeCaseVariant
variant [[Char]]
pcs) = [Lisp [Char]] -> TCMT IO [Lisp [Char]]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return
  [ Integer -> Lisp [Char] -> Lisp [Char]
lastTag Integer
2 (Lisp [Char] -> Lisp [Char]) -> Lisp [Char] -> Lisp [Char]
forall a b. (a -> b) -> a -> b
$ [Lisp [Char]] -> Lisp [Char]
forall a. [Lisp a] -> Lisp a
L [ [Char] -> Lisp [Char]
forall a. a -> Lisp a
A [Char]
cmd, Lisp [Char] -> Lisp [Char]
forall a. Lisp a -> Lisp a
Q (Lisp [Char] -> Lisp [Char]) -> Lisp [Char] -> Lisp [Char]
forall a b. (a -> b) -> a -> b
$ [Lisp [Char]] -> Lisp [Char]
forall a. [Lisp a] -> Lisp a
L ([Lisp [Char]] -> Lisp [Char]) -> [Lisp [Char]] -> Lisp [Char]
forall a b. (a -> b) -> a -> b
$ ([Char] -> Lisp [Char]) -> [[Char]] -> [Lisp [Char]]
forall a b. (a -> b) -> [a] -> [b]
map ([Char] -> Lisp [Char]
forall a. a -> Lisp a
A ([Char] -> Lisp [Char])
-> ([Char] -> [Char]) -> [Char] -> Lisp [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> [Char]
quote) [[Char]]
pcs ] ]
  where
  cmd :: [Char]
cmd = case MakeCaseVariant
variant of
    MakeCaseVariant
R.Function       -> [Char]
"agda2-make-case-action"
    MakeCaseVariant
R.ExtendedLambda -> [Char]
"agda2-make-case-action-extendlam"
lispifyResponse (Resp_SolveAll [(InteractionId, Expr)]
ps) = [Lisp [Char]] -> TCMT IO [Lisp [Char]]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return
  [ Integer -> Lisp [Char] -> Lisp [Char]
lastTag Integer
2 (Lisp [Char] -> Lisp [Char]) -> Lisp [Char] -> Lisp [Char]
forall a b. (a -> b) -> a -> b
$
      [Lisp [Char]] -> Lisp [Char]
forall a. [Lisp a] -> Lisp a
L [ [Char] -> Lisp [Char]
forall a. a -> Lisp a
A [Char]
"agda2-solveAll-action", Lisp [Char] -> Lisp [Char]
forall a. Lisp a -> Lisp a
Q (Lisp [Char] -> Lisp [Char])
-> ([Lisp [Char]] -> Lisp [Char]) -> [Lisp [Char]] -> Lisp [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Lisp [Char]] -> Lisp [Char]
forall a. [Lisp a] -> Lisp a
L ([Lisp [Char]] -> Lisp [Char]) -> [Lisp [Char]] -> Lisp [Char]
forall a b. (a -> b) -> a -> b
$ ((InteractionId, Expr) -> [Lisp [Char]])
-> [(InteractionId, Expr)] -> [Lisp [Char]]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (InteractionId, Expr) -> [Lisp [Char]]
forall {a}. Pretty a => (InteractionId, a) -> [Lisp [Char]]
prn [(InteractionId, Expr)]
ps ]
  ]
  where
    prn :: (InteractionId, a) -> [Lisp [Char]]
prn (InteractionId
ii,a
e)= [InteractionId -> Lisp [Char]
showNumIId InteractionId
ii, [Char] -> Lisp [Char]
forall a. a -> Lisp a
A ([Char] -> Lisp [Char]) -> [Char] -> Lisp [Char]
forall a b. (a -> b) -> a -> b
$ [Char] -> [Char]
quote ([Char] -> [Char]) -> [Char] -> [Char]
forall a b. (a -> b) -> a -> b
$ a -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow a
e]

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

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

-- | Format responses of DisplayInfo

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

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

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

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

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

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

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

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


-- | Serializing Info_Error
showInfoError :: Info_Error -> TCM String
showInfoError :: Info_Error -> TCM [Char]
showInfoError (Info_GenericError TCErr
err) = do
  [Char]
e <- TCErr -> TCM [Char]
forall (tcm :: * -> *). MonadTCM tcm => TCErr -> tcm [Char]
prettyError TCErr
err
  [[Char]]
w <- [TCWarning] -> TCM [[Char]]
prettyTCWarnings' ([TCWarning] -> TCM [[Char]])
-> TCMT IO [TCWarning] -> TCM [[Char]]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCErr -> TCMT IO [TCWarning]
getAllWarningsOfTCErr TCErr
err

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

-- | Pretty-prints the context of the given meta-variable.

prettyResponseContext
  :: InteractionId  -- ^ Context of this meta-variable.
  -> Bool           -- ^ Print the elements in reverse order?
  -> [ResponseContextEntry]
  -> TCM Doc
prettyResponseContext :: InteractionId -> Bool -> [ResponseContextEntry] -> TCMT IO Doc
prettyResponseContext InteractionId
ii Bool
rev [ResponseContextEntry]
ctx = InteractionId -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *) a.
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
 MonadTCEnv m, MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
ii (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ do
  Modality
mod   <- (TCEnv -> Modality) -> TCMT IO Modality
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Modality
forall a. LensModality a => a -> Modality
getModality
  Nat -> [([Char], Doc)] -> Doc
align Nat
10 ([([Char], Doc)] -> Doc)
-> ([[([Char], Doc)]] -> [([Char], Doc)])
-> [[([Char], Doc)]]
-> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[([Char], Doc)]] -> [([Char], Doc)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[([Char], Doc)]] -> [([Char], Doc)])
-> ([[([Char], Doc)]] -> [[([Char], Doc)]])
-> [[([Char], Doc)]]
-> [([Char], Doc)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool
-> ([[([Char], Doc)]] -> [[([Char], Doc)]])
-> [[([Char], Doc)]]
-> [[([Char], Doc)]]
forall a. Bool -> (a -> a) -> a -> a
applyWhen Bool
rev [[([Char], Doc)]] -> [[([Char], Doc)]]
forall a. [a] -> [a]
reverse ([[([Char], Doc)]] -> Doc)
-> TCMT IO [[([Char], Doc)]] -> TCMT IO Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
    [ResponseContextEntry]
-> (ResponseContextEntry -> TCMT IO [([Char], Doc)])
-> TCMT IO [[([Char], Doc)]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [ResponseContextEntry]
ctx ((ResponseContextEntry -> TCMT IO [([Char], Doc)])
 -> TCMT IO [[([Char], Doc)]])
-> (ResponseContextEntry -> TCMT IO [([Char], Doc)])
-> TCMT IO [[([Char], Doc)]]
forall a b. (a -> b) -> a -> b
$ \ (ResponseContextEntry Name
n Name
x (Arg ArgInfo
ai Expr
expr) Maybe Expr
letv NameInScope
nis) -> do
      let
        prettyCtxName :: String
        prettyCtxName :: [Char]
prettyCtxName
          | Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
x                 = Name -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow Name
x
          | Name -> NameInScope
forall a. LensInScope a => a -> NameInScope
isInScope Name
n NameInScope -> NameInScope -> Bool
forall a. Eq a => a -> a -> Bool
== NameInScope
InScope = Name -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow Name
n [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Name -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow Name
x
          | Bool
otherwise              = Name -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow Name
x

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

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

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

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


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

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

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