{-# LANGUAGE CPP #-}

module Agda.Convert where

import Render ( Block(..), Inlines, renderATop, Render(..) )

import Agda.IR (FromAgda (..))
import qualified Agda.IR as IR
import Agda.Interaction.Base
import Agda.Interaction.BasicOps as B
import Agda.Interaction.EmacsCommand (Lisp)
import Agda.Interaction.Highlighting.Common (chooseHighlightingMethod, toAtoms)
import Agda.Interaction.Highlighting.Precise (Aspects (..), DefinitionSite (..), HighlightingInfo, TokenBased (..))
import qualified Agda.Interaction.Highlighting.Range as Highlighting
import Agda.Interaction.InteractionTop (localStateCommandM)
import Agda.Interaction.Response as R
import Agda.Syntax.Abstract as A
import Agda.Syntax.Abstract.Pretty (prettyATop)
import Agda.Syntax.Common
import Agda.Syntax.Concrete as C
import Agda.Syntax.Internal (alwaysUnblock)
import Agda.Syntax.Position (HasRange (getRange), Range, noRange)
import Agda.Syntax.Scope.Base
import Agda.TypeChecking.Errors (getAllWarningsOfTCErr, prettyError)
import Agda.TypeChecking.Monad hiding (Function)
import Agda.TypeChecking.Monad.MetaVars (withInteractionId)
import Agda.TypeChecking.Pretty (prettyTCM)
import qualified Agda.TypeChecking.Pretty as TCP
import Agda.TypeChecking.Pretty.Warning (filterTCWarnings, prettyTCWarnings, prettyTCWarnings')
import Agda.TypeChecking.Warnings (WarningsAndNonFatalErrors (..))
import Agda.Utils.FileName (filePath)
import Agda.Utils.Function (applyWhen)
import Agda.Utils.IO.TempFile (writeToTempFile)
import Agda.Utils.Impossible (__IMPOSSIBLE__)
import Agda.Utils.Maybe (catMaybes)
import Agda.Utils.Null (empty)
import Agda.Utils.Pretty hiding (render)
import Agda.Utils.RangeMap ( IsBasicRangeMap(toList) )
import Agda.Utils.String (delimiter)
import Agda.Utils.Time (CPUTime)
import Agda.VersionCommit (versionWithCommitInfo)
import Control.Monad
import Control.Monad.State hiding (state)
import qualified Data.Aeson as JSON
import qualified Data.ByteString.Lazy.Char8 as BS8
import qualified Data.List as List
import qualified Data.Map as Map
import Data.String (IsString)
import qualified Render

responseAbbr :: IsString a => Response -> a
responseAbbr :: forall a. IsString a => Response -> a
responseAbbr Response
res = case Response
res of
  Resp_HighlightingInfo {} -> a
"Resp_HighlightingInfo"
  Resp_Status {} -> a
"Resp_Status"
  Resp_JumpToError {} -> a
"Resp_JumpToError"
  Resp_InteractionPoints {} -> a
"Resp_InteractionPoints"
  Resp_GiveAction {} -> a
"Resp_GiveAction"
  Resp_MakeCase {} -> a
"Resp_MakeCase"
  Resp_SolveAll {} -> a
"Resp_SolveAll"
  Resp_DisplayInfo {} -> a
"Resp_DisplayInfo"
  Resp_RunningInfo {} -> a
"Resp_RunningInfo"
  Resp_ClearRunningInfo {} -> a
"Resp_ClearRunningInfo"
  Resp_ClearHighlighting {} -> a
"Resp_ClearHighlighting"
  Resp_DoneAborting {} -> a
"Resp_DoneAborting"
  Resp_DoneExiting {} -> a
"Resp_DoneExiting"

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

serialize :: Lisp String -> String
serialize :: Lisp [Char] -> [Char]
serialize = Doc -> [Char]
forall a. Show a => a -> [Char]
show (Doc -> [Char]) -> (Lisp [Char] -> Doc) -> Lisp [Char] -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lisp [Char] -> Doc
forall a. Pretty a => a -> Doc
pretty

fromResponse :: Response -> TCM IR.Response
fromResponse :: Response -> TCM Response
fromResponse (Resp_HighlightingInfo HighlightingInfo
info RemoveTokenBasedHighlighting
remove HighlightingMethod
method ModuleToSource
modFile) =
  HighlightingInfo
-> RemoveTokenBasedHighlighting
-> HighlightingMethod
-> ModuleToSource
-> TCM Response
fromHighlightingInfo HighlightingInfo
info RemoveTokenBasedHighlighting
remove HighlightingMethod
method ModuleToSource
modFile
fromResponse (Resp_DisplayInfo DisplayInfo
info) = DisplayInfo -> Response
IR.ResponseDisplayInfo (DisplayInfo -> Response) -> TCMT IO DisplayInfo -> TCM Response
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DisplayInfo -> TCMT IO DisplayInfo
fromDisplayInfo DisplayInfo
info
fromResponse (Resp_ClearHighlighting TokenBased
TokenBased) = Response -> TCM Response
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Response
IR.ResponseClearHighlightingTokenBased
fromResponse (Resp_ClearHighlighting TokenBased
NotOnlyTokenBased) = Response -> TCM Response
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Response
IR.ResponseClearHighlightingNotOnlyTokenBased
fromResponse Response
Resp_DoneAborting = Response -> TCM Response
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Response
IR.ResponseDoneAborting
fromResponse Response
Resp_DoneExiting = Response -> TCM Response
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Response
IR.ResponseDoneExiting
fromResponse Response
Resp_ClearRunningInfo = Response -> TCM Response
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Response
IR.ResponseClearRunningInfo
fromResponse (Resp_RunningInfo Int
n [Char]
s) = Response -> TCM Response
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Response -> TCM Response) -> Response -> TCM Response
forall a b. (a -> b) -> a -> b
$ Int -> [Char] -> Response
IR.ResponseRunningInfo Int
n [Char]
s
fromResponse (Resp_Status Status
s) = Response -> TCM Response
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Response -> TCM Response) -> Response -> TCM Response
forall a b. (a -> b) -> a -> b
$ Bool -> Bool -> Response
IR.ResponseStatus (Status -> Bool
sChecked Status
s) (Status -> Bool
sShowImplicitArguments Status
s)
fromResponse (Resp_JumpToError [Char]
f Int32
p) = Response -> TCM Response
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Response -> TCM Response) -> Response -> TCM Response
forall a b. (a -> b) -> a -> b
$ [Char] -> Int -> Response
IR.ResponseJumpToError [Char]
f (Int32 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int32
p)
fromResponse (Resp_InteractionPoints [InteractionId]
is) =
  Response -> TCM Response
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Response -> TCM Response) -> Response -> TCM Response
forall a b. (a -> b) -> a -> b
$ [Int] -> Response
IR.ResponseInteractionPoints ((InteractionId -> Int) -> [InteractionId] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap InteractionId -> Int
interactionId [InteractionId]
is)
fromResponse (Resp_GiveAction (InteractionId Int
i) GiveResult
giveAction) =
  Response -> TCM Response
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Response -> TCM Response) -> Response -> TCM Response
forall a b. (a -> b) -> a -> b
$ Int -> GiveResult -> Response
IR.ResponseGiveAction Int
i (GiveResult -> GiveResult
forall a b. FromAgda a b => a -> b
fromAgda GiveResult
giveAction)
fromResponse (Resp_MakeCase InteractionId
_ MakeCaseVariant
Function [[Char]]
pcs) = Response -> TCM Response
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Response -> TCM Response) -> Response -> TCM Response
forall a b. (a -> b) -> a -> b
$ [[Char]] -> Response
IR.ResponseMakeCaseFunction [[Char]]
pcs
fromResponse (Resp_MakeCase InteractionId
_ MakeCaseVariant
ExtendedLambda [[Char]]
pcs) = Response -> TCM Response
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Response -> TCM Response) -> Response -> TCM Response
forall a b. (a -> b) -> a -> b
$ [[Char]] -> Response
IR.ResponseMakeCaseExtendedLambda [[Char]]
pcs
fromResponse (Resp_SolveAll [(InteractionId, Expr)]
ps) = Response -> TCM Response
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Response -> TCM Response) -> Response -> TCM Response
forall a b. (a -> b) -> a -> b
$ [(Int, [Char])] -> Response
IR.ResponseSolveAll (((InteractionId, Expr) -> (Int, [Char]))
-> [(InteractionId, Expr)] -> [(Int, [Char])]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (InteractionId, Expr) -> (Int, [Char])
forall {a}. Pretty a => (InteractionId, a) -> (Int, [Char])
prn [(InteractionId, Expr)]
ps)
  where
    prn :: (InteractionId, a) -> (Int, [Char])
prn (InteractionId Int
i, a
e) = (Int
i, a -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow a
e)

fromHighlightingInfo ::
  HighlightingInfo ->
  RemoveTokenBasedHighlighting ->
  HighlightingMethod ->
  ModuleToSource ->
  TCM IR.Response
