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.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 = forall a. Show a => a -> [Char]
show forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DisplayInfo -> TCM DisplayInfo
fromDisplayInfo DisplayInfo
info
fromResponse (Resp_ClearHighlighting TokenBased
TokenBased) = forall (m :: * -> *) a. Monad m => a -> m a
return Response
IR.ResponseClearHighlightingTokenBased
fromResponse (Resp_ClearHighlighting TokenBased
NotOnlyTokenBased) = forall (m :: * -> *) a. Monad m => a -> m a
return Response
IR.ResponseClearHighlightingNotOnlyTokenBased
fromResponse Response
Resp_DoneAborting = forall (m :: * -> *) a. Monad m => a -> m a
return Response
IR.ResponseDoneAborting
fromResponse Response
Resp_DoneExiting = forall (m :: * -> *) a. Monad m => a -> m a
return Response
IR.ResponseDoneExiting
fromResponse Response
Resp_ClearRunningInfo = forall (m :: * -> *) a. Monad m => a -> m a
return Response
IR.ResponseClearRunningInfo
fromResponse (Resp_RunningInfo Int
n [Char]
s) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Int -> [Char] -> Response
IR.ResponseRunningInfo Int
n [Char]
s
fromResponse (Resp_Status Status
s) = forall (m :: * -> *) a. Monad m => a -> m a
return 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) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Char] -> Int -> Response
IR.ResponseJumpToError [Char]
f (forall a b. (Integral a, Num b) => a -> b
fromIntegral Int32
p)
fromResponse (Resp_InteractionPoints [InteractionId]
is) =
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Int] -> Response
IR.ResponseInteractionPoints (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) =
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Int -> GiveResult -> Response
IR.ResponseGiveAction Int
i (forall a b. FromAgda a b => a -> b
fromAgda GiveResult
giveAction)
fromResponse (Resp_MakeCase InteractionId
_ MakeCaseVariant
Function [[Char]]
pcs) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [[Char]] -> Response
IR.ResponseMakeCaseFunction [[Char]]
pcs
fromResponse (Resp_MakeCase InteractionId
_ MakeCaseVariant
ExtendedLambda [[Char]]
pcs) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [[Char]] -> Response
IR.ResponseMakeCaseExtendedLambda [[Char]]
pcs
fromResponse (Resp_SolveAll [(InteractionId, Expr)]
ps) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [(Int, [Char])] -> Response
IR.ResponseSolveAll (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap 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, 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ HighlightingInfos -> Response
IR.ResponseHighlightingInfoDirect HighlightingInfos
info
    HighlightingMethod
Indirect -> [Char] -> Response
IR.ResponseHighlightingInfoIndirect forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM [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 forall a. Eq a => a -> a -> Bool
== TokenBased
TokenBased)
        (Aspects -> [Char]
note Aspects
aspects)
        (DefinitionSite -> ([Char], Int)
defSite 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 (forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault forall a. HasCallStack => a
__IMPOSSIBLE__ TopLevelModuleName
moduleName ModuleToSource
modFile), Int
offset)

    infos :: [IR.HighlightingInfo]
    infos :: [HighlightingInfo]
infos = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Range, Aspects) -> HighlightingInfo
fromAspects (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 :: TCM [Char]
indirect = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ [Char] -> IO [Char]
writeToTempFile (ByteString -> [Char]
BS8.unpack (forall a. ToJSON a => a -> ByteString
JSON.encode HighlightingInfos
info))

fromDisplayInfo :: DisplayInfo -> TCM IR.DisplayInfo
fromDisplayInfo :: DisplayInfo -> TCM 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 <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [TCWarning]
filteredWarnings
    [Doc]
errors <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [TCWarning]
filteredErrors
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [[Char]] -> [[Char]] -> DisplayInfo
IR.DisplayInfoCompilationOk (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Show a => a -> [Char]
show [Doc]
warnings) (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap 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
    forall (m :: * -> *) a. Monad m => a -> m a
return 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 forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> [Char]
show forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Pretty a => a -> Doc
pretty [OutputForm Expr Expr]
s) forall a. Maybe a
Nothing forall a. Maybe a
Nothing]
  Info_AllGoalsWarnings ([OutputConstraint Expr InteractionId]
ims, [OutputConstraint Expr NamedMeta]
hms) WarningsAndNonFatalErrors
ws -> do
    -- visible metas (goals)
    [Block]
