module Agda.Interaction.JSONTop
    ( jsonREPL
    ) where
import Control.Monad.State
import Control.Monad

import Data.Aeson hiding (Result(..))
import Data.ByteString.Lazy (ByteString)
import qualified Data.ByteString.Lazy.Char8 as BS
import qualified Data.Text as T

import Agda.Interaction.AgdaTop
import Agda.Interaction.Base
  (CommandState(..), 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 qualified Agda.Syntax.Abstract as A
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)
import Agda.Syntax.Position (noRange, Range, rangeIntervals, Interval'(..), Position'(..))
import Agda.VersionCommit

import Agda.TypeChecking.Monad (Comparison(..), inTopContext, ProblemId(..), TCM)
import Agda.TypeChecking.Monad.MetaVars (getInteractionRange)
import Agda.TypeChecking.Pretty (PrettyTCM(..), prettyTCM)
-- borrowed from EmacsTop, for temporarily serialising stuff
import Agda.TypeChecking.Pretty.Warning (prettyTCWarnings, prettyTCWarnings')
import Agda.TypeChecking.Warnings (WarningsAndNonFatalErrors(..))
import Agda.Utils.Pretty (Pretty(..), render)
import Agda.Utils.Time (CPUTime(..))

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

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

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

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

instance EncodeTCM Status where
instance ToJSON Status where
  toJSON :: Status -> Value
toJSON Status
status = [Pair] -> Value
object
    [ Text
"showImplicitArguments" Text -> Bool -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= Status -> Bool
sShowImplicitArguments Status
status
    , Text
"checked"               Text -> Bool -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= 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 kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= CommandState -> [InteractionId]
theInteractionPoints CommandState
commandState
    , Text
"currentFile"       Text -> Maybe (AbsolutePath, ClockTime) -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= CommandState -> Maybe (AbsolutePath, ClockTime)
theCurrentFile CommandState
commandState
    -- more?
    ]

instance EncodeTCM ResponseContextEntry where
  encodeTCM :: ResponseContextEntry -> TCM Value
encodeTCM ResponseContextEntry
entry = [TCM Pair] -> TCM Value
obj
    [ Text
"originalName" Text -> Value -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= Name -> Value
forall a. Pretty a => a -> Value
encodePretty (ResponseContextEntry -> Name
respOrigName ResponseContextEntry
entry)
    , Text
"reifiedName"  Text -> Value -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= Name -> Value
forall a. Pretty a => a -> Value
encodePretty (ResponseContextEntry -> Name
respReifName ResponseContextEntry
entry)
    , Text
"binding"      Text -> TCM Value -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= Arg Expr -> TCM Value
forall a. PrettyTCM a => a -> TCM Value
encodePrettyTCM (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 kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= 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 kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= 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 kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= 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 kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= Interval' a -> Position' a
forall a. Interval' a -> Position' a
iStart Interval' a
i, Text
"end" Text -> Position' a -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= Interval' a -> Position' a
forall a. Interval' a -> Position' a
iEnd Interval' a
i ]

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

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

instance EncodeTCM GiveResult where
instance ToJSON GiveResult where
  toJSON :: GiveResult -> Value
toJSON (Give_String String
s) = [Pair] -> Value
object [ Text
"str" Text -> String -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= String
s ]
  toJSON GiveResult
Give_Paren   = [Pair] -> Value
object [ Text
"paren" Text -> Bool -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= Bool
True ]
  toJSON GiveResult
Give_NoParen = [Pair] -> Value
object [ Text
"paren" Text -> Bool -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= 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 :: 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 :: 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 :: 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
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 -> Value)
  -> Comparison -> a -> a -> T.Text
  -> TCM Value
encodeOCCmp :: (a -> Value) -> Comparison -> a -> a -> Text -> TCM Value
encodeOCCmp a -> 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 -> [Value] -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= (a -> Value) -> [a] -> [Value]
forall a b. (a -> b) -> [a] -> [b]
map a -> Value
f [a
i, a
j]
  ]

  -- Goals
encodeOC :: (a -> Value)
  -> (b -> TCM Value)
  -> OutputConstraint b a
  -> TCM Value
encodeOC :: (a -> Value)
-> (b -> TCM Value) -> OutputConstraint b a -> TCM Value
encodeOC a -> Value
f b -> TCM Value
encodePrettyTCM = \case
 OfType a
i b
a -> Text -> [TCM Pair] -> TCM Value
kind Text
"OfType"
  [ Text
"constraintObj" Text -> Value -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= a -> Value
f a
i
  , Text
"type"          Text -> TCM Value -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= b -> TCM Value
encodePrettyTCM 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
encodePrettyTCM b
a
  , Text
"constraintObjs" Text -> [Value] -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= (a -> Value) -> [a] -> [Value]
forall a b. (a -> b) -> [a] -> [b]
map a -> 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
encodePrettyTCM b
a
  , Text
"constraintObjs" Text -> [[Value]] -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= ([a] -> [Value]) -> [[a]] -> [[Value]]
forall a b. (a -> b) -> [a] -> [b]
map ((a -> Value) -> [a] -> [Value]
forall a b. (a -> b) -> [a] -> [b]
map a -> Value
f) [[a]
is, [a]
js]
  ]
 JustType a
a -> Text -> [TCM Pair] -> TCM Value
kind Text
"JustType"
  [ Text
"constraintObj"  Text -> Value -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= a -> Value
f a
a
  ]
 JustSort a
a -> Text -> [TCM Pair] -> TCM Value
kind Text
"JustSort"
  [ Text
"constraintObj"  Text -> Value -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= a -> Value
f a
a
  ]
 CmpTypes  Comparison
c a
i a
j -> (a -> Value) -> Comparison -> a -> a -> Text -> TCM Value
forall a. (a -> Value) -> Comparison -> a -> a -> Text -> TCM Value
encodeOCCmp a -> Value
f Comparison
c a
i a
j Text
"CmpTypes"
 CmpLevels Comparison
c a
i a
j -> (a -> Value) -> Comparison -> a -> a -> Text -> TCM Value
forall a. (a -> Value) -> Comparison -> a -> a -> Text -> TCM Value
encodeOCCmp a -> Value
f Comparison
c a
i a
j Text
"CmpLevels"
 CmpTeles  Comparison
c a
i a
j -> (a -> Value) -> Comparison -> a -> a -> Text -> TCM Value
forall a. (a -> Value) -> Comparison -> a -> a -> Text -> TCM Value
encodeOCCmp a -> Value
f Comparison
c a
i a
j Text
"CmpTeles"
 CmpSorts  Comparison
c a
i a
j -> (a -> Value) -> Comparison -> a -> a -> Text -> TCM Value
forall a. (a -> Value) -> Comparison -> a -> a -> Text -> TCM Value
encodeOCCmp a -> Value
f Comparison
c a
i a
j Text
"CmpSorts"
 Guard OutputConstraint b a
oc ProblemId
a -> Text -> [TCM Pair] -> TCM Value
kind Text
"Guard"
  [ Text
"constraint"     Text -> TCM Value -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= (a -> Value)
-> (b -> TCM Value) -> OutputConstraint b a -> TCM Value
forall a b.
(a -> Value)
-> (b -> TCM Value) -> OutputConstraint b a -> TCM Value
encodeOC a -> Value
f b -> TCM Value
encodePrettyTCM OutputConstraint b a
oc
  , Text
"problem"        Text -> ProblemId -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= ProblemId
a
  ]
 Assign a
i b
a -> Text -> [TCM Pair] -> TCM Value
kind Text
"Assign"
  [ Text
"constraintObj"  Text -> Value -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= a -> Value
f a
i
  , Text
"value"          Text -> TCM Value -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= b -> TCM Value
encodePrettyTCM b
a
  ]
 TypedAssign a
i b
v b
t -> Text -> [TCM Pair] -> TCM Value
kind Text
"TypedAssign"
  [ Text
"constraintObj"  Text -> Value -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= a -> Value
f a
i
  , Text
"value"          Text -> TCM Value -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= b -> TCM Value
encodePrettyTCM b
v
  , Text
"type"           Text -> TCM Value -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= b -> TCM Value
encodePrettyTCM b
t
  ]
 PostponedCheckArgs a
i [b]
es b
t0 b
t1 -> Text -> [TCM Pair] -> TCM Value
kind Text
"PostponedCheckArgs"
  [ Text
"constraintObj"  Text -> Value -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= a -> Value
f a
i
  , Text
"ofType"         Text -> TCM Value -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= b -> TCM Value
encodePrettyTCM 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
encodePrettyTCM
  , Text
"type"           Text -> TCM Value -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= b -> TCM Value
encodePrettyTCM 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
encodePrettyTCM 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
encodePrettyTCM b
a
  ]
 FindInstanceOF a
i b
t [(b, b)]
cs -> Text -> [TCM Pair] -> TCM Value
kind Text
"FindInstanceOF"
  [ Text
"constraintObj"  Text -> Value -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= a -> Value
f a
i
  , Text
"candidates"     Text -> TCM [Value] -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= [(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)]
cs (b, b) -> TCM Value
encodeKVPairs
  , Text
"type"           Text -> TCM Value -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= b -> TCM Value
encodePrettyTCM b
t
  ]
  where encodeKVPairs :: (b, b) -> TCM Value
encodeKVPairs (b
v, b
t) = [TCM Pair] -> TCM Value
obj
          [ Text
"value"  Text -> TCM Value -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= b -> TCM Value
encodePrettyTCM b
v
          , Text
"type"   Text -> TCM Value -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= b -> TCM Value
encodePrettyTCM b
t
          ]
 PTSInstance a
a a
b -> Text -> [TCM Pair] -> TCM Value
kind Text
"PTSInstance"
  [ Text
"constraintObjs" Text -> [Value] -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= (a -> Value) -> [a] -> [Value]
forall a b. (a -> b) -> [a] -> [b]
map a -> Value
f [a
a, a
b]
  ]
 PostponedCheckFunDef QName
name b
a -> 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
encodePrettyTCM b
a
  ]