fromHighlightingInfo :: HighlightingInfo
-> RemoveTokenBasedHighlighting
-> HighlightingMethod
-> ModuleToSource
-> TCM Response
fromHighlightingInfo HighlightingInfo
h RemoveTokenBasedHighlighting
remove HighlightingMethod
method ModuleToSource
modFile =
  case HighlightingInfo -> HighlightingMethod -> HighlightingMethod
chooseHighlightingMethod HighlightingInfo
h HighlightingMethod
method of
    HighlightingMethod
Direct -> Response -> TCM Response
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Response -> TCM Response) -> Response -> TCM Response
forall a b. (a -> b) -> a -> b
$ HighlightingInfos -> Response
IR.ResponseHighlightingInfoDirect HighlightingInfos
info
    HighlightingMethod
Indirect -> [Char] -> Response
IR.ResponseHighlightingInfoIndirect ([Char] -> Response) -> TCMT IO [Char] -> TCM Response
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO [Char]
indirect
  where
    fromAspects ::
      (Highlighting.Range, Aspects) ->
      IR.HighlightingInfo
    fromAspects :: (Range, Aspects) -> HighlightingInfo
fromAspects (Range
range, Aspects
aspects) =
      Int
-> Int
-> [[Char]]
-> Bool
-> [Char]
-> Maybe ([Char], Int)
-> HighlightingInfo
IR.HighlightingInfo
        (Range -> Int
Highlighting.from Range
range)
        (Range -> Int
Highlighting.to Range
range)
        (Aspects -> [[Char]]
toAtoms Aspects
aspects)
        (Aspects -> TokenBased
tokenBased Aspects
aspects TokenBased -> TokenBased -> Bool
forall a. Eq a => a -> a -> Bool
== TokenBased
TokenBased)
        (Aspects -> [Char]
note Aspects
aspects)
        (DefinitionSite -> ([Char], Int)
defSite (DefinitionSite -> ([Char], Int))
-> Maybe DefinitionSite -> Maybe ([Char], Int)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Aspects -> Maybe DefinitionSite
definitionSite Aspects
aspects)
      where
        defSite :: DefinitionSite -> ([Char], Int)
defSite (DefinitionSite TopLevelModuleName
moduleName Int
offset Bool
_ Maybe [Char]
_) =
          (AbsolutePath -> [Char]
filePath (AbsolutePath
-> TopLevelModuleName -> ModuleToSource -> AbsolutePath
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault AbsolutePath
forall a. HasCallStack => a
__IMPOSSIBLE__ TopLevelModuleName
moduleName ModuleToSource
modFile), Int
offset)

    infos :: [IR.HighlightingInfo]
    infos :: [HighlightingInfo]
infos = ((Range, Aspects) -> HighlightingInfo)
-> [(Range, Aspects)] -> [HighlightingInfo]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Range, Aspects) -> HighlightingInfo
fromAspects (HighlightingInfo -> [(Range, Aspects)]
forall a m. IsBasicRangeMap a m => m -> [(Range, a)]
toList HighlightingInfo
h)

    keepHighlighting :: Bool
    keepHighlighting :: Bool
keepHighlighting =
      case RemoveTokenBasedHighlighting
remove of
        RemoveTokenBasedHighlighting
RemoveHighlighting -> Bool
False
        RemoveTokenBasedHighlighting
KeepHighlighting -> Bool
True

    info :: IR.HighlightingInfos
    info :: HighlightingInfos
info = Bool -> [HighlightingInfo] -> HighlightingInfos
IR.HighlightingInfos Bool
keepHighlighting [HighlightingInfo]
infos

    indirect :: TCM FilePath
    indirect :: TCMT IO [Char]
indirect = IO [Char] -> TCMT IO [Char]
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO [Char] -> TCMT IO [Char]) -> IO [Char] -> TCMT IO [Char]
forall a b. (a -> b) -> a -> b
$ [Char] -> IO [Char]
writeToTempFile (ByteString -> [Char]
BS8.unpack (HighlightingInfos -> ByteString
forall a. ToJSON a => a -> ByteString
JSON.encode HighlightingInfos
info))

fromDisplayInfo :: DisplayInfo -> TCM IR.DisplayInfo
fromDisplayInfo :: DisplayInfo -> TCMT IO DisplayInfo
fromDisplayInfo = \case
  Info_CompilationOk CompilerBackend
_ WarningsAndNonFatalErrors
ws -> do
    -- filter
    let filteredWarnings :: [TCWarning]
filteredWarnings = [TCWarning] -> [TCWarning]
filterTCWarnings (WarningsAndNonFatalErrors -> [TCWarning]
tcWarnings WarningsAndNonFatalErrors
ws)
    let filteredErrors :: [TCWarning]
filteredErrors = [TCWarning] -> [TCWarning]
filterTCWarnings (WarningsAndNonFatalErrors -> [TCWarning]
nonFatalErrors WarningsAndNonFatalErrors
ws)
    -- serializes
    [Doc]
warnings <- (TCWarning -> TCMT IO Doc) -> [TCWarning] -> TCMT IO [Doc]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM TCWarning -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => TCWarning -> m Doc
prettyTCM [TCWarning]
filteredWarnings
    [Doc]
errors <- (TCWarning -> TCMT IO Doc) -> [TCWarning] -> TCMT IO [Doc]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM TCWarning -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => TCWarning -> m Doc
prettyTCM [TCWarning]
filteredErrors
    DisplayInfo -> TCMT IO DisplayInfo
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (DisplayInfo -> TCMT IO DisplayInfo)
-> DisplayInfo -> TCMT IO DisplayInfo
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [[Char]] -> DisplayInfo
IR.DisplayInfoCompilationOk ((Doc -> [Char]) -> [Doc] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Doc -> [Char]
forall a. Show a => a -> [Char]
show [Doc]
warnings) ((Doc -> [Char]) -> [Doc] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Doc -> [Char]
forall a. Show a => a -> [Char]
show [Doc]
errors)
  Info_Constraints [OutputForm Expr Expr]
s -> do
    -- constraints <- forM s $ \e -> do
    --   rendered <- renderTCM e
    --   let raw = show (pretty e)
    --   return $ Unlabeled rendered (Just raw)
    -- return $ IR.DisplayInfoGeneric "Constraints" constraints
    DisplayInfo -> TCMT IO DisplayInfo
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (DisplayInfo -> TCMT IO DisplayInfo)
-> DisplayInfo -> TCMT IO DisplayInfo
forall a b. (a -> b) -> a -> b
$ [Char] -> [Block] -> DisplayInfo
IR.DisplayInfoGeneric [Char]
"Constraints" [Inlines -> Maybe [Char] -> Maybe Range -> Block
Unlabeled ([Char] -> Inlines
Render.text ([Char] -> Inlines) -> [Char] -> Inlines
forall a b. (a -> b) -> a -> b
$ Doc -> [Char]
forall a. Show a => a -> [Char]
show (Doc -> [Char]) -> Doc -> [Char]
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (OutputForm Expr Expr -> Doc) -> [OutputForm Expr Expr] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap OutputForm Expr Expr -> Doc
forall a. Pretty a => a -> Doc
pretty [OutputForm Expr Expr]
s) Maybe [Char]
forall a. Maybe a
Nothing Maybe Range
forall a. Maybe a
Nothing]
  Info_AllGoalsWarnings ([OutputConstraint Expr InteractionId]
ims, [OutputConstraint Expr NamedMeta]
hms) WarningsAndNonFatalErrors
ws -> do
    -- visible metas (goals)
    [Block]
goals <- (OutputConstraint Expr InteractionId -> TCMT IO Block)
-> [OutputConstraint Expr InteractionId] -> TCMT IO [Block]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM OutputConstraint Expr InteractionId -> TCMT IO Block
convertGoal [OutputConstraint Expr InteractionId]
ims
    -- hidden (unsolved) metas
    [Block]
metas <- (OutputConstraint Expr NamedMeta -> TCMT IO Block)
-> [OutputConstraint Expr NamedMeta] -> TCMT IO [Block]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM OutputConstraint Expr NamedMeta -> TCMT IO Block
convertHiddenMeta [OutputConstraint Expr NamedMeta]
hms

    -- errors / warnings
    -- filter
    let filteredWarnings :: [TCWarning]
filteredWarnings = [TCWarning] -> [TCWarning]
filterTCWarnings (WarningsAndNonFatalErrors -> [TCWarning]
tcWarnings WarningsAndNonFatalErrors
ws)
    let filteredErrors :: [TCWarning]
filteredErrors = [TCWarning] -> [TCWarning]
filterTCWarnings (WarningsAndNonFatalErrors -> [TCWarning]
nonFatalErrors WarningsAndNonFatalErrors
ws)
    -- serializes
    [Doc]
warnings <- (TCWarning -> TCMT IO Doc) -> [TCWarning] -> TCMT IO [Doc]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM TCWarning -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => TCWarning -> m Doc
prettyTCM [TCWarning]
filteredWarnings
    [Doc]
errors <- (TCWarning -> TCMT IO Doc) -> [TCWarning] -> TCMT IO [Doc]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM TCWarning -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => TCWarning -> m Doc
prettyTCM [TCWarning]
filteredErrors

    let isG :: Bool
isG = Bool -> Bool
not ([Block] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Block]
goals Bool -> Bool -> Bool
&& [Block] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Block]
metas)
    let isW :: Bool
