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) "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 info :: HighlightingInfo
info remove :: RemoveTokenBasedHighlighting
remove method :: HighlightingMethod
method modFile :: 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 info :: DisplayInfo
info) = DisplayInfo -> TCMT IO [Lisp String]
lispifyDisplayInfo DisplayInfo
info
lispifyResponse (Resp_ClearHighlighting tokenBased :: 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 "agda2-highlight-clear" Lisp String -> [Lisp String] -> [Lisp String]
forall a. a -> [a] -> [a]
:
               case TokenBased
tokenBased of
                 NotOnlyTokenBased -> []
                 TokenBased        ->
                   [ Lisp String -> Lisp String
forall a. Lisp a -> Lisp a
Q (TokenBased -> Lisp String
lispifyTokenBased TokenBased
tokenBased) ]
         ]
lispifyResponse 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 "agda2-abort-done" ] ]
lispifyResponse 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 "agda2-exit-done"  ] ]
lispifyResponse Resp_ClearRunningInfo = [Lisp String] -> TCMT IO [Lisp String]
forall (m :: * -> *) a. Monad m => a -> m a
return [ Lisp String
clearRunningInfo ]
lispifyResponse (Resp_RunningInfo n :: Int
n s :: String
s)
  | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= 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 "agda2-verbose", String -> Lisp String
forall a. a -> Lisp a
A (String -> String
quote String
s)] ]
lispifyResponse (Resp_Status s :: 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 "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
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) "Checked"
    showImpl :: Maybe String
showImpl = Bool -> String -> Maybe String
forall a. Bool -> a -> Maybe a
boolToMaybe (Status -> Bool
sShowImplicitArguments Status
s) "ShowImplicit"

lispifyResponse (Resp_JumpToError f :: String
f p :: Int32
p) = [Lisp String] -> TCMT IO [Lisp String]
forall (m :: * -> *) a. Monad m => a -> m a
return
  [ Integer -> Lisp String -> Lisp String
lastTag 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 "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 -> Lisp String
forall a. a -> Lisp a
A (Int32 -> String
forall a. Show a => a -> String
show Int32
p)] ]
  ]
