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.Utils.Pretty as P
import Agda.Utils.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 (forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> IO ()
BS.putStrLn forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Response -> TCM ByteString
jsonifyResponse) String
"JSON> "

instance EncodeTCM NameInScope where
instance ToJSON NameInScope where
  toJSON :: NameInScope -> Value
toJSON NameInScope
InScope    = forall a. ToJSON a => a -> Value
toJSON Bool
True
  toJSON NameInScope
NotInScope = 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"   forall a. ToJSON a => Text -> a -> Pair
.= Status -> Bool
sShowImplicitArguments Status
status
    , Text
"showIrrelevantArguments" forall a. ToJSON a => Text -> a -> Pair
.= Status -> Bool
sShowIrrelevantArguments Status
status
    , Text
"checked"                 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" forall a. ToJSON a => Text -> a -> Pair
.= CommandState -> [InteractionId]
theInteractionPoints CommandState
commandState
    , Text
"currentFile"       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) = 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" forall a. EncodeTCM a => Text -> a -> TCM Pair
@= forall a. Pretty a => a -> Value
encodePretty (ResponseContextEntry -> Name
respOrigName ResponseContextEntry
entry)
    , Text
"reifiedName"  forall a. EncodeTCM a => Text -> a -> TCM Pair
@= forall a. Pretty a => a -> Value
encodePretty (ResponseContextEntry -> Name
respReifName ResponseContextEntry
entry)
    , Text
"binding"      forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyATop (forall e. Arg e -> e
unArg (ResponseContextEntry -> Arg Expr
respType ResponseContextEntry
entry))
    , Text
"inScope"      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"  forall a. ToJSON a => Text -> a -> Pair
.= forall a. ToJSON a => a -> Value
toJSON (forall a. Position' a -> Int32
posPos Position' ()
p)
    , Text
"line" forall a. ToJSON a => Text -> a -> Pair
.= forall a. ToJSON a => a -> Value
toJSON (forall a. Position' a -> Int32
posLine Position' ()
p)
    , Text
"col"  forall a. ToJSON a => Text -> a -> Pair
.= forall a. ToJSON a => a -> Value
toJSON (forall a. Position' a -> Int32
posCol Position' ()
p)
    ]

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

instance ToJSON ModuleNameHash where
  toJSON :: ModuleNameHash -> Value
toJSON (ModuleNameHash Word64
h) = forall a. ToJSON a => a -> Value
toJSON Word64
h

instance ToJSON MetaId where
  toJSON :: MetaId -> Value
toJSON MetaId
m = [Pair] -> Value
object
    [ Text
"id"     forall a. ToJSON a => Text -> a -> Pair
.= forall a. ToJSON a => a -> Value
toJSON (MetaId -> Word64
metaId MetaId
m)
    , Text
"module" forall a. ToJSON a => Text -> a -> Pair
.= 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"    forall a. EncodeTCM a => Text -> a -> TCM Pair
@= forall a. ToJSON a => a -> Value
toJSON Nat
i
    , Text
"range" forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= TCM Value
intervalsTCM
    ]
    where
      intervalsTCM :: TCM Value
intervalsTCM = forall a. ToJSON a => a -> Value
toJSON forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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) = 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"  forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= TCM Value
nameTCM
    , Text
"range" forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= TCM Value
intervalsTCM
    ]
    where
      nameTCM :: TCM Value
nameTCM = forall a. Show a => a -> Value
encodeShow forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a.
(HasCallStack, MonadDebug m, MonadTCEnv m, MonadTrace m,
 ReadTCState m) =>
MetaId -> m a -> m a
withMetaId (NamedMeta -> MetaId
nmid NamedMeta
m) (forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyATop NamedMeta
m)
      intervalsTCM :: TCM Value
intervalsTCM = forall a. ToJSON a => a -> Value
toJSON forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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" forall a. ToJSON a => Text -> a -> Pair
.= String
s ]
  toJSON GiveResult