isW = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [Doc] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Doc]
warnings
    let isE :: Bool
isE = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [Doc] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Doc]
errors
    let title :: [Char]
title =
          [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
List.intercalate [Char]
"," ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$
            [Maybe [Char]] -> [[Char]]
forall a. [Maybe a] -> [a]
catMaybes
              [ [Char]
" Goals" [Char] -> Maybe () -> Maybe [Char]
forall a b. a -> Maybe b -> Maybe a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard Bool
isG,
                [Char]
" Errors" [Char] -> Maybe () -> Maybe [Char]
forall a b. a -> Maybe b -> Maybe a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard Bool
isE,
                [Char]
" Warnings" [Char] -> Maybe () -> Maybe [Char]
forall a b. a -> Maybe b -> Maybe a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard Bool
isW,
                [Char]
" Done" [Char] -> Maybe () -> Maybe [Char]
forall a b. a -> Maybe b -> Maybe a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Bool
not (Bool
isG Bool -> Bool -> Bool
|| Bool
isW Bool -> Bool -> Bool
|| Bool
isE))
              ]

    DisplayInfo -> TCMT IO DisplayInfo
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (DisplayInfo -> TCMT IO DisplayInfo)
-> DisplayInfo -> TCMT IO DisplayInfo
forall a b. (a -> b) -> a -> b
$ [Char] -> [Block] -> [Block] -> [[Char]] -> [[Char]] -> DisplayInfo
IR.DisplayInfoAllGoalsWarnings ([Char]
"*All" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
title [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"*") [Block]
goals [Block]
metas ((Doc -> [Char]) -> [Doc] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Doc -> [Char]
forall a. Show a => a -> [Char]
show [Doc]
warnings) ((Doc -> [Char]) -> [Doc] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Doc -> [Char]
forall a. Show a => a -> [Char]
show [Doc]
errors)
    where
      convertHiddenMeta :: OutputConstraint A.Expr NamedMeta -> TCM Block
      convertHiddenMeta :: OutputConstraint Expr NamedMeta -> TCMT IO Block
convertHiddenMeta OutputConstraint Expr NamedMeta
m = do
        let i :: MetaId
i = NamedMeta -> MetaId
nmid (NamedMeta -> MetaId) -> NamedMeta -> MetaId
forall a b. (a -> b) -> a -> b
$ OutputConstraint Expr NamedMeta -> NamedMeta
forall a. OutputConstraint Expr a -> a
namedMetaOf OutputConstraint Expr NamedMeta
m
        -- output constrain
        Inlines
meta <- MetaId -> TCMT IO Inlines -> TCMT IO Inlines
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m, MonadTCEnv m, MonadTrace m,
 ReadTCState m) =>
MetaId -> m a -> m a
withMetaId MetaId
i (TCMT IO Inlines -> TCMT IO Inlines)
-> TCMT IO Inlines -> TCMT IO Inlines
forall a b. (a -> b) -> a -> b
$ OutputConstraint Expr NamedMeta -> TCMT IO Inlines
forall c a.
(Render c, ToConcrete a, ConOfAbs a ~ c) =>
a -> TCMT IO Inlines
renderATop OutputConstraint Expr NamedMeta
m
        [Char]
serialized <- Doc -> [Char]
forall a. Show a => a -> [Char]
show (Doc -> [Char]) -> TCMT IO Doc -> TCMT IO [Char]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m, MonadTCEnv m, MonadTrace m,
 ReadTCState m) =>
MetaId -> m a -> m a
withMetaId MetaId
i (OutputConstraint Expr NamedMeta -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyATop OutputConstraint Expr NamedMeta
m)
        -- range
        Range
range <- MetaId -> TCMT IO Range
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m Range
getMetaRange MetaId
i

        Block -> TCMT IO Block
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Block -> TCMT IO Block) -> Block -> TCMT IO Block
forall a b. (a -> b) -> a -> b
$ Inlines -> Maybe [Char] -> Maybe Range -> Block
Unlabeled Inlines
meta ([Char] -> Maybe [Char]
forall a. a -> Maybe a
Just [Char]
serialized) (Range -> Maybe Range
forall a. a -> Maybe a
Just Range
range)

      convertGoal :: OutputConstraint A.Expr InteractionId -> TCM Block
      convertGoal :: OutputConstraint Expr InteractionId -> TCMT IO Block
convertGoal OutputConstraint Expr InteractionId
i = do
        -- output constrain
        Inlines
goal <-
          InteractionId -> TCMT IO Inlines -> TCMT IO Inlines
forall (m :: * -> *) a.
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
 MonadTCEnv m, MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId (OutputForm Expr InteractionId -> InteractionId
forall a b. OutputForm a b -> b
outputFormId (OutputForm Expr InteractionId -> InteractionId)
-> OutputForm Expr InteractionId -> InteractionId
forall a b. (a -> b) -> a -> b
$ Range
-> [ProblemId]
-> Blocker
-> OutputConstraint Expr InteractionId
-> OutputForm Expr InteractionId
forall a b.
Range
-> [ProblemId] -> Blocker -> OutputConstraint a b -> OutputForm a b
OutputForm Range
forall a. Range' a
noRange [] Blocker
alwaysUnblock OutputConstraint Expr InteractionId
i) (TCMT IO Inlines -> TCMT IO Inlines)
-> TCMT IO Inlines -> TCMT IO Inlines
forall a b. (a -> b) -> a -> b
$
            OutputConstraint Expr InteractionId -> TCMT IO Inlines
forall c a.
(Render c, ToConcrete a, ConOfAbs a ~ c) =>
a -> TCMT IO Inlines
renderATop OutputConstraint Expr InteractionId
i

        Doc
serialized <-
          InteractionId -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *) a.
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
 MonadTCEnv m, MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId (OutputForm Expr InteractionId -> InteractionId
forall a b. OutputForm a b -> b
outputFormId (OutputForm Expr InteractionId -> InteractionId)
-> OutputForm Expr InteractionId -> InteractionId
forall a b. (a -> b) -> a -> b
$ Range
-> [ProblemId]
-> Blocker
-> OutputConstraint Expr InteractionId
-> OutputForm Expr InteractionId
forall a b.
Range
-> [ProblemId] -> Blocker -> OutputConstraint a b -> OutputForm a b
OutputForm Range
forall a. Range' a
noRange [] Blocker
alwaysUnblock OutputConstraint Expr InteractionId
i) (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$
            OutputConstraint Expr InteractionId -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyATop OutputConstraint Expr InteractionId
i
        Block -> TCMT IO Block
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Block -> TCMT IO Block) -> Block -> TCMT IO Block
forall a b. (a -> b) -> a -> b
$ Inlines -> Maybe [Char] -> Maybe Range -> Block
Unlabeled Inlines
goal ([Char] -> Maybe [Char]
forall a. a -> Maybe a
Just ([Char] -> Maybe [Char]) -> [Char] -> Maybe [Char]
forall a b. (a -> b) -> a -> b
$ Doc -> [Char]
forall a. Show a => a -> [Char]
show Doc
serialized) Maybe Range
forall a. Maybe a
Nothing
  Info_Auto [Char]
s -> DisplayInfo -> TCMT IO DisplayInfo
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (DisplayInfo -> TCMT IO DisplayInfo)
-> DisplayInfo -> TCMT IO DisplayInfo
forall a b. (a -> b) -> a -> b
$ [Char] -> DisplayInfo
IR.DisplayInfoAuto [Char]
s
  Info_Error Info_Error
err -> do
    [Char]
s <- Info_Error -> TCMT IO [Char]
showInfoError Info_Error
err
    DisplayInfo -> TCMT IO DisplayInfo
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (DisplayInfo -> TCMT IO DisplayInfo)
-> DisplayInfo -> TCMT IO DisplayInfo
forall a b. (a -> b) -> a -> b
$ [Char] -> DisplayInfo
IR.DisplayInfoError [Char]
s
  Info_Time CPUTime
s ->
    DisplayInfo -> TCMT IO DisplayInfo
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (DisplayInfo -> TCMT IO DisplayInfo)
-> DisplayInfo -> TCMT IO DisplayInfo
forall a b. (a -> b) -> a -> b
$ [Char] -> DisplayInfo
IR.DisplayInfoTime (Doc -> [Char]
forall a. Show a => a -> [Char]
show (CPUTime -> Doc
prettyTimed CPUTime
s))
  Info_NormalForm CommandState
state ComputeMode
cmode Maybe CPUTime
time Expr
expr -> do
    Doc
exprDoc <- StateT CommandState (TCMT IO) Doc -> CommandState -> TCMT IO Doc
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT StateT CommandState (TCMT IO) Doc
prettyExpr CommandState
state
    let doc :: Doc
doc = Doc -> (CPUTime -> Doc) -> Maybe CPUTime -> Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc
forall a. Null a => a
empty CPUTime -> Doc
prettyTimed Maybe CPUTime
time Doc -> Doc -> Doc
$$ Doc
exprDoc
    DisplayInfo -> TCMT IO DisplayInfo
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (DisplayInfo -> TCMT IO DisplayInfo)
-> DisplayInfo -> TCMT IO DisplayInfo
forall a b. (a -> b) -> a -> b
$ [Char] -> DisplayInfo
IR.DisplayInfoNormalForm (Doc -> [Char]
forall a. Show a => a -> [Char]
show Doc
doc)
    where
      prettyExpr :: StateT CommandState (TCMT IO) Doc
