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