encodeNamedPretty :: PrettyTCM a => (Name, a) -> TCM Value
encodeNamedPretty :: (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 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
"constraint" Text -> TCM Value -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= (Expr -> Value)
-> (Expr -> TCM Value) -> OutputConstraint Expr Expr -> TCM Value
forall a b.
(a -> Value)
-> (b -> TCM Value) -> OutputConstraint b a -> TCM Value
encodeOC Expr -> Value
forall a. Show a => a -> Value
encodeShow (Value -> TCM Value
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value -> TCM Value) -> (Expr -> Value) -> Expr -> TCM Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Value
forall a. Show a => a -> Value
encodeShow) OutputConstraint Expr Expr
oc
    ]

instance EncodeTCM DisplayInfo where
  encodeTCM :: DisplayInfo -> TCM Value
encodeTCM (Info_CompilationOk WarningsAndNonFatalErrors
wes) = Text -> [TCM Pair] -> TCM Value
kind Text
"CompilationOk"
    [ Text
"warnings"          Text -> TCM String -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= [TCWarning] -> TCM String
prettyTCWarnings (WarningsAndNonFatalErrors -> [TCWarning]
tcWarnings WarningsAndNonFatalErrors
wes)
    , Text
"errors"            Text -> TCM String -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= [TCWarning] -> TCM String
prettyTCWarnings (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 ((InteractionId -> Value)
-> (Expr -> TCM Value)
-> OutputConstraint Expr InteractionId
-> TCM Value
forall a b.
(a -> Value)
-> (b -> TCM Value) -> OutputConstraint b a -> TCM Value
encodeOC InteractionId -> Value
forall a. ToJSON a => a -> Value
toJSON Expr -> TCM Value
forall a. PrettyTCM a => a -> TCM Value
encodePrettyTCM)
    , 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 -> Value)
-> (Expr -> TCM Value)
-> OutputConstraint Expr NamedMeta
-> TCM Value
forall a b.
(a -> Value)
-> (b -> TCM Value) -> OutputConstraint b a -> TCM Value
encodeOC NamedMeta -> Value
forall a. Pretty a => a -> Value
encodePretty Expr -> TCM Value
forall a. PrettyTCM a => a -> TCM Value
encodePrettyTCM)
    , Text
