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.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.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 :: 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 String -> String
serialize = Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> (Lisp String -> Doc) -> Lisp String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lisp String -> 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 (m :: * -> *) a. Monad m => a -> m a
return Response
IR.ResponseClearHighlightingTokenBased
fromResponse (Resp_ClearHighlighting TokenBased
NotOnlyTokenBased) = Response -> TCM Response
forall (m :: * -> *) a. Monad m => a -> m a
return Response
IR.ResponseClearHighlightingNotOnlyTokenBased
fromResponse Response
Resp_DoneAborting = Response -> TCM Response
forall (m :: * -> *) a. Monad m => a -> m a
return Response
IR.ResponseDoneAborting
fromResponse Response
Resp_DoneExiting = Response -> TCM Response
forall (m :: * -> *) a. Monad m => a -> m a
return Response
IR.ResponseDoneExiting
fromResponse Response
Resp_ClearRunningInfo = Response -> TCM Response
forall (m :: * -> *) a. Monad m => a -> m a
return Response
IR.ResponseClearRunningInfo
fromResponse (Resp_RunningInfo Int
n String
s) = Response -> TCM Response
forall (m :: * -> *) a. Monad m => a -> m a
return (Response -> TCM Response) -> Response -> TCM Response
forall a b. (a -> b) -> a -> b
$ Int -> String -> Response
IR.ResponseRunningInfo Int
n String
s
fromResponse (Resp_Status Status
s) = Response -> TCM Response
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 String
f Int32
p) = Response -> TCM Response
forall (m :: * -> *) a. Monad m => a -> m a
return (Response -> TCM Response) -> Response -> TCM Response
forall a b. (a -> b) -> a -> b
$ String -> Int -> Response
IR.ResponseJumpToError String
f (Int32 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int32
p)
fromResponse (Resp_InteractionPoints [InteractionId]
is) =
  Response -> TCM Response
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 (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 (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 [String]
pcs) = Response -> TCM Response
forall (m :: * -> *) a. Monad m => a -> m a
return (Response -> TCM Response) -> Response -> TCM Response
forall a b. (a -> b) -> a -> b
$ [String] -> Response
IR.ResponseMakeCaseFunction [String]
pcs
fromResponse (Resp_MakeCase InteractionId
_ MakeCaseVariant
ExtendedLambda [String]
pcs) = Response -> TCM Response
forall (m :: * -> *) a. Monad m => a -> m a
return (Response -> TCM Response) -> Response -> TCM Response
forall a b. (a -> b) -> a -> b
$ [String] -> Response
IR.ResponseMakeCaseExtendedLambda [String]
pcs
fromResponse (Resp_SolveAll [(InteractionId, Expr)]
ps) = Response -> TCM Response
forall (m :: * -> *) a. Monad m => a -> m a
return (Response -> TCM Response) -> Response -> TCM Response
forall a b. (a -> b) -> a -> b
$ [(Int, String)] -> Response
IR.ResponseSolveAll (((InteractionId, Expr) -> (Int, String))
-> [(InteractionId, Expr)] -> [(Int, String)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (InteractionId, Expr) -> (Int, String)
forall a. Pretty a => (InteractionId, a) -> (Int, String)
prn [(InteractionId, Expr)]
ps)
  where
    prn :: (InteractionId, a) -> (Int, String)
prn (InteractionId Int
i, a
e) = (Int
i, a -> String
forall a. Pretty a => a -> String
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 (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 -> String -> Response
IR.ResponseHighlightingInfoIndirect (String -> Response) -> TCMT IO String -> TCM Response
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO String
indirect
  where
    fromAspects ::
      (Highlighting.Range, Aspects) ->
      IR.HighlightingInfo
    fromAspects :: (Range, Aspects) -> HighlightingInfo
fromAspects (Range
range, Aspects
aspects) =
      Int
-> Int
-> [String]
-> Bool
-> String
-> Maybe (String, Int)
-> HighlightingInfo
IR.HighlightingInfo
        (Range -> Int
Highlighting.from Range
range)
        (Range -> Int
Highlighting.to Range
range)
        (Aspects -> [String]
toAtoms Aspects
aspects)
        (Aspects -> TokenBased
tokenBased Aspects
aspects TokenBased -> TokenBased -> Bool
forall a. Eq a => a -> a -> Bool
== TokenBased
TokenBased)
        (Aspects -> String
note Aspects
aspects)
        (DefinitionSite -> (String, Int)
defSite (DefinitionSite -> (String, Int))
-> Maybe DefinitionSite -> Maybe (String, Int)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Aspects -> Maybe DefinitionSite
definitionSite Aspects
aspects)
      where
        defSite :: DefinitionSite -> (String, Int)
defSite (DefinitionSite TopLevelModuleName
moduleName Int
offset Bool
_ Maybe String
_) =
          (AbsolutePath -> String
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 (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 String
indirect = IO String -> TCMT IO String
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO String -> TCMT IO String) -> IO String -> TCMT IO String
forall a b. (a -> b) -> a -> b
$ String -> IO String
writeToTempFile (ByteString -> String
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 DisplayInfo
info = case DisplayInfo
info of
  Info_CompilationOk 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)
mapM TCWarning -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> 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)
mapM TCWarning -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [TCWarning]
filteredErrors
    DisplayInfo -> TCMT IO DisplayInfo
forall (m :: * -> *) a. Monad m => a -> m a
return (DisplayInfo -> TCMT IO DisplayInfo)
-> DisplayInfo -> TCMT IO DisplayInfo
forall a b. (a -> b) -> a -> b
$ [String] -> [String] -> DisplayInfo
IR.DisplayInfoCompilationOk ((Doc -> String) -> [Doc] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Doc -> String
forall a. Show a => a -> String
show [Doc]
warnings) ((Doc -> String) -> [Doc] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Doc -> String
forall a. Show a => a -> String
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 (m :: * -> *) a. Monad m => a -> m a
return (DisplayInfo -> TCMT IO DisplayInfo)
-> DisplayInfo -> TCMT IO DisplayInfo
forall a b. (a -> b) -> a -> b
$ String -> [Block] -> DisplayInfo
IR.DisplayInfoGeneric String
"Constraints" [Inlines -> Maybe String -> Maybe Range -> Block
Unlabeled (String -> Inlines
Render.text (String -> Inlines) -> String -> Inlines
forall a b. (a -> b) -> a -> b
$ Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> Doc -> String
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 (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 String
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)
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)
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)
mapM TCWarning -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> 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)
mapM TCWarning -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [TCWarning]
filteredErrors

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

    DisplayInfo -> TCMT IO DisplayInfo
forall (m :: * -> *) a. Monad m => a -> m a
return (DisplayInfo -> TCMT IO DisplayInfo)
-> DisplayInfo -> TCMT IO DisplayInfo
forall a b. (a -> b) -> a -> b
$ String -> [Block] -> [Block] -> [String] -> [String] -> DisplayInfo
IR.DisplayInfoAllGoalsWarnings (String
"*All" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
title String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"*") [Block]
goals [Block]
metas ((Doc -> String) -> [Doc] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Doc -> String
forall a. Show a => a -> String
show [Doc]
warnings) ((Doc -> String) -> [Doc] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Doc -> String
forall a. Show a => a -> String
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 -> TCM Inlines -> TCM Inlines
forall a. MetaId -> TCM a -> TCM a
withMetaId MetaId
i (TCM Inlines -> TCM Inlines) -> TCM Inlines -> TCM Inlines
forall a b. (a -> b) -> a -> b
$ OutputConstraint Expr NamedMeta -> TCM Inlines
forall c a.
(Render c, ToConcrete a, ConOfAbs a ~ c) =>
a -> TCM Inlines
renderATop OutputConstraint Expr NamedMeta
m
        String
serialized <- Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> TCMT IO Doc -> TCMT IO String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> TCMT IO Doc -> TCMT IO Doc
forall a. MetaId -> TCM a -> TCM 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 :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Range
getMetaRange MetaId
i

        Block -> TCMT IO Block
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 String -> Maybe Range -> Block
Unlabeled Inlines
meta (String -> Maybe String
forall a. a -> Maybe a
Just String
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 -> TCM Inlines -> TCM Inlines
forall a. InteractionId -> TCM a -> TCM 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) (TCM Inlines -> TCM Inlines) -> TCM Inlines -> TCM Inlines
forall a b. (a -> b) -> a -> b
$
            OutputConstraint Expr InteractionId -> TCM Inlines
forall c a.
(Render c, ToConcrete a, ConOfAbs a ~ c) =>
a -> TCM Inlines
renderATop OutputConstraint Expr InteractionId
i

        Doc
serialized <-
          InteractionId -> TCMT IO Doc -> TCMT IO Doc
forall a. InteractionId -> TCM a -> TCM 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 (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 String -> Maybe Range -> Block
Unlabeled Inlines
goal (String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ Doc -> String
forall a. Show a => a -> String
show Doc
serialized) Maybe Range
forall a. Maybe a
Nothing
  Info_Auto String
s -> DisplayInfo -> TCMT IO DisplayInfo
forall (m :: * -> *) a. Monad m => a -> m a
return (DisplayInfo -> TCMT IO DisplayInfo)
-> DisplayInfo -> TCMT IO DisplayInfo
forall a b. (a -> b) -> a -> b
$ String -> DisplayInfo
IR.DisplayInfoAuto String
s
  Info_Error Info_Error
err -> do
    String
s <- Info_Error -> TCMT IO String
showInfoError Info_Error
err
    DisplayInfo -> TCMT IO DisplayInfo
forall (m :: * -> *) a. Monad m => a -> m a
return (DisplayInfo -> TCMT IO DisplayInfo)
-> DisplayInfo -> TCMT IO DisplayInfo
forall a b. (a -> b) -> a -> b
$ String -> DisplayInfo
IR.DisplayInfoError String
s
  Info_Time CPUTime
s ->
    DisplayInfo -> TCMT IO DisplayInfo
forall (m :: * -> *) a. Monad m => a -> m a
return (DisplayInfo -> TCMT IO DisplayInfo)
-> DisplayInfo -> TCMT IO DisplayInfo
forall a b. (a -> b) -> a -> b
$ String -> DisplayInfo
IR.DisplayInfoTime (Doc -> String
forall a. Show a => a -> String
show (CPUTime -> Doc
prettyTimed CPUTime
s))
  Info_NormalForm CommandState
state ComputeMode
cmode Maybe CPUTime
time Expr
expr -> do
    Doc
exprDoc <- StateT CommandState TCM Doc -> CommandState -> TCMT IO 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
    DisplayInfo -> TCMT IO DisplayInfo
forall (m :: * -> *) a. Monad m => a -> m a
return (DisplayInfo -> TCMT IO DisplayInfo)
-> DisplayInfo -> TCMT IO DisplayInfo
forall a b. (a -> b) -> a -> b
$ String -> DisplayInfo
IR.DisplayInfoNormalForm (Doc -> String
forall a. Show a => a -> String
show Doc
doc)
    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
$
          TCMT IO Doc -> StateT CommandState TCM Doc
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO Doc -> StateT CommandState TCM Doc)
-> TCMT IO Doc -> StateT CommandState TCM 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 TCM Inlines -> CommandState -> TCM Inlines)
-> CommandState -> StateT CommandState TCM Inlines -> TCM Inlines
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT CommandState TCM Inlines -> CommandState -> TCM Inlines
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT CommandState
state (StateT CommandState TCM Inlines -> TCM Inlines)
-> StateT CommandState TCM Inlines -> TCM Inlines
forall a b. (a -> b) -> a -> b
$
        StateT CommandState TCM Inlines -> StateT CommandState TCM Inlines
forall a. CommandM a -> CommandM a
localStateCommandM (StateT CommandState TCM Inlines
 -> StateT CommandState TCM Inlines)
-> StateT CommandState TCM Inlines
-> StateT CommandState TCM Inlines
forall a b. (a -> b) -> a -> b
$
          TCM Inlines -> StateT CommandState TCM Inlines
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM Inlines -> StateT CommandState TCM Inlines)
-> TCM Inlines -> StateT CommandState TCM Inlines
forall a b. (a -> b) -> a -> b
$
            TCM Inlines -> TCM Inlines
forall a. TCM a -> TCM a
B.atTopLevel (TCM Inlines -> TCM Inlines) -> TCM Inlines -> TCM Inlines
forall a b. (a -> b) -> a -> b
$
              Expr -> TCM Inlines
forall c a.
(Render c, ToConcrete a, ConOfAbs a ~ c) =>
a -> TCM 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 TCM Doc -> CommandState -> TCMT IO Doc)
-> CommandState -> StateT CommandState TCM Doc -> TCMT IO Doc
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT CommandState TCM Doc -> CommandState -> TCMT IO Doc
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT CommandState
state (StateT CommandState TCM Doc -> TCMT IO Doc)
-> StateT CommandState TCM Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$
        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
$
          TCMT IO Doc -> StateT CommandState TCM Doc
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO Doc -> StateT CommandState TCM Doc)
-> TCMT IO Doc -> StateT CommandState TCM 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 :: String
raw = Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> Doc -> String
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 (m :: * -> *) a. Monad m => a -> m a
return (DisplayInfo -> TCMT IO DisplayInfo)
-> DisplayInfo -> TCMT IO DisplayInfo
forall a b. (a -> b) -> a -> b
$ String -> [Block] -> DisplayInfo
IR.DisplayInfoGeneric String
"Inferred Type" [Inlines -> Maybe String -> Maybe Range -> Block
Unlabeled Inlines
rendered (String -> Maybe String
forall a. a -> Maybe a
Just String
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
      [(String, Doc)]
typeDocs <- Telescope -> TCMT IO [(String, Doc)] -> TCMT IO [(String, Doc)]
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel (TCMT IO [(String, Doc)] -> TCMT IO [(String, Doc)])
-> TCMT IO [(String, Doc)] -> TCMT IO [(String, Doc)]
forall a b. (a -> b) -> a -> b
$
        [(Name, Type)]
-> ((Name, Type) -> TCMT IO (String, Doc))
-> TCMT IO [(String, Doc)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Name, Type)]
types (((Name, Type) -> TCMT IO (String, Doc))
 -> TCMT IO [(String, Doc)])
-> ((Name, Type) -> TCMT IO (String, Doc))
-> TCMT IO [(String, Doc)]
forall a b. (a -> b) -> a -> b
$ \(Name
x, Type
t) -> do
          Doc
doc <- Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
          (String, Doc) -> TCMT IO (String, Doc)
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> String
forall a. Pretty a => a -> String
prettyShow Name
x, Doc
":" Doc -> Doc -> Doc
<+> Doc
doc)
      Doc -> TCMT IO Doc
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 (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 -> [(String, Doc)] -> Doc
align Int
10 [(String, Doc)]
typeDocs
          ]
    DisplayInfo -> TCMT IO DisplayInfo
forall (m :: * -> *) a. Monad m => a -> m a
return (DisplayInfo -> TCMT IO DisplayInfo)
-> DisplayInfo -> TCMT IO DisplayInfo
forall a b. (a -> b) -> a -> b
$ String -> [Block] -> DisplayInfo
IR.DisplayInfoGeneric String
"Module contents" [Inlines -> Maybe String -> Maybe Range -> Block
Unlabeled (String -> Inlines
Render.text (String -> Inlines) -> String -> Inlines
forall a b. (a -> b) -> a -> b
$ Doc -> String
forall a. Show a => a -> String
show Doc
doc) Maybe String
forall a. Maybe a
Nothing Maybe Range
forall a. Maybe a
Nothing]
  Info_SearchAbout [(Name, Type)]
hits String
names -> do
    [(String, Doc)]
hitDocs <- [(Name, Type)]
-> ((Name, Type) -> TCMT IO (String, Doc))
-> TCMT IO [(String, Doc)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Name, Type)]
hits (((Name, Type) -> TCMT IO (String, Doc))
 -> TCMT IO [(String, Doc)])
