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.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
.= 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 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, 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) -> 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
          ]
 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 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 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 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 (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.
(MonadDebug m, 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 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
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, 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 [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 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 -> 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 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 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 -> 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_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 a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
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
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 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, 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
        ]

-- | 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