prettyExpr =
        StateT CommandState (TCMT IO) Doc
-> StateT CommandState (TCMT IO) Doc
forall a. CommandM a -> CommandM a
localStateCommandM (StateT CommandState (TCMT IO) Doc
 -> StateT CommandState (TCMT IO) Doc)
-> StateT CommandState (TCMT IO) Doc
-> StateT CommandState (TCMT IO) Doc
forall a b. (a -> b) -> a -> b
$
          TCMT IO Doc -> StateT CommandState (TCMT IO) Doc
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO Doc -> StateT CommandState (TCMT IO) Doc)
-> TCMT IO Doc -> StateT CommandState (TCMT IO) Doc
forall a b. (a -> b) -> a -> b
$
            TCMT IO Doc -> TCMT IO Doc
forall a. TCM a -> TCM a
B.atTopLevel (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$
              TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
allowNonTerminatingReductions (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$
                (if ComputeMode -> Bool
computeIgnoreAbstract ComputeMode
cmode then TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
ignoreAbstractMode else TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
inConcreteMode) (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$
                  ComputeMode -> Expr -> TCMT IO Doc
B.showComputed ComputeMode
cmode Expr
expr
  Info_InferredType CommandState
state Maybe CPUTime
time Expr
expr -> do
    Inlines
renderedExpr <-
      (StateT CommandState (TCMT IO) Inlines
 -> CommandState -> TCMT IO Inlines)
-> CommandState
-> StateT CommandState (TCMT IO) Inlines
-> TCMT IO Inlines
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT CommandState (TCMT IO) Inlines
-> CommandState -> TCMT IO Inlines
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT CommandState
state (StateT CommandState (TCMT IO) Inlines -> TCMT IO Inlines)
-> StateT CommandState (TCMT IO) Inlines -> TCMT IO Inlines
forall a b. (a -> b) -> a -> b
$
        StateT CommandState (TCMT IO) Inlines
-> StateT CommandState (TCMT IO) Inlines
forall a. CommandM a -> CommandM a
localStateCommandM (StateT CommandState (TCMT IO) Inlines
 -> StateT CommandState (TCMT IO) Inlines)
-> StateT CommandState (TCMT IO) Inlines
-> StateT CommandState (TCMT IO) Inlines
forall a b. (a -> b) -> a -> b
$
          TCMT IO Inlines -> StateT CommandState (TCMT IO) Inlines
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO Inlines -> StateT CommandState (TCMT IO) Inlines)
-> TCMT IO Inlines -> StateT CommandState (TCMT IO) Inlines
forall a b. (a -> b) -> a -> b
$
            TCMT IO Inlines -> TCMT IO Inlines
forall a. TCM a -> TCM a
B.atTopLevel (TCMT IO Inlines -> TCMT IO Inlines)
-> TCMT IO Inlines -> TCMT IO Inlines
forall a b. (a -> b) -> a -> b
$
              Expr -> TCMT IO Inlines
forall c a.
(Render c, ToConcrete a, ConOfAbs a ~ c) =>
a -> TCMT IO Inlines
Render.renderA Expr
expr
    let rendered :: Inlines
rendered = case Maybe CPUTime
time of
          Maybe CPUTime
Nothing -> Inlines
renderedExpr
          -- TODO: handle this newline
          Just CPUTime
t -> Inlines
"Time:" Inlines -> Inlines -> Inlines
Render.<+> CPUTime -> Inlines
forall a. Render a => a -> Inlines
Render.render CPUTime
t Inlines -> Inlines -> Inlines
Render.<+> Inlines
"\n" Inlines -> Inlines -> Inlines
Render.<+> Inlines
renderedExpr
    Doc
exprDoc <-
      (StateT CommandState (TCMT IO) Doc -> CommandState -> TCMT IO Doc)
-> CommandState -> StateT CommandState (TCMT IO) Doc -> TCMT IO Doc
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT CommandState (TCMT IO) Doc -> CommandState -> TCMT IO Doc
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT CommandState
state (StateT CommandState (TCMT IO) Doc -> TCMT IO Doc)
-> StateT CommandState (TCMT IO) Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$
        StateT CommandState (TCMT IO) Doc
-> StateT CommandState (TCMT IO) Doc
forall a. CommandM a -> CommandM a
localStateCommandM (StateT CommandState (TCMT IO) Doc
 -> StateT CommandState (TCMT IO) Doc)
-> StateT CommandState (TCMT IO) Doc
-> StateT CommandState (TCMT IO) Doc
forall a b. (a -> b) -> a -> b
$
          TCMT IO Doc -> StateT CommandState (TCMT IO) Doc
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO Doc -> StateT CommandState (TCMT IO) Doc)
-> TCMT IO Doc -> StateT CommandState (TCMT IO) Doc
forall a b. (a -> b) -> a -> b
$
            TCMT IO Doc -> TCMT IO Doc
forall a. TCM a -> TCM a
B.atTopLevel (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$
              Expr -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
TCP.prettyA Expr
expr
    let raw :: [Char]
raw = Doc -> [Char]
forall a. Show a => a -> [Char]
show (Doc -> [Char]) -> Doc -> [Char]
forall a b. (a -> b) -> a -> b
$ 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
    DisplayInfo -> TCMT IO DisplayInfo
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (DisplayInfo -> TCMT IO DisplayInfo)
-> DisplayInfo -> TCMT IO DisplayInfo
forall a b. (a -> b) -> a -> b
$ [Char] -> [Block] -> DisplayInfo
IR.DisplayInfoGeneric [Char]
"Inferred Type" [Inlines -> Maybe [Char] -> Maybe Range -> Block
Unlabeled Inlines
rendered ([Char] -> Maybe [Char]
forall a. a -> Maybe a
Just [Char]
raw) Maybe Range
forall a. Maybe a
Nothing]
  Info_ModuleContents [Name]
modules Telescope
tel [(Name, Type)]
types -> do
    Doc
doc <- TCMT IO Doc -> TCMT IO Doc
forall a. TCM a -> TCM a
localTCState (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ do
      [([Char], Doc)]
typeDocs <- Telescope -> TCMT IO [([Char], Doc)] -> TCMT IO [([Char], Doc)]
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
tel (TCMT IO [([Char], Doc)] -> TCMT IO [([Char], Doc)])
-> TCMT IO [([Char], Doc)] -> TCMT IO [([Char], Doc)]
forall a b. (a -> b) -> a -> b
$
        [(Name, Type)]
-> ((Name, Type) -> TCMT IO ([Char], Doc))
-> TCMT IO [([Char], Doc)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Name, Type)]
types (((Name, Type) -> TCMT IO ([Char], Doc))
 -> TCMT IO [([Char], Doc)])
-> ((Name, Type) -> TCMT IO ([Char], Doc))
-> TCMT IO [([Char], Doc)]
forall a b. (a -> b) -> a -> b
$ \(Name
x, Type
t) -> do
          Doc
doc <- Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t
          ([Char], Doc) -> TCMT IO ([Char], Doc)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow Name
x, Doc
":" Doc -> Doc -> Doc
<+> Doc
doc)
      Doc -> TCMT IO Doc
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> TCMT IO Doc) -> Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$
        [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat
          [ Doc
"Modules",
            Int -> Doc -> Doc
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (Name -> Doc) -> [Name] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap 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 -> [([Char], Doc)] -> Doc
align Int
10 [([Char], Doc)]
typeDocs
          ]
    DisplayInfo -> TCMT IO DisplayInfo
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (DisplayInfo -> TCMT IO DisplayInfo)
-> DisplayInfo -> TCMT IO DisplayInfo
forall a b. (a -> b) -> a -> b
$ [Char] -> [Block] -> DisplayInfo
IR.DisplayInfoGeneric [Char]
"Module contents" [Inlines -> Maybe [Char] -> Maybe Range -> Block
Unlabeled ([Char] -> Inlines
Render.text ([Char] -> Inlines) -> [Char] -> Inlines
forall a b. (a -> b) -> a -> b
$ Doc -> [Char]
forall a. Show a => a -> [Char]
show Doc
doc) Maybe [Char]
forall a. Maybe a
Nothing Maybe Range
forall a. Maybe a
Nothing]
  Info_SearchAbout [(Name, Type)]
hits [Char]
names -> do
    [([Char], Doc)]
hitDocs <- [(Name, Type)]
-> ((Name, Type) -> TCMT IO ([Char], Doc))
-> TCMT IO [([Char], Doc)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Name, Type)]
hits (((Name, Type) -> TCMT IO ([Char], Doc))
 -> TCMT IO [([Char], Doc)])
-> ((Name, Type) -> TCMT IO ([Char], Doc))
-> TCMT IO [([Char], Doc)]
forall a b. (a -> b) -> a -> b
$ \(Name
x, Type
t) -> do
      Doc