-> ((Name, Type) -> TCMT IO (String, Doc))
-> TCMT IO [(String, Doc)]
forall a b. (a -> b) -> a -> b
$ \(Name
x, Type
t) -> do
      Doc
doc <- Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
      (String, Doc) -> TCMT IO (String, Doc)
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> String
forall a. Pretty a => a -> String
prettyShow Name
x, Doc
":" Doc -> Doc -> Doc
<+> Doc
doc)
    let doc :: Doc
doc =
          Doc
"Definitions about"
            Doc -> Doc -> Doc
<+> String -> Doc
text (String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
List.intercalate String
", " ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ String -> [String]
words String
names) Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
nest Int
2 (Int -> [(String, Doc)] -> Doc
align Int
10 [(String, Doc)]
hitDocs)
    DisplayInfo -> TCMT IO DisplayInfo
forall (m :: * -> *) a. Monad m => a -> m a
return (DisplayInfo -> TCMT IO DisplayInfo)
-> DisplayInfo -> TCMT IO DisplayInfo
forall a b. (a -> b) -> a -> b
$ String -> [Block] -> DisplayInfo
IR.DisplayInfoGeneric String
"Search About" [Inlines -> Maybe String -> Maybe Range -> Block
Unlabeled (String -> Inlines
Render.text (String -> Inlines) -> String -> Inlines
forall a b. (a -> b) -> a -> b
$ Doc -> String
forall a. Show a => a -> String
show Doc
doc) Maybe String
forall a. Maybe a
Nothing Maybe Range
forall a. Maybe a
Nothing]
  Info_WhyInScope String
