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 (forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ([Char] -> IO ()
putStrLn forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Pretty a => a -> [Char]
prettyShow) forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Response -> TCM [Lisp [Char]]
lispifyResponse) [Char]
"Agda2> "

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

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

lispifyResponse (Resp_JumpToError [Char]
f Int32
p) = forall (m :: * -> *) a. Monad m => a -> m a
return
  [ Integer -> Lisp [Char] -> Lisp [Char]
lastTag Integer
3 forall a b. (a -> b) -> a -> b
$
      forall a. [Lisp a] -> Lisp a
L [ forall a. a -> Lisp a
A [Char]
"agda2-maybe-goto", forall a. Lisp a -> Lisp a
Q forall a b. (a -> b) -> a -> b
$ forall a. [Lisp a] -> Lisp a
L [forall a. a -> Lisp a
A ([Char] -> [Char]
quote [Char]
f), forall a. a -> Lisp a
A [Char]
".", forall a. a -> Lisp a
A (forall a. Show a => a -> [Char]
show Int32
p)] ]
  ]
lispifyResponse (Resp_InteractionPoints [InteractionId]
is) = forall (m :: * -> *) a. Monad m => a -> m a
return
  [ Integer -> Lisp [Char] -> Lisp [Char]
lastTag Integer
1 forall a b. (a -> b) -> a -> b
$
      forall a. [Lisp a] -> Lisp a
L [forall a. a -> Lisp a
A [Char]
"agda2-goals-action", forall a. Lisp a -> Lisp a
Q forall a b. (a -> b) -> a -> b
$ forall a. [Lisp a] -> Lisp a
L forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map InteractionId -> Lisp [Char]
showNumIId [InteractionId]
is]
  ]
lispifyResponse (Resp_GiveAction InteractionId
ii GiveResult
s)
    = forall (m :: * -> *) a. Monad m => a -> m a