doc <- Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t
      ([Char], Doc) -> TCMT IO ([Char], Doc)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow Name
x, Doc
":" Doc -> Doc -> Doc
<+> Doc
doc)
    let doc :: Doc
doc =
          Doc
"Definitions about"
            Doc -> Doc -> Doc
<+> [Char] -> Doc
text ([Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
List.intercalate [Char]
", " ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$ [Char] -> [[Char]]
words [Char]
names) Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
nest Int
2 (Int -> [([Char], Doc)] -> Doc
align Int
10 [([Char], Doc)]
hitDocs)
    DisplayInfo -> TCMT IO DisplayInfo
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (DisplayInfo -> TCMT IO DisplayInfo)
-> DisplayInfo -> TCMT IO DisplayInfo
forall a b. (a -> b) -> a -> b
$ [Char] -> [Block] -> DisplayInfo
IR.DisplayInfoGeneric [Char]
"Search About" [Inlines -> Maybe [Char] -> Maybe Range -> Block
Unlabeled ([Char] -> Inlines
Render.text ([Char] -> Inlines) -> [Char] -> Inlines
forall a b. (a -> b) -> a -> b
$ Doc -> [Char]
forall a. Show a => a -> [Char]
show Doc
doc) Maybe [Char]
forall a. Maybe a
Nothing Maybe Range
forall a. Maybe a
Nothing]
#if MIN_VERSION_Agda(2,6,3)
  Info_WhyInScope (WhyInScopeData QName
q [Char]
cwd Maybe LocalVar
v [AbstractName]
xs [AbstractModule]
ms) -> do
    Doc
doc <- [Char]
-> [Char]
-> Maybe LocalVar
-> [AbstractName]
-> [AbstractModule]
-> TCMT IO Doc
explainWhyInScope (QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow QName
q) [Char]
cwd Maybe LocalVar
v [AbstractName]
xs [AbstractModule]
ms
#else
  Info_WhyInScope s cwd v xs ms -> do
    doc <- explainWhyInScope s cwd v xs ms
#endif
    DisplayInfo -> TCMT IO DisplayInfo
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (DisplayInfo -> TCMT IO DisplayInfo)
-> DisplayInfo -> TCMT IO DisplayInfo
forall a b. (a -> b) -> a -> b
$ [Char] -> [Block] -> DisplayInfo
IR.DisplayInfoGeneric [Char]
"Scope Info" [Inlines -> Maybe [Char] -> Maybe Range -> Block
Unlabeled ([Char] -> Inlines
Render.text ([Char] -> Inlines) -> [Char] -> Inlines
forall a b. (a -> b) -> a -> b
$ Doc -> [Char]
forall a. Show a => a -> [Char]
show Doc
doc) Maybe [Char]
forall a. Maybe a
Nothing Maybe Range
forall a. Maybe a
Nothing]
  Info_Context InteractionId
ii [ResponseContextEntry]
ctx -> do
    Doc
doc <- TCMT IO Doc -> TCMT IO Doc
forall a. TCM a -> TCM a
localTCState (InteractionId -> Bool -> [ResponseContextEntry] -> TCMT IO Doc
prettyResponseContexts InteractionId
ii Bool
False [ResponseContextEntry]
ctx)
    DisplayInfo -> TCMT IO DisplayInfo
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (DisplayInfo -> TCMT IO DisplayInfo)
-> DisplayInfo -> TCMT IO DisplayInfo
forall a b. (a -> b) -> a -> b
$ [Char] -> [Block] -> DisplayInfo
IR.DisplayInfoGeneric [Char]
"Context" [Inlines -> Maybe [Char] -> Maybe Range -> Block
Unlabeled ([Char] -> Inlines
Render.text ([Char] -> Inlines) -> [Char] -> Inlines
forall a b. (a -> b) -> a -> b
$ Doc -> [Char]
forall a. Show a => a -> [Char]
show Doc
doc) Maybe [Char]
forall a. Maybe a
Nothing Maybe Range
forall a. Maybe a
Nothing]
  DisplayInfo
Info_Intro_NotFound ->
    DisplayInfo -> TCMT IO DisplayInfo
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (DisplayInfo -> TCMT IO DisplayInfo)
-> DisplayInfo -> TCMT IO DisplayInfo
forall a b. (a -> b) -> a -> b
$ [Char] -> [Block] -> DisplayInfo
IR.DisplayInfoGeneric [Char]
"Intro" [Inlines -> Maybe [Char] -> Maybe Range -> Block
Unlabeled ([Char] -> Inlines
Render.text [Char]
"No introduction forms found.") Maybe [Char]
forall a. Maybe a
Nothing Maybe Range
forall a. Maybe a
Nothing]
  Info_Intro_ConstructorUnknown [[Char]]
ss -> do
    let doc :: Doc
doc =
          [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
sep
            [ Doc
"Don't know which constructor to introduce of",
              let mkOr :: [[Char]] -> [Doc]
mkOr [] = []
                  mkOr [[Char]
x, [Char]
y] = [[Char] -> Doc
text [Char]
x Doc -> Doc -> Doc
<+> Doc
"or" Doc -> Doc -> Doc
<+> [Char] -> Doc
text [Char]
y]
                  mkOr ([Char]
x : [[Char]]
xs) = [Char] -> Doc
text [Char]
x Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: [[Char]] -> [Doc]
mkOr [[Char]]
xs
               in Int -> Doc -> Doc
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
forall (t :: * -> *). Foldable t => Doc -> t Doc -> [Doc]
punctuate Doc
comma ([[Char]] -> [Doc]
mkOr [[Char]]
ss)
            ]
    DisplayInfo -> TCMT IO DisplayInfo
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (DisplayInfo -> TCMT IO DisplayInfo)
-> DisplayInfo -> TCMT IO DisplayInfo
forall a b. (a -> b) -> a -> b
$ [Char] -> [Block] -> DisplayInfo
IR.DisplayInfoGeneric [Char]
"Intro" [Inlines -> Maybe [Char] -> Maybe Range -> Block
Unlabeled ([Char] -> Inlines
Render.text ([Char] -> Inlines) -> [Char] -> Inlines
forall a b. (a -> b) -> a -> b
$ Doc -> [Char]
forall a. Show a => a -> [Char]
show Doc
doc) Maybe [Char]
forall a. Maybe a
Nothing Maybe Range
forall a. Maybe a
Nothing]
  DisplayInfo
Info_Version ->
    DisplayInfo -> TCMT IO DisplayInfo
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (DisplayInfo -> TCMT IO DisplayInfo)
-> DisplayInfo -> TCMT IO DisplayInfo
forall a b. (a -> b) -> a -> b
$ [Char] -> [Block] -> DisplayInfo
IR.DisplayInfoGeneric [Char]
"Agda Version" [Inlines -> Maybe [Char] -> Maybe Range -> Block
Unlabeled ([Char] -> Inlines
Render.text ([Char] -> Inlines) -> [Char] -> Inlines
forall a b. (a -> b) -> a -> b
$ [Char]
"Agda version " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
versionWithCommitInfo) Maybe [Char]
forall a. Maybe a
Nothing Maybe Range
forall a. Maybe a
Nothing]
  Info_GoalSpecific InteractionId
ii GoalDisplayInfo
kind -> InteractionId -> GoalDisplayInfo -> TCMT IO DisplayInfo
lispifyGoalSpecificDisplayInfo InteractionId
ii GoalDisplayInfo
kind

lispifyGoalSpecificDisplayInfo :: InteractionId -> GoalDisplayInfo -> TCM IR.DisplayInfo
lispifyGoalSpecificDisplayInfo :: InteractionId -> GoalDisplayInfo -> TCMT IO DisplayInfo
lispifyGoalSpecificDisplayInfo InteractionId
ii GoalDisplayInfo
kind = TCMT IO DisplayInfo -> TCMT IO DisplayInfo
forall a. TCM a -> TCM a
localTCState (TCMT IO DisplayInfo -> TCMT IO DisplayInfo)
-> TCMT IO DisplayInfo -> TCMT IO DisplayInfo
forall a b. (a -> b) -> a -> b
$
  InteractionId -> TCMT IO DisplayInfo -> TCMT IO DisplayInfo
forall (m :: * -> *) a.
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
 MonadTCEnv m, MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
ii (TCMT IO DisplayInfo -> TCMT IO DisplayInfo)
-> TCMT IO DisplayInfo -> TCMT IO DisplayInfo
forall a b. (a -> b) -> a -> b
$
    case GoalDisplayInfo
kind of
      Goal_HelperFunction OutputConstraint' Expr Expr
helperType -> do
        Doc
doc <- TCMT IO Doc -> TCMT IO Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ OutputConstraint' Expr Expr -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyATop OutputConstraint' Expr Expr
helperType
        DisplayInfo -> TCMT IO DisplayInfo
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (DisplayInfo -> TCMT IO DisplayInfo)
-> DisplayInfo -> TCMT IO DisplayInfo
forall a b. (a -> b) -> a -> b
$ [Char] -> [Block] -> DisplayInfo
IR.DisplayInfoGeneric [Char]
"Helper function" [Inlines -> Maybe [Char] -> Maybe Range -> Block
Unlabeled ([Char] -> Inlines
Render.text ([Char] -> Inlines) -> [Char] -> Inlines
forall a b. (a -> b) -> a -> b
$ Doc -> [Char]
forall a. Show a => a -> [Char]
show Doc
doc [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n") Maybe [Char]
forall a. Maybe a
Nothing Maybe Range
forall a. Maybe a
Nothing]
      Goal_NormalForm ComputeMode
cmode Expr
expr -> do
        Doc
doc <- ComputeMode -> Expr -> TCMT IO Doc
showComputed ComputeMode
cmode Expr
expr
        DisplayInfo -> TCMT IO DisplayInfo
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (DisplayInfo -> TCMT IO DisplayInfo)
-> DisplayInfo -> TCMT IO DisplayInfo
forall a b. (a -> b) -> a -> b
$ [Char] -> [Block] -> DisplayInfo
IR.DisplayInfoGeneric [Char]
"Normal Form" [Inlines -> Maybe [Char] -> Maybe Range -> Block
Unlabeled ([Char] -> Inlines
Render.text ([Char] -> Inlines) -> [Char] -> Inlines
forall a b. (a -> b) -> a -> b
$ Doc -> [Char]
forall a. Show a => a -> [Char]
show Doc
doc) Maybe [Char]
forall a. Maybe a
Nothing Maybe Range
forall a. Maybe a
Nothing]
      Goal_GoalType Rewrite
norm GoalTypeAux
aux [ResponseContextEntry]
resCtxs [IPBoundary' Expr]
boundaries [OutputForm Expr Expr]
constraints -> do
        [Block]
goalSect <- do
          (Inlines
rendered, [Char]
raw) <- Rewrite -> InteractionId -> TCM (Inlines, [Char])
prettyTypeOfMeta Rewrite
norm InteractionId
ii
          [Block] -> TCMT IO [Block]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [Inlines -> Maybe [Char] -> Maybe Range -> [Char] -> [Char] -> Block
Labeled Inlines
rendered ([Char] -> Maybe [Char]
forall a. a -> Maybe a
Just [Char]
raw) Maybe Range
forall a. Maybe a
Nothing [Char]
"Goal" [Char]
"special"]

        [Block]
auxSect <- case GoalTypeAux
aux of
          GoalTypeAux
GoalOnly -> [Block] -> TCMT IO [Block]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return []
          GoalAndHave Expr
expr -> do
            Inlines
rendered <- Expr -> TCMT IO Inlines
forall c a.
(Render c, ToConcrete a, ConOfAbs a ~ c) =>
a -> TCMT IO Inlines
renderATop Expr
expr
            [Char]
raw <- Doc -> [Char]
forall a. Show a => a -> [Char]
show (Doc -> [Char]) -> TCMT IO Doc -> TCMT IO [Char]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyATop Expr
expr
            [Block] -> TCMT IO [Block]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [Inlines -> Maybe [Char] -> Maybe Range -> [Char] -> [Char] -> Block
Labeled Inlines
rendered ([Char] -> Maybe [Char]
forall a. a -> Maybe a
Just [Char]
raw) Maybe Range
forall a. Maybe a
Nothing [Char]
"Have" [Char]
"special"]
          GoalAndElaboration Term
term -> do
            let rendered :: Inlines
rendered = Term -> Inlines
forall a. Render a => a -> Inlines
render Term
term
            [Char]
raw <- Doc -> [Char]
forall a. Show a => a -> [Char]
show (Doc -> [Char]) -> TCMT IO Doc -> TCMT IO [Char]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
TCP.prettyTCM Term
term
            [Block] -> TCMT IO [Block]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [Inlines -> Maybe [Char] -> Maybe Range -> [Char] -> [Char] -> Block
Labeled Inlines
rendered ([Char] -> Maybe [Char]
forall a. a -> Maybe a
Just [Char]
raw) Maybe Range
forall a. Maybe a
Nothing [Char]
"Elaborates to" [Char]
"special"]
        let boundarySect :: [Block]
boundarySect =
              if [IPBoundary' Expr] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [IPBoundary' Expr]
boundaries
                then []
                else
                  [Char] -> Block
Header [Char]
"Boundary" Block -> [Block] -> [Block]
forall a. a -> [a] -> [a]
:
                  (IPBoundary' Expr -> Block) -> [IPBoundary' Expr] -> [Block]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\IPBoundary' Expr
boundary -> Inlines -> Maybe [Char] -> Maybe Range -> Block
Unlabeled (IPBoundary' Expr -> Inlines
forall a. Render a => a -> Inlines
render IPBoundary' Expr
boundary) ([Char] -> Maybe [Char]
forall a. a -> Maybe a
Just ([Char] -> Maybe [Char]) -> [Char] -> Maybe [Char]
forall a b. (a -> b) -> a -> b
$ Doc -> [Char]
forall a. Show a => a -> [Char]
show (Doc -> [Char]) -> Doc -> [Char]
forall a b. (a -> b) -> a -> b
$ IPBoundary' Expr -> Doc
forall a. Pretty a => a -> Doc
pretty IPBoundary' Expr
boundary) Maybe Range
forall a. Maybe a
Nothing) [IPBoundary' Expr]
boundaries
        [Block]
contextSect <- [Block] -> [Block]
forall a. [a] -> [a]
reverse ([Block] -> [Block])
-> ([[Block]] -> [Block]) -> [[Block]] -> [Block]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[Block]] -> [Block]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Block]] -> [Block]) -> TCMT IO [[Block]] -> TCMT IO [Block]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ResponseContextEntry -> TCMT IO [Block])
-> [ResponseContextEntry] -> TCMT IO [[Block]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (InteractionId -> ResponseContextEntry -> TCMT IO [Block]
renderResponseContext InteractionId
ii) [ResponseContextEntry]
resCtxs
        let constraintSect :: [Block]
constraintSect =
                if [OutputForm Expr Expr] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [OutputForm Expr Expr]
constraints
                  then []
                  else
                    [Char] -> Block
Header [Char]
"Constraints" Block -> [Block] -> [Block]
forall a. a -> [a] -> [a]
:
                    (OutputForm Expr Expr -> Block)
-> [OutputForm Expr Expr] -> [Block]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\OutputForm Expr Expr
constraint -> Inlines -> Maybe [Char] -> Maybe Range -> Block
Unlabeled (OutputForm Expr Expr -> Inlines
forall a. Render a => a -> Inlines
render OutputForm Expr Expr
constraint) ([Char] -> Maybe [Char]
forall a. a -> Maybe a
Just ([Char] -> Maybe [Char]) -> [Char] -> Maybe [Char]
forall a b. (a -> b) -> a -> b
$ Doc -> [Char]
forall a. Show a => a -> [Char]
show (Doc -> [Char]) -> Doc -> [Char]
forall a b. (a -> b) -> a -> b
$ OutputForm Expr Expr -> Doc
forall a. Pretty a => a -> Doc
pretty OutputForm Expr Expr
constraint) Maybe Range
forall a. Maybe a
Nothing) [OutputForm Expr Expr]
constraints

        DisplayInfo -> TCMT IO DisplayInfo
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (DisplayInfo -> TCMT IO DisplayInfo)
-> DisplayInfo -> TCMT IO DisplayInfo
forall a b. (a -> b) -> a -> b
$
          [Char] -> [Block] -> DisplayInfo
