module Agda.Interaction.JSONTop
( jsonREPL
) where
import Control.Monad ( (<=<), forM )
import Control.Monad.IO.Class ( MonadIO(..) )
import Data.ByteString.Lazy (ByteString)
import qualified Data.ByteString.Lazy.Char8 as BS
import qualified Data.Text as T
import qualified Data.Set as Set
import Agda.Interaction.AgdaTop
import Agda.Interaction.Base
(CommandState(..), CurrentFile(..), ComputeMode(..), Rewrite(..), OutputForm(..), OutputConstraint(..))
import qualified Agda.Interaction.BasicOps as B
import Agda.Interaction.EmacsTop
import Agda.Interaction.JSON
import Agda.Interaction.Response as R
import Agda.Interaction.Highlighting.JSON
import Agda.Syntax.Abstract.Pretty (prettyATop)
import Agda.Syntax.Common
import qualified Agda.Syntax.Concrete as C
import Agda.Syntax.Concrete.Name (NameInScope(..), Name)
import Agda.Syntax.Internal (telToList, Dom'(..), Dom, MetaId(..), ProblemId(..), Blocker(..), alwaysUnblock)
import Agda.Syntax.Position (Range, rangeIntervals, Interval'(..), Position'(..), noRange)
import Agda.VersionCommit
import Agda.TypeChecking.Errors (getAllWarningsOfTCErr)
import Agda.TypeChecking.Monad (Comparison(..), inTopContext, TCM, TCErr, TCWarning, NamedMeta(..), withInteractionId)
import Agda.TypeChecking.Monad.MetaVars (getInteractionRange, getMetaRange, withMetaId)
import Agda.TypeChecking.Pretty (PrettyTCM(..), prettyTCM)
import Agda.TypeChecking.Pretty.Warning (filterTCWarnings)
import Agda.TypeChecking.Warnings (WarningsAndNonFatalErrors(..))
import Agda.Utils.Pretty (Pretty(..))
import qualified Agda.Utils.Pretty as P
import Agda.Utils.Time (CPUTime(..))
jsonREPL :: 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
]
instance EncodeTCM CurrentFile where
instance ToJSON CurrentFile where
toJSON :: CurrentFile -> Value
toJSON (CurrentFile AbsolutePath
path [String]
_ ClockTime
time) = forall a. ToJSON a => a -> Value
toJSON (AbsolutePath
path, ClockTime
time)
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 MetaId where toJSON :: MetaId -> Value
toJSON (MetaId Nat
i) = 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" 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.
(MonadFail m, MonadTCEnv m, ReadTCState m, MonadTrace 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 :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Range
getMetaRange (NamedMeta -> MetaId
nmid NamedMeta
m)
instance EncodeTCM GiveResult where
instance ToJSON GiveResult where
toJSON :: GiveResult -> Value
toJSON (Give_String String
s) = [Pair] -> Value
object [ Text
"str" 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]
]
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
[ 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
]
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 (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.
(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
domFinite 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 String
thing String
path Maybe LocalVar
v [AbstractName]
xs [AbstractModule]
ms) = Text -> [TCM Pair] -> TCM Value
kind Text
"WhyInScope"
[ Text
"thing" forall a. EncodeTCM a => Text -> a -> TCM Pair
@= String
thing
, Text
"filepath" forall a. EncodeTCM a => Text -> a -> TCM Pair
@= forall a. ToJSON a => a -> Value
toJSON String
path
, Text
"message" 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" 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.
(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, Show 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. Show a => a -> String
show a
expr
]
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