return [ forall a. [Lisp a] -> Lisp a
L [ forall a. a -> Lisp a
A [Char]
"agda2-give-action", InteractionId -> Lisp [Char]
showNumIId InteractionId
ii, 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) = forall (m :: * -> *) a. Monad m => a -> m a
return
  [ Integer -> Lisp [Char] -> Lisp [Char]
lastTag Integer
2 forall a b. (a -> b) -> a -> b
$ forall a. [Lisp a] -> Lisp a
L [ forall a. a -> Lisp a
A [Char]
cmd, forall a. Lisp a -> Lisp a
Q forall a b. (a -> b) -> a -> b
$ forall a. [Lisp a] -> Lisp a
L forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall a. a -> Lisp a
A 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) = forall (m :: * -> *) a. Monad m => a -> m a
return
  [ Integer -> Lisp [Char] -> Lisp [Char]
lastTag Integer
2 forall a b. (a -> b) -> a -> b
$
      forall a. [Lisp a] -> Lisp a
L [ forall a. a -> Lisp a
A [Char]
"agda2-solveAll-action", forall a. Lisp a -> Lisp a
Q forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [Lisp a] -> Lisp a
L forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap 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, forall a. a -> Lisp a
A forall a b. (a -> b) -> a -> b
$ [Char] -> [Char]
quote forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> [Char]
prettyShow a
e]

lispifyDisplayInfo :: DisplayInfo -> TCM [Lisp String]
lispifyDisplayInfo :: DisplayInfo -> TCM [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 = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
          [ [Char]
"The module was successfully compiled with backend "
          , 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] -> TCM [Lisp [Char]]
format [Char]
body [Char]
"*Compilation result*"
    Info_Constraints [OutputForm Expr Expr]
s -> do
      Doc
doc <- forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
TCP.vcat forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [OutputForm Expr Expr]
s
      [Char] -> [Char] -> TCM [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] -> TCM [Lisp [Char]]
format [Char]
body ([Char]
"*All" forall a. [a] -> [a] -> [a]
++ [Char]
title forall a. [a] -> [a] -> [a]
++ [Char]
"*")
    Info_Auto [Char]
s -> [Char] -> [Char] -> TCM [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] -> TCM [Lisp [Char]]
format [Char]
s [Char]
"*Error*"
    Info_Time CPUTime
s -> [Char] -> [Char] -> TCM [Lisp [Char]]
format (Doc -> [Char]
render 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 <- forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT CommandM Doc
prettyExpr CommandState
state
      let doc :: Doc
doc = forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. Null a => a
empty CPUTime -> Doc
prettyTimed Maybe CPUTime
time Doc -> Doc -> Doc
$$ Doc
exprDoc
          lbl :: [Char]
lbl | ComputeMode
cmode forall a. Eq a => a -> a -> Bool
== ComputeMode
HeadCompute = [Char]
"*Head Normal Form*"
              | Bool
otherwise            = [Char]
"*Normal Form*"
      [Char] -> [Char] -> TCM [Lisp [Char]]
format (Doc -> [Char]
render Doc
doc) [Char]
lbl
      where
        prettyExpr :: CommandM Doc
prettyExpr = forall a. CommandM a -> CommandM a
localStateCommandM
            forall a b. (a -> b) -> a -> b
$ forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift
            forall a b. (a -> b) -> a -> b
$ forall a. TCM a -> TCM a
B.atTopLevel
            forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
allowNonTerminatingReductions
            forall a b. (a -> b) -> a -> b
$ (if ComputeMode -> Bool
computeIgnoreAbstract ComputeMode
cmode then forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
ignoreAbstractMode else forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
inConcreteMode)
            forall a b. (a -> b) -> a -> b
$ (ComputeMode -> Expr -> TCMT IO Doc
B.showComputed ComputeMode
cmode)
            forall a b. (a -> b) -> a -> b
$ Expr
expr
    Info_InferredType CommandState
state Maybe CPUTime
time Expr
expr -> do
      Doc
exprDoc <- forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT CommandM Doc
prettyExpr CommandState
state
      let doc :: Doc
doc = forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. Null a => a
empty CPUTime -> Doc
prettyTimed Maybe CPUTime
time Doc -> Doc -> Doc
$$ Doc
exprDoc
      [Char] -> [Char] -> TCM [Lisp [Char]]
format (Doc -> [Char]
render Doc
doc) [Char]
"*Inferred Type*"
      where
        prettyExpr :: CommandM Doc
prettyExpr = forall a. CommandM a -> CommandM a
localStateCommandM
            forall a b. (a -> b) -> a -> b
$ forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift
            forall a b. (a -> b) -> a -> b
$ forall a. TCM a -> TCM a
B.atTopLevel
            forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
TCP.prettyA
            forall a b. (a -> b) -> a -> b
$ Expr
expr
    Info_ModuleContents [Name]
modules Telescope
tel [(Name, Type)]
types -> do
      Doc
doc <- forall a. TCM a -> TCM a
localTCState forall a b. (a -> b) -> a -> b
$ do
        [([Char], Doc)]
typeDocs <- forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Name, Type)]
types forall a b. (a -> b) -> a -> b
$ \ (Name
x, Type
t) -> do
          Doc
doc <- forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
          forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Pretty a => a -> [Char]
prettyShow Name
x, Doc
":" Doc -> Doc -> Doc
<+> Doc
doc)
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat
          [ Doc
"Modules"
          , Nat -> Doc -> Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. Pretty a => a -> Doc
pretty [Name]
modules
          , Doc
"Names"
          , Nat -> Doc -> Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ Nat -> [([Char], Doc)] -> Doc
align Nat
10 [([Char], Doc)]
typeDocs
          ]
      [Char] -> [Char] -> TCM [Lisp [Char]]
format (Doc -> [Char]
render Doc
doc) [Char]
"*Module contents*"
    Info_SearchAbout [(Name, Type)]
hits [Char]
names -> do
      [([Char], Doc)]
hitDocs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Name, Type)]
hits forall a b. (a -> b) -> a -> b
$ \ (Name
x, Type
t) -> do
        Doc
doc <- forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
        forall (m :: * -> *) a. Monad m => a -> m a
