    module Agda.Interaction.JSONTop
        ( jsonREPL
        ) where

    import Control.Monad          ( (<=<), forM )
    import Control.Monad.IO.Class ( MonadIO(..) )

    import Data.ByteString.Lazy (ByteString)
    import qualified Data.ByteString.Lazy.Char8 as BS
    import qualified Data.Text as T
    import qualified Data.Set as Set

    import Agda.Interaction.AgdaTop
    import Agda.Interaction.Base
      (CommandState(..), CurrentFile(..), ComputeMode(..), Rewrite(..), OutputForm(..), OutputConstraint(..))
    import qualified Agda.Interaction.BasicOps as B
    import Agda.Interaction.EmacsTop
    import Agda.Interaction.JSON
    import Agda.Interaction.Response as R
    import Agda.Interaction.Highlighting.JSON
    import Agda.Syntax.Abstract.Pretty (prettyATop)
    import Agda.Syntax.Common
    import qualified Agda.Syntax.Concrete as C
    import Agda.Syntax.Concrete.Name (NameInScope(..), Name)
    import Agda.Syntax.Internal (telToList, Dom'(..), Dom, MetaId(..), ProblemId(..), Blocker(..), alwaysUnblock)
    import Agda.Syntax.Position (Range, rangeIntervals, Interval'(..), Position'(..), noRange)
    import Agda.VersionCommit

    import Agda.TypeChecking.Errors (getAllWarningsOfTCErr)
    import Agda.TypeChecking.Monad (Comparison(..), inTopContext, TCM, TCErr, TCWarning, NamedMeta(..), withInteractionId)
    import Agda.TypeChecking.Monad.MetaVars (getInteractionRange, getMetaRange, withMetaId)
    import Agda.TypeChecking.Pretty (PrettyTCM(..), prettyTCM)
    -- borrowed from EmacsTop, for temporarily serialising stuff
    import Agda.TypeChecking.Pretty.Warning (filterTCWarnings)
    import Agda.TypeChecking.Warnings (WarningsAndNonFatalErrors(..))
    import Agda.Utils.Pretty (Pretty(..))
    import qualified Agda.Utils.Pretty as P
    import Agda.Utils.Time (CPUTime(..))

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

    -- | 'jsonREPL' is a interpreter like 'mimicGHCi', but outputs JSON-encoded strings.
    --
    --   'jsonREPL' reads Haskell values (that starts from 'IOTCM' ...) from stdin,
    --   interprets them, and outputs JSON-encoded strings. into stdout.

    jsonREPL :: TCM () -> TCM ()
    jsonREPL :: TCM () -> TCM ()
    jsonREPL = InteractionOutputCallback -> String -> TCM () -> TCM ()
    repl (IO () -> TCM ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO () -> TCM ()) -> (ByteString -> IO ()) -> ByteString -> TCM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ByteString -> IO ()
    BS.putStrLn (ByteString -> TCM ())
    -> (Response -> TCMT IO ByteString) -> InteractionOutputCallback
    forall (m :: * -> *) b c a.
    Monad m =>
    (b -> m c) -> (a -> m b) -> a -> m c
    <=< Response -> TCMT IO ByteString
    jsonifyResponse) String
    "JSON> "

    instance EncodeTCM NameInScope where
    instance ToJSON NameInScope where
      toJSON :: NameInScope -> Value
    toJSON NameInScope
    InScope    = Bool -> Value
    forall a. ToJSON a => a -> Value
    toJSON Bool
    True
      toJSON NameInScope
    NotInScope = Bool -> Value
    forall a. ToJSON a => a -> Value
    toJSON Bool
    False

    instance EncodeTCM Status where
    instance ToJSON Status where
      toJSON :: Status -> Value
    toJSON Status
    status = [Pair] -> Value
    object
        [ Text
    "showImplicitArguments"   Text -> Bool -> Pair
    forall a. ToJSON a => Text -> a -> Pair
    .= Status -> Bool
    sShowImplicitArguments Status
    status
        , Text
    "showIrrelevantArguments" Text -> Bool -> Pair
    forall a. ToJSON a => Text -> a -> Pair
    .= Status -> Bool
    sShowIrrelevantArguments Status
    status
        , Text
    "checked"                 Text -> Bool -> Pair
    forall a. ToJSON a => Text -> a -> Pair
    .= Status -> Bool
    sChecked Status
    status
        ]

    instance EncodeTCM CommandState where
    instance ToJSON CommandState where
      toJSON :: CommandState -> Value
    toJSON CommandState
    commandState = [Pair] -> Value
    object
        [ Text
    "interactionPoints" Text -> [InteractionId] -> Pair
    forall a. ToJSON a => Text -> a -> Pair
    .= CommandState -> [InteractionId]
    theInteractionPoints CommandState
    commandState
        , Text
    "currentFile"       Text -> Maybe CurrentFile -> Pair
    forall a. ToJSON a => Text -> a -> Pair
    .= CommandState -> Maybe CurrentFile
    theCurrentFile CommandState
    commandState
        -- more?
        ]

    instance EncodeTCM CurrentFile where
    instance ToJSON CurrentFile where
      toJSON :: CurrentFile -> Value
    toJSON (CurrentFile AbsolutePath
    path [String]
    _ ClockTime
    time) = (AbsolutePath, ClockTime) -> Value
    forall a. ToJSON a => a -> Value
    toJSON (AbsolutePath
    path, ClockTime
    time)  -- backwards compat.

    instance EncodeTCM ResponseContextEntry where
      encodeTCM :: ResponseContextEntry -> TCM Value
    encodeTCM ResponseContextEntry
    entry = [TCM Pair] -> TCM Value
    obj
        [ Text
    "originalName" Text -> Value -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= Name -> Value
    forall a. Pretty a => a -> Value
    encodePretty (ResponseContextEntry -> Name
    respOrigName ResponseContextEntry
    entry)
        , Text
    "reifiedName"  Text -> Value -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= Name -> Value
    forall a. Pretty a => a -> Value
    encodePretty (ResponseContextEntry -> Name
    respReifName ResponseContextEntry
    entry)
        , Text
    "binding"      Text -> TCM Doc -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= Expr -> TCM Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyATop (Arg Expr -> Expr
    forall e. Arg e -> e
    unArg (ResponseContextEntry -> Arg Expr
    respType ResponseContextEntry
    entry))
        , Text
    "inScope"      Text -> NameInScope -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= ResponseContextEntry -> NameInScope
    respInScope ResponseContextEntry
    entry
        ]

    instance EncodeTCM (Position' ()) where
    instance ToJSON (Position' ()) where
      toJSON :: Position' () -> Value
    toJSON Position' ()
    p = [Pair] -> Value
    object
        [ Text
    "pos"  Text -> Value -> Pair
    forall a. ToJSON a => Text -> a -> Pair
    .= Int32 -> Value
    forall a. ToJSON a => a -> Value
    toJSON (Position' () -> Int32
    forall a. Position' a -> Int32
    posPos Position' ()
    p)
        , Text
    "line" Text -> Value -> Pair
    forall a. ToJSON a => Text -> a -> Pair
    .= Int32 -> Value
    forall a. ToJSON a => a -> Value
    toJSON (Position' () -> Int32
    forall a. Position' a -> Int32
    posLine Position' ()
    p)
        , Text
    "col"  Text -> Value -> Pair
    forall a. ToJSON a => Text -> a -> Pair
    .= Int32 -> Value
    forall a. ToJSON a => a -> Value
    toJSON (Position' () -> Int32
    forall a. Position' a -> Int32
    posCol Position' ()
    p)
        ]

    instance EncodeTCM Range where
    instance ToJSON Range where
      toJSON :: Range -> Value
    toJSON = [Value] -> Value
    forall a. ToJSON a => a -> Value
    toJSON ([Value] -> Value) -> (Range -> [Value]) -> Range -> Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Interval' () -> Value) -> [Interval' ()] -> [Value]
    forall a b. (a -> b) -> [a] -> [b]
    map Interval' () -> Value
    forall {a}. ToJSON (Position' a) => Interval' a -> Value
    prettyInterval ([Interval' ()] -> [Value])
    -> (Range -> [Interval' ()]) -> Range -> [Value]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Range -> [Interval' ()]
    forall a. Range' a -> [Interval' ()]
    rangeIntervals
        where prettyInterval :: Interval' a -> Value
    prettyInterval Interval' a
    i = [Pair] -> Value
    object [ Text
    "start" Text -> Position' a -> Pair
    forall a. ToJSON a => Text -> a -> Pair
    .= Interval' a -> Position' a
    forall a. Interval' a -> Position' a
    iStart Interval' a
    i, Text
    "end" Text -> Position' a -> Pair
    forall a. ToJSON a => Text -> a -> Pair
    .= Interval' a -> Position' a
    forall a. Interval' a -> Position' a
    iEnd Interval' a
    i ]

    instance EncodeTCM ProblemId where
    instance EncodeTCM MetaId    where

    instance ToJSON ProblemId where toJSON :: ProblemId -> Value
    toJSON (ProblemId Nat
    i) = Nat -> Value
    forall a. ToJSON a => a -> Value
    toJSON Nat
    i
    instance ToJSON MetaId    where toJSON :: MetaId -> Value
    toJSON (MetaId    Nat
    i) = Nat -> Value
    forall a. ToJSON a => a -> Value
    toJSON Nat
    i

    instance EncodeTCM InteractionId where
      encodeTCM :: InteractionId -> TCM Value
    encodeTCM ii :: InteractionId
    ii@(InteractionId Nat
    i) = [TCM Pair] -> TCM Value
    obj
        [ Text
    "id"    Text -> Value -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= Nat -> Value
    forall a. ToJSON a => a -> Value
    toJSON Nat
    i
        , Text
    "range" Text -> TCM Value -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= TCM Value
    intervalsTCM
        ]
        where
          intervalsTCM :: TCM Value
    intervalsTCM = Range -> Value
    forall a. ToJSON a => a -> Value
    toJSON (Range -> Value) -> TCMT IO Range -> TCM Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> InteractionId -> TCMT IO Range
    forall (m :: * -> *).
    (MonadInteractionPoints m, MonadFail m, MonadError TCErr m) =>
    InteractionId -> m Range
    getInteractionRange InteractionId
    ii
    instance ToJSON InteractionId where
      toJSON :: InteractionId -> Value
    toJSON (InteractionId Nat
    i) = Nat -> Value
    forall a. ToJSON a => a -> Value
    toJSON Nat
    i

    instance EncodeTCM NamedMeta where
      encodeTCM :: NamedMeta -> TCM Value
    encodeTCM NamedMeta
    m = [TCM Pair] -> TCM Value
    obj
        [ Text
    "name"  Text -> TCM Value -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= TCM Value
    nameTCM
        , Text
    "range" Text -> TCM Value -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= TCM Value
    intervalsTCM
        ]
        where
          nameTCM :: TCM Value
    nameTCM = Doc -> Value
    forall a. Show a => a -> Value
    encodeShow (Doc -> Value) -> TCM Doc -> TCM Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MetaId -> TCM Doc -> TCM Doc
    forall (m :: * -> *) a.
    (MonadFail m, MonadTCEnv m, ReadTCState m, MonadTrace m) =>
    MetaId -> m a -> m a
    withMetaId (NamedMeta -> MetaId
    nmid NamedMeta
    m) (NamedMeta -> TCM Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyATop NamedMeta
    m)
          intervalsTCM :: TCM Value
    intervalsTCM = Range -> Value
    forall a. ToJSON a => a -> Value
    toJSON (Range -> Value) -> TCMT IO Range -> TCM Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MetaId -> TCMT IO Range
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m Range
    getMetaRange (NamedMeta -> MetaId
    nmid NamedMeta
    m)

    instance EncodeTCM GiveResult where
    instance ToJSON GiveResult where
      toJSON :: GiveResult -> Value
    toJSON (Give_String String
    s) = [Pair] -> Value
    object [ Text
    "str" Text -> String -> Pair
    forall a. ToJSON a => Text -> a -> Pair
    .= String
    s ]
      toJSON GiveResult
    Give_Paren   = [Pair] -> Value
    object [ Text
    "paren" Text -> Bool -> Pair
    forall a. ToJSON a => Text -> a -> Pair
    .= Bool
    True ]
      toJSON GiveResult
    Give_NoParen = [Pair] -> Value
    object [ Text
    "paren" Text -> Bool -> Pair
    forall a. ToJSON a => Text -> a -> Pair
    .= Bool
    False ]

    instance EncodeTCM MakeCaseVariant where
    instance ToJSON MakeCaseVariant where
      toJSON :: MakeCaseVariant -> Value
    toJSON MakeCaseVariant
    R.Function = Text -> Value
    String Text
    "Function"
      toJSON MakeCaseVariant
    R.ExtendedLambda = Text -> Value
    String Text
    "ExtendedLambda"

    encodePretty :: Pretty a => a -> Value
    encodePretty :: forall a. Pretty a => a -> Value
    encodePretty = Doc -> Value
    forall a. Show a => a -> Value
    encodeShow (Doc -> Value) -> (a -> Doc) -> a -> Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> Doc
    forall a. Pretty a => a -> Doc
    pretty

    encodeShow :: Show a => a -> Value
    encodeShow :: forall a. Show a => a -> Value
    encodeShow = Text -> Value
    String (Text -> Value) -> (a -> Text) -> a -> Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> Text
    T.pack (String -> Text) -> (a -> String) -> a -> Text
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> String
    forall a. Show a => a -> String
    show

    encodePrettyTCM :: PrettyTCM a => a -> TCM Value
    encodePrettyTCM :: forall a. PrettyTCM a => a -> TCM Value
    encodePrettyTCM = (Doc -> Value
    forall a. Show a => a -> Value
    encodeShow (Doc -> Value) -> TCM Doc -> TCM Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>) (TCM Doc -> TCM Value) -> (a -> TCM Doc) -> a -> TCM Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> TCM Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM

    instance EncodeTCM Rewrite where
    instance ToJSON Rewrite where toJSON :: Rewrite -> Value
    toJSON = Rewrite -> Value
    forall a. Show a => a -> Value
    encodeShow

    instance EncodeTCM CPUTime where
    instance ToJSON CPUTime where toJSON :: CPUTime -> Value
    toJSON = CPUTime -> Value
    forall a. Pretty a => a -> Value
    encodePretty

    instance EncodeTCM ComputeMode where
    instance ToJSON ComputeMode where toJSON :: ComputeMode -> Value
    toJSON = ComputeMode -> Value
    forall a. Show a => a -> Value
    encodeShow

    encodeOCCmp :: (a -> TCM Value)
      -> Comparison -> a -> a -> T.Text
      -> TCM Value
    encodeOCCmp :: forall a.
    (a -> TCM Value) -> Comparison -> a -> a -> Text -> TCM Value
    encodeOCCmp a -> TCM Value
    f Comparison
    c a
    i a
    j Text
    k = Text -> [TCM Pair] -> TCM Value
    kind Text
    k
      [ Text
    "comparison"     Text -> Value -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= Comparison -> Value
    forall a. Show a => a -> Value
    encodeShow Comparison
    c
      , Text
    "constraintObjs" Text -> TCM [Value] -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= (a -> TCM Value) -> [a] -> TCM [Value]
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse a -> TCM Value
    f [a
    i, a
    j]
      ]

      -- Goals
    encodeOC :: (a -> TCM Value)
      -> (b -> TCM Value)
      -> OutputConstraint b a
      -> TCM Value
    encodeOC :: forall a b.
    (a -> TCM Value)
    -> (b -> TCM Value) -> OutputConstraint b a -> TCM Value
    encodeOC a -> TCM Value
    f b -> TCM Value
    encPrettyTCM = \case
     OfType a
    i b
    a -> Text -> [TCM Pair] -> TCM Value
    kind Text
    "OfType"
      [ Text
    "constraintObj" Text -> TCM Value -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= a -> TCM Value
    f a
    i
      , Text
    "type"          Text -> TCM Value -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= b -> TCM Value
    encPrettyTCM b
    a
      ]
     CmpInType Comparison
    c b
    a a
    i a
    j -> Text -> [TCM Pair] -> TCM Value
    kind Text
    "CmpInType"
      [ Text
    "comparison"     Text -> Value -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= Comparison -> Value
    forall a. Show a => a -> Value
    encodeShow Comparison
    c
      , Text
    "type"           Text -> TCM Value -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= b -> TCM Value
    encPrettyTCM b
    a
      , Text
    "constraintObjs" Text -> TCM [Value] -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= (a -> TCM Value) -> [a] -> TCM [Value]
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse a -> TCM Value
    f [a
    i, a
    j]
      ]
     CmpElim [Polarity]
    ps b
    a [a]
    is [a]
    js -> Text -> [TCM Pair] -> TCM Value
    kind Text
    "CmpElim"
      [ Text
    "polarities"     Text -> [Value] -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= (Polarity -> Value) -> [Polarity] -> [Value]
    forall a b. (a -> b) -> [a] -> [b]
    map Polarity -> Value
    forall a. Show a => a -> Value
    encodeShow [Polarity]
    ps
      , Text
    "type"           Text -> TCM Value -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= b -> TCM Value
    encPrettyTCM b
    a
      , Text
    "constraintObjs" Text -> TCM [[Value]] -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= ([a] -> TCM [Value]) -> [[a]] -> TCM [[Value]]
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse ((a -> TCM Value) -> [a] -> TCM [Value]
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse a -> TCM Value
    f) [[a]
    is, [a]
    js]
      ]
     JustType a
    a -> Text -> [TCM Pair] -> TCM Value
    kind Text
    "JustType"
      [ Text
    "constraintObj"  Text -> TCM Value -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= a -> TCM Value
    f a
    a
      ]
     JustSort a
    a -> Text -> [TCM Pair] -> TCM Value
    kind Text
    "JustSort"
      [ Text
    "constraintObj"  Text -> TCM Value -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= a -> TCM Value
    f a
    a
      ]
     CmpTypes  Comparison
    c a
    i a
    j -> (a -> TCM Value) -> Comparison -> a -> a -> Text -> TCM Value
    forall a.
    (a -> TCM Value) -> Comparison -> a -> a -> Text -> TCM Value
    encodeOCCmp a -> TCM Value
    f Comparison
    c a
    i a
    j Text
    "CmpTypes"
     CmpLevels Comparison
    c a
    i a
    j -> (a -> TCM Value) -> Comparison -> a -> a -> Text -> TCM Value
    forall a.
    (a -> TCM Value) -> Comparison -> a -> a -> Text -> TCM Value
    encodeOCCmp a -> TCM Value
    f Comparison
    c a
    i a
    j Text
    "CmpLevels"
     CmpTeles  Comparison
    c a
    i a
    j -> (a -> TCM Value) -> Comparison -> a -> a -> Text -> TCM Value
    forall a.
    (a -> TCM Value) -> Comparison -> a -> a -> Text -> TCM Value
    encodeOCCmp a -> TCM Value
    f Comparison
    c a
    i a
    j Text
    "CmpTeles"
     CmpSorts  Comparison
    c a
    i a
    j -> (a -> TCM Value) -> Comparison -> a -> a -> Text -> TCM Value
    forall a.
    (a -> TCM Value) -> Comparison -> a -> a -> Text -> TCM Value
    encodeOCCmp a -> TCM Value
    f Comparison
    c a
    i a
    j Text
    "CmpSorts"
     Assign a
    i b
    a -> Text -> [TCM Pair] -> TCM Value
    kind Text
    "Assign"
      [ Text
    "constraintObj"  Text -> TCM Value -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= a -> TCM Value
    f a
    i
      , Text
    "value"          Text -> TCM Value -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= b -> TCM Value
    encPrettyTCM b
    a
      ]
     TypedAssign a
    i b
    v b
    t -> Text -> [TCM Pair] -> TCM Value
    kind Text
    "TypedAssign"
      [ Text
    "constraintObj"  Text -> TCM Value -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= a -> TCM Value
    f a
    i
      , Text
    "value"          Text -> TCM Value -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= b -> TCM Value
    encPrettyTCM b
    v
      , Text
    "type"           Text -> TCM Value -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= b -> TCM Value
    encPrettyTCM b
    t
      ]
     PostponedCheckArgs a
    i [b]
    es b
    t0 b
    t1 -> Text -> [TCM Pair] -> TCM Value
    kind Text
    "PostponedCheckArgs"
      [ Text
    "constraintObj"  Text -> TCM Value -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= a -> TCM Value
    f a
    i
      , Text
    "ofType"         Text -> TCM Value -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= b -> TCM Value
    encPrettyTCM b
    t0
      , Text
    "arguments"      Text -> TCM [Value] -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= [b] -> (b -> TCM Value) -> TCM [Value]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM [b]
    es b -> TCM Value
    encPrettyTCM
      , Text
    "type"           Text -> TCM Value -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= b -> TCM Value
    encPrettyTCM b
    t1
      ]
     IsEmptyType b
    a -> Text -> [TCM Pair] -> TCM Value
    kind Text
    "IsEmptyType"
      [ Text
    "type"           Text -> TCM Value -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= b -> TCM Value
    encPrettyTCM b
    a
      ]
     SizeLtSat b
    a -> Text -> [TCM Pair] -> TCM Value
    kind Text
    "SizeLtSat"
      [ Text
    "type"           Text -> TCM Value -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= b -> TCM Value
    encPrettyTCM b
    a
      ]
     FindInstanceOF a
    i b
    t [(b, b, b)]
    cs -> Text -> [TCM Pair] -> TCM Value
    kind Text
    "FindInstanceOF"
      [ Text
    "constraintObj"  Text -> TCM Value -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= a -> TCM Value
    f a
    i
      , Text
    "candidates"     Text -> TCM [Value] -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= [(b, b, b)] -> ((b, b, b) -> TCM Value) -> TCM [Value]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM [(b, b, b)]
    cs (b, b, b) -> TCM Value
    encodeKVPairs
      , Text
    "type"           Text -> TCM Value -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= b -> TCM Value
    encPrettyTCM b
    t
      ]
      where encodeKVPairs :: (b, b, b) -> TCM Value
    encodeKVPairs (b
    _, b
    v, b
    t) = [TCM Pair] -> TCM Value
    obj -- TODO: encode kind
              [ Text
    "value"  Text -> TCM Value -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= b -> TCM Value
    encPrettyTCM b
    v
              , Text
    "type"   Text -> TCM Value -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= b -> TCM Value
    encPrettyTCM b
    t
              ]
     PTSInstance a
    a a
    b -> Text -> [TCM Pair] -> TCM Value
    kind Text
    "PTSInstance"
      [ Text
    "constraintObjs" Text -> TCM [Value] -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= (a -> TCM Value) -> [a] -> TCM [Value]
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse a -> TCM Value
    f [a
    a, a
    b]
      ]
     PostponedCheckFunDef QName
    name b
    a TCErr
    err -> Text -> [TCM Pair] -> TCM Value
    kind Text
    "PostponedCheckFunDef"
      [ Text
    "name"           Text -> Value -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= QName -> Value
    forall a. Pretty a => a -> Value
    encodePretty QName
    name
      , Text
    "type"           Text -> TCM Value -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= b -> TCM Value
    encPrettyTCM b
    a
      , Text
    "error"          Text -> TCM Value -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= TCErr -> TCM Value
    forall a. EncodeTCM a => a -> TCM Value
    encodeTCM TCErr
    err
      ]
     CheckLock a
    t a
    lk -> Text -> [TCM Pair] -> TCM Value
    kind Text
    "CheckLock"
      [ Text
    "head"           Text -> TCM Value -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= a -> TCM Value
    f a
    t
      , Text
    "lock"           Text -> TCM Value -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= a -> TCM Value
    f a
    lk
      ]
     UsableAtMod Modality
    mod a
    t -> Text -> [TCM Pair] -> TCM Value
    kind Text
    "UsableAtMod"
      [ Text
    "mod"           Text -> Value -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= Modality -> Value
    forall a. Pretty a => a -> Value
    encodePretty Modality
    mod
      , Text
    "term"          Text -> TCM Value -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= a -> TCM Value
    f a
    t
      ]

    encodeNamedPretty :: PrettyTCM a => (Name, a) -> TCM Value
    encodeNamedPretty :: forall a. PrettyTCM a => (Name, a) -> TCM Value
    encodeNamedPretty (Name
    name, a
    a) = [TCM Pair] -> TCM Value
    obj
      [ Text
    "name" Text -> Value -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= Name -> Value
    forall a. Pretty a => a -> Value
    encodePretty Name
    name
      , Text
    "term" Text -> TCM Value -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= a -> TCM Value
    forall a. PrettyTCM a => a -> TCM Value
    encodePrettyTCM a
    a
      ]

    instance EncodeTCM (OutputForm C.Expr C.Expr) where
      encodeTCM :: OutputForm Expr Expr -> TCM Value
    encodeTCM (OutputForm Range
    range [ProblemId]
    problems Blocker
    unblock OutputConstraint Expr Expr
    oc) = [TCM Pair] -> TCM Value
    obj
        [ Text
    "range"      Text -> Range -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= Range
    range
        , Text
    "problems"   Text -> [ProblemId] -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= [ProblemId]
    problems
        , Text
    "unblocker"  Text -> Blocker -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= Blocker
    unblock
        , Text
    "constraint" Text -> TCM Value -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= (Expr -> TCM Value)
    -> (Expr -> TCM Value) -> OutputConstraint Expr Expr -> TCM Value
    forall a b.
    (a -> TCM Value)
    -> (b -> TCM Value) -> OutputConstraint b a -> TCM Value
    encodeOC (Value -> TCM Value
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> TCM Value) -> (Expr -> Value) -> Expr -> TCM Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Expr -> Value
    forall a. Pretty a => a -> Value
    encodePretty) (Value -> TCM Value
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> TCM Value) -> (Expr -> Value) -> Expr -> TCM Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Expr -> Value
    forall a. Pretty a => a -> Value
    encodePretty) OutputConstraint Expr Expr
    oc
        ]

    instance EncodeTCM Blocker where
      encodeTCM :: Blocker -> TCM Value
    encodeTCM (UnblockOnMeta MetaId
    x)    = Text -> [TCM Pair] -> TCM Value
    kind Text
    "UnblockOnMeta" [ Text
    "meta" Text -> MetaId -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= MetaId
    x ]
      encodeTCM (UnblockOnProblem ProblemId
    p) = Text -> [TCM Pair] -> TCM Value
    kind Text
    "UnblockOnProblem" [ Text
    "id" Text -> ProblemId -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= ProblemId
    p ]
      encodeTCM (UnblockOnAll Set Blocker
    us)    = Text -> [TCM Pair] -> TCM Value
    kind Text
    "UnblockOnAll" [ Text
    "blockers" Text -> [Blocker] -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= Set Blocker -> [Blocker]
    forall a. Set a -> [a]
    Set.toList Set Blocker
    us ]
      encodeTCM (UnblockOnAny Set Blocker
    us)    = Text -> [TCM Pair] -> TCM Value
    kind Text
    "UnblockOnAny" [ Text
    "blockers" Text -> [Blocker] -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= Set Blocker -> [Blocker]
    forall a. Set a -> [a]
    Set.toList Set Blocker
    us ]

    instance EncodeTCM DisplayInfo where
      encodeTCM :: DisplayInfo -> TCM Value
    encodeTCM (Info_CompilationOk CompilerBackend
    backend WarningsAndNonFatalErrors
    wes) = Text -> [TCM Pair] -> TCM Value
    kind Text
    "CompilationOk"
        [ Text
    "backend"           Text -> Value -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= CompilerBackend -> Value
    forall a. Pretty a => a -> Value
    encodePretty CompilerBackend
    backend
        , Text
    "warnings"          Text -> TCM Value -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= [TCWarning] -> TCM Value
    forall a. EncodeTCM a => a -> TCM Value
    encodeTCM ([TCWarning] -> [TCWarning]
    filterTCWarnings (WarningsAndNonFatalErrors -> [TCWarning]
    tcWarnings WarningsAndNonFatalErrors
    wes))
        , Text
    "errors"            Text -> TCM Value -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= [TCWarning] -> TCM Value
    forall a. EncodeTCM a => a -> TCM Value
    encodeTCM ([TCWarning] -> [TCWarning]
    filterTCWarnings (WarningsAndNonFatalErrors -> [TCWarning]
    nonFatalErrors WarningsAndNonFatalErrors
    wes))
        ]
      encodeTCM (Info_Constraints [OutputForm Expr Expr]
    constraints) = Text -> [TCM Pair] -> TCM Value
    kind Text
    "Constraints"
        [ Text
    "constraints"       Text -> TCM [Value] -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= [OutputForm Expr Expr]
    -> (OutputForm Expr Expr -> TCM Value) -> TCM [Value]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM [OutputForm Expr Expr]
    constraints OutputForm Expr Expr -> TCM Value
    forall a. EncodeTCM a => a -> TCM Value
    encodeTCM
        ]
      encodeTCM (Info_AllGoalsWarnings ([OutputConstraint Expr InteractionId]
    vis, [OutputConstraint Expr NamedMeta]
    invis) WarningsAndNonFatalErrors
    wes) = Text -> [TCM Pair] -> TCM Value
    kind Text
    "AllGoalsWarnings"
        [ Text
    "visibleGoals"      Text -> TCM [Value] -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= [OutputConstraint Expr InteractionId]
    -> (OutputConstraint Expr InteractionId -> TCM Value)
    -> TCM [Value]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM [OutputConstraint Expr InteractionId]
    vis (\OutputConstraint Expr InteractionId
    i -> InteractionId -> TCM Value -> TCM Value
    forall (m :: * -> *) a.
    (MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m,
     MonadTrace m) =>
    InteractionId -> m a -> m a
    withInteractionId (OutputForm Expr InteractionId -> InteractionId
    forall a b. OutputForm a b -> b
    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 Value -> TCM Value) -> TCM Value -> TCM Value
    forall a b. (a -> b) -> a -> b
    $ (InteractionId -> TCM Value)
    -> (Expr -> TCM Value)
    -> OutputConstraint Expr InteractionId
    -> TCM Value
    forall a b.
    (a -> TCM Value)
    -> (b -> TCM Value) -> OutputConstraint b a -> TCM Value
    encodeOC InteractionId -> TCM Value
    forall a. EncodeTCM a => a -> TCM Value
    encodeTCM Expr -> TCM Value
    forall a. PrettyTCM a => a -> TCM Value
    encodePrettyTCM OutputConstraint Expr InteractionId
    i)
        , Text
    "invisibleGoals"    Text -> TCM [Value] -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= [OutputConstraint Expr NamedMeta]
    -> (OutputConstraint Expr NamedMeta -> TCM Value) -> TCM [Value]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM [OutputConstraint Expr NamedMeta]
    invis ((NamedMeta -> TCM Value)
    -> (Expr -> TCM Value)
    -> OutputConstraint Expr NamedMeta
    -> TCM Value
    forall a b.
    (a -> TCM Value)
    -> (b -> TCM Value) -> OutputConstraint b a -> TCM Value
    encodeOC NamedMeta -> TCM Value
    forall a. EncodeTCM a => a -> TCM Value
    encodeTCM Expr -> TCM Value
    forall a. PrettyTCM a => a -> TCM Value
    encodePrettyTCM)
        , Text
    "warnings"          Text -> TCM Value -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= [TCWarning] -> TCM Value
    forall a. EncodeTCM a => a -> TCM Value
    encodeTCM ([TCWarning] -> [TCWarning]
    filterTCWarnings (WarningsAndNonFatalErrors -> [TCWarning]
    tcWarnings WarningsAndNonFatalErrors
    wes))
        , Text
    "errors"            Text -> TCM Value -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= [TCWarning] -> TCM Value
    forall a. EncodeTCM a => a -> TCM Value
    encodeTCM ([TCWarning] -> [TCWarning]
    filterTCWarnings (WarningsAndNonFatalErrors -> [TCWarning]
    nonFatalErrors WarningsAndNonFatalErrors
    wes))
        ]
      encodeTCM (Info_Time CPUTime
    time) = Text -> [TCM Pair] -> TCM Value
    kind Text
    "Time"
        [ Text
    "time"              Text -> CPUTime -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= CPUTime
    time
        ]
      encodeTCM (Info_Error Info_Error
    err) = Info_Error -> TCM Value
    forall a. EncodeTCM a => a -> TCM Value
    encodeTCM Info_Error
    err
      encodeTCM DisplayInfo
    Info_Intro_NotFound = Text -> [TCM Pair] -> TCM Value
    kind Text
    "IntroNotFound" []
      encodeTCM (Info_Intro_ConstructorUnknown [String]
    introductions) = Text -> [TCM Pair] -> TCM Value
    kind Text
    "IntroConstructorUnknown"
        [ Text
    "constructors"      Text -> [Value] -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= (String -> Value) -> [String] -> [Value]
    forall a b. (a -> b) -> [a] -> [b]
    map String -> Value
    forall a. ToJSON a => a -> Value
    toJSON [String]
    introductions
        ]
      encodeTCM (Info_Auto String
    info) = Text -> [TCM Pair] -> TCM Value
    kind Text
    "Auto"
        [ Text
    "info"              Text -> Value -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= String -> Value
    forall a. ToJSON a => a -> Value
    toJSON String
    info
        ]
      encodeTCM (Info_ModuleContents [Name]
    names Telescope
    tele [(Name, Type)]
    contents) = Text -> [TCM Pair] -> TCM Value
    kind Text
    "ModuleContents"
        [ Text
    "contents"          Text -> TCM [Value] -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= [(Name, Type)] -> ((Name, Type) -> TCM Value) -> TCM [Value]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM [(Name, Type)]
    contents (Name, Type) -> TCM Value
    forall a. PrettyTCM a => (Name, a) -> TCM Value
    encodeNamedPretty
        , Text
    "telescope"         Text -> TCM [Value] -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= [Dom (String, Type)]
    -> (Dom (String, Type) -> TCM Value) -> TCM [Value]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM (Telescope -> [Dom (String, Type)]
    forall t. Tele (Dom t) -> [Dom (String, t)]
    telToList Telescope
    tele) Dom (String, Type) -> TCM Value
    forall a. PrettyTCM a => Dom (String, a) -> TCM Value
    encodeDomType
        , Text
    "names"             Text -> [Value] -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= (Name -> Value) -> [Name] -> [Value]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> Value
    forall a. Pretty a => a -> Value
    encodePretty [Name]
    names
        ]
        where
          encodeDomType :: PrettyTCM a => Dom (ArgName, a) -> TCM Value
          encodeDomType :: forall a. PrettyTCM a => Dom (String, a) -> TCM Value
    encodeDomType Dom (String, a)
    dom = [TCM Pair] -> TCM Value
    obj
            [ Text
    "dom"       Text -> TCM Value -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= (String, a) -> TCM Value
    forall a. PrettyTCM a => a -> TCM Value
    encodePrettyTCM (Dom (String, a) -> (String, a)
    forall t e. Dom' t e -> e
    unDom Dom (String, a)
    dom)
            , Text
    "name"      Text -> Maybe Value -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= (String -> Value) -> Maybe String -> Maybe Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap String -> Value
    forall a. Pretty a => a -> Value
    encodePretty (Dom (String, a) -> Maybe String
    forall a. (LensNamed a, NameOf a ~ NamedName) => a -> Maybe String
    bareNameOf Dom (String, a)
    dom)
            , Text
    "finite"    Text -> Value -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= Bool -> Value
    forall a. ToJSON a => a -> Value
    toJSON (Dom (String, a) -> Bool
    forall t e. Dom' t e -> Bool
    domFinite Dom (String, a)
    dom)
            , Text
    "cohesion"  Text -> Value -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= Cohesion -> Value
    forall a. Show a => a -> Value
    encodeShow (Modality -> Cohesion
    modCohesion (Modality -> Cohesion)
    -> (ArgInfo -> Modality) -> ArgInfo -> Cohesion
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ArgInfo -> Modality
    argInfoModality (ArgInfo -> Cohesion) -> ArgInfo -> Cohesion
    forall a b. (a -> b) -> a -> b
    $ Dom (String, a) -> ArgInfo
    forall t e. Dom' t e -> ArgInfo
    domInfo Dom (String, a)
    dom)
            , Text
    "relevance" Text -> Value -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= Relevance -> Value
    forall a. Show a => a -> Value
    encodeShow (Modality -> Relevance
    modRelevance (Modality -> Relevance)
    -> (ArgInfo -> Modality) -> ArgInfo -> Relevance
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ArgInfo -> Modality
    argInfoModality (ArgInfo -> Relevance) -> ArgInfo -> Relevance
    forall a b. (a -> b) -> a -> b
    $ Dom (String, a) -> ArgInfo
    forall t e. Dom' t e -> ArgInfo
    domInfo Dom (String, a)
    dom)
            , Text
    "hiding"    Text -> String -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= case ArgInfo -> Hiding
    argInfoHiding (ArgInfo -> Hiding) -> ArgInfo -> Hiding
    forall a b. (a -> b) -> a -> b
    $ Dom (String, a) -> ArgInfo
    forall t e. Dom' t e -> ArgInfo
    domInfo Dom (String, a)
    dom of
              Instance Overlappable
    o -> Overlappable -> String
    forall a. Show a => a -> String
    show Overlappable
    o
              Hiding
    o -> Hiding -> String
    forall a. Show a => a -> String
    show Hiding
    o
            ]
      encodeTCM (Info_SearchAbout [(Name, Type)]
    results String
    search) = Text -> [TCM Pair] -> TCM Value
    kind Text
    "SearchAbout"
        [ Text
    "results"           Text -> TCM [Value] -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= [(Name, Type)] -> ((Name, Type) -> TCM Value) -> TCM [Value]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM [(Name, Type)]
    results (Name, Type) -> TCM Value
    forall a. PrettyTCM a => (Name, a) -> TCM Value
    encodeNamedPretty
        , Text
    "search"            Text -> Value -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= String -> Value
    forall a. ToJSON a => a -> Value
    toJSON String
    search
        ]
      encodeTCM (Info_WhyInScope String
    thing String
    path Maybe LocalVar
    v [AbstractName]
    xs [AbstractModule]
    ms) = Text -> [TCM Pair] -> TCM Value
    kind Text
    "WhyInScope"
        [ Text
    "thing"             Text -> String -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= String
    thing
        , Text
    "filepath"          Text -> Value -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= String -> Value
    forall a. ToJSON a => a -> Value
    toJSON String
    path
        -- use Emacs message first
        , Text
    "message"           Text -> TCM Doc -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= String
    -> String
    -> Maybe LocalVar
    -> [AbstractName]
    -> [AbstractModule]
    -> TCM Doc
    explainWhyInScope String
    thing String
    path Maybe LocalVar
    v [AbstractName]
    xs [AbstractModule]
    ms
        ]
      encodeTCM (Info_NormalForm CommandState
    commandState ComputeMode
    computeMode Maybe CPUTime
    time Expr
    expr) = Text -> [TCM Pair] -> TCM Value
    kind Text
    "NormalForm"
        [ Text
    "commandState"      Text -> CommandState -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= CommandState
    commandState
        , Text
    "computeMode"       Text -> ComputeMode -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= ComputeMode
    computeMode
        , Text
    "time"              Text -> Maybe CPUTime -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= Maybe CPUTime
    time
        , Text
    "expr"              Text -> TCM Value -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= Expr -> TCM Value
    forall a. PrettyTCM a => a -> TCM Value
    encodePrettyTCM Expr
    expr
        ]
      encodeTCM (Info_InferredType CommandState
    commandState Maybe CPUTime
    time Expr
    expr) = Text -> [TCM Pair] -> TCM Value
    kind Text
    "InferredType"
        [ Text
    "commandState"      Text -> CommandState -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= CommandState
    commandState
        , Text
    "time"              Text -> Maybe CPUTime -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= Maybe CPUTime
    time
        , Text
    "expr"              Text -> TCM Value -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= Expr -> TCM Value
    forall a. PrettyTCM a => a -> TCM Value
    encodePrettyTCM Expr
    expr
        ]
      encodeTCM (Info_Context InteractionId
    ii [ResponseContextEntry]
    ctx) = Text -> [TCM Pair] -> TCM Value
    kind Text
    "Context"
        [ Text
    "interactionPoint"  Text -> InteractionId -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= InteractionId
    ii
        , Text
    "context"           Text -> [ResponseContextEntry] -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= [ResponseContextEntry]
    ctx
        ]
      encodeTCM DisplayInfo
    Info_Version = Text -> [TCM Pair] -> TCM Value
    kind Text
    "Version"
        [ Text
    "version"           Text -> String -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= (String
    versionWithCommitInfo :: String)
        ]
      encodeTCM (Info_GoalSpecific InteractionId
    ii GoalDisplayInfo
    info) = Text -> [TCM Pair] -> TCM Value
    kind Text
    "GoalSpecific"
        [ Text
    "interactionPoint"  Text -> InteractionId -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= InteractionId
    ii
        , Text
    "goalInfo"          Text -> TCM Value -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= InteractionId -> TCM Value -> TCM Value
    forall (m :: * -> *) a.
    (MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m,
     MonadTrace m) =>
    InteractionId -> m a -> m a
    withInteractionId InteractionId
    ii (InteractionId -> GoalDisplayInfo -> TCM Value
    encodeGoalSpecific InteractionId
    ii GoalDisplayInfo
    info)
        ]

    instance EncodeTCM GoalTypeAux where
      encodeTCM :: GoalTypeAux -> TCM Value
    encodeTCM GoalTypeAux
    GoalOnly = Text -> [TCM Pair] -> TCM Value
    kind Text
    "GoalOnly" []
      encodeTCM (GoalAndHave Expr
    expr) = Text -> [TCM Pair] -> TCM Value
    kind Text
    "GoalAndHave"
        [ Text
    "expr" Text -> TCM Value -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= Expr -> TCM Value
    forall a. PrettyTCM a => a -> TCM Value
    encodePrettyTCM Expr
    expr ]
      encodeTCM (GoalAndElaboration Term
    term) = Text -> [TCM Pair] -> TCM Value
    kind Text
    "GoalAndElaboration"
        [ Text
    "term" Text -> TCM Value -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= Term -> TCM Value
    forall a. PrettyTCM a => a -> TCM Value
    encodePrettyTCM Term
    term ]

    encodeGoalSpecific :: InteractionId -> GoalDisplayInfo -> TCM Value
    encodeGoalSpecific :: InteractionId -> GoalDisplayInfo -> TCM Value
    encodeGoalSpecific InteractionId
    ii = GoalDisplayInfo -> TCM Value
    go
      where
      go :: GoalDisplayInfo -> TCM Value
    go (Goal_HelperFunction OutputConstraint' Expr Expr
    helperType) = Text -> [TCM Pair] -> TCM Value
    kind Text
    "HelperFunction"
        [ Text
    "signature"   Text -> TCM Doc -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= TCM Doc -> TCM Doc
    forall (tcm :: * -> *) a.
    (MonadTCEnv tcm, ReadTCState tcm) =>
    tcm a -> tcm a
    inTopContext (OutputConstraint' Expr Expr -> TCM Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyATop OutputConstraint' Expr Expr
    helperType)
        ]
      go (Goal_NormalForm ComputeMode
    computeMode Expr
    expr) = Text -> [TCM Pair] -> TCM Value
    kind Text
    "NormalForm"
        [ Text
    "computeMode" Text -> ComputeMode -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= ComputeMode
    computeMode
        , Text
    "expr"        Text -> TCM Doc -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= ComputeMode -> Expr -> TCM Doc
    B.showComputed ComputeMode
    computeMode Expr
    expr
        ]
      go (Goal_GoalType Rewrite
    rewrite GoalTypeAux
    goalType [ResponseContextEntry]
    entries [IPBoundary' Expr]
    boundary [OutputForm Expr Expr]
    outputForms) = Text -> [TCM Pair] -> TCM Value
    kind Text
    "GoalType"
        [ Text
    "rewrite"     Text -> Rewrite -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= Rewrite
    rewrite
        , Text
    "typeAux"     Text -> GoalTypeAux -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= GoalTypeAux
    goalType
        , Text
    "type"        Text -> TCM Doc -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= Rewrite -> InteractionId -> TCM Doc
    prettyTypeOfMeta Rewrite
    rewrite InteractionId
    ii
        , Text
    "entries"     Text -> [ResponseContextEntry] -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= [ResponseContextEntry]
    entries
        , Text
    "boundary"    Text -> [Value] -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= (IPBoundary' Expr -> Value) -> [IPBoundary' Expr] -> [Value]
    forall a b. (a -> b) -> [a] -> [b]
    map IPBoundary' Expr -> Value
    forall a. Pretty a => a -> Value
    encodePretty [IPBoundary' Expr]
    boundary
        , Text
    "outputForms" Text -> [Value] -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= (OutputForm Expr Expr -> Value)
    -> [OutputForm Expr Expr] -> [Value]
    forall a b. (a -> b) -> [a] -> [b]
    map OutputForm Expr Expr -> Value
    forall a. Pretty a => a -> Value
    encodePretty [OutputForm Expr Expr]
    outputForms
        ]
      go (Goal_CurrentGoal Rewrite
    rewrite) = Text -> [TCM Pair] -> TCM Value
    kind Text
    "CurrentGoal"
        [ Text
    "rewrite"     Text -> Rewrite -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= Rewrite
    rewrite
        , Text
    "type"        Text -> TCM Doc -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= Rewrite -> InteractionId -> TCM Doc
    prettyTypeOfMeta Rewrite
    rewrite InteractionId
    ii
        ]
      go (Goal_InferredType Expr
    expr) = Text -> [TCM Pair] -> TCM Value
    kind Text
    "InferredType"
        [ Text
    "expr"        Text -> TCM Doc -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= Expr -> TCM Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyATop Expr
    expr
        ]

    instance EncodeTCM Info_Error where
      encodeTCM :: Info_Error -> TCM Value
    encodeTCM (Info_GenericError TCErr
    err) = Text -> [TCM Pair] -> TCM Value
    kind Text
    "Error"
        [ Text
    "warnings"          Text -> TCM Value -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= (TCErr -> TCM [TCWarning]
    getAllWarningsOfTCErr TCErr
    err
                                TCM [TCWarning] -> ([TCWarning] -> TCM Value) -> TCM Value
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= [TCWarning] -> TCM Value
    forall a. EncodeTCM a => a -> TCM Value
    encodeTCM ([TCWarning] -> TCM Value)
    -> ([TCWarning] -> [TCWarning]) -> [TCWarning] -> TCM Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [TCWarning] -> [TCWarning]
    filterTCWarnings)
        , Text
    "error"             Text -> TCM Value -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= TCErr -> TCM Value
    forall a. EncodeTCM a => a -> TCM Value
    encodeTCM TCErr
    err
        ]
      encodeTCM Info_Error
    err = Text -> [TCM Pair] -> TCM Value
    kind Text
    "Error"
        [ Text
    "warnings"          Text -> [String] -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= ([] :: [String])
        , Text
    "error"             Text -> TCM Value -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= [TCM Pair] -> TCM Value
    obj
          [ Text
    "message"           Text -> TCM String -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= Info_Error -> TCM String
    showInfoError Info_Error
    err
          ]
        ]

    instance EncodeTCM TCErr where
      encodeTCM :: TCErr -> TCM Value
    encodeTCM TCErr
    err = [TCM Pair] -> TCM Value
    obj
        [ Text
    "message"     Text -> TCM Value -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= TCErr -> TCM Value
    forall a. PrettyTCM a => a -> TCM Value
    encodePrettyTCM TCErr
    err
        ]

    instance EncodeTCM TCWarning where
      encodeTCM :: TCWarning -> TCM Value
    encodeTCM TCWarning
    w = [TCM Pair] -> TCM Value
    obj
        [ Text
    "message"     Text -> TCM String -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= (Doc -> String
    P.render (Doc -> String) -> TCM Doc -> TCM String
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCWarning -> TCM Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM TCWarning
    w)
        ]

    instance EncodeTCM Response where
      encodeTCM :: Response -> TCM Value
    encodeTCM (Resp_HighlightingInfo HighlightingInfo
    info RemoveTokenBasedHighlighting
    remove HighlightingMethod
    method ModuleToSource
    modFile) =
        IO Value -> TCM Value
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO Value -> TCM Value) -> IO Value -> TCM Value
    forall a b. (a -> b) -> a -> b
    $ HighlightingInfo
    -> RemoveTokenBasedHighlighting
    -> HighlightingMethod
    -> ModuleToSource
    -> IO Value
    jsonifyHighlightingInfo HighlightingInfo
    info RemoveTokenBasedHighlighting
    remove HighlightingMethod
    method ModuleToSource
    modFile
      encodeTCM (Resp_DisplayInfo DisplayInfo
    info) = Text -> [TCM Pair] -> TCM Value
    kind Text
    "DisplayInfo"
        [ Text
    "info"          Text -> DisplayInfo -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= DisplayInfo
    info
        ]
      encodeTCM (Resp_ClearHighlighting TokenBased
    tokenBased) = Text -> [TCM Pair] -> TCM Value
    kind Text
    "ClearHighlighting"
        [ Text
    "tokenBased"    Text -> TokenBased -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= TokenBased
    tokenBased
        ]
      encodeTCM Response
    Resp_DoneAborting = Text -> [TCM Pair] -> TCM Value
    kind Text
    "DoneAborting" []
      encodeTCM Response
    Resp_DoneExiting = Text -> [TCM Pair] -> TCM Value
    kind Text
    "DoneExiting" []
      encodeTCM Response
    Resp_ClearRunningInfo = Text -> [TCM Pair] -> TCM Value
    kind Text
    "ClearRunningInfo" []
      encodeTCM (Resp_RunningInfo Nat
    debugLevel String
    msg) = Text -> [TCM Pair] -> TCM Value
    kind Text
    "RunningInfo"
        [ Text
    "debugLevel"    Text -> Nat -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= Nat
    debugLevel
        , Text
    "message"       Text -> String -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= String
    msg
        ]
      encodeTCM (Resp_Status Status
    status) = Text -> [TCM Pair] -> TCM Value
    kind Text
    "Status"
        [ Text
    "status"        Text -> Status -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= Status
    status
        ]
      encodeTCM (Resp_JumpToError String
    filepath Int32
    position) = Text -> [TCM Pair] -> TCM Value
    kind Text
    "JumpToError"
        [ Text
    "filepath"      Text -> String -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= String
    filepath
        , Text
    "position"      Text -> Int32 -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= Int32
    position
        ]
      encodeTCM (Resp_InteractionPoints [InteractionId]
    interactionPoints) = Text -> [TCM Pair] -> TCM Value
    kind Text
    "InteractionPoints"
        [ Text
    "interactionPoints" Text -> [InteractionId] -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= [InteractionId]
    interactionPoints
        ]
      encodeTCM (Resp_GiveAction InteractionId
    i GiveResult
    giveResult) = Text -> [TCM Pair] -> TCM Value
    kind Text
    "GiveAction"
        [ Text
    "interactionPoint"  Text -> InteractionId -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= InteractionId
    i
        , Text
    "giveResult"        Text -> GiveResult -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= GiveResult
    giveResult
        ]
      encodeTCM (Resp_MakeCase InteractionId
    id MakeCaseVariant
    variant [String]
    clauses) = Text -> [TCM Pair] -> TCM Value
    kind Text
    "MakeCase"
        [ Text
    "interactionPoint"  Text -> InteractionId -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= InteractionId
    id
        , Text
    "variant"           Text -> MakeCaseVariant -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= MakeCaseVariant
    variant
        , Text
    "clauses"           Text -> [String] -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= [String]
    clauses
        ]
      encodeTCM (Resp_SolveAll [(InteractionId, Expr)]
    solutions) = Text -> [TCM Pair] -> TCM Value
    kind Text
    "SolveAll"
        [ Text
    "solutions"     Text -> [Value] -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= ((InteractionId, Expr) -> Value)
    -> [(InteractionId, Expr)] -> [Value]
    forall a b. (a -> b) -> [a] -> [b]
    map (InteractionId, Expr) -> Value
    forall {a} {a}. (ToJSON a, Show a) => (a, a) -> Value
    encodeSolution [(InteractionId, Expr)]
    solutions
        ]
        where
          encodeSolution :: (a, a) -> Value
    encodeSolution (a
    i, a
    expr) = [Pair] -> Value
    object
            [ Text
    "interactionPoint"  Text -> a -> Pair
    forall a. ToJSON a => Text -> a -> Pair
    .= a
    i
            , Text
    "expression"        Text -> String -> Pair
    forall a. ToJSON a => Text -> a -> Pair
    .= a -> String
    forall a. Show a => a -> String
    show a
    expr
            ]

    -- | Convert Response to an JSON value for interactive editor frontends.
    jsonifyResponse :: Response -> TCM ByteString
    jsonifyResponse :: Response -> TCMT IO ByteString
    jsonifyResponse = ByteString -> TCMT IO ByteString
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (ByteString -> TCMT IO ByteString)
    -> (Value -> ByteString) -> Value -> TCMT IO ByteString
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Value -> ByteString
    forall a. ToJSON a => a -> ByteString
    encode (Value -> TCMT IO ByteString)
    -> (Response -> TCM Value) -> Response -> TCMT IO ByteString
    forall (m :: * -> *) b c a.
    Monad m =>
    (b -> m c) -> (a -> m b) -> a -> m c
    <=< Response -> TCM Value
    forall a. EncodeTCM a => a -> TCM Value
    encodeTCM