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

import Control.Monad.State hiding (state)
import qualified Data.List as List

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

import Agda.TypeChecking.Errors (prettyError)
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.Interaction.Imports (getAllWarningsOfTCErr)
import Agda.Utils.Impossible (__IMPOSSIBLE__)
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 -> String -> TCM () -> TCM ()
repl (IO () -> TCM ()
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
. (Lisp String -> IO ()) -> [Lisp String] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Lisp String -> IO ()
forall a. Show a => a -> IO ()
print ([Lisp String] -> TCM ())
-> (Response -> TCMT IO [Lisp String]) -> InteractionOutputCallback
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Response -> 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 -> TCMT IO [Lisp String]
lispifyResponse (Resp_HighlightingInfo HighlightingInfo
info RemoveTokenBasedHighlighting
remove HighlightingMethod
method ModuleToSource
modFile) =
  (Lisp String -> [Lisp String] -> [Lisp String]
forall a. a -> [a] -> [a]
:[]) (Lisp String -> [Lisp String])
-> TCMT IO (Lisp String) -> TCMT IO [Lisp String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO (Lisp String) -> TCMT IO (Lisp String)
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)
lispifyResponse (Resp_DisplayInfo DisplayInfo
info) = DisplayInfo -> TCMT IO [Lisp String]
lispifyDisplayInfo DisplayInfo
info
lispifyResponse (Resp_ClearHighlighting TokenBased
tokenBased) =
  [Lisp String] -> TCMT IO [Lisp String]
forall (m :: * -> *) a. Monad m => a -> m a
return [ [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
NotOnlyTokenBased -> []
                 TokenBased
TokenBased        ->
                   [ Lisp String -> Lisp String
forall a. Lisp a -> Lisp a
Q (TokenBased -> Lisp String
lispifyTokenBased TokenBased
tokenBased) ]
         ]
lispifyResponse Response
Resp_DoneAborting = [Lisp String] -> TCMT IO [Lisp String]
forall (m :: * -> *) a. Monad m => a -> m a
return [ [Lisp String] -> Lisp String
forall a. [Lisp a] -> Lisp a
L [ String -> Lisp String
forall a. a -> Lisp a
A String
"agda2-abort-done" ] ]
lispifyResponse Response
Resp_DoneExiting  = [Lisp String] -> TCMT IO [Lisp String]
forall (m :: * -> *) a. Monad m => a -> m a
return [ [Lisp String] -> Lisp String
forall a. [Lisp a] -> Lisp a
L [ String -> Lisp String
forall a. a -> Lisp a
A String
"agda2-exit-done"  ] ]
lispifyResponse Response
Resp_ClearRunningInfo = [Lisp String] -> TCMT IO [Lisp String]
forall (m :: * -> *) a. Monad m => a -> m a
return [ Lisp String
clearRunningInfo ]
lispifyResponse (Resp_RunningInfo Int
n String
s)
  | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
1    = [Lisp String] -> TCMT IO [Lisp String]
forall (m :: * -> *) a. Monad m => a -> m a
return [ String -> Lisp String
displayRunningInfo String
s ]
  | Bool
otherwise = [Lisp String] -> TCMT IO [Lisp String]
forall (m :: * -> *) a. Monad m => a -> m a
return [ [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
s)] ]
lispifyResponse (Resp_Status Status
s)
    = [Lisp String] -> TCMT IO [Lisp String]
forall (m :: * -> *) a. Monad m => a -> m a
return [ [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])
                 ]
             ]
  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"

lispifyResponse (Resp_JumpToError String
f Int32
p) = [Lisp String] -> TCMT IO [Lisp String]
forall (m :: * -> *) a. Monad m => a -> m a
return
  [ 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 (Int32 -> String
forall a. Show a => a -> String
show Int32
p)] ]
  ]
lispifyResponse (Resp_InteractionPoints [InteractionId]
is) = [Lisp String] -> TCMT IO [Lisp String]
forall (m :: * -> *) a. Monad m => a -> m a
return
  [ 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]
  ]
lispifyResponse (Resp_GiveAction InteractionId
ii GiveResult
s)
    = [Lisp String] -> TCMT IO [Lisp String]