lispifyResponse (Resp_InteractionPoints is :: [InteractionId]
is) = [Lisp String] -> TCMT IO [Lisp String]
forall (m :: * -> *) a. Monad m => a -> m a
return
  [ Integer -> Lisp String -> Lisp String
lastTag 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 "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 ii :: InteractionId
ii s :: 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 "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 str :: String
str -> String -> String
quote String
str
        Give_Paren      -> "'paren"
        Give_NoParen    -> "'no-paren"
lispifyResponse (Resp_MakeCase ii :: InteractionId
ii variant :: MakeCaseVariant
variant pcs :: [String]
pcs) = [Lisp String] -> TCMT IO [Lisp String]
forall (m :: * -> *) a. Monad m => a -> m a
return
  [ Integer -> Lisp String -> Lisp String
lastTag 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
    R.Function       -> "agda2-make-case-action"
    R.ExtendedLambda -> "agda2-make-case-action-extendlam"
lispifyResponse (Resp_SolveAll ps :: [(InteractionId, Expr)]
ps) = [Lisp String] -> TCMT IO [Lisp String]
forall (m :: * -> *) a. Monad m => a -> m a
return
  [ Integer -> Lisp String -> Lisp String
lastTag 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 "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 (ii :: InteractionId
ii,e :: 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 info :: DisplayInfo
info = case DisplayInfo
info of
    Info_CompilationOk ws :: 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 (body :: String
body, _) = String -> String -> String -> (String, String)
formatWarningsAndErrors
                        "The module was successfully compiled.\n"
                        String
warnings
                        String
errors
      String -> String -> TCMT IO [Lisp String]
format String
body "*Compilation result*"
    Info_Constraints s :: [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) "*Constraints*"
    Info_AllGoalsWarnings ms :: Goals
ms ws :: 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 (body :: String
body, title :: String
title) = String -> String -> String -> (String, String)
formatWarningsAndErrors String
goals String
warnings String
errors
      String -> String -> TCMT IO [Lisp String]
format String
body ("*All" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
title String -> String -> String
forall a. [a] -> [a] -> [a]
++ "*")
    Info_Auto s :: String
s -> String -> String -> TCMT IO [Lisp String]
format String
s "*Auto*"
    Info_Error err :: Info_Error
err -> do
      String
s <- Info_Error -> TCM String
showInfoError Info_Error
err
      String -> String -> TCMT IO [Lisp String]
format String
s "*Error*"
    Info_Time s :: 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) "*Time*"
    Info_NormalForm state :: CommandState
state cmode :: ComputeMode
cmode time :: Maybe CPUTime
time expr :: 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) "*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 state :: CommandState
state time :: Maybe CPUTime
time expr :: 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) "*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 modules :: [Name]
modules tel :: Telescope
tel types :: [(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
$ \ (x :: Name
x, t :: 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 -> 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
          [ "Modules"
          , Int -> Doc -> Doc
nest 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
          , "Names"
          , Int -> Doc -> Doc
nest 2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Int -> [(String, Doc)] -> Doc
align 10 [(String, Doc)]
typeDocs
          ]
      String -> String -> TCMT IO [Lisp String]
format (Doc -> String
render Doc
doc) "*Module contents*"
    Info_SearchAbout hits :: [(Name, Type)]
hits names :: 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
$ \ (x :: Name
x, t :: 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)
      let 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
forall a b. (a -> b) -> a -> b
$ String -> [String]
words String
names) Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
nest 2 (Int -> [(String, Doc)] -> Doc
align 10 [(String, Doc)]
hitDocs)
      String -> String -> TCMT IO [Lisp String]
format (Doc -> String
render Doc
doc) "*Search About*"
    Info_WhyInScope s :: String
s cwd :: String
cwd v :: Maybe LocalVar
v xs :: [AbstractName]
xs ms :: [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) "*Scope Info*"
    Info_Context ii :: InteractionId
ii ctx :: [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) "*Context*"
    Info_Intro_NotFound -> String -> String -> TCMT IO [Lisp String]
format "No introduction forms found." "*Intro*"
    Info_Intro_ConstructorUnknown ss :: [String]
ss -> do
      let doc :: Doc
doc = [Doc] -> Doc
sep [ "Don't know which constructor to introduce of"
                    , let mkOr :: [String] -> [Doc]
mkOr []     = []
                          mkOr [x :: String
x, y :: String
y] = [String -> Doc
text String
x Doc -> Doc -> Doc
<+> "or" Doc -> Doc -> Doc
<+> String -> Doc
text String
y]
                          mkOr (x :: String
x:xs :: [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 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) "*Intro*"
    Info_Version -> String -> String -> TCMT IO [Lisp String]
format ("Agda version " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
versionWithCommitInfo) "*Agda Version*"
    Info_GoalSpecific ii :: InteractionId
ii kind :: 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 ii :: InteractionId
ii kind :: 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 helperType :: 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 "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 "*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]
++ "\n")
                 , String -> Lisp String
forall a. a -> Lisp a
A "nil"
                 ]
             ]
    Goal_NormalForm cmode :: ComputeMode
cmode expr :: 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) "*Normal Form*"   -- show?
    Goal_GoalType norm :: Rewrite