s String
cwd Maybe LocalVar
v [AbstractName]
xs [AbstractModule]
ms -> do
    Doc
doc <- String
-> String
-> Maybe LocalVar
-> [AbstractName]
-> [AbstractModule]
-> TCMT IO Doc
explainWhyInScope String
s String
cwd Maybe LocalVar
v [AbstractName]
xs [AbstractModule]
ms
    DisplayInfo -> TCMT IO DisplayInfo
forall (m :: * -> *) a. Monad m => a -> m a
return (DisplayInfo -> TCMT IO DisplayInfo)
-> DisplayInfo -> TCMT IO DisplayInfo
forall a b. (a -> b) -> a -> b
$ String -> [Block] -> DisplayInfo
IR.DisplayInfoGeneric String
"Scope Info" [Inlines -> Maybe String -> Maybe Range -> Block
Unlabeled (String -> Inlines
Render.text (String -> Inlines) -> String -> Inlines
forall a b. (a -> b) -> a -> b
$ Doc -> String
forall a. Show a => a -> String
show Doc
doc) Maybe String
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 (m :: * -> *) a. Monad m => a -> m a
return (DisplayInfo -> TCMT IO DisplayInfo)
-> DisplayInfo -> TCMT IO DisplayInfo
forall a b. (a -> b) -> a -> b
$ String -> [Block] -> DisplayInfo
IR.DisplayInfoGeneric String
"Context" [Inlines -> Maybe String -> Maybe Range -> Block
Unlabeled (String -> Inlines
Render.text (String -> Inlines) -> String -> Inlines
forall a b. (a -> b) -> a -> b
$ Doc -> String
forall a. Show a => a -> String
show Doc
doc) Maybe String
forall a. Maybe a
Nothing Maybe Range
forall a. Maybe a
Nothing]
  DisplayInfo
Info_Intro_NotFound ->
    DisplayInfo -> TCMT IO DisplayInfo
forall (m :: * -> *) a. Monad m => a -> m a
return (DisplayInfo -> TCMT IO DisplayInfo)
-> DisplayInfo -> TCMT IO DisplayInfo
forall a b. (a -> b) -> a -> b
$ String -> [Block] -> DisplayInfo
IR.DisplayInfoGeneric String
"Intro" [Inlines -> Maybe String -> Maybe Range -> Block
Unlabeled (String -> Inlines
Render.text String
"No introduction forms found.") Maybe String
forall a. Maybe a
Nothing Maybe Range
forall a. Maybe a
Nothing]
  Info_Intro_ConstructorUnknown [String]
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 :: [String] -> [Doc]
mkOr [] = []
                  mkOr [String
x, String
y] = [String -> Doc
text String
x Doc -> Doc -> Doc
<+> Doc
"or" Doc -> Doc -> Doc
<+> String -> Doc
text String
y]
                  mkOr (String
x : [String]
xs) = String -> Doc
text String
x Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: [String] -> [Doc]
mkOr [String]
xs
               in Int -> Doc -> Doc
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
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 ([String] -> [Doc]
mkOr [String]
ss)
            ]
    DisplayInfo -> TCMT IO DisplayInfo