"warnings"          Text -> TCM String -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= [TCWarning] -> TCM String
prettyTCWarnings (WarningsAndNonFatalErrors -> [TCWarning]
tcWarnings WarningsAndNonFatalErrors
wes)
    , Text
"errors"            Text -> TCM String -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= [TCWarning] -> TCM String
prettyTCWarnings (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
msg) = Text -> [TCM Pair] -> TCM Value
kind Text
"Error"
    [ Text
"message"           Text -> TCM String -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= Info_Error -> TCM String
showInfoError Info_Error
msg
    ]
  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 :: Dom (String, a) -> TCM Value
encodeDomType Dom (String, a)
dom = [TCM Pair] -> TCM Value
obj
        [ Text
"dom"       Text -> TCM Value -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= (String, a) -> TCM Value
forall a. PrettyTCM a => a -> TCM Value
encodePrettyTCM (Dom (String, a) -> (String, a)
forall t e. Dom' t e -> e
unDom Dom (String, a)
dom)
        , Text
"name"      Text -> Maybe Value -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= (String -> Value) -> Maybe String -> Maybe Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap String -> Value
forall a. Pretty a => a -> Value
encodePretty (Dom (String, a) -> Maybe String
forall a. LensNamed NamedName a => a -> Maybe String
bareNameOf Dom (String, a)
dom)
        , Text
"finite"    Text -> Value -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= Bool -> Value
forall a. ToJSON a => a -> Value
toJSON (Dom (String, a) -> Bool
forall t e. Dom' t e -> Bool
domFinite Dom (String, a)
dom)
        , Text
"cohesion"  Text -> Value -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= Cohesion -> Value
forall a. Show a => a -> Value
encodeShow (Modality -> Cohesion
modCohesion (Modality -> Cohesion)
-> (ArgInfo -> Modality) -> ArgInfo -> Cohesion
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ArgInfo -> Modality
argInfoModality (ArgInfo -> Cohesion) -> ArgInfo -> Cohesion
forall a b. (a -> b) -> a -> b
$ Dom (String, a) -> ArgInfo
forall t e. Dom' t e -> ArgInfo
domInfo Dom (String, a)
dom)
        , Text
"relevance" Text -> Value -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= Relevance -> Value
forall a. Show a => a -> Value
encodeShow (Modality -> Relevance
modRelevance (Modality -> Relevance)
-> (ArgInfo -> Modality) -> ArgInfo -> Relevance
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ArgInfo -> Modality
argInfoModality (ArgInfo -> Relevance) -> ArgInfo -> Relevance
forall a b. (a -> b) -> a -> b
$ Dom (String, a) -> ArgInfo
forall t e. Dom' t e -> ArgInfo
domInfo Dom (String, a)
dom)
        , Text
"hiding"    Text -> String -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= case ArgInfo -> Hiding
argInfoHiding (ArgInfo -> Hiding) -> ArgInfo -> Hiding
forall a b. (a -> b) -> a -> b
$ Dom (String, a) -> ArgInfo
forall t e. Dom' t e -> ArgInfo
domInfo Dom (String, a)
dom of
          Instance Overlappable
o -> Overlappable -> String
forall a. Show a => a -> String
show Overlappable
o
          Hiding
o -> Hiding -> String
forall a. Show a => a -> String
show Hiding
o
        ]
  encodeTCM (Info_SearchAbout [(Name, Type)]
results String
search) = Text -> [TCM Pair] -> TCM Value
kind Text
"SearchAbout"
    [ Text
"results"           Text -> TCM [Value] -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= [(Name, Type)] -> ((Name, Type) -> TCM Value) -> TCM [Value]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Name, Type)]
results (Name, Type) -> TCM Value
forall a. PrettyTCM a => (Name, a) -> TCM Value
encodeNamedPretty
    , Text