Give_Paren   = [Pair] -> Value
object [ Text
"paren" forall a. ToJSON a => Text -> a -> Pair
.= Bool
True ]
  toJSON GiveResult
Give_NoParen = [Pair] -> Value
object [ Text
"paren" 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 = forall a. Show a => a -> Value
encodeShow forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Pretty a => a -> Doc
pretty

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

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

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

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

instance EncodeTCM ComputeMode where
instance ToJSON ComputeMode where toJSON :: ComputeMode -> Value
toJSON = 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"     forall a. EncodeTCM a => Text -> a -> TCM Pair
@= forall a. Show a => a -> Value
encodeShow Comparison
c
  , Text
"constraintObjs" forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= 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" forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= a -> TCM Value
f a
i
  , Text
"type"          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"     forall a. EncodeTCM a => Text -> a -> TCM Pair
@= forall a. Show a => a -> Value
encodeShow Comparison
c
  , Text
"type"           forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= b -> TCM Value
encPrettyTCM b
a
  , Text
"constraintObjs" forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= 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"     forall a. EncodeTCM a => Text -> a -> TCM Pair
@= forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> Value
encodeShow [Polarity]
ps
  , Text
"type"           forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= b -> TCM Value
encPrettyTCM b
a
  , Text
"constraintObjs" forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (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"  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"  forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= a -> TCM Value
f a
a
  ]
 CmpTypes  Comparison
c a
i a
j -> 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 -> 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 -> 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 -> 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"  forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= a -> TCM Value
f a
i
  , Text
"value"          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"  forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= a -> TCM Value
f a
i
  , Text
"value"          forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= b -> TCM Value
encPrettyTCM b
v
  , Text
"type"           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"  forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= a -> TCM Value
f a
i
  , Text
"ofType"         forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= b -> TCM Value
encPrettyTCM b
t0
  , Text
"arguments"      forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= 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"           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"           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"           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"  forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= a -> TCM Value
f a
i
  , Text
"candidates"     forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= 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"           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"  forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= b -> TCM Value
encPrettyTCM b
v
          , Text
"type"   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" forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= 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"           forall a. EncodeTCM a => Text -> a -> TCM Pair
@= forall a. Pretty a => a -> Value
encodePretty QName
name
  , Text
"type"           forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= b -> TCM Value
encPrettyTCM b
a
  , Text
"error"          forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= 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"           forall a. EncodeTCM a => Text -> a -> TCM Pair
@= forall a. Pretty a => a -> Value
encodePretty QName
q
  , Text
"sort"           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"           forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= a -> TCM Value
f a
t
  , Text
"lock"           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"           forall a. EncodeTCM a => Text -> a -> TCM Pair
@= forall a. Pretty a => a -> Value
encodePretty Modality
mod
  , Text
"term"          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" forall a. EncodeTCM a => Text -> a -> TCM Pair
@= forall a. Pretty a => a -> Value
encodePretty Name
name
  , Text
"term" forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= 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"      forall a. EncodeTCM a => Text -> a -> TCM Pair
@= Range
range
    , Text
"problems"   forall a. EncodeTCM a => Text -> a -> TCM Pair
@= [ProblemId]
problems
    , Text
"unblocker"  forall a. EncodeTCM a => Text -> a -> TCM Pair
@= Blocker
unblock
    , Text
"constraint" forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= forall a b.
(a -> TCM Value)
-> (b -> TCM Value) -> OutputConstraint b a -> TCM Value
encodeOC (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Pretty a => a -> Value
encodePretty) (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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" forall a. EncodeTCM a => Text -> a -> TCM Pair
@= MetaId
x ]
  encodeTCM (UnblockOnProblem ProblemId
p) = Text -> [TCM Pair] -> TCM Value
kind Text
"UnblockOnProblem" [ Text
"id" forall a. EncodeTCM a => Text -> a -> TCM Pair
@= ProblemId
p ]
  encodeTCM (UnblockOnDef QName
q)     = Text -> [TCM Pair] -> TCM Value
kind Text
"UnblockOnDef" [ Text
"name" forall a. EncodeTCM a => Text -> a -> TCM Pair
@= forall a. Pretty a => a -> Value
encodePretty QName
q ]
  encodeTCM (UnblockOnAll Set Blocker
us)    = Text -> [TCM Pair] -> TCM Value
kind Text
"UnblockOnAll" [ Text
"blockers" forall a. EncodeTCM a => Text -> a -> TCM Pair
@= 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" forall a. EncodeTCM a => Text -> a -> TCM Pair
@= 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"           forall a. EncodeTCM a => Text -> a -> TCM Pair
@= forall a. Pretty a => a -> Value
encodePretty CompilerBackend
backend
    , Text
"warnings"          forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= forall a. EncodeTCM a => a -> TCM Value
encodeTCM ([TCWarning] -> [TCWarning]
filterTCWarnings (WarningsAndNonFatalErrors -> [TCWarning]
tcWarnings WarningsAndNonFatalErrors
wes))
    , Text
"errors"            forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= 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"       forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [OutputForm Expr Expr]
constraints 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"      forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= 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 -> forall (m :: * -> *) a.
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
 MonadTCEnv m, MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId (forall a b. OutputForm a b -> b
B.outputFormId forall a b. (a -> b) -> a -> b
$ forall a b.
Range
-> [ProblemId] -> Blocker -> OutputConstraint a b -> OutputForm a b
OutputForm forall a. Range' a
noRange [] Blocker
alwaysUnblock OutputConstraint Expr InteractionId
i) forall a b. (a -> b) -> a -> b
$ forall a b.
(a -> TCM Value)
-> (b -> TCM Value) -> OutputConstraint b a -> TCM Value
encodeOC forall a. EncodeTCM a => a -> TCM Value
encodeTCM forall a. PrettyTCM a => a -> TCM Value
encodePrettyTCM OutputConstraint Expr InteractionId
i)
    , Text
"invisibleGoals"    forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [OutputConstraint Expr NamedMeta]
invis (forall a b.
(a -> TCM Value)
-> (b -> TCM Value) -> OutputConstraint b a -> TCM Value
encodeOC forall a. EncodeTCM a => a -> TCM Value
encodeTCM forall a. PrettyTCM a => a -> TCM Value
encodePrettyTCM)
    , Text
"warnings"          forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= forall a. EncodeTCM a => a -> TCM Value
encodeTCM ([TCWarning] -> [TCWarning]
filterTCWarnings (WarningsAndNonFatalErrors -> [TCWarning]
tcWarnings WarningsAndNonFatalErrors
wes))
    , Text
"errors"            forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= 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"              forall a. EncodeTCM a => Text -> a -> TCM Pair
@= CPUTime
time
    ]
  encodeTCM (Info_Error Info_Error
err) = 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"      forall a. EncodeTCM a => Text -> a -> TCM Pair
@= forall a b. (a -> b) -> [a] -> [b]
map forall a. ToJSON a => a -> Value
toJSON [String]
introductions
    ]
  encodeTCM (Info_Auto String
info) = Text -> [TCM Pair] -> TCM Value
kind Text
"Auto"
    [ Text
"info"              forall a. EncodeTCM a => Text -> a -> TCM Pair
@= 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"          forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Name, Type)]
contents forall a. PrettyTCM a => (Name, a) -> TCM Value
encodeNamedPretty
    , Text
"telescope"         forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (forall t. Tele (Dom t) -> [Dom (String, t)]
telToList Telescope
tele) forall a. PrettyTCM a => Dom (String, a) -> TCM Value
encodeDomType
    , Text
"names"             forall a. EncodeTCM a => Text -> a -> TCM Pair
@= forall a b. (a -> b) -> [a] -> [b]
map 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"       forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= forall a. PrettyTCM a => a -> TCM Value
encodePrettyTCM (forall t e. Dom' t e -> e
unDom Dom (String, a)
dom)
        , Text
"name"      forall a. EncodeTCM a => Text -> a -> TCM Pair
@= forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Pretty a => a -> Value
encodePretty (forall a. (LensNamed a, NameOf a ~ NamedName) => a -> Maybe String
bareNameOf Dom (String, a)
dom)
        , Text
"finite"    forall a. EncodeTCM a => Text -> a -> TCM Pair
@= forall a. ToJSON a => a -> Value
toJSON (forall t e. Dom' t e -> Bool
domIsFinite Dom (String, a)
dom)
        , Text
"cohesion"  forall a. EncodeTCM a => Text -> a -> TCM Pair
@= forall a. Show a => a -> Value
encodeShow (Modality -> Cohesion
modCohesion forall b c a. (b -> c) -> (a -> b) -> a -> c
. ArgInfo -> Modality
argInfoModality forall a b. (a -> b) -> a -> b
$ forall t e. Dom' t e -> ArgInfo
domInfo Dom (String, a)
dom)
        , Text
"relevance" forall a. EncodeTCM a => Text -> a -> TCM Pair
@= forall a. Show a => a -> Value
encodeShow (Modality -> Relevance
modRelevance forall b c a. (b -> c) -> (a -> b) -> a -> c
. ArgInfo -> Modality
argInfoModality forall a b. (a -> b) -> a -> b
$ forall t e. Dom' t e -> ArgInfo
domInfo Dom (String, a)
dom)
        , Text
"hiding"    forall a. EncodeTCM a => Text -> a -> TCM Pair
@= case ArgInfo -> Hiding
argInfoHiding forall a b. (a -> b) -> a -> b
$ forall t e. Dom' t e -> ArgInfo
domInfo Dom (String, a)
dom of
          Instance Overlappable
o -> forall a. Show a => a -> String
show Overlappable
o
          Hiding
o -> 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"           forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Name, Type)]
results forall a. PrettyTCM a => (Name, a) -> TCM Value
encodeNamedPretty
    , Text
"search"            forall a. EncodeTCM a => Text -> a -> TCM Pair
@= 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"             forall a. EncodeTCM a => Text -> a -> TCM Pair
@= forall a. Pretty a => a -> String
prettyShow QName
y
    , Text
"filepath"          forall a. EncodeTCM a => Text -> a -> TCM Pair
@= forall a. ToJSON a => a -> Value
toJSON String
path
    -- use Emacs message first
    , Text
"message"           forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= 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"      forall a. EncodeTCM a => Text -> a -> TCM Pair
@= CommandState
commandState
    , Text
"computeMode"       forall a. EncodeTCM a => Text -> a -> TCM Pair
@= ComputeMode
computeMode
    , Text
"time"              forall a. EncodeTCM a => Text -> a -> TCM Pair
@= Maybe CPUTime
time
    , Text
"expr"              forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= 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"      forall a. EncodeTCM a => Text -> a -> TCM Pair
@= CommandState
commandState
    , Text
"time"              forall a. EncodeTCM a => Text -> a -> TCM Pair
@= Maybe CPUTime
time
    , Text
"expr"              forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= 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"  forall a. EncodeTCM a => Text -> a -> TCM Pair
@= InteractionId
ii
    , Text
"context"           forall a. EncodeTCM a => Text -> a -> TCM Pair
@= [ResponseContextEntry]
ctx
    ]
  encodeTCM DisplayInfo