return (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 (forall a. [a] -> [[a]] -> [a]
List.intercalate [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] -> TCM [Lisp [Char]]
format (Doc -> [Char]
render Doc
doc) [Char]
"*Search About*"
    Info_WhyInScope WhyInScopeData
why -> do
      Doc
doc <- forall (m :: * -> *). MonadPretty m => WhyInScopeData -> m Doc
explainWhyInScope WhyInScopeData
why
      [Char] -> [Char] -> TCM [Lisp [Char]]
format (Doc -> [Char]
render Doc
doc) [Char]
"*Scope Info*"
    Info_Context InteractionId
ii [ResponseContextEntry]
ctx -> do
      Doc
doc <- forall a. TCM a -> TCM a
localTCState (InteractionId -> Bool -> [ResponseContextEntry] -> TCMT IO Doc
prettyResponseContext InteractionId
ii Bool
False [ResponseContextEntry]
ctx)
      [Char] -> [Char] -> TCM [Lisp [Char]]
format (Doc -> [Char]
render Doc
doc) [Char]
"*Context*"
    DisplayInfo
Info_Intro_NotFound -> [Char] -> [Char] -> TCM [Lisp [Char]]
format [Char]
"No introduction forms found." [Char]
"*Intro*"
    Info_Intro_ConstructorUnknown [[Char]]
ss -> do
      let 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 forall a. a -> [a] -> [a]
: [[Char]] -> [Doc]
mkOr [[Char]]
xs
                      in Nat -> Doc -> Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *). Foldable t => Doc -> t Doc -> [Doc]
punctuate Doc
comma ([[Char]] -> [Doc]
mkOr [[Char]]
ss)
                    ]
      [Char] -> [Char] -> TCM [Lisp [Char]]
format (Doc -> [Char]
render Doc
doc) [Char]
"*Intro*"
    DisplayInfo
Info_Version -> [Char] -> [Char] -> TCM [Lisp [Char]]
format ([Char]
"Agda version " forall a. [a] -> [a] -> [a]
++ [Char]
versionWithCommitInfo) [Char]
"*Agda Version*"
    Info_GoalSpecific InteractionId
ii GoalDisplayInfo
kind -> InteractionId -> GoalDisplayInfo -> TCM [Lisp [Char]]
lispifyGoalSpecificDisplayInfo InteractionId
ii GoalDisplayInfo
kind

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

-- | Format responses of DisplayInfo

format :: String -> String -> TCM [Lisp String]
format :: [Char] -> [Char] -> TCM [Lisp [Char]]
format [Char]
content [Char]
bufname = 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 = forall a. Lisp a -> Lisp a -> Lisp a
Cons (forall a. Lisp a -> Lisp a -> Lisp a
Cons (forall a. a -> Lisp a
A [Char]
"last") (forall a. a -> Lisp a
A forall a b. (a -> b) -> a -> b
$ 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 = forall a. a -> Lisp a
A forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> [Char]
show 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 forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Char]
g
    isW :: Bool
isW = Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Char]
w
    isE :: Bool
isE = Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Char]
e
    title :: [Char]
title = forall a. [a] -> [[a]] -> [a]
List.intercalate [Char]
"," forall a b. (a -> b) -> a -> b
$ forall a. [Maybe a] -> [a]
catMaybes
              [ [Char]
" Goals"    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (f :: * -> *). Alternative f => Bool -> f ()
guard Bool
isG
              , [Char]
" Errors"   forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (f :: * -> *). Alternative f => Bool -> f ()
guard Bool
isE
              , [Char]
" Warnings" forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (f :: * -> *). Alternative f => Bool -> f ()
guard Bool
isW
              , [Char]
" Done"     forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ 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 = forall a. [a] -> [[a]] -> [a]
List.intercalate [Char]
"\n" forall a b. (a -> b) -> a -> b
$ forall a. [Maybe a] -> [a]
catMaybes
             [ [Char]
g                    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (f :: * -> *). Alternative f => Bool -> f ()
guard Bool
isG
             , [Char] -> [Char]
delimiter [Char]
"Errors"   forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool
isE Bool -> Bool -> Bool
&& (Bool
isG Bool -> Bool -> Bool
|| Bool
isW))
             , [Char]
e                    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (f :: * -> *). Alternative f => Bool -> f ()
guard Bool
isE
             , [Char] -> [Char]
delimiter [Char]
"Warnings" forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool
isW Bool -> Bool -> Bool
&& (Bool
isG Bool -> Bool -> Bool
|| Bool
isE))
             , [Char]