"search"            Text -> Value -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= String -> Value
forall a. ToJSON a => a -> Value
toJSON String
search
    ]
  encodeTCM (Info_WhyInScope String
thing String
path Maybe LocalVar
v [AbstractName]
xs [AbstractModule]
ms) = Text -> [TCM Pair] -> TCM Value
kind Text
"WhyInScope"
    [ Text
"thing"             Text -> String -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= String
thing
    , Text
"filepath"          Text -> Value -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= String -> Value
forall a. ToJSON a => a -> Value
toJSON String
path
    -- use Emacs message first
    , Text
"message"           Text -> TCMT IO Doc -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= String
-> String
-> Maybe LocalVar
-> [AbstractName]
-> [AbstractModule]
-> TCMT IO Doc
explainWhyInScope String
thing String
path Maybe LocalVar
v [AbstractName]
xs [AbstractModule]
ms
    ]
  encodeTCM (Info_NormalForm CommandState
commandState ComputeMode
computeMode Maybe CPUTime
time Expr
expr) = Text -> [TCM Pair] -> TCM Value
kind Text
"NormalForm"
    [ Text
"commandState"      Text -> CommandState -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= CommandState
commandState
    , Text
"computeMode"       Text -> ComputeMode -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= ComputeMode
computeMode
    , Text
"time"              Text -> Maybe CPUTime -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= Maybe CPUTime
time
    , Text
"expr"              Text -> TCM Value -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= Expr -> TCM Value
forall a. PrettyTCM a => a -> TCM Value
encodePrettyTCM Expr
expr
    ]
  encodeTCM (Info_InferredType CommandState
commandState Maybe CPUTime
time Expr
expr) = Text -> [TCM Pair] -> TCM Value
kind Text
"InferredType"
    [ Text
"commandState"      Text -> CommandState -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= CommandState
commandState
    , Text
"time"              Text -> Maybe CPUTime -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= Maybe CPUTime
time
    , Text
"expr"              Text -> TCM Value -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= Expr -> TCM Value
forall a. PrettyTCM a => a -> TCM Value
encodePrettyTCM Expr
expr
    ]
  encodeTCM (Info_Context InteractionId
ii [ResponseContextEntry]
ctx) = Text -> [TCM Pair] -> TCM Value
kind Text
"Context"
    [ Text
"interactionPoint"  Text -> InteractionId -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= InteractionId
ii
    , Text
"context"           Text -> [ResponseContextEntry] -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= [ResponseContextEntry]
ctx
    ]
  encodeTCM DisplayInfo