forall (m :: * -> *) a. Monad m => a -> m a
return [ [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"
lispifyResponse (Resp_MakeCase InteractionId
ii MakeCaseVariant
variant [String]
pcs) = [Lisp String] -> TCMT IO [Lisp String]
forall (m :: * -> *) a. Monad m => a -> m a
return
  [ 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"
lispifyResponse (Resp_SolveAll [(InteractionId, Expr)]
ps) = [Lisp String] -> TCMT IO [Lisp String]
forall (m :: * -> *) a. Monad m => a -> m a
return
  [ 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) -> [Lisp String] -> Lisp String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [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]

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

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

-- | Format responses of DisplayInfo

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

-- | 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
. Int -> String
forall a. Show a => a -> String
show (Int -> String)
-> (InteractionId -> Int) -> InteractionId -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InteractionId -> Int
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 :: String -> String -> String -> (String, String)
formatWarningsAndErrors String
g String
w String
e = (String
body, String
title)
  where
    isG :: Bool
isG = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
g
    isW :: Bool
isW = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
w
    isE :: Bool
isE = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
e
    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
$ [Maybe String] -> [String]
forall a. [Maybe a] -> [a]
catMaybes
              [ String
" Goals"    String -> Maybe () -> Maybe String
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard Bool
isG
              , String
" Errors"   String -> Maybe () -> Maybe String
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard Bool
isE
              , String
" Warnings" String -> Maybe () -> Maybe String
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard Bool
isW
              , String
" Done"     String -> Maybe () -> Maybe String
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 :: String
body = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
List.intercalate String
"\n" ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [Maybe String] -> [String]
forall a. [Maybe a] -> [a]
catMaybes
             [ String
g                    String -> Maybe () -> Maybe String
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard Bool
isG
             , String -> String
delimiter String
"Errors"   String -> Maybe () -> Maybe String
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))
             , String
e                    String -> Maybe () -> Maybe String
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard Bool
isE
             , String -> String
delimiter String
"Warnings" String -> Maybe () -> Maybe String
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))
             , String
w                    String -> Maybe () -> Maybe String
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 String
showInfoError (Info_GenericError TCErr
err) = do
  String
e <- TCErr -> TCM String
forall (tcm :: * -> *). MonadTCM tcm => TCErr -> tcm String
prettyError TCErr
err
  [String]
w <- [TCWarning] -> TCM [String]
prettyTCWarnings' ([TCWarning] -> TCM [String])
-> TCMT IO [TCWarning] -> TCM [String]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCErr -> TCMT IO [TCWarning]
getAllWarningsOfTCErr TCErr
err

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

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

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

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

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


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

prettyResponseContext
  :: InteractionId  -- ^ Context of this meta-variable.
  -> Bool           -- ^ Print the elements in reverse order?
  -> [ResponseContextEntry]
  -> TCM Doc
prettyResponseContext :: InteractionId -> Bool -> [ResponseContextEntry] -> TCM Doc
prettyResponseContext InteractionId
ii Bool
rev [ResponseContextEntry]
ctx = InteractionId -> TCM Doc -> TCM Doc
forall a. InteractionId -> TCM a -> TCM a
withInteractionId InteractionId
ii (TCM Doc -> TCM Doc) -> TCM Doc -> TCM 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
  Int -> [(String, Doc)] -> Doc
align Int
10 ([(String, Doc)] -> Doc)
-> ([[(String, Doc)]] -> [(String, Doc)])
-> [[(String, Doc)]]
-> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[(String, Doc)]] -> [(String, Doc)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[(String, Doc)]] -> [(String, Doc)])
-> ([[(String, Doc)]] -> [[(String, Doc)]])
-> [[(String, Doc)]]
-> [(String, Doc)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool
-> ([[(String, Doc)]] -> [[(String, Doc)]])
-> [[(String, Doc)]]
-> [[(String, Doc)]]
forall a. Bool -> (a -> a) -> a -> a
applyWhen Bool
rev [[(String, Doc)]] -> [[(String, Doc)]]
forall a. [a] -> [a]
reverse ([[(String, Doc)]] -> Doc) -> TCMT IO [[(String, Doc)]] -> TCM Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
    [ResponseContextEntry]
-> (ResponseContextEntry -> TCMT IO [(String, Doc)])
-> TCMT IO [[(String, Doc)]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [ResponseContextEntry]
ctx ((ResponseContextEntry -> TCMT IO [(String, Doc)])
 -> TCMT IO [[(String, Doc)]])
-> (ResponseContextEntry -> TCMT IO [(String, Doc)])
-> TCMT IO [[(String, 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 :: 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 (t :: * -> *) a. Foldable t => t 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)

        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 -> TCM Doc
forall c a (m :: * -> *).
(Pretty c, ToConcrete a c, MonadAbsToCon m) =>
a -> m Doc
prettyATop Expr
expr
      Maybe Doc
maybeVal <- (Expr -> TCM Doc) -> Maybe Expr -> TCMT IO (Maybe Doc)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Expr -> TCM Doc
forall c a (m :: * -> *).
(Pretty c, ToConcrete a c, MonadAbsToCon m) =>
a -> m Doc
prettyATop Maybe Expr
letv

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

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


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

prettyTypeOfMeta :: Rewrite -> InteractionId -> TCM Doc
prettyTypeOfMeta :: Rewrite -> InteractionId -> TCM 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 -> TCM Doc
forall c a (m :: * -> *).
(Pretty c, ToConcrete a c, MonadAbsToCon m) =>
a -> m Doc
prettyATop Expr
e
    OutputConstraint Expr InteractionId
_            -> OutputConstraint Expr InteractionId -> TCM Doc
forall c a (m :: * -> *).
(Pretty c, ToConcrete a c, 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