forall (m :: * -> *) a. Monad m => a -> m a
return (DisplayInfo -> TCMT IO DisplayInfo)
-> DisplayInfo -> TCMT IO DisplayInfo
forall a b. (a -> b) -> a -> b
$ String -> [Block] -> DisplayInfo
IR.DisplayInfoGeneric String
"Intro" [Inlines -> Maybe String -> Maybe Range -> Block
Unlabeled (String -> Inlines
Render.text (String -> Inlines) -> String -> Inlines
forall a b. (a -> b) -> a -> b
$ Doc -> String
forall a. Show a => a -> String
show Doc
doc) Maybe String
forall a. Maybe a
Nothing Maybe Range
forall a. Maybe a
Nothing]
  DisplayInfo
Info_Version ->
    DisplayInfo -> TCMT IO DisplayInfo
forall (m :: * -> *) a. Monad m => a -> m a
return (DisplayInfo -> TCMT IO DisplayInfo)
-> DisplayInfo -> TCMT IO DisplayInfo
forall a b. (a -> b) -> a -> b
$ String -> [Block] -> DisplayInfo
IR.DisplayInfoGeneric String
"Agda Version" [Inlines -> Maybe String -> Maybe Range -> Block
Unlabeled (String -> Inlines
Render.text (String -> Inlines) -> String -> Inlines
forall a b. (a -> b) -> a -> b
$ String
"Agda version " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
versionWithCommitInfo) Maybe String
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 a. InteractionId -> TCM a -> TCM a
B.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 (m :: * -> *) a. Monad m => a -> m a
return (DisplayInfo -> TCMT IO DisplayInfo)
-> DisplayInfo -> TCMT IO DisplayInfo
forall a b. (a -> b) -> a -> b
$ String -> [Block] -> DisplayInfo
IR.DisplayInfoGeneric String
"Helper function" [Inlines -> Maybe String -> Maybe Range -> Block
Unlabeled (String -> Inlines
Render.text (String -> Inlines) -> String -> Inlines
forall a b. (a -> b) -> a -> b
$ Doc -> String
forall a. Show a => a -> String
show Doc
doc String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n") Maybe String
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 (m :: * -> *) a. Monad m => a -> m a
return (DisplayInfo -> TCMT IO DisplayInfo)
-> DisplayInfo -> TCMT IO DisplayInfo
forall a b. (a -> b) -> a -> b
$ String -> [Block] -> DisplayInfo
IR.DisplayInfoGeneric String
"Normal Form" [Inlines -> Maybe String -> Maybe Range -> Block
Unlabeled (String -> Inlines
Render.text (String -> Inlines) -> String -> Inlines
forall a b. (a -> b) -> a -> b
$ Doc -> String
forall a. Show a => a -> String
show Doc
doc) Maybe String
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, String
raw) <- Rewrite -> InteractionId -> TCM (Inlines, String)
prettyTypeOfMeta Rewrite
norm InteractionId
ii
          [Block] -> TCMT IO [Block]
forall (m :: * -> *) a. Monad m => a -> m a
return [Inlines -> Maybe String -> Maybe Range -> String -> String -> Block
Labeled Inlines
rendered (String -> Maybe String
forall a. a -> Maybe a
Just String
raw) Maybe Range
forall a. Maybe a
Nothing String
"Goal" String
"special"]

        [Block]
auxSect <- case GoalTypeAux
aux of
          GoalTypeAux
GoalOnly -> [Block] -> TCMT IO [Block]
forall (m :: * -> *) a. Monad m => a -> m a
return []
          GoalAndHave Expr
expr -> do
            Inlines
rendered <- Expr -> TCM Inlines
forall c a.
(Render c, ToConcrete a, ConOfAbs a ~ c) =>
a -> TCM Inlines
renderATop Expr
expr
            String
raw <- Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> TCMT IO Doc -> TCMT IO String
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 (m :: * -> *) a. Monad m => a -> m a
return [Inlines -> Maybe String -> Maybe Range -> String -> String -> Block
Labeled Inlines
rendered (String -> Maybe String
forall a. a -> Maybe a
Just String
raw) Maybe Range
forall a. Maybe a
Nothing String
"Have" String
"special"]
          GoalAndElaboration Term
term -> do
            let rendered :: Inlines
rendered = Term -> Inlines
forall a. Render a => a -> Inlines
render Term
term
            String
raw <- Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> TCMT IO Doc -> TCMT IO String
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
TCP.prettyTCM Term
term
            [Block] -> TCMT IO [Block]
forall (m :: * -> *) a. Monad m => a -> m a
return [Inlines -> Maybe String -> Maybe Range -> String -> String -> Block
Labeled Inlines
rendered (String -> Maybe String
forall a. a -> Maybe a
Just String
raw) Maybe Range
forall a. Maybe a
Nothing String
"Elaborates to" String
"special"]
        let boundarySect :: [Block]
boundarySect =
              if [IPBoundary' Expr] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [IPBoundary' Expr]
boundaries
                then []
                else
                  String -> Block
Header String
"Boundary" Block -> [Block] -> [Block]
forall a. a -> [a] -> [a]
:
                  (IPBoundary' Expr -> Block) -> [IPBoundary' Expr] -> [Block]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\IPBoundary' Expr
boundary -> Inlines -> Maybe String -> Maybe Range -> Block
Unlabeled (IPBoundary' Expr -> Inlines
forall a. Render a => a -> Inlines
render IPBoundary' Expr
boundary) (String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> Doc -> String
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)
mapM (InteractionId -> ResponseContextEntry -> TCMT IO [Block]
renderResponseContext InteractionId
ii) [ResponseContextEntry]
resCtxs
        let constraintSect :: [Block]
constraintSect =
                if [OutputForm Expr Expr] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [OutputForm Expr Expr]
constraints
                  then []
                  else
                    String -> Block
Header String
"Constraints" Block -> [Block] -> [Block]
forall a. a -> [a] -> [a]
:
                    (OutputForm Expr Expr -> Block)
-> [OutputForm Expr Expr] -> [Block]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\OutputForm Expr Expr
constraint -> Inlines -> Maybe String -> Maybe Range -> Block
Unlabeled (OutputForm Expr Expr -> Inlines
forall a. Render a => a -> Inlines
render OutputForm Expr Expr
constraint) (String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> Doc -> String
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 (m :: * -> *) a. Monad m => a -> m a
return (DisplayInfo -> TCMT IO DisplayInfo)
-> DisplayInfo -> TCMT IO DisplayInfo
forall a b. (a -> b) -> a -> b
$
          String -> [Block] -> DisplayInfo
IR.DisplayInfoGeneric String
"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, String
raw) <- Rewrite -> InteractionId -> TCM (Inlines, String)
prettyTypeOfMeta Rewrite
norm InteractionId
ii
        DisplayInfo -> TCMT IO DisplayInfo
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 String -> Maybe Range -> Block
Unlabeled Inlines
rendered (String -> Maybe String
forall a. a -> Maybe a
Just String
raw) Maybe Range
forall a. Maybe a
Nothing)
      Goal_InferredType Expr
expr -> do
        Inlines
rendered <- Expr -> TCM Inlines
forall c a.
(Render c, ToConcrete a, ConOfAbs a ~ c) =>
a -> TCM Inlines
renderATop Expr
expr
        String
raw <- Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> TCMT IO Doc -> TCMT IO String
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 (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 String -> Maybe Range -> Block
Unlabeled Inlines
rendered (String -> Maybe String
forall a. a -> Maybe a
Just String
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 String
showInfoError (Info_GenericError TCErr
err) = do
  String
e <- TCErr -> TCMT IO String
forall (tcm :: * -> *). MonadTCM tcm => TCErr -> tcm String
prettyError TCErr
err
  [String]
w <- [TCWarning] -> TCM [String]
prettyTCWarnings' ([TCWarning] -> TCM [String])
-> TCMT IO [TCWarning] -> TCM [String]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCErr -> TCMT IO [TCWarning]
getAllWarningsOfTCErr TCErr
err

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

explainWhyInScope ::
  FilePath ->
  String ->
  Maybe LocalVar ->
  [AbstractName] ->
  [AbstractModule] ->
  TCM Doc
explainWhyInScope :: String
-> String
-> Maybe LocalVar
-> [AbstractName]
-> [AbstractModule]
-> TCMT IO Doc
explainWhyInScope String
s String
_ Maybe LocalVar
Nothing [] [] = String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
TCP.text (String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" is not in scope.")
explainWhyInScope String
s String
_ Maybe LocalVar
v [AbstractName]
xs [AbstractModule]
ms =
  [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
TCP.vcat
    [ String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
TCP.text (String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" 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 (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
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 (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 (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.<+> String -> TCMT IO Doc
forall (m :: * -> *). Applicative 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 -> 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.<+> String -> TCMT IO Doc
forall (m :: * -> *). Applicative 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 -> 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
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
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
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
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
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
  [[(String, Doc)]]
rows <- (ResponseContextEntry -> TCMT IO [(String, Doc)])
-> [ResponseContextEntry] -> TCMT IO [[(String, Doc)]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (InteractionId -> ResponseContextEntry -> TCMT IO [(String, Doc)]
prettyResponseContext InteractionId
ii) [ResponseContextEntry]
ctxs
  Doc -> TCMT IO Doc
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 -> [(String, Doc)] -> Doc
align Int
10 ([(String, Doc)] -> Doc) -> [(String, Doc)] -> Doc
forall a b. (a -> b) -> a -> b
$ [[(String, Doc)]] -> [(String, Doc)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[(String, Doc)]] -> [(String, Doc)])
-> [[(String, Doc)]] -> [(String, Doc)]
forall a b. (a -> b) -> a -> b
$ 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)]]
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 [(String, Doc)]
prettyResponseContext InteractionId
ii (ResponseContextEntry Name
n Name
x (Arg ArgInfo
ai Expr
expr) Maybe Expr
letv NameInScope
nis) = InteractionId -> TCMT IO [(String, Doc)] -> TCMT IO [(String, Doc)]
forall a. InteractionId -> TCM a -> TCM a
withInteractionId InteractionId
ii (TCMT IO [(String, Doc)] -> TCMT IO [(String, Doc)])
-> TCMT IO [(String, Doc)] -> TCMT IO [(String, 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 :: String
prettyCtxName
          | Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
x = Name -> String
forall a. Pretty a => a -> String
prettyShow Name
x
          | Name -> NameInScope
forall a. LensInScope a => a -> NameInScope
isInScope Name
n NameInScope -> NameInScope -> Bool
forall a. Eq a => a -> a -> Bool
== NameInScope
InScope = Name -> String
forall a. Pretty a => a -> String
prettyShow Name
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Pretty a => a -> String
prettyShow Name
x
          | Bool
otherwise = Name -> String
forall a. Pretty a => a -> String
prettyShow Name
x

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

        extras :: [Doc]
        extras :: [Doc]
extras =
          [[Doc]] -> [Doc]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
            [ [Doc
"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

    [(String, Doc)]
letv' <- case Maybe Expr
letv of
      Maybe Expr
Nothing -> [(String, Doc)] -> TCMT IO [(String, Doc)]
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
        [(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
val')]

    [(String, Doc)] -> TCMT IO [(String, Doc)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(String, Doc)] -> TCMT IO [(String, Doc)])
-> [(String, Doc)] -> TCMT IO [(String, Doc)]
forall a b. (a -> b) -> a -> b
$
      (String
attribute String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
prettyCtxName, Doc
":" Doc -> Doc -> Doc
<+> Doc
ty Doc -> Doc -> Doc
<+> [Doc] -> Doc
parenSep [Doc]
extras) (String, Doc) -> [(String, Doc)] -> [(String, Doc)]
forall a. a -> [a] -> [a]
: [(String, Doc)]
letv'
  where
    parenSep :: [Doc] -> Doc
    parenSep :: [Doc] -> Doc
parenSep [Doc]
docs
      | [Doc] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Doc]
docs = Doc
forall a. Null a => a
empty
      | Bool
otherwise = (Doc
" " Doc -> Doc -> Doc
<+>) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
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 a. InteractionId -> TCM a -> TCM 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 :: String
rawCtxName
          | Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
x = Name -> String
forall a. Pretty a => a -> String
prettyShow Name
x
          | Name -> NameInScope
forall a. LensInScope a => a -> NameInScope
isInScope Name
n NameInScope -> NameInScope -> Bool
forall a. Eq a => a -> a -> Bool
== NameInScope
InScope = Name -> String
forall a. Pretty a => a -> String
prettyShow Name
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Pretty a => a -> String
prettyShow Name
x
          | Bool
otherwise = Name -> String
forall a. Pretty a => a -> String
prettyShow Name
x

        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 :: String
rawAttribute = String
c String -> String -> String
forall a. [a] -> [a] -> [a]
++ if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
c then String
"" else String
" "
          where
            c :: String
c = Cohesion -> String
forall a. Pretty a => a -> String
prettyShow (ArgInfo -> Cohesion
forall a. LensCohesion a => a -> Cohesion
getCohesion ArgInfo
ai)

        renderedAttribute :: Inlines
        renderedAttribute :: Inlines
renderedAttribute = Inlines
c Inlines -> Inlines -> Inlines
forall a. Semigroup a => a -> a -> a
<> if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Inlines -> String
forall a. Show a => a -> String
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 :: [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 :: String
rawType = Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ Int -> [(String, Doc)] -> Doc
align Int
10 [(String
rawAttribute String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
rawCtxName, Doc
":" Doc -> Doc -> Doc
<+> Doc
rawExpr Doc -> Doc -> Doc
<+> [Doc] -> Doc
parenSep [Doc]
forall a. IsString a => [a]
extras)]
    -- rendered  
    Inlines
renderedExpr <- Expr -> TCM Inlines
forall c a.
(Render c, ToConcrete a, ConOfAbs a ~ c) =>
a -> TCM 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 String -> Maybe Range -> Block
Unlabeled Inlines
renderedType (String -> Maybe String
forall a. a -> Maybe a
Just String
rawType) Maybe Range
forall a. Maybe a
Nothing

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

    [Block] -> TCMT IO [Block]
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 (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 (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, String)
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 -> TCM Inlines
forall c a.
(Render c, ToConcrete a, ConOfAbs a ~ c) =>
a -> TCM Inlines
renderATop Expr
e
      String
raw <- Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> TCMT IO Doc -> TCMT IO String
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, String) -> TCM (Inlines, String)
forall (m :: * -> *) a. Monad m => a -> m a
return (Inlines
rendered, String
raw)
    OutputConstraint Expr InteractionId
_ -> do
      Inlines
rendered <- OutputConstraint Expr InteractionId -> TCM Inlines
forall c a.
(Render c, ToConcrete a, ConOfAbs a ~ c) =>
a -> TCM Inlines
renderATop OutputConstraint Expr InteractionId
form
      String
raw <- Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> TCMT IO Doc -> TCMT IO String
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, String) -> TCM (Inlines, String)
forall (m :: * -> *) a. Monad m => a -> m a
return (Inlines
rendered, String
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