Info_Version = Text -> [TCM Pair] -> TCM Value
kind Text
"Version"
    [ Text
"version"           Text -> String -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= (String
versionWithCommitInfo :: String)
    ]
  encodeTCM (Info_GoalSpecific InteractionId
ii GoalDisplayInfo
info) = Text -> [TCM Pair] -> TCM Value
kind Text
"GoalSpecific"
    [ Text
"interactionPoint"  Text -> InteractionId -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= InteractionId
ii
    , Text
"goalInfo"          Text -> TCM Value -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= InteractionId -> GoalDisplayInfo -> TCM Value
encodeGoalSpecific InteractionId
ii GoalDisplayInfo
info
    ]

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

encodeGoalSpecific :: InteractionId -> GoalDisplayInfo -> TCM Value
encodeGoalSpecific :: InteractionId -> GoalDisplayInfo -> TCM Value
encodeGoalSpecific InteractionId
ii = GoalDisplayInfo -> TCM Value
go
  where
  go :: GoalDisplayInfo -> TCM Value
go (Goal_HelperFunction OutputConstraint' Expr Expr
helperType) = Text -> [TCM Pair] -> TCM Value
kind Text
"HelperFunction"
    [ Text
"signature"   Text -> 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 c a (m :: * -> *).
(Pretty c, ToConcrete a c, 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 [IPBoundary' Expr]
boundary [OutputForm Expr Expr]
outputForms) = Text -> [TCM Pair] -> TCM Value
kind Text
"GoalType"
    [ Text
"rewrite"     Text -> Rewrite -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= Rewrite
rewrite
    , Text
"typeAux"     Text -> GoalTypeAux -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= GoalTypeAux
goalType
    , Text
"type"        Text -> 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
@= (IPBoundary' Expr -> Value) -> [IPBoundary' Expr] -> [Value]
forall a b. (a -> b) -> [a] -> [b]
map IPBoundary' Expr -> Value
forall a. Pretty a => a -> Value
encodePretty [IPBoundary' Expr]
boundary
    , Text
"outputForms" Text -> [Value] -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= (OutputForm Expr Expr -> Value)
-> [OutputForm Expr Expr] -> [Value]
forall a b. (a -> b) -> [a] -> [b]
map OutputForm Expr Expr -> Value
forall a. Pretty a => a -> Value
encodePretty [OutputForm Expr Expr]
outputForms
    ]
  go (Goal_CurrentGoal Rewrite
rewrite) = Text -> [TCM Pair] -> TCM Value
kind Text
"CurrentGoal"
    [ Text
"rewrite"     Text -> Rewrite -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= Rewrite
rewrite
    , Text
"type"        Text -> 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 c a (m :: * -> *).
(Pretty c, ToConcrete a c, MonadAbsToCon m) =>
a -> m Doc
prettyATop Expr
expr
    ]

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

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