goals <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM OutputConstraint Expr InteractionId -> TCM Block
convertGoal [OutputConstraint Expr InteractionId]
ims
    -- hidden (unsolved) metas
    [Block]
metas <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM OutputConstraint Expr NamedMeta -> TCM 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 <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [TCWarning]
filteredWarnings
    [Doc]
errors <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [TCWarning]
filteredErrors

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

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

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

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

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

lispifyGoalSpecificDisplayInfo :: InteractionId -> GoalDisplayInfo -> TCM IR.DisplayInfo
lispifyGoalSpecificDisplayInfo :: InteractionId -> GoalDisplayInfo -> TCM DisplayInfo
lispifyGoalSpecificDisplayInfo InteractionId
ii GoalDisplayInfo
kind = forall a. TCM a -> TCM a
localTCState forall a b. (a -> b) -> a -> b
$
  forall (m :: * -> *) a.
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m,
 MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
ii forall a b. (a -> b) -> a -> b
$
    case GoalDisplayInfo
kind of
      Goal_HelperFunction OutputConstraint' Expr Expr
helperType -> do
        Doc
doc <- forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyATop OutputConstraint' Expr Expr
helperType
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Char] -> [Block] -> DisplayInfo
IR.DisplayInfoGeneric [Char]
"Helper function" [Inlines -> Maybe [Char] -> Maybe Range -> Block
Unlabeled ([Char] -> Inlines
Render.text forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> [Char]
show Doc
doc forall a. [a] -> [a] -> [a]
++ [Char]
"\n") forall a. Maybe a
Nothing forall a. Maybe a
Nothing]
      Goal_NormalForm ComputeMode
cmode Expr
expr -> do
        Doc
doc <- ComputeMode -> Expr -> TCMT IO Doc
showComputed ComputeMode
cmode Expr
expr
        forall (m :: * -> *) a. Monad m => a -> m a
return 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 forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> [Char]
show Doc
doc) forall a. Maybe a
Nothing 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
          forall (m :: * -> *) a. Monad m => a -> m a
return [Inlines -> Maybe [Char] -> Maybe Range -> [Char] -> [Char] -> Block
Labeled Inlines
rendered (forall a. a -> Maybe a
Just [Char]
raw) forall a. Maybe a
Nothing [Char]
"Goal" [Char]
"special"]

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

        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
          [Char] -> [Block] -> DisplayInfo
IR.DisplayInfoGeneric [Char]
"Goal type etc" forall a b. (a -> b) -> a -> b
$ [Block]
goalSect forall a. [a] -> [a] -> [a]
++ [Block]
auxSect forall a. [a] -> [a] -> [a]
++ [Block]
boundarySect forall a. [a] -> [a] -> [a]
++ [Block]
contextSect 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
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Block -> DisplayInfo
IR.DisplayInfoCurrentGoal (Inlines -> Maybe [Char] -> Maybe Range -> Block
Unlabeled Inlines
rendered (forall a. a -> Maybe a
Just [Char]
raw) forall a. Maybe a
Nothing)
      Goal_InferredType Expr
expr -> do
        Inlines
rendered <- forall c a.
(Render c, ToConcrete a, ConOfAbs a ~ c) =>
a -> TCMT IO Inlines
renderATop Expr
expr
        [Char]