IR.DisplayInfoGeneric [Char]
"Goal type etc" ([Block] -> DisplayInfo) -> [Block] -> DisplayInfo
forall a b. (a -> b) -> a -> b
$ [Block]
goalSect [Block] -> [Block] -> [Block]
forall a. [a] -> [a] -> [a]
++ [Block]
auxSect [Block] -> [Block] -> [Block]
forall a. [a] -> [a] -> [a]
++ [Block]
boundarySect [Block] -> [Block] -> [Block]
forall a. [a] -> [a] -> [a]
++ [Block]
contextSect [Block] -> [Block] -> [Block]
forall a. [a] -> [a] -> [a]
++ [Block]
constraintSect
      Goal_CurrentGoal Rewrite
norm -> do
        (Inlines
rendered, [Char]
raw) <- Rewrite -> InteractionId -> TCM (Inlines, [Char])
prettyTypeOfMeta Rewrite
norm InteractionId
ii
        DisplayInfo -> TCMT IO DisplayInfo
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (DisplayInfo -> TCMT IO DisplayInfo)
-> DisplayInfo -> TCMT IO DisplayInfo
forall a b. (a -> b) -> a -> b
$ Block -> DisplayInfo
IR.DisplayInfoCurrentGoal (Inlines -> Maybe [Char] -> Maybe Range -> Block
Unlabeled Inlines
rendered ([Char] -> Maybe [Char]
forall a. a -> Maybe a
Just [Char]
raw) Maybe Range
forall a. Maybe a
Nothing)
      Goal_InferredType Expr
expr -> do
        Inlines
rendered <- Expr -> TCMT IO Inlines
forall c a.
(Render c, ToConcrete a, ConOfAbs a ~ c) =>
a -> TCMT IO Inlines
renderATop Expr
expr
        [Char]