Info_Version = Text -> [TCM Pair] -> TCM Value
kind Text
"Version"
    [ Text
"version"           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"  forall a. EncodeTCM a => Text -> a -> TCM Pair
@= InteractionId
ii
    , Text
"goalInfo"          forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= 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) = Text -> [TCM Pair] -> TCM Value
kind Text
"GoalAndHave"
    [ Text
"expr" forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= forall a. PrettyTCM a => a -> TCM Value
encodePrettyTCM Expr
expr ]
  encodeTCM (GoalAndElaboration Term
term) = Text -> [TCM Pair] -> TCM Value
kind Text
"GoalAndElaboration"
    [ Text
"term" forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= 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"   forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (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" forall a. EncodeTCM a => Text -> a -> TCM Pair
@= ComputeMode
computeMode
    , Text
"expr"        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 [IPBoundary' Expr]
boundary [OutputForm Expr Expr]
outputForms) = Text -> [TCM Pair] -> TCM Value
kind Text
"GoalType"
    [ Text
"rewrite"     forall a. EncodeTCM a => Text -> a -> TCM Pair
@= Rewrite
rewrite
    , Text
"typeAux"     forall a. EncodeTCM a => Text -> a -> TCM Pair
@= GoalTypeAux
goalType
    , Text
"type"        forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= Rewrite -> InteractionId -> TCMT IO Doc
prettyTypeOfMeta Rewrite
rewrite InteractionId
ii
    , Text
"entries"     forall a. EncodeTCM a => Text -> a -> TCM Pair
@= [ResponseContextEntry]
entries
    , Text
"boundary"    forall a. EncodeTCM a => Text -> a -> TCM Pair
@= forall a b. (a -> b) -> [a] -> [b]
map forall a. Pretty a => a -> Value
encodePretty [IPBoundary' Expr]
boundary
    , Text
"outputForms" forall a. EncodeTCM a => Text -> a -> TCM Pair
@= forall a b. (a -> b) -> [a] -> [b]
map 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"     forall a. EncodeTCM a => Text -> a -> TCM Pair
@= Rewrite
rewrite
    , Text
"type"        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"        forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= 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"          forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= (TCErr -> TCM [TCWarning]
getAllWarningsOfTCErr TCErr
err
                            forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall a. EncodeTCM a => a -> TCM Value
encodeTCM forall b c a. (b -> c) -> (a -> b) -> a -> c
. [TCWarning] -> [TCWarning]
filterTCWarnings)
    , Text
"error"             forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= forall a. EncodeTCM a => a -> TCM Value
encodeTCM TCErr
err
    ]
  encodeTCM Info_Error
err = Text -> [TCM Pair] -> TCM Value
kind Text
"Error"
    [ Text
"warnings"          forall a. EncodeTCM a => Text -> a -> TCM Pair
@= ([] :: [String])
    , Text
"error"             forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= [TCM Pair] -> TCM Value
obj
      [ Text
"message"           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"     forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= 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"     forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= (Doc -> String
P.render forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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) =
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO 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"          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"    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"    forall a. EncodeTCM a => Text -> a -> TCM Pair
@= Nat
debugLevel
    , Text
"message"       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"        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"      forall a. EncodeTCM a => Text -> a -> TCM Pair
@= String
filepath
    , Text
"position"      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" 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"  forall a. EncodeTCM a => Text -> a -> TCM Pair
@= InteractionId
i
    , Text
"giveResult"        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"  forall a. EncodeTCM a => Text -> a -> TCM Pair
@= InteractionId
id
    , Text
"variant"           forall a. EncodeTCM a => Text -> a -> TCM Pair
@= MakeCaseVariant
variant
    , Text
"clauses"           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"     forall a. EncodeTCM a => Text -> a -> TCM Pair
@= forall a b. (a -> b) -> [a] -> [b]
map 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"  forall a. ToJSON a => Text -> a -> Pair
.= a
i
        , Text
"expression"        forall a. ToJSON a => Text -> a -> Pair
.= 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 -> TCM ByteString
jsonifyResponse = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. ToJSON a => a -> ByteString
encode forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall a. EncodeTCM a => a -> TCM Value
encodeTCM