raw <- forall a. Show a => a -> [Char]
show forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyATop Expr
expr
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Block -> DisplayInfo
IR.DisplayInfoInferredType (Inlines -> Maybe [Char] -> Maybe Range -> Block
Unlabeled Inlines
rendered (forall a. a -> Maybe a
Just [Char]
raw) 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 -> TCM [Char]
showInfoError (Info_GenericError TCErr
err) = do
  [Char]
e <- forall (tcm :: * -> *). MonadTCM tcm => TCErr -> tcm [Char]
prettyError TCErr
err
  [[Char]]
w <- [TCWarning] -> TCMT IO [[Char]]
prettyTCWarnings' forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCErr -> TCM [TCWarning]
getAllWarningsOfTCErr TCErr
err

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

explainWhyInScope ::
  FilePath ->
  String ->
  Maybe LocalVar ->
  [AbstractName] ->
  [AbstractModule] ->
  TCM Doc
explainWhyInScope :: [Char]
-> [Char]
-> Maybe LocalVar
-> [AbstractName]
-> [AbstractModule]
-> TCMT IO Doc
explainWhyInScope [Char]
s [Char]
_ Maybe LocalVar
Nothing [] [] = forall (m :: * -> *). Applicative m => [Char] -> m Doc
TCP.text ([Char]
s forall a. [a] -> [a] -> [a]
++ [Char]
" is not in scope.")
explainWhyInScope [Char]
s [Char]
_ Maybe LocalVar
v [AbstractName]
xs [AbstractModule]
ms =
  forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
TCP.vcat
    [ forall (m :: * -> *). Applicative m => [Char] -> m Doc
TCP.text ([Char]
s forall a. [a] -> [a] -> [a]
++ [Char]
" is in scope as"),
      forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
TCP.nest Int
2 forall a b. (a -> b) -> a -> b
$ 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
      | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [AbstractName]
vs = TCMT IO Doc
asVar
      | Bool
otherwise =
        forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
TCP.vcat
          [ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
TCP.sep [TCMT IO Doc
asVar, forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
TCP.nest Int
2 forall a b. (a -> b) -> a -> b
$ LocalVar -> TCMT IO Doc
shadowing LocalVar
x],
            forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
TCP.nest Int
2 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" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TCP.<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
TCP.prettyTCM (Name -> Range
nameBindingSite 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 = forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
TCP.vcat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap AbstractName -> TCMT IO Doc
pName
    modules :: [AbstractModule] -> TCMT IO Doc
modules = forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
TCP.vcat forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 =
      forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
TCP.sep
        [ TCMT IO Doc
"* a"
            forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TCP.<+> KindOfName -> TCMT IO Doc
pKind (AbstractName -> KindOfName
anameKind AbstractName
a)
            forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TCP.<+> forall (m :: * -> *). Applicative m => [Char] -> m Doc
TCP.text (forall a. Pretty a => a -> [Char]
prettyShow forall a b. (a -> b) -> a -> b
$ AbstractName -> QName
anameName AbstractName
a),
          forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
TCP.nest Int
2 TCMT IO Doc
"brought into scope by"
        ]
        forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TCP.$$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
TCP.nest Int
2 (Range -> WhyInScope -> TCMT IO Doc
pWhy (Name -> Range
nameBindingSite forall a b. (a -> b) -> a -> b
$ QName -> Name
qnameName 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 =
      forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
TCP.sep
        [ TCMT IO Doc
"* a module" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TCP.<+> forall (m :: * -> *). Applicative m => [Char] -> m Doc
TCP.text (forall a. Pretty a => a -> [Char]
prettyShow forall a b. (a -> b) -> a -> b
$ AbstractModule -> ModuleName
amodName AbstractModule
a),
          forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
TCP.nest Int
2 TCMT IO Doc
"brought into scope by"
        ]
        forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TCP.$$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
TCP.nest Int
2 (Range -> WhyInScope -> TCMT IO Doc
pWhy (Name -> Range
nameBindingSite forall a b. (a -> b) -> a -> b
$ QName -> Name
qnameName forall a b. (a -> b) -> a -> b
$ ModuleName -> QName
mnameToQName 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" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TCP.<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
TCP.prettyTCM Range
r
    pWhy Range
r (Opened (C.QName Name
x) WhyInScope
w) | 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"
        forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TCP.<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
TCP.prettyTCM QName
m
        forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TCP.<+> TCMT IO Doc
"at"
        forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TCP.<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
TCP.prettyTCM (forall a. HasRange a => a -> Range
getRange QName
m)
        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"
        forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TCP.<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
TCP.prettyTCM QName
m
        forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TCP.<+> TCMT IO Doc
"at"
        forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TCP.<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
TCP.prettyTCM (forall a. HasRange a => a -> Range
getRange QName
m)
        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 <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (InteractionId -> ResponseContextEntry -> TCMT IO [([Char], Doc)]
prettyResponseContext InteractionId
ii) [ResponseContextEntry]
ctxs
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Int -> [([Char], Doc)] -> Doc
align Int
10 forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall a b. (a -> b) -> a -> b
$ forall a. Bool -> (a -> a) -> a -> a
applyWhen Bool
rev 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) = forall (m :: * -> *) a.
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m,
 MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
ii forall a b. (a -> b) -> a -> b
$ do
  Modality
modality <- forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC forall a. LensModality a => a -> Modality
getModality
  do
    let prettyCtxName :: String
        prettyCtxName :: [Char]
prettyCtxName
          | Name
n forall a. Eq a => a -> a -> Bool
== Name
x = forall a. Pretty a => a -> [Char]
prettyShow Name
x
          | forall a. LensInScope a => a -> NameInScope
isInScope Name
n forall a. Eq a => a -> a -> Bool
== NameInScope
InScope = forall a. Pretty a => a -> [Char]
prettyShow Name
n forall a. [a] -> [a] -> [a]
++ [Char]
" = " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow Name
x
          | Bool
otherwise = forall a. Pretty a => a -> [Char]
prettyShow Name
x

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

        extras :: [Doc]
        extras :: [Doc]
extras =
          forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
            [ [Doc
"not in scope" | forall a. LensInScope a => a -> NameInScope
isInScope NameInScope
nis forall a. Eq a => a -> a -> Bool
== NameInScope
C.NotInScope],
              -- Print erased if hypothesis is erased by goal is non-erased.
              [Doc
"erased" | Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall a. LensQuantity a => a -> Quantity
getQuantity ArgInfo
ai Quantity -> Quantity -> Bool
`moreQuantity` forall a. LensQuantity a => a -> Quantity
getQuantity Modality
modality],
              -- Print irrelevant if hypothesis is strictly less relevant than goal.
              [Doc
"irrelevant" | Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall a. LensRelevance a => a -> Relevance
getRelevance ArgInfo
ai Relevance -> Relevance -> Bool
`moreRelevant` forall a. LensRelevance a => a -> Relevance
getRelevance Modality
modality],
              -- Print instance if variable is considered by instance search
              [Doc
"instance" | forall a. LensHiding a => a -> Bool
isInstance ArgInfo
ai]
            ]
    Doc
ty <- forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyATop Expr
expr

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

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

-- | 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) = forall (m :: * -> *) a.
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m,
 MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
ii forall a b. (a -> b) -> a -> b
$ do
  Modality
modality <- forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC forall a. LensModality a => a -> Modality
getModality
  do
    let
        rawCtxName :: String
        rawCtxName :: [Char]
rawCtxName
          | Name
n forall a. Eq a => a -> a -> Bool
== Name
x = forall a. Pretty a => a -> [Char]
prettyShow Name
x
          | forall a. LensInScope a => a -> NameInScope
isInScope Name
n forall a. Eq a => a -> a -> Bool
== NameInScope
InScope = forall a. Pretty a => a -> [Char]
prettyShow Name
n forall a. [a] -> [a] -> [a]
++ [Char]
" = " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow Name
x
          | Bool
otherwise = forall a. Pretty a => a -> [Char]
prettyShow Name
x

        renderedCtxName :: Inlines
        renderedCtxName :: Inlines
renderedCtxName
          | Name
n forall a. Eq a => a -> a -> Bool
== Name
x = forall a. Render a => a -> Inlines
render Name
x
          | forall a. LensInScope a => a -> NameInScope
isInScope Name
n forall a. Eq a => a -> a -> Bool
== NameInScope
InScope = forall a. Render a => a -> Inlines
render Name
n Inlines -> Inlines -> Inlines
Render.<+> Inlines
"=" Inlines -> Inlines -> Inlines
Render.<+> forall a. Render a => a -> Inlines
render Name
x
          | Bool
otherwise = 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 forall a. [a] -> [a] -> [a]
++ if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Char]
c then [Char]
"" else [Char]
" "
          where
            c :: [Char]
c = forall a. Pretty a => a -> [Char]
prettyShow (forall a. LensCohesion a => a -> Cohesion
getCohesion ArgInfo
ai)

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

        extras :: IsString a => [a]
        extras :: forall a. IsString a => [a]
extras =
          forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
            [ [a
"not in scope" | forall a. LensInScope a => a -> NameInScope
isInScope NameInScope
nis forall a. Eq a => a -> a -> Bool
== NameInScope
C.NotInScope],
              -- Print erased if hypothesis is erased by goal is non-erased.
              [a
"erased" | Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall a. LensQuantity a => a -> Quantity
getQuantity ArgInfo
ai Quantity -> Quantity -> Bool
`moreQuantity` forall a. LensQuantity a => a -> Quantity
getQuantity Modality
modality],
              -- Print irrelevant if hypothesis is strictly less relevant than goal.
              [a
"irrelevant" | Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall a. LensRelevance a => a -> Relevance
getRelevance ArgInfo
ai Relevance -> Relevance -> Bool
`moreRelevant` forall a. LensRelevance a => a -> Relevance
getRelevance Modality
modality],
              -- Print instance if variable is considered by instance search
              [a
"instance" | forall a. LensHiding a => a -> Bool
isInstance ArgInfo
ai]
            ]

        extras2 :: [Inlines]
        extras2 :: [Inlines]
extras2 =
          forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
            [ [Inlines
"not in scope" | forall a. LensInScope a => a -> NameInScope
isInScope NameInScope
nis forall a. Eq a => a -> a -> Bool
== NameInScope
C.NotInScope],
              -- Print erased if hypothesis is erased by goal is non-erased.
              [Inlines
"erased" | Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall a. LensQuantity a => a -> Quantity
getQuantity ArgInfo
ai Quantity -> Quantity -> Bool
`moreQuantity` forall a. LensQuantity a => a -> Quantity
getQuantity Modality
modality],
              -- Print irrelevant if hypothesis is strictly less relevant than goal.
              [Inlines
"irrelevant" | Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall a. LensRelevance a => a -> Relevance
getRelevance ArgInfo
ai Relevance -> Relevance -> Bool
`moreRelevant` forall a. LensRelevance a => a -> Relevance
getRelevance Modality
modality],
              -- Print instance if variable is considered by instance search
              [Inlines
"instance" | forall a. LensHiding a => a -> Bool
isInstance ArgInfo
ai]
            ]

    -- raw
    Doc
rawExpr <- forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyATop Expr
expr
    let rawType :: [Char]
rawType = forall a. Show a => a -> [Char]
show forall a b. (a -> b) -> a -> b
$ Int -> [([Char], Doc)] -> Doc
align Int
10 [([Char]
rawAttribute forall a. [a] -> [a] -> [a]
++ [Char]
rawCtxName, Doc
":" Doc -> Doc -> Doc
<+> Doc
rawExpr Doc -> Doc -> Doc
<+> [Doc] -> Doc
parenSep forall a. IsString a => [a]
extras)]
    -- rendered  
    Inlines
renderedExpr <- forall c a.
(Render c, ToConcrete a, ConOfAbs a ~ c) =>
a -> TCMT IO Inlines
renderATop Expr
expr
    let renderedType :: Inlines
renderedType = (Inlines
renderedCtxName 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 (forall a. a -> Maybe a
Just [Char]
rawType) forall a. Maybe a
Nothing

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

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

    parenSep2 :: [Inlines] -> Inlines
    parenSep2 :: [Inlines] -> Inlines
parenSep2 [Inlines]
docs
      | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Inlines]
docs = forall a. Monoid a => a
mempty
      | Bool
otherwise = (Inlines
" " Inlines -> Inlines -> Inlines
Render.<+>) forall a b. (a -> b) -> a -> b
$ Inlines -> Inlines
Render.parens forall a b. (a -> b) -> a -> b
$ [Inlines] -> Inlines
Render.fsep 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 <- forall c a.
(Render c, ToConcrete a, ConOfAbs a ~ c) =>
a -> TCMT IO Inlines
renderATop Expr
e
      [Char]
raw <- forall a. Show a => a -> [Char]
show forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyATop Expr
e
      forall (m :: * -> *) a. Monad m => a -> m a
return (Inlines
rendered, [Char]
raw)
    OutputConstraint Expr InteractionId
_ -> do
      Inlines
rendered <- forall c a.
(Render c, ToConcrete a, ConOfAbs a ~ c) =>
a -> TCMT IO Inlines
renderATop OutputConstraint Expr InteractionId
form
      [Char]
raw <- forall a. Show a => a -> [Char]
show forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyATop OutputConstraint Expr InteractionId
form
      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
<+> forall a. Pretty a => a -> Doc
pretty CPUTime
time