raw <- Doc -> [Char]
forall a. Show a => a -> [Char]
show (Doc -> [Char]) -> TCMT IO Doc -> TCMT IO [Char]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyATop Expr
expr
        DisplayInfo -> TCMT IO DisplayInfo
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (DisplayInfo -> TCMT IO DisplayInfo)
-> DisplayInfo -> TCMT IO DisplayInfo
forall a b. (a -> b) -> a -> b
$ Block -> DisplayInfo
IR.DisplayInfoInferredType (Inlines -> Maybe [Char] -> Maybe Range -> Block
Unlabeled Inlines
rendered ([Char] -> Maybe [Char]
forall a. a -> Maybe a
Just [Char]
raw) Maybe Range
forall a. Maybe a
Nothing)

-- -- | Format responses of DisplayInfo
-- formatPrim :: Bool -> [Block] -> String -> TCM IR.DisplayInfo
-- formatPrim _copy items header = return $ IR.DisplayInfoGeneric header items

-- -- | Format responses of DisplayInfo ("agda2-info-action")
-- format :: [Block] -> String -> TCM IR.DisplayInfo
-- format = formatPrim False

-- -- | Format responses of DisplayInfo ("agda2-info-action-copy")
-- formatAndCopy :: [Block] -> String -> TCM IR.DisplayInfo
-- formatAndCopy = formatPrim True

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

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

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

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

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

    pName :: AbstractName -> TCM Doc
    pName :: AbstractName -> TCMT IO Doc