norm aux :: GoalTypeAux
aux ctx :: [ResponseContextEntry]
ctx bndry :: [IPBoundary' Expr]
bndry constraints :: [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
            GoalOnly -> Doc -> TCM Doc
forall (m :: * -> *) a. Monad m => a -> m a
return Doc
forall a. Null a => a
empty
            GoalAndHave expr :: 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
$ "Have:" Doc -> Doc -> Doc
<+> Doc
doc
            GoalAndElaboration term :: 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
$ "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 "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 "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
$
            [ "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 60 '\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) "*Goal type etc.*"
    Goal_CurrentGoal norm :: 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) "*Current Goal*"
    Goal_InferredType expr :: 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) "*Inferred Type*"

-- | Format responses of DisplayInfo

format :: String -> String -> TCM [Lisp String]
format :: String -> String -> TCMT IO [Lisp String]
format content :: String
content bufname :: 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 n :: Integer
n r :: 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 "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 g :: String
g w :: String
w e :: 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
forall a b. (a -> b) -> a -> b
$ [Maybe String] -> [String]
forall a. [Maybe a] -> [a]
catMaybes
              [ " 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
              , " 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
              , " 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
              , " 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 "\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 "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 "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 err :: 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 "Error" String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\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 "\n" ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ String -> String
delimiter "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]
++ "\n\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
warningMsg
showInfoError (Info_CompilationError warnings :: [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
            [ "You need to fix the following errors before you can compile"
            , "the module:"
            , ""
            , String
s
            ]
showInfoError (Info_HighlightingParseError ii :: 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
$ "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 ii :: 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
$ "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 s :: String
s _ Nothing [] [] = String -> TCM Doc
forall (m :: * -> *). Monad m => String -> m Doc
TCP.text (String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ " is not in scope.")
explainWhyInScope s :: String
s _ v :: Maybe LocalVar
v xs :: [AbstractName]
xs ms :: [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]
++ " is in scope as")
  , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
TCP.nest 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 Nothing vs :: [AbstractName]
vs = [AbstractName] -> TCM Doc
names [AbstractName]
vs
    variable (Just x :: LocalVar
x) vs :: [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 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 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
          "* 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 _ _ [])    = "shadowing"
        shadowing _ = "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
      ConName                  -> "constructor"
      FldName                  -> "record field"
      PatternSynName           -> "pattern synonym"
      GeneralizeName           -> "generalizable variable"
      DisallowedGeneralizeName -> "generalizable variable from let open"
      MacroName                -> "macro name"
      QuotableName             -> "quotable name"
      -- previously DefName:
      DataName                 -> "data type"
      RecName                  -> "record type"
      AxiomName                -> "postulate"
      PrimName                 -> "primitive function"
      FunName                  -> "defined name"
      OtherDefName             -> "defined name"

    pName :: AbstractName -> TCM Doc
    pName :: AbstractName -> TCM Doc
pName a :: AbstractName
a = [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
TCP.sep
      [ "* 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 2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ "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 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  a :: AbstractModule
a = [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
TCP.sep
      [ "* 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 2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ "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 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 r :: Range
r Defined = "- 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 r :: Range
r (Opened (C.QName x :: Name
x) w :: WhyInScope
w) | Name -> Bool
forall a. IsNoName a => a -> Bool
isNoName Name
x = Range -> WhyInScope -> TCM Doc
pWhy Range
r WhyInScope
w
    pWhy r :: Range
r (Opened m :: QName
m w :: WhyInScope
w) =
      "- 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.<+> "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 r :: Range
r (Applied m :: QName
m w :: WhyInScope
w) =
      "- 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.<+> "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 ii :: InteractionId
ii rev :: Bool
rev ctx :: [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 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 n :: Name
n x :: Name
x (Arg ai :: ArgInfo
ai expr :: Expr
expr) letv :: Maybe Expr
letv nis :: 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
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 "" else " "
          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
$
          [ [ "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.
          , [ "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.
          , [ "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
          , [ "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
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
val) | Doc
val <- Maybe Doc -> [Doc]
forall a. Maybe a -> [a]
maybeToList Maybe Doc
maybeVal ]

  where
    parenSep :: [Doc] -> Doc
    parenSep :: [Doc] -> Doc
parenSep docs :: [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
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 norm :: Rewrite
norm ii :: 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 _ e :: 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 -> 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 time :: CPUTime
time = "Time:" Doc -> Doc -> Doc
<+> CPUTime -> Doc
forall a. Pretty a => a -> Doc
pretty CPUTime
time