w                    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ 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 <- forall (tcm :: * -> *). MonadTCM tcm => TCErr -> tcm [Char]
prettyError TCErr
err
  [[Char]]
w <- [TCWarning] -> TCMT IO [[Char]]
prettyTCWarnings' forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCErr -> TCM [TCWarning]
getAllWarningsOfTCErr TCErr
err

  let errorMsg :: [Char]
errorMsg  = if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [[Char]]
w
                      then [Char]
e
                      else [Char] -> [Char]
delimiter [Char]
"Error" forall a. [a] -> [a] -> [a]
++ [Char]
"\n" forall a. [a] -> [a] -> [a]
++ [Char]
e
  let warningMsg :: [Char]
warningMsg = forall a. [a] -> [[a]] -> [a]
List.intercalate [Char]
"\n" forall a b. (a -> b) -> a -> b
$ [Char] -> [Char]
delimiter [Char]
"Warning(s)"
                                      forall a. a -> [a] -> [a]
: forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> Bool
null) [[Char]]
w
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [[Char]]
w
            then [Char]
errorMsg
            else [Char]
errorMsg forall a. [a] -> [a] -> [a]
++ [Char]
"\n\n" forall a. [a] -> [a] -> [a]
++ [Char]
warningMsg
showInfoError (Info_CompilationError [TCWarning]
warnings) = do
  [Char]
s <- [TCWarning] -> TCM [Char]
prettyTCWarnings [TCWarning]
warnings
  forall (m :: * -> *) a. Monad m => a -> m a
return 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) =
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Char]
"Highlighting failed to parse expression in " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show InteractionId
ii
showInfoError (Info_HighlightingScopeCheckError InteractionId
ii) =
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Char]
"Highlighting failed to scope check expression in " forall a. [a] -> [a] -> [a]
++ 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 = forall (m :: * -> *) a.
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
 MonadTCEnv m, MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
ii forall a b. (a -> b) -> a -> b
$ do
  Modality
mod   <- forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC forall a. LensModality a => a -> Modality
getModality
  Nat -> [([Char], Doc)] -> Doc
align Nat
10 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Bool -> (a -> a) -> a -> a
applyWhen Bool
rev forall a. [a] -> [a]
reverse forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
    forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [ResponseContextEntry]
ctx 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 forall a. Eq a => a -> a -> Bool
== Name
x                 = forall a. Pretty a => a -> [Char]
prettyShow Name
x
          | forall a. LensInScope a => a -> NameInScope
isInScope Name
n forall a. Eq a => a -> a -> Bool
== NameInScope
InScope = forall a. Pretty a => a -> [Char]
prettyShow Name
n forall a. [a] -> [a] -> [a]
++ [Char]
" = " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow Name
x
          | Bool
otherwise              = 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 forall a. [a] -> [a] -> [a]
++ if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Char]
c then [Char]
"" else [Char]
" "
          where c :: [Char]
c = forall a. Pretty a => a -> [Char]
prettyShow (forall a. LensCohesion a => a -> Cohesion
getCohesion ArgInfo
ai)

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

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

  where
    parenSep :: [Doc] -> Doc
    parenSep :: [Doc] -> Doc
parenSep [Doc]
docs
      | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Doc]
docs = forall a. Null a => a
empty
      | Bool
otherwise = (Doc
" " Doc -> Doc -> Doc
<+>) forall a b. (a -> b) -> a -> b
$ Doc -> Doc
parens forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep forall a b. (a -> b) -> a -> b
$ 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 -> forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyATop Expr
e
    OutputConstraint Expr InteractionId
_            -> 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
<+> forall a. Pretty a => a -> Doc
pretty CPUTime
time