pName AbstractName
a =
      [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
TCP.sep
        [ TCMT IO Doc
"* a"
            TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TCP.<+> KindOfName -> TCMT IO Doc
pKind (AbstractName -> KindOfName
anameKind AbstractName
a)
            TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TCP.<+> [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
TCP.text (QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow (QName -> [Char]) -> QName -> [Char]
forall a b. (a -> b) -> a -> b
$ AbstractName -> QName
anameName AbstractName
a),
          Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
TCP.nest Int
2 TCMT IO Doc
"brought into scope by"
        ]
        TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TCP.$$ Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
TCP.nest Int
2 (Range -> WhyInScope -> TCMT IO 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 -> TCMT IO Doc
pMod AbstractModule
a =
      [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
TCP.sep
        [ TCMT IO Doc
"* a module" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TCP.<+> [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
TCP.text (ModuleName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow (ModuleName -> [Char]) -> ModuleName -> [Char]
forall a b. (a -> b) -> a -> b
$ AbstractModule -> ModuleName
amodName AbstractModule
a),
          Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
TCP.nest Int
2 TCMT IO Doc
"brought into scope by"
        ]
        TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TCP.$$ Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
TCP.nest Int
2 (Range -> WhyInScope -> TCMT IO 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 -> TCMT IO Doc
pWhy Range
r WhyInScope
Defined = TCMT IO Doc
"- its definition at" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TCP.<+> Range -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Range -> 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 -> TCMT IO Doc
pWhy Range
r WhyInScope
w
    pWhy Range
r (Opened QName
m WhyInScope
w) =
      TCMT IO Doc
"- the opening of"
        TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TCP.<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
TCP.prettyTCM QName
m
        TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TCP.<+> TCMT IO Doc
"at"
        TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TCP.<+> Range -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Range -> m Doc
TCP.prettyTCM (QName -> Range
forall a. HasRange a => a -> Range
getRange QName
m)
        TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TCP.$$ Range -> WhyInScope -> TCMT IO Doc
pWhy Range
r WhyInScope
w
    pWhy Range
r (Applied QName
m WhyInScope
w) =
      TCMT IO Doc
"- the application of"
        TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TCP.<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
TCP.prettyTCM QName
m
        TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TCP.<+> TCMT IO Doc
"at"
        TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TCP.<+> Range -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Range -> m Doc
TCP.prettyTCM (QName -> Range
forall a. HasRange a => a -> Range
getRange QName
m)
        TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TCP.$$ Range -> WhyInScope -> TCMT IO Doc
pWhy Range
r WhyInScope
w

-- | Pretty-prints the context of the given meta-variable.
prettyResponseContexts ::
  -- | Context of this meta-variable.
  InteractionId ->
  -- | Print the elements in reverse order?
  Bool ->
  [ResponseContextEntry] ->
  TCM Doc
prettyResponseContexts :: InteractionId -> Bool -> [ResponseContextEntry] -> TCMT IO Doc
prettyResponseContexts InteractionId
ii Bool
rev [ResponseContextEntry]
ctxs = do
  [[([Char], Doc)]]
rows <- (ResponseContextEntry -> TCMT IO [([Char], Doc)])
-> [ResponseContextEntry] -> TCMT IO [[([Char], Doc)]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (InteractionId -> ResponseContextEntry -> TCMT IO [([Char], Doc)]
prettyResponseContext InteractionId
ii) [ResponseContextEntry]
ctxs
  Doc -> TCMT IO Doc
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> TCMT IO Doc) -> Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Int -> [([Char], Doc)] -> Doc
align Int
10 ([([Char], Doc)] -> Doc) -> [([Char], Doc)] -> Doc
forall a b. (a -> b) -> a -> b
$ [[([Char], Doc)]] -> [([Char], Doc)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[([Char], Doc)]] -> [([Char], Doc)])
-> [[([Char], Doc)]] -> [([Char], Doc)]
forall a b. (a -> b) -> a -> b
$ Bool
-> ([[([Char], Doc)]] -> [[([Char], Doc)]])
-> [[([Char], Doc)]]
-> [[([Char], Doc)]]
forall a. Bool -> (a -> a) -> a -> a
applyWhen Bool
rev [[([Char], Doc)]] -> [[([Char], Doc)]]
forall a. [a] -> [a]
reverse [[([Char], Doc)]]
rows

-- | Pretty-prints the context of the given meta-variable.
prettyResponseContext ::
  -- | Context of this meta-variable.
  InteractionId ->
  ResponseContextEntry ->
  TCM [(String, Doc)]
prettyResponseContext :: InteractionId -> ResponseContextEntry -> TCMT IO [([Char], Doc)]
prettyResponseContext InteractionId
ii (ResponseContextEntry Name
n Name
x (Arg ArgInfo
ai Expr
expr) Maybe Expr
letv NameInScope
nis) = InteractionId -> TCMT IO [([Char], Doc)] -> TCMT IO [([Char], Doc)]
forall (m :: * -> *) a.
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
 MonadTCEnv m, MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
ii (TCMT IO [([Char], Doc)] -> TCMT IO [([Char], Doc)])
-> TCMT IO [([Char], Doc)] -> TCMT IO [([Char], Doc)]
forall a b. (a -> b) -> a -> b
$ do
  Modality
modality <- (TCEnv -> Modality) -> TCMT IO Modality
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Modality
forall a. LensModality a => a -> Modality
getModality
  do
    let prettyCtxName :: String
        prettyCtxName :: [Char]
prettyCtxName
          | Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
x = Name -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow Name
x
          | Name -> NameInScope
forall a. LensInScope a => a -> NameInScope
isInScope Name
n NameInScope -> NameInScope -> Bool
forall a. Eq a => a -> a -> Bool
== NameInScope
InScope = Name -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow Name
n [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Name -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow Name
x
          | Bool
otherwise = Name -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow Name
x

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

        extras :: [Doc]
        extras :: [Doc]
extras =
          [[Doc]] -> [Doc]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
            [ [Doc
"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
modality],
              -- 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
modality],
              -- Print instance if variable is considered by instance search
              [Doc
"instance" | ArgInfo -> Bool
forall a. LensHiding a => a -> Bool
isInstance ArgInfo
ai]
            ]
    Doc
ty <- Expr -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyATop Expr
expr

    [([Char], Doc)]
letv' <- case Maybe Expr
letv of
      Maybe Expr
Nothing -> [([Char], Doc)] -> TCMT IO [([Char], Doc)]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return []
      Just Expr
val -> do
        Doc
val' <- Expr -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyATop Expr
val
        [([Char], Doc)] -> TCMT IO [([Char], Doc)]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [(Name -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow Name
x, Doc
"=" Doc -> Doc -> Doc
<+> Doc
val')]

    [([Char], Doc)] -> TCMT IO [([Char], Doc)]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([([Char], Doc)] -> TCMT IO [([Char], Doc)])
-> [([Char], Doc)] -> TCMT IO [([Char], Doc)]
forall a b. (a -> b) -> a -> b
$
      ([Char]
attribute [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
prettyCtxName, Doc
":" Doc -> Doc -> Doc
<+> Doc
ty Doc -> Doc -> Doc
<+> [Doc] -> Doc
parenSep [Doc]
extras) ([Char], Doc) -> [([Char], Doc)] -> [([Char], Doc)]
forall a. a -> [a] -> [a]
: [([Char], Doc)]
letv'
  where
    parenSep :: [Doc] -> Doc
    parenSep :: [Doc] -> Doc
parenSep [Doc]
docs
      | [Doc] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Doc]
docs = Doc
forall a. Null a => a
empty
      | Bool
otherwise = (Doc
" " Doc -> Doc -> Doc
<+>) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
forall (t :: * -> *). Foldable t => Doc -> t Doc -> [Doc]
punctuate Doc
comma [Doc]
docs

-- | Render the context of the given meta-variable.
renderResponseContext ::
  -- | Context of this meta-variable.
  InteractionId ->
  ResponseContextEntry ->
  TCM [Block]
renderResponseContext :: InteractionId -> ResponseContextEntry -> TCMT IO [Block]
renderResponseContext InteractionId
ii (ResponseContextEntry Name
n Name
x (Arg ArgInfo
ai Expr
expr) Maybe Expr
letv NameInScope
nis) = InteractionId -> TCMT IO [Block] -> TCMT IO [Block]
forall (m :: * -> *) a.
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
 MonadTCEnv m, MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
ii (TCMT IO [Block] -> TCMT IO [Block])
-> TCMT IO [Block] -> TCMT IO [Block]
forall a b. (a -> b) -> a -> b
$ do
  Modality
modality <- (TCEnv -> Modality) -> TCMT IO Modality
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Modality
forall a. LensModality a => a -> Modality
getModality
  do
    let
        rawCtxName :: String
        rawCtxName :: [Char]
rawCtxName
          | Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
x = Name -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow Name
x
          | Name -> NameInScope
forall a. LensInScope a => a -> NameInScope
isInScope Name
n NameInScope -> NameInScope -> Bool
forall a. Eq a => a -> a -> Bool
== NameInScope
InScope = Name -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow Name
n [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Name -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow Name
x
          | Bool
otherwise = Name -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow Name
x

        renderedCtxName :: Inlines
        renderedCtxName :: Inlines
renderedCtxName
          | Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
x = Name -> Inlines
forall a. Render a => a -> Inlines
render 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 -> Inlines
forall a. Render a => a -> Inlines
render Name
n Inlines -> Inlines -> Inlines
Render.<+> Inlines
"=" Inlines -> Inlines -> Inlines
Render.<+> Name -> Inlines
forall a. Render a => a -> Inlines
render Name
x
          | Bool
otherwise = Name -> Inlines
forall a. Render a => a -> Inlines
render Name
x

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

        renderedAttribute :: Inlines
        renderedAttribute :: Inlines
renderedAttribute = Inlines
c Inlines -> Inlines -> Inlines
forall a. Semigroup a => a -> a -> a
<> if [Char] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Inlines -> [Char]
forall a. Show a => a -> [Char]
show Inlines
c) then Inlines
"" else Inlines
" "
          where
            c :: Inlines
c = Cohesion -> Inlines
forall a. Render a => a -> Inlines
render (ArgInfo -> Cohesion
forall a. LensCohesion a => a -> Cohesion
getCohesion ArgInfo
ai)

        extras :: IsString a => [a]
        extras :: forall a. IsString a => [a]
extras =
          [[a]] -> [a]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
            [ [a
"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.
              [a
"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
modality],
              -- Print irrelevant if hypothesis is strictly less relevant than goal.
              [a
"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
modality],
              -- Print instance if variable is considered by instance search
              [a
"instance" | ArgInfo -> Bool
forall a. LensHiding a => a -> Bool
isInstance ArgInfo
ai]
            ]

        extras2 :: [Inlines]
        extras2 :: [Inlines]
extras2 =
          [[Inlines]] -> [Inlines]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
            [ [Inlines
"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.
              [Inlines
"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
modality],
              -- Print irrelevant if hypothesis is strictly less relevant than goal.
              [Inlines
"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
modality],
              -- Print instance if variable is considered by instance search
              [Inlines
"instance" | ArgInfo -> Bool
forall a. LensHiding a => a -> Bool
isInstance ArgInfo
ai]
            ]

    -- raw
    Doc
rawExpr <- Expr -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyATop Expr
expr
    let rawType :: [Char]
rawType = Doc -> [Char]
forall a. Show a => a -> [Char]
show (Doc -> [Char]) -> Doc -> [Char]
forall a b. (a -> b) -> a -> b
$ Int -> [([Char], Doc)] -> Doc
align Int
10 [([Char]
rawAttribute [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
rawCtxName, Doc
":" Doc -> Doc -> Doc
<+> Doc
rawExpr Doc -> Doc -> Doc
<+> [Doc] -> Doc
parenSep [Doc]
forall a. IsString a => [a]
extras)]
    -- rendered
    Inlines
renderedExpr <- Expr -> TCMT IO Inlines
forall c a.
(Render c, ToConcrete a, ConOfAbs a ~ c) =>
a -> TCMT IO Inlines
renderATop Expr
expr
    let renderedType :: Inlines
renderedType = (Inlines
renderedCtxName Inlines -> Inlines -> Inlines
forall a. Semigroup a => a -> a -> a
<> Inlines
renderedAttribute) Inlines -> Inlines -> Inlines
Render.<+> Inlines
":" Inlines -> Inlines -> Inlines
Render.<+> Inlines
renderedExpr Inlines -> Inlines -> Inlines
Render.<+> [Inlines] -> Inlines
parenSep2 [Inlines]
extras2
      -- (Render.fsep $ Render.punctuate "," extras)

    -- result
    let typeItem :: Block
typeItem = Inlines -> Maybe [Char] -> Maybe Range -> Block
Unlabeled Inlines
renderedType ([Char] -> Maybe [Char]
forall a. a -> Maybe a
Just [Char]
rawType) Maybe Range
forall a. Maybe a
Nothing

    [Block]
valueItem <- case Maybe Expr
letv of
      Maybe Expr
Nothing -> [Block] -> TCMT IO [Block]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return []
      Just Expr
val -> do
        Inlines
valText <- Expr -> TCMT IO Inlines
forall c a.
(Render c, ToConcrete a, ConOfAbs a ~ c) =>
a -> TCMT IO Inlines
renderATop Expr
val
        Doc
valString <- Expr -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyATop Expr
val
        let renderedValue :: Inlines
renderedValue = Name -> Inlines
forall a. Render a => a -> Inlines
Render.render Name
x Inlines -> Inlines -> Inlines
Render.<+> Inlines
"=" Inlines -> Inlines -> Inlines
Render.<+> Inlines
valText
        let rawValue :: [Char]
rawValue = Doc -> [Char]
forall a. Show a => a -> [Char]
show (Doc -> [Char]) -> Doc -> [Char]
forall a b. (a -> b) -> a -> b
$ Int -> [([Char], Doc)] -> Doc
align Int
10 [(Name -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow Name
x, Doc
"=" Doc -> Doc -> Doc
<+> Doc
valString)]
        [Block] -> TCMT IO [Block]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return
          [ Inlines -> Maybe [Char] -> Maybe Range -> Block
Unlabeled Inlines
renderedValue ([Char] -> Maybe [Char]
forall a. a -> Maybe a
Just [Char]
rawValue) Maybe Range
forall a. Maybe a
Nothing
          ]

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

    parenSep2 :: [Inlines] -> Inlines
    parenSep2 :: [Inlines] -> Inlines
parenSep2 [Inlines]
docs
      | [Inlines] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Inlines]
docs = Inlines
forall a. Monoid a => a
mempty
      | Bool
otherwise = (Inlines
" " Inlines -> Inlines -> Inlines
Render.<+>) (Inlines -> Inlines) -> Inlines -> Inlines
forall a b. (a -> b) -> a -> b
$ Inlines -> Inlines
Render.parens (Inlines -> Inlines) -> Inlines -> Inlines
forall a b. (a -> b) -> a -> b
$ [Inlines] -> Inlines
Render.fsep ([Inlines] -> Inlines) -> [Inlines] -> Inlines
forall a b. (a -> b) -> a -> b
$ Inlines -> [Inlines] -> [Inlines]
Render.punctuate Inlines
"," [Inlines]
docs


-- | Pretty-prints the type of the meta-variable.
prettyTypeOfMeta :: Rewrite -> InteractionId -> TCM (Inlines, String)
prettyTypeOfMeta :: Rewrite -> InteractionId -> TCM (Inlines, [Char])
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 -> do
      Inlines
rendered <- Expr -> TCMT IO Inlines
forall c a.
(Render c, ToConcrete a, ConOfAbs a ~ c) =>
a -> TCMT IO Inlines
renderATop Expr
e
      [Char]
raw <- Doc -> [Char]
forall a. Show a => a -> [Char]
show (Doc -> [Char]) -> TCMT IO Doc -> TCMT IO [Char]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyATop Expr
e
      (Inlines, [Char]) -> TCM (Inlines, [Char])
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Inlines
rendered, [Char]
raw)
    OutputConstraint Expr InteractionId
_ -> do
      Inlines
rendered <- OutputConstraint Expr InteractionId -> TCMT IO Inlines
forall c a.
(Render c, ToConcrete a, ConOfAbs a ~ c) =>
a -> TCMT IO Inlines
renderATop OutputConstraint Expr InteractionId
form
      [Char]
raw <- Doc -> [Char]
forall a. Show a => a -> [Char]
show (Doc -> [Char]) -> TCMT IO Doc -> TCMT IO [Char]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> OutputConstraint Expr InteractionId -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyATop OutputConstraint Expr InteractionId
form
      (Inlines, [Char]) -> TCM (Inlines, [Char])
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Inlines
rendered, [Char]
raw)

-- | 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