    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(..)
             , OutputConstraint_boot(..), OutputForm_boot(..))
    import Agda.Interaction.Output (OutputConstraint, OutputForm)
    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.Syntax.Scope.Base
             ( WhyInScopeData(..) )

    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 qualified Agda.Syntax.Common.Pretty as P
    import Agda.Syntax.Common.Pretty
             ( Pretty(..), prettyShow )
    import Agda.Utils.Time
             ( CPUTime(..) )

    import Agda.VersionCommit

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

    -- | '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 a. IO a -> TCMT IO a
    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 TopLevelModuleName
    _ [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 -> TCMT IO Doc -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= Expr -> TCMT IO 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
    .= Word32 -> Value
    forall a. ToJSON a => a -> Value
    toJSON (Position' () -> Word32
    forall a. Position' a -> Word32
    posPos Position' ()
    p)
        , Text
    "line" Text -> Value -> Pair
    forall a. ToJSON a => Text -> a -> Pair
    .= Word32 -> Value
    forall a. ToJSON a => a -> Value
    toJSON (Position' () -> Word32
    forall a. Position' a -> Word32
    posLine Position' ()
    p)
        , Text
    "col"  Text -> Value -> Pair
    forall a. ToJSON a => Text -> a -> Pair
    .= Word32 -> Value
    forall a. ToJSON a => a -> Value
    toJSON (Position' () -> Word32
    forall a. Position' a -> Word32
    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
    f Position' ()
    s Position' ()
    e) = [Pair] -> Value
    object [ Text
    "start" Text -> Position' a -> Pair
    forall a. ToJSON a => Text -> a -> Pair
    .= (a
    f a -> Position' () -> Position' a
    forall a b. a -> Position' b -> Position' a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Position' ()
    s), Text
    "end" Text -> Position' a -> Pair
    forall a. ToJSON a => Text -> a -> Pair
    .= (a
    f a -> Position' () -> Position' a
    forall a b. a -> Position' b -> Position' a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Position' ()
    e) ]

    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 ModuleNameHash where
      toJSON :: ModuleNameHash -> Value
    toJSON (ModuleNameHash Word64
    h) = Word64 -> Value
    forall a. ToJSON a => a -> Value
    toJSON Word64
    h

    instance ToJSON MetaId where
      toJSON :: MetaId -> Value
    toJSON MetaId
    m = [Pair] -> Value
    object
        [ Text
    "id"     Text -> Value -> Pair
    forall a. ToJSON a => Text -> a -> Pair
    .= Word64 -> Value
    forall a. ToJSON a => a -> Value
    toJSON (MetaId -> Word64
    metaId MetaId
    m)
        , Text
    "module" Text -> Value -> Pair
    forall a. ToJSON a => Text -> a -> Pair
    .= ModuleNameHash -> Value
    forall a. ToJSON a => a -> Value
    toJSON (MetaId -> ModuleNameHash
    metaModule MetaId
    m)
        ]

    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, MonadDebug 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) -> TCMT IO Doc -> TCM Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MetaId -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *) a.
    (HasCallStack, MonadDebug m, MonadTCEnv m, MonadTrace m,
     ReadTCState m) =>
    MetaId -> m a -> m a
    withMetaId (NamedMeta -> MetaId
    nmid NamedMeta
    m) (NamedMeta -> TCMT IO 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 :: * -> *).
    (HasCallStack, MonadDebug 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) -> TCMT IO Doc -> TCM Value
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>) (TCMT IO Doc -> TCM Value) -> (a -> TCMT IO Doc) -> a -> TCM Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). 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)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> [a] -> f [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)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> [a] -> f [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)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> [a] -> f [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)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> [a] -> f [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
              ]
     ResolveInstanceOF QName
    q -> Text -> [TCM Pair] -> TCM Value
    kind Text
    "ResolveInstanceOF"
      [ Text
    "name"           Text -> Value -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= QName -> Value
    forall a. Pretty a => a -> Value
    encodePretty QName
    q
      ]
     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)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> [a] -> f [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
      ]
     DataSort QName
    q a
    s -> Text -> [TCM Pair] -> TCM Value
    kind Text
    "DataSort"
      [ Text
    "name"           Text -> Value -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= QName -> Value
    forall a. Pretty a => a -> Value
    encodePretty QName
    q
      , Text
    "sort"           Text -> TCM Value -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= a -> TCM Value
    f a
    s
      ]
     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_boot TCErr Expr Expr -> TCM Value
    encodeTCM (OutputForm Range
    range [ProblemId]
    problems Blocker
    unblock OutputConstraint_boot TCErr 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_boot TCErr Expr Expr
    -> TCM Value
    forall a b.
    (a -> TCM Value)
    -> (b -> TCM Value) -> OutputConstraint b a -> TCM Value
    encodeOC (Value -> TCM Value
    forall a. a -> TCMT IO a
    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 a. a -> TCMT IO a
    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_boot TCErr 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 (UnblockOnDef QName
    q)     = Text -> [TCM Pair] -> TCM Value
    kind Text
    "UnblockOnDef" [ Text
    "name" Text -> Value -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= QName -> Value
    forall a. Pretty a => a -> Value
    encodePretty QName
    q ]
      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 :: DisplayInfo -> TCM Value
    encodeTCM (Info_CompilationOk CompilerBackend
    backend WarningsAndNonFatalErrors
    wes) = do
        ws <- Set TCWarning -> TCM [TCWarning]
    filterTCWarnings (WarningsAndNonFatalErrors -> Set TCWarning
    tcWarnings WarningsAndNonFatalErrors
    wes)
        es <- filterTCWarnings (nonFatalErrors wes)
        kind "CompilationOk"
          [ "backend"           @= encodePretty backend
          , "warnings"          #= encodeTCM ws
          , "errors"            #= encodeTCM es
          ]
      encodeTCM (Info_Constraints [OutputForm_boot TCErr 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_boot TCErr Expr Expr]
    -> (OutputForm_boot TCErr 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_boot TCErr Expr Expr]
    constraints OutputForm_boot TCErr Expr Expr -> TCM Value
    forall a. EncodeTCM a => a -> TCM Value
    encodeTCM
        ]
      encodeTCM (Info_AllGoalsWarnings ([OutputConstraint_boot TCErr Expr InteractionId]
    vis, [OutputConstraint_boot TCErr Expr NamedMeta]
    invis) WarningsAndNonFatalErrors
    wes) = do
        ws <- Set TCWarning -> TCM [TCWarning]
    filterTCWarnings (WarningsAndNonFatalErrors -> Set TCWarning
    tcWarnings WarningsAndNonFatalErrors
    wes)
        es <- filterTCWarnings (nonFatalErrors wes)
        kind "AllGoalsWarnings"
          [ "visibleGoals"      #= forM vis (\OutputConstraint_boot TCErr Expr InteractionId
    i -> InteractionId -> TCM Value -> TCM Value
    forall (m :: * -> *) a.
    (MonadDebug 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_boot TCErr Expr InteractionId
    -> OutputForm Expr InteractionId
    forall tcErr a b.
    Range
    -> [ProblemId]
    -> Blocker
    -> OutputConstraint_boot tcErr a b
    -> OutputForm_boot tcErr a b
    OutputForm Range
    forall a. Range' a
    noRange [] Blocker
    alwaysUnblock OutputConstraint_boot TCErr 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_boot TCErr 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_boot TCErr Expr InteractionId
    i)
          , "invisibleGoals"    #= forM invis (encodeOC encodeTCM encodePrettyTCM)
          , "warnings"          #= encodeTCM ws
          , "errors"            #= encodeTCM es
          ]
      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_boot TCErr TCWarning
    err) = Info_Error_boot TCErr TCWarning -> TCM Value
    forall a. EncodeTCM a => a -> TCM Value
    encodeTCM Info_Error_boot TCErr TCWarning
    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 a b. (a -> b) -> Maybe a -> Maybe b
    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
    domIsFinite 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 why :: WhyInScopeData
    why@(WhyInScopeData QName
    y String
    path Maybe LocalVar
    _ [AbstractName]
    _ [AbstractModule]
    _)) = Text -> [TCM Pair] -> TCM Value
    kind Text
    "WhyInScope"
        [ Text
    "thing"             Text -> String -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= QName -> String
    forall a. Pretty a => a -> String
    prettyShow QName
    y
        , 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 -> TCMT IO Doc -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= WhyInScopeData -> TCMT IO Doc
    forall (m :: * -> *). MonadPretty m => WhyInScopeData -> m Doc
    explainWhyInScope WhyInScopeData
    why
        ]
      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_boot TCErr
    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.
    (MonadDebug m, ReadTCState m, MonadError TCErr m, MonadTCEnv m,
     MonadTrace m) =>
    InteractionId -> m a -> m a
    withInteractionId InteractionId
    ii (InteractionId -> GoalDisplayInfo_boot TCErr -> TCM Value
    encodeGoalSpecific InteractionId
    ii GoalDisplayInfo_boot TCErr
    info)
        ]

    instance EncodeTCM GoalTypeAux where
      encodeTCM :: GoalTypeAux -> TCM Value
    encodeTCM GoalTypeAux
    GoalOnly = Text -> [TCM Pair] -> TCM Value
    kind Text
    "GoalOnly" []
      encodeTCM (GoalAndHave Expr
    expr [IPFace' 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 Expr
    expr) = Text -> [TCM Pair] -> TCM Value
    kind Text
    "GoalAndElaboration"
        [ Text
    "term" 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 ]

    encodeGoalSpecific :: InteractionId -> GoalDisplayInfo -> TCM Value
    encodeGoalSpecific :: InteractionId -> GoalDisplayInfo_boot TCErr -> TCM Value
    encodeGoalSpecific InteractionId
    ii = GoalDisplayInfo_boot TCErr -> TCM Value
    go
      where
      go :: GoalDisplayInfo_boot TCErr -> TCM Value
    go (Goal_HelperFunction OutputConstraint' Expr Expr
    helperType) = Text -> [TCM Pair] -> TCM Value
    kind Text
    "HelperFunction"
        [ Text
    "signature"   Text -> TCMT IO Doc -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= TCMT IO Doc -> TCMT IO Doc
    forall (tcm :: * -> *) a.
    (MonadTCEnv tcm, ReadTCState tcm) =>
    tcm a -> tcm a
    inTopContext (OutputConstraint' Expr Expr -> TCMT IO 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 -> TCMT IO Doc -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= ComputeMode -> Expr -> TCMT IO Doc
    B.showComputed ComputeMode
    computeMode Expr
    expr
        ]
      go (Goal_GoalType Rewrite
    rewrite GoalTypeAux
    goalType [ResponseContextEntry]
    entries [IPFace' Expr]
    boundary [OutputForm_boot TCErr 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 -> TCMT IO Doc -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= Rewrite -> InteractionId -> TCMT IO 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
    @= (IPFace' Expr -> Value) -> [IPFace' Expr] -> [Value]
    forall a b. (a -> b) -> [a] -> [b]
    map IPFace' Expr -> Value
    forall a. Pretty a => a -> Value
    encodePretty [IPFace' Expr]
    boundary
        , Text
    "outputForms" Text -> [Value] -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= (OutputForm_boot TCErr Expr Expr -> Value)
    -> [OutputForm_boot TCErr Expr Expr] -> [Value]
    forall a b. (a -> b) -> [a] -> [b]
    map OutputForm_boot TCErr Expr Expr -> Value
    forall a. Pretty a => a -> Value
    encodePretty [OutputForm_boot TCErr 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 -> TCMT IO Doc -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= Rewrite -> InteractionId -> TCMT IO Doc
    prettyTypeOfMeta Rewrite
    rewrite InteractionId
    ii
        ]
      go (Goal_InferredType Expr
    expr) = Text -> [TCM Pair] -> TCM Value
    kind Text
    "InferredType"
        [ Text
    "expr"        Text -> TCMT IO Doc -> TCM Pair
    forall a. ToJSON a => Text -> TCM a -> TCM Pair
    #= Expr -> TCMT IO 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_Error_boot TCErr TCWarning -> TCM Value
    encodeTCM (Info_GenericError TCErr
    err) = do
        ws <- Set TCWarning -> TCM [TCWarning]
    filterTCWarnings (Set TCWarning -> TCM [TCWarning])
    -> TCMT IO (Set TCWarning) -> TCM [TCWarning]
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TCErr -> TCMT IO (Set TCWarning)
    getAllWarningsOfTCErr TCErr
    err
        kind "Error"
          [ "warnings"          #= encodeTCM ws
          , "error"             #= encodeTCM err
          ]
      encodeTCM Info_Error_boot TCErr TCWarning
    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_boot TCErr TCWarning -> TCM String
    showInfoError Info_Error_boot TCErr TCWarning
    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
    forall a. Doc a -> String
    P.render (Doc -> String) -> TCMT IO Doc -> TCM String
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCWarning -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => TCWarning -> 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 a. IO a -> TCMT IO a
    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 Word32
    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 -> Word32 -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= Word32
    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, Pretty 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. Pretty a => a -> String
    P.prettyShow a
    expr
            ]
      encodeTCM (Resp_Mimer InteractionId
    ii Maybe String
    str) = Text -> [TCM Pair] -> TCM Value
    kind Text
    "Mimer"
        [ Text
    "solution" Text -> Maybe String -> TCM Pair
    forall a. EncodeTCM a => Text -> a -> TCM Pair
    @= Maybe String
    str
        ]

    -- | 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 a. a -> TCMT IO a
    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