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(..)
, OutputConstraint_boot(..), OutputForm_boot(..))
import Agda.Interaction.Output (OutputConstraint, OutputForm)
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 )
import Agda.TypeChecking.Pretty.Warning
( filterTCWarnings )
import Agda.TypeChecking.Warnings
( WarningsAndNonFatalErrors(..) )
import qualified Agda.Syntax.Common.Pretty as P
import Agda.Syntax.Common.Pretty
( Pretty(..), prettyShow )
import Agda.Utils.Time
( CPUTime(..) )
import Agda.VersionCommit
jsonREPL :: TCM () -> TCM ()
jsonREPL :: TCM () -> TCM ()
jsonREPL = InteractionOutputCallback -> String -> TCM () -> TCM ()
repl (IO () -> TCM ()
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> TCM ()) -> (ByteString -> IO ()) -> ByteString -> TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> IO ()
BS.putStrLn (ByteString -> TCM ())
-> (Response -> TCMT IO ByteString) -> InteractionOutputCallback
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Response -> TCMT IO ByteString
jsonifyResponse) String
"JSON> "
instance EncodeTCM NameInScope where
instance ToJSON NameInScope where
toJSON :: NameInScope -> Value
toJSON NameInScope
InScope = Bool -> Value
forall a. ToJSON a => a -> Value
toJSON Bool
True
toJSON NameInScope
NotInScope = Bool -> Value
forall a. ToJSON a => a -> Value
toJSON Bool
False
instance EncodeTCM Status where
instance ToJSON Status where
toJSON :: Status -> Value
toJSON Status
status = [Pair] -> Value
object
[ Text
"showImplicitArguments" Text -> Bool -> Pair
forall a. ToJSON a => Text -> a -> Pair
.= Status -> Bool
sShowImplicitArguments Status
status
, Text
"showIrrelevantArguments" Text -> Bool -> Pair
forall a. ToJSON a => Text -> a -> Pair
.= Status -> Bool
sShowIrrelevantArguments Status
status
, Text
"checked" Text -> Bool -> Pair
forall a. ToJSON a => Text -> a -> Pair
.= Status -> Bool
sChecked Status
status
]
instance EncodeTCM CommandState where
instance ToJSON CommandState where
toJSON :: CommandState -> Value
toJSON CommandState
commandState = [Pair] -> Value
object
[ Text
"interactionPoints" Text -> [InteractionId] -> Pair
forall a. ToJSON a => Text -> a -> Pair
.= CommandState -> [InteractionId]
theInteractionPoints CommandState
commandState
, Text
"currentFile" Text -> Maybe CurrentFile -> Pair
forall a. ToJSON a => Text -> a -> Pair
.= CommandState -> Maybe CurrentFile
theCurrentFile CommandState
commandState
]
instance EncodeTCM CurrentFile where
instance ToJSON CurrentFile where
toJSON :: CurrentFile -> Value
toJSON (CurrentFile AbsolutePath
path TopLevelModuleName
_ [String]
_ ClockTime
time) = (AbsolutePath, ClockTime) -> Value
forall a. ToJSON a => a -> Value
toJSON (AbsolutePath
path, ClockTime
time)
instance EncodeTCM ResponseContextEntry where
encodeTCM :: ResponseContextEntry -> TCM Value
encodeTCM ResponseContextEntry
entry = [TCM Pair] -> TCM Value
obj
[ Text
"originalName" Text -> Value -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= Name -> Value
forall a. Pretty a => a -> Value
encodePretty (ResponseContextEntry -> Name
respOrigName ResponseContextEntry
entry)
, Text
"reifiedName" Text -> Value -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= Name -> Value
forall a. Pretty a => a -> Value
encodePretty (ResponseContextEntry -> Name
respReifName ResponseContextEntry
entry)
, Text
"binding" Text -> TCMT IO Doc -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= Expr -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyATop (Arg Expr -> Expr
forall e. Arg e -> e
unArg (ResponseContextEntry -> Arg Expr
respType ResponseContextEntry
entry))
, Text
"inScope" Text -> NameInScope -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= ResponseContextEntry -> NameInScope
respInScope ResponseContextEntry
entry
]
instance EncodeTCM (Position' ()) where
instance ToJSON (Position' ()) where
toJSON :: Position' () -> Value
toJSON Position' ()
p = [Pair] -> Value
object
[ Text
"pos" Text -> Value -> Pair
forall a. ToJSON a => Text -> a -> Pair
.= Int32 -> Value
forall a. ToJSON a => a -> Value
toJSON (Position' () -> Int32
forall a. Position' a -> Int32
posPos Position' ()
p)
, Text
"line" Text -> Value -> Pair
forall a. ToJSON a => Text -> a -> Pair
.= Int32 -> Value
forall a. ToJSON a => a -> Value
toJSON (Position' () -> Int32
forall a. Position' a -> Int32
posLine Position' ()
p)
, Text
"col" Text -> Value -> Pair
forall a. ToJSON a => Text -> a -> Pair
.= Int32 -> Value
forall a. ToJSON a => a -> Value
toJSON (Position' () -> Int32
forall a. Position' a -> Int32
posCol Position' ()
p)
]
instance EncodeTCM Range where
instance ToJSON Range where
toJSON :: Range -> Value
toJSON = [Value] -> Value
forall a. ToJSON a => a -> Value
toJSON ([Value] -> Value) -> (Range -> [Value]) -> Range -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Interval' () -> Value) -> [Interval' ()] -> [Value]
forall a b. (a -> b) -> [a] -> [b]
map Interval' () -> Value
forall {a}. ToJSON (Position' a) => Interval' a -> Value
prettyInterval ([Interval' ()] -> [Value])
-> (Range -> [Interval' ()]) -> Range -> [Value]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range -> [Interval' ()]
forall a. Range' a -> [Interval' ()]
rangeIntervals
where prettyInterval :: Interval' a -> Value
prettyInterval Interval' a
i = [Pair] -> Value
object [ Text
"start" Text -> Position' a -> Pair
forall a. ToJSON a => Text -> a -> Pair
.= Interval' a -> Position' a
forall a. Interval' a -> Position' a
iStart Interval' a
i, Text
"end" Text -> Position' a -> Pair
forall a. ToJSON a => Text -> a -> Pair
.= Interval' a -> Position' a
forall a. Interval' a -> Position' a
iEnd Interval' a
i ]
instance EncodeTCM ProblemId where
instance EncodeTCM MetaId where
instance ToJSON ProblemId where toJSON :: ProblemId -> Value
toJSON (ProblemId Nat
i) = Nat -> Value
forall a. ToJSON a => a -> Value
toJSON Nat
i
instance ToJSON ModuleNameHash where
toJSON :: ModuleNameHash -> Value
toJSON (ModuleNameHash Word64
h) = Word64 -> Value
forall a. ToJSON a => a -> Value
toJSON Word64
h
instance ToJSON MetaId where
toJSON :: MetaId -> Value
toJSON MetaId
m = [Pair] -> Value
object
[ Text
"id" Text -> Value -> Pair
forall a. ToJSON a => Text -> a -> Pair
.= Word64 -> Value
forall a. ToJSON a => a -> Value
toJSON (MetaId -> Word64
metaId MetaId
m)
, Text
"module" Text -> Value -> Pair
forall a. ToJSON a => Text -> a -> Pair
.= ModuleNameHash -> Value
forall a. ToJSON a => a -> Value
toJSON (MetaId -> ModuleNameHash
metaModule MetaId
m)
]
instance EncodeTCM InteractionId where
encodeTCM :: InteractionId -> TCM Value
encodeTCM ii :: InteractionId
ii@(InteractionId Nat
i) = [TCM Pair] -> TCM Value
obj
[ Text
"id" Text -> Value -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= Nat -> Value
forall a. ToJSON a => a -> Value
toJSON Nat
i
, Text
"range" Text -> TCM Value -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= TCM Value
intervalsTCM
]
where
intervalsTCM :: TCM Value
intervalsTCM = Range -> Value
forall a. ToJSON a => a -> Value
toJSON (Range -> Value) -> TCMT IO Range -> TCM Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> InteractionId -> TCMT IO Range
forall (m :: * -> *).
(MonadInteractionPoints m, MonadFail m, MonadError TCErr m) =>
InteractionId -> m Range
getInteractionRange InteractionId
ii
instance ToJSON InteractionId where
toJSON :: InteractionId -> Value
toJSON (InteractionId Nat
i) = Nat -> Value
forall a. ToJSON a => a -> Value
toJSON Nat
i
instance EncodeTCM NamedMeta where
encodeTCM :: NamedMeta -> TCM Value
encodeTCM NamedMeta
m = [TCM Pair] -> TCM Value
obj
[ Text
"name" Text -> TCM Value -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= TCM Value
nameTCM
, Text
"range" Text -> TCM Value -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= TCM Value
intervalsTCM
]
where
nameTCM :: TCM Value
nameTCM = Doc -> Value
forall a. Show a => a -> Value
encodeShow (Doc -> Value) -> TCMT IO Doc -> TCM Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m, MonadTCEnv m, MonadTrace m,
ReadTCState m) =>
MetaId -> m a -> m a
withMetaId (NamedMeta -> MetaId
nmid NamedMeta
m) (NamedMeta -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyATop NamedMeta
m)
intervalsTCM :: TCM Value
intervalsTCM = Range -> Value
forall a. ToJSON a => a -> Value
toJSON (Range -> Value) -> TCMT IO Range -> TCM Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> TCMT IO Range
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m Range
getMetaRange (NamedMeta -> MetaId
nmid NamedMeta
m)
instance EncodeTCM GiveResult where
instance ToJSON GiveResult where
toJSON :: GiveResult -> Value
toJSON (Give_String String
s) = [Pair] -> Value
object [ Text
"str" Text -> String -> Pair
forall a. ToJSON a => Text -> a -> Pair
.= String
s ]
toJSON GiveResult
Give_Paren = [Pair] -> Value
object [ Text
"paren" Text -> Bool -> Pair
forall a. ToJSON a => Text -> a -> Pair
.= Bool
True ]
toJSON GiveResult
Give_NoParen = [Pair] -> Value
object [ Text
"paren" Text -> Bool -> Pair
forall a. ToJSON a => Text -> a -> Pair
.= Bool
False ]
instance EncodeTCM MakeCaseVariant where
instance ToJSON MakeCaseVariant where
toJSON :: MakeCaseVariant -> Value
toJSON MakeCaseVariant
R.Function = Text -> Value
String Text
"Function"
toJSON MakeCaseVariant
R.ExtendedLambda = Text -> Value
String Text
"ExtendedLambda"
encodePretty :: Pretty a => a -> Value
encodePretty :: forall a. Pretty a => a -> Value
encodePretty = Doc -> Value
forall a. Show a => a -> Value
encodeShow (Doc -> Value) -> (a -> Doc) -> a -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Doc
forall a. Pretty a => a -> Doc
pretty
encodeShow :: Show a => a -> Value
encodeShow :: forall a. Show a => a -> Value
encodeShow = Text -> Value
String (Text -> Value) -> (a -> Text) -> a -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Text
T.pack (String -> Text) -> (a -> String) -> a -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> String
forall a. Show a => a -> String
show
encodePrettyTCM :: PrettyTCM a => a -> TCM Value
encodePrettyTCM :: forall a. PrettyTCM a => a -> TCM Value
encodePrettyTCM = (Doc -> Value
forall a. Show a => a -> Value
encodeShow (Doc -> Value) -> TCMT IO Doc -> TCM Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) (TCMT IO Doc -> TCM Value) -> (a -> TCMT IO Doc) -> a -> TCM Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => a -> m Doc
prettyTCM
instance EncodeTCM Rewrite where
instance ToJSON Rewrite where toJSON :: Rewrite -> Value
toJSON = Rewrite -> Value
forall a. Show a => a -> Value
encodeShow
instance EncodeTCM CPUTime where
instance ToJSON CPUTime where toJSON :: CPUTime -> Value
toJSON = CPUTime -> Value
forall a. Pretty a => a -> Value
encodePretty
instance EncodeTCM ComputeMode where
instance ToJSON ComputeMode where toJSON :: ComputeMode -> Value
toJSON = ComputeMode -> Value
forall a. Show a => a -> Value
encodeShow
encodeOCCmp :: (a -> TCM Value)
-> Comparison -> a -> a -> T.Text
-> TCM Value
encodeOCCmp :: forall a.
(a -> TCM Value) -> Comparison -> a -> a -> Text -> TCM Value
encodeOCCmp a -> TCM Value
f Comparison
c a
i a
j Text
k = Text -> [TCM Pair] -> TCM Value
kind Text
k
[ Text
"comparison" Text -> Value -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= Comparison -> Value
forall a. Show a => a -> Value
encodeShow Comparison
c
, Text
"constraintObjs" Text -> TCM [Value] -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= (a -> TCM Value) -> [a] -> TCM [Value]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse a -> TCM Value
f [a
i, a
j]
]
encodeOC :: (a -> TCM Value)
-> (b -> TCM Value)
-> OutputConstraint b a
-> TCM Value
encodeOC :: forall a b.
(a -> TCM Value)
-> (b -> TCM Value) -> OutputConstraint b a -> TCM Value
encodeOC a -> TCM Value
f b -> TCM Value
encPrettyTCM = \case
OfType a
i b
a -> Text -> [TCM Pair] -> TCM Value
kind Text
"OfType"
[ Text
"constraintObj" Text -> TCM Value -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= a -> TCM Value
f a
i
, Text
"type" Text -> TCM Value -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= b -> TCM Value
encPrettyTCM b
a
]
CmpInType Comparison
c b
a a
i a
j -> Text -> [TCM Pair] -> TCM Value
kind Text
"CmpInType"
[ Text
"comparison" Text -> Value -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= Comparison -> Value
forall a. Show a => a -> Value
encodeShow Comparison
c
, Text
"type" Text -> TCM Value -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= b -> TCM Value
encPrettyTCM b
a
, Text
"constraintObjs" Text -> TCM [Value] -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= (a -> TCM Value) -> [a] -> TCM [Value]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse a -> TCM Value
f [a
i, a
j]
]
CmpElim [Polarity]
ps b
a [a]
is [a]
js -> Text -> [TCM Pair] -> TCM Value
kind Text
"CmpElim"
[ Text
"polarities" Text -> [Value] -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= (Polarity -> Value) -> [Polarity] -> [Value]
forall a b. (a -> b) -> [a] -> [b]
map Polarity -> Value
forall a. Show a => a -> Value
encodeShow [Polarity]
ps
, Text
"type" Text -> TCM Value -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= b -> TCM Value
encPrettyTCM b
a
, Text
"constraintObjs" Text -> TCM [[Value]] -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= ([a] -> TCM [Value]) -> [[a]] -> TCM [[Value]]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse ((a -> TCM Value) -> [a] -> TCM [Value]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse a -> TCM Value
f) [[a]
is, [a]
js]
]
JustType a
a -> Text -> [TCM Pair] -> TCM Value
kind Text
"JustType"
[ Text
"constraintObj" Text -> TCM Value -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= a -> TCM Value
f a
a
]
JustSort a
a -> Text -> [TCM Pair] -> TCM Value
kind Text
"JustSort"
[ Text
"constraintObj" Text -> TCM Value -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= a -> TCM Value
f a
a
]
CmpTypes Comparison
c a
i a
j -> (a -> TCM Value) -> Comparison -> a -> a -> Text -> TCM Value
forall a.
(a -> TCM Value) -> Comparison -> a -> a -> Text -> TCM Value
encodeOCCmp a -> TCM Value
f Comparison
c a
i a
j Text
"CmpTypes"
CmpLevels Comparison
c a
i a
j -> (a -> TCM Value) -> Comparison -> a -> a -> Text -> TCM Value
forall a.
(a -> TCM Value) -> Comparison -> a -> a -> Text -> TCM Value
encodeOCCmp a -> TCM Value
f Comparison
c a
i a
j Text
"CmpLevels"
CmpTeles Comparison
c a
i a
j -> (a -> TCM Value) -> Comparison -> a -> a -> Text -> TCM Value
forall a.
(a -> TCM Value) -> Comparison -> a -> a -> Text -> TCM Value
encodeOCCmp a -> TCM Value
f Comparison
c a
i a
j Text
"CmpTeles"
CmpSorts Comparison
c a
i a
j -> (a -> TCM Value) -> Comparison -> a -> a -> Text -> TCM Value
forall a.
(a -> TCM Value) -> Comparison -> a -> a -> Text -> TCM Value
encodeOCCmp a -> TCM Value
f Comparison
c a
i a
j Text
"CmpSorts"
Assign a
i b
a -> Text -> [TCM Pair] -> TCM Value
kind Text
"Assign"
[ Text
"constraintObj" Text -> TCM Value -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= a -> TCM Value
f a
i
, Text
"value" Text -> TCM Value -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= b -> TCM Value
encPrettyTCM b
a
]
TypedAssign a
i b
v b
t -> Text -> [TCM Pair] -> TCM Value
kind Text
"TypedAssign"
[ Text
"constraintObj" Text -> TCM Value -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= a -> TCM Value
f a
i
, Text
"value" Text -> TCM Value -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= b -> TCM Value
encPrettyTCM b
v
, Text
"type" Text -> TCM Value -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= b -> TCM Value
encPrettyTCM b
t
]
PostponedCheckArgs a
i [b]
es b
t0 b
t1 -> Text -> [TCM Pair] -> TCM Value
kind Text
"PostponedCheckArgs"
[ Text
"constraintObj" Text -> TCM Value -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= a -> TCM Value
f a
i
, Text
"ofType" Text -> TCM Value -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= b -> TCM Value
encPrettyTCM b
t0
, Text
"arguments" Text -> TCM [Value] -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= [b] -> (b -> TCM Value) -> TCM [Value]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [b]
es b -> TCM Value
encPrettyTCM
, Text
"type" Text -> TCM Value -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= b -> TCM Value
encPrettyTCM b
t1
]
IsEmptyType b
a -> Text -> [TCM Pair] -> TCM Value
kind Text
"IsEmptyType"
[ Text
"type" Text -> TCM Value -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= b -> TCM Value
encPrettyTCM b
a
]
SizeLtSat b
a -> Text -> [TCM Pair] -> TCM Value
kind Text
"SizeLtSat"
[ Text
"type" Text -> TCM Value -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= b -> TCM Value
encPrettyTCM b
a
]
FindInstanceOF a
i b
t [(b, b, b)]
cs -> Text -> [TCM Pair] -> TCM Value
kind Text
"FindInstanceOF"
[ Text
"constraintObj" Text -> TCM Value -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= a -> TCM Value
f a
i
, Text
"candidates" Text -> TCM [Value] -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= [(b, b, b)] -> ((b, b, b) -> TCM Value) -> TCM [Value]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(b, b, b)]
cs (b, b, b) -> TCM Value
encodeKVPairs
, Text
"type" Text -> TCM Value -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= b -> TCM Value
encPrettyTCM b
t
]
where encodeKVPairs :: (b, b, b) -> TCM Value
encodeKVPairs (b
_, b
v, b
t) = [TCM Pair] -> TCM Value
obj
[ Text
"value" Text -> TCM Value -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= b -> TCM Value
encPrettyTCM b
v
, Text
"type" Text -> TCM Value -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= b -> TCM Value
encPrettyTCM b
t
]
ResolveInstanceOF QName
q -> Text -> [TCM Pair] -> TCM Value
kind Text
"ResolveInstanceOF"
[ Text
"name" Text -> Value -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= QName -> Value
forall a. Pretty a => a -> Value
encodePretty QName
q
]
PTSInstance a
a a
b -> Text -> [TCM Pair] -> TCM Value
kind Text
"PTSInstance"
[ Text
"constraintObjs" Text -> TCM [Value] -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= (a -> TCM Value) -> [a] -> TCM [Value]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse a -> TCM Value
f [a
a, a
b]
]
PostponedCheckFunDef QName
name b
a TCErr
err -> Text -> [TCM Pair] -> TCM Value
kind Text
"PostponedCheckFunDef"
[ Text
"name" Text -> Value -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= QName -> Value
forall a. Pretty a => a -> Value
encodePretty QName
name
, Text
"type" Text -> TCM Value -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= b -> TCM Value
encPrettyTCM b
a
, Text
"error" Text -> TCM Value -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= TCErr -> TCM Value
forall a. EncodeTCM a => a -> TCM Value
encodeTCM TCErr
err
]
DataSort QName
q a
s -> Text -> [TCM Pair] -> TCM Value
kind Text
"DataSort"
[ Text
"name" Text -> Value -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= QName -> Value
forall a. Pretty a => a -> Value
encodePretty QName
q
, Text
"sort" Text -> TCM Value -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= a -> TCM Value
f a
s
]
CheckLock a
t a
lk -> Text -> [TCM Pair] -> TCM Value
kind Text
"CheckLock"
[ Text
"head" Text -> TCM Value -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= a -> TCM Value
f a
t
, Text
"lock" Text -> TCM Value -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= a -> TCM Value
f a
lk
]
UsableAtMod Modality
mod a
t -> Text -> [TCM Pair] -> TCM Value
kind Text
"UsableAtMod"
[ Text
"mod" Text -> Value -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= Modality -> Value
forall a. Pretty a => a -> Value
encodePretty Modality
mod
, Text
"term" Text -> TCM Value -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= a -> TCM Value
f a
t
]
encodeNamedPretty :: PrettyTCM a => (Name, a) -> TCM Value
encodeNamedPretty :: forall a. PrettyTCM a => (Name, a) -> TCM Value
encodeNamedPretty (Name
name, a
a) = [TCM Pair] -> TCM Value
obj
[ Text
"name" Text -> Value -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= Name -> Value
forall a. Pretty a => a -> Value
encodePretty Name
name
, Text
"term" Text -> TCM Value -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= a -> TCM Value
forall a. PrettyTCM a => a -> TCM Value
encodePrettyTCM a
a
]
instance EncodeTCM (OutputForm C.Expr C.Expr) where
encodeTCM :: OutputForm_boot TCErr Expr Expr -> TCM Value
encodeTCM (OutputForm Range
range [ProblemId]
problems Blocker
unblock OutputConstraint_boot TCErr Expr Expr
oc) = [TCM Pair] -> TCM Value
obj
[ Text
"range" Text -> Range -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= Range
range
, Text
"problems" Text -> [ProblemId] -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= [ProblemId]
problems
, Text
"unblocker" Text -> Blocker -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= Blocker
unblock
, Text
"constraint" Text -> TCM Value -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= (Expr -> TCM Value)
-> (Expr -> TCM Value)
-> OutputConstraint_boot TCErr Expr Expr
-> TCM Value
forall a b.
(a -> TCM Value)
-> (b -> TCM Value) -> OutputConstraint b a -> TCM Value
encodeOC (Value -> TCM Value
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value -> TCM Value) -> (Expr -> Value) -> Expr -> TCM Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Value
forall a. Pretty a => a -> Value
encodePretty) (Value -> TCM Value
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value -> TCM Value) -> (Expr -> Value) -> Expr -> TCM Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Value
forall a. Pretty a => a -> Value
encodePretty) OutputConstraint_boot TCErr Expr Expr
oc
]
instance EncodeTCM Blocker where
encodeTCM :: Blocker -> TCM Value
encodeTCM (UnblockOnMeta MetaId
x) = Text -> [TCM Pair] -> TCM Value
kind Text
"UnblockOnMeta" [ Text
"meta" Text -> MetaId -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= MetaId
x ]
encodeTCM (UnblockOnProblem ProblemId
p) = Text -> [TCM Pair] -> TCM Value
kind Text
"UnblockOnProblem" [ Text
"id" Text -> ProblemId -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= ProblemId
p ]
encodeTCM (UnblockOnDef QName
q) = Text -> [TCM Pair] -> TCM Value
kind Text
"UnblockOnDef" [ Text
"name" Text -> Value -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= QName -> Value
forall a. Pretty a => a -> Value
encodePretty QName
q ]
encodeTCM (UnblockOnAll Set Blocker
us) = Text -> [TCM Pair] -> TCM Value
kind Text
"UnblockOnAll" [ Text
"blockers" Text -> [Blocker] -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= Set Blocker -> [Blocker]
forall a. Set a -> [a]
Set.toList Set Blocker
us ]
encodeTCM (UnblockOnAny Set Blocker
us) = Text -> [TCM Pair] -> TCM Value
kind Text
"UnblockOnAny" [ Text
"blockers" Text -> [Blocker] -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= Set Blocker -> [Blocker]
forall a. Set a -> [a]
Set.toList Set Blocker
us ]
instance EncodeTCM DisplayInfo where
encodeTCM :: DisplayInfo -> TCM Value
encodeTCM (Info_CompilationOk CompilerBackend
backend WarningsAndNonFatalErrors
wes) = Text -> [TCM Pair] -> TCM Value
kind Text
"CompilationOk"
[ Text
"backend" Text -> Value -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= CompilerBackend -> Value
forall a. Pretty a => a -> Value
encodePretty CompilerBackend
backend
, Text
"warnings" Text -> TCM Value -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= [TCWarning] -> TCM Value
forall a. EncodeTCM a => a -> TCM Value
encodeTCM ([TCWarning] -> [TCWarning]
filterTCWarnings (WarningsAndNonFatalErrors -> [TCWarning]
tcWarnings WarningsAndNonFatalErrors
wes))
, Text
"errors" Text -> TCM Value -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= [TCWarning] -> TCM Value
forall a. EncodeTCM a => a -> TCM Value
encodeTCM ([TCWarning] -> [TCWarning]
filterTCWarnings (WarningsAndNonFatalErrors -> [TCWarning]
nonFatalErrors WarningsAndNonFatalErrors
wes))
]
encodeTCM (Info_Constraints [OutputForm_boot TCErr 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_boot TCErr Expr Expr]
-> (OutputForm_boot TCErr 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_boot TCErr Expr Expr]
constraints OutputForm_boot TCErr Expr Expr -> TCM Value
forall a. EncodeTCM a => a -> TCM Value
encodeTCM
]
encodeTCM (Info_AllGoalsWarnings ([OutputConstraint_boot TCErr Expr InteractionId]
vis, [OutputConstraint_boot TCErr 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_boot TCErr Expr InteractionId]
-> (OutputConstraint_boot TCErr 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_boot TCErr Expr InteractionId]
vis (\OutputConstraint_boot TCErr Expr InteractionId
i -> InteractionId -> TCM Value -> TCM Value
forall (m :: * -> *) a.
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
MonadTCEnv m, MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId (OutputForm Expr InteractionId -> InteractionId
forall a b. OutputForm a b -> b
B.outputFormId (OutputForm Expr InteractionId -> InteractionId)
-> OutputForm Expr InteractionId -> InteractionId
forall a b. (a -> b) -> a -> b
$ Range
-> [ProblemId]
-> Blocker
-> OutputConstraint_boot TCErr Expr InteractionId
-> OutputForm Expr InteractionId
forall tcErr a b.
Range
-> [ProblemId]
-> Blocker
-> OutputConstraint_boot tcErr a b
-> OutputForm_boot tcErr a b
OutputForm Range
forall a. Range' a
noRange [] Blocker
alwaysUnblock OutputConstraint_boot TCErr Expr InteractionId
i) (TCM Value -> TCM Value) -> TCM Value -> TCM Value
forall a b. (a -> b) -> a -> b
$ (InteractionId -> TCM Value)
-> (Expr -> TCM Value)
-> OutputConstraint_boot TCErr Expr InteractionId
-> TCM Value
forall a b.
(a -> TCM Value)
-> (b -> TCM Value) -> OutputConstraint b a -> TCM Value
encodeOC InteractionId -> TCM Value
forall a. EncodeTCM a => a -> TCM Value
encodeTCM Expr -> TCM Value
forall a. PrettyTCM a => a -> TCM Value
encodePrettyTCM OutputConstraint_boot TCErr Expr InteractionId
i)
, Text
"invisibleGoals" Text -> TCM [Value] -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= [OutputConstraint_boot TCErr Expr NamedMeta]
-> (OutputConstraint_boot TCErr 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_boot TCErr Expr NamedMeta]
invis ((NamedMeta -> TCM Value)
-> (Expr -> TCM Value)
-> OutputConstraint_boot TCErr Expr NamedMeta
-> TCM Value
forall a b.
(a -> TCM Value)
-> (b -> TCM Value) -> OutputConstraint b a -> TCM Value
encodeOC NamedMeta -> TCM Value
forall a. EncodeTCM a => a -> TCM Value
encodeTCM Expr -> TCM Value
forall a. PrettyTCM a => a -> TCM Value
encodePrettyTCM)
, Text
"warnings" Text -> TCM Value -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= [TCWarning] -> TCM Value
forall a. EncodeTCM a => a -> TCM Value
encodeTCM ([TCWarning] -> [TCWarning]
filterTCWarnings (WarningsAndNonFatalErrors -> [TCWarning]
tcWarnings WarningsAndNonFatalErrors
wes))
, Text
"errors" Text -> TCM Value -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= [TCWarning] -> TCM Value
forall a. EncodeTCM a => a -> TCM Value
encodeTCM ([TCWarning] -> [TCWarning]
filterTCWarnings (WarningsAndNonFatalErrors -> [TCWarning]
nonFatalErrors WarningsAndNonFatalErrors
wes))
]
encodeTCM (Info_Time CPUTime
time) = Text -> [TCM Pair] -> TCM Value
kind Text
"Time"
[ Text
"time" Text -> CPUTime -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= CPUTime
time
]
encodeTCM (Info_Error Info_Error_boot TCErr TCWarning
err) = Info_Error_boot TCErr TCWarning -> TCM Value
forall a. EncodeTCM a => a -> TCM Value
encodeTCM Info_Error_boot TCErr TCWarning
err
encodeTCM DisplayInfo
Info_Intro_NotFound = Text -> [TCM Pair] -> TCM Value
kind Text
"IntroNotFound" []
encodeTCM (Info_Intro_ConstructorUnknown [String]
introductions) = Text -> [TCM Pair] -> TCM Value
kind Text
"IntroConstructorUnknown"
[ Text
"constructors" Text -> [Value] -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= (String -> Value) -> [String] -> [Value]
forall a b. (a -> b) -> [a] -> [b]
map String -> Value
forall a. ToJSON a => a -> Value
toJSON [String]
introductions
]
encodeTCM (Info_Auto String
info) = Text -> [TCM Pair] -> TCM Value
kind Text
"Auto"
[ Text
"info" Text -> Value -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= String -> Value
forall a. ToJSON a => a -> Value
toJSON String
info
]
encodeTCM (Info_ModuleContents [Name]
names Telescope
tele [(Name, Type)]
contents) = Text -> [TCM Pair] -> TCM Value
kind Text
"ModuleContents"
[ Text
"contents" Text -> TCM [Value] -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= [(Name, Type)] -> ((Name, Type) -> TCM Value) -> TCM [Value]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Name, Type)]
contents (Name, Type) -> TCM Value
forall a. PrettyTCM a => (Name, a) -> TCM Value
encodeNamedPretty
, Text
"telescope" Text -> TCM [Value] -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= [Dom (String, Type)]
-> (Dom (String, Type) -> TCM Value) -> TCM [Value]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (Telescope -> [Dom (String, Type)]
forall t. Tele (Dom t) -> [Dom (String, t)]
telToList Telescope
tele) Dom (String, Type) -> TCM Value
forall a. PrettyTCM a => Dom (String, a) -> TCM Value
encodeDomType
, Text
"names" Text -> [Value] -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= (Name -> Value) -> [Name] -> [Value]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Value
forall a. Pretty a => a -> Value
encodePretty [Name]
names
]
where
encodeDomType :: PrettyTCM a => Dom (ArgName, a) -> TCM Value
encodeDomType :: forall a. PrettyTCM a => Dom (String, a) -> TCM Value
encodeDomType Dom (String, a)
dom = [TCM Pair] -> TCM Value
obj
[ Text
"dom" Text -> TCM Value -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= (String, a) -> TCM Value
forall a. PrettyTCM a => a -> TCM Value
encodePrettyTCM (Dom (String, a) -> (String, a)
forall t e. Dom' t e -> e
unDom Dom (String, a)
dom)
, Text
"name" Text -> Maybe Value -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= (String -> Value) -> Maybe String -> Maybe Value
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap String -> Value
forall a. Pretty a => a -> Value
encodePretty (Dom (String, a) -> Maybe String
forall a. (LensNamed a, NameOf a ~ NamedName) => a -> Maybe String
bareNameOf Dom (String, a)
dom)
, Text
"finite" Text -> Value -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= Bool -> Value
forall a. ToJSON a => a -> Value
toJSON (Dom (String, a) -> Bool
forall t e. Dom' t e -> Bool
domIsFinite Dom (String, a)
dom)
, Text
"cohesion" Text -> Value -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= Cohesion -> Value
forall a. Show a => a -> Value
encodeShow (Modality -> Cohesion
modCohesion (Modality -> Cohesion)
-> (ArgInfo -> Modality) -> ArgInfo -> Cohesion
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ArgInfo -> Modality
argInfoModality (ArgInfo -> Cohesion) -> ArgInfo -> Cohesion
forall a b. (a -> b) -> a -> b
$ Dom (String, a) -> ArgInfo
forall t e. Dom' t e -> ArgInfo
domInfo Dom (String, a)
dom)
, Text
"relevance" Text -> Value -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= Relevance -> Value
forall a. Show a => a -> Value
encodeShow (Modality -> Relevance
modRelevance (Modality -> Relevance)
-> (ArgInfo -> Modality) -> ArgInfo -> Relevance
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ArgInfo -> Modality
argInfoModality (ArgInfo -> Relevance) -> ArgInfo -> Relevance
forall a b. (a -> b) -> a -> b
$ Dom (String, a) -> ArgInfo
forall t e. Dom' t e -> ArgInfo
domInfo Dom (String, a)
dom)
, Text
"hiding" Text -> String -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= case ArgInfo -> Hiding
argInfoHiding (ArgInfo -> Hiding) -> ArgInfo -> Hiding
forall a b. (a -> b) -> a -> b
$ Dom (String, a) -> ArgInfo
forall t e. Dom' t e -> ArgInfo
domInfo Dom (String, a)
dom of
Instance Overlappable
o -> Overlappable -> String
forall a. Show a => a -> String
show Overlappable
o
Hiding
o -> Hiding -> String
forall a. Show a => a -> String
show Hiding
o
]
encodeTCM (Info_SearchAbout [(Name, Type)]
results String
search) = Text -> [TCM Pair] -> TCM Value
kind Text
"SearchAbout"
[ Text
"results" Text -> TCM [Value] -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= [(Name, Type)] -> ((Name, Type) -> TCM Value) -> TCM [Value]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Name, Type)]
results (Name, Type) -> TCM Value
forall a. PrettyTCM a => (Name, a) -> TCM Value
encodeNamedPretty
, Text
"search" Text -> Value -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= String -> Value
forall a. ToJSON a => a -> Value
toJSON String
search
]
encodeTCM (Info_WhyInScope why :: WhyInScopeData
why@(WhyInScopeData QName
y String
path Maybe LocalVar
_ [AbstractName]
_ [AbstractModule]
_)) = Text -> [TCM Pair] -> TCM Value
kind Text
"WhyInScope"
[ Text
"thing" Text -> String -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= QName -> String
forall a. Pretty a => a -> String
prettyShow QName
y
, Text
"filepath" Text -> Value -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= String -> Value
forall a. ToJSON a => a -> Value
toJSON String
path
, Text
"message" Text -> TCMT IO Doc -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= WhyInScopeData -> TCMT IO Doc
forall (m :: * -> *). MonadPretty m => WhyInScopeData -> m Doc
explainWhyInScope WhyInScopeData
why
]
encodeTCM (Info_NormalForm CommandState
commandState ComputeMode
computeMode Maybe CPUTime
time Expr
expr) = Text -> [TCM Pair] -> TCM Value
kind Text
"NormalForm"
[ Text
"commandState" Text -> CommandState -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= CommandState
commandState
, Text
"computeMode" Text -> ComputeMode -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= ComputeMode
computeMode
, Text
"time" Text -> Maybe CPUTime -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= Maybe CPUTime
time
, Text
"expr" Text -> TCM Value -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= Expr -> TCM Value
forall a. PrettyTCM a => a -> TCM Value
encodePrettyTCM Expr
expr
]
encodeTCM (Info_InferredType CommandState
commandState Maybe CPUTime
time Expr
expr) = Text -> [TCM Pair] -> TCM Value
kind Text
"InferredType"
[ Text
"commandState" Text -> CommandState -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= CommandState
commandState
, Text
"time" Text -> Maybe CPUTime -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= Maybe CPUTime
time
, Text
"expr" Text -> TCM Value -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= Expr -> TCM Value
forall a. PrettyTCM a => a -> TCM Value
encodePrettyTCM Expr
expr
]
encodeTCM (Info_Context InteractionId
ii [ResponseContextEntry]
ctx) = Text -> [TCM Pair] -> TCM Value
kind Text
"Context"
[ Text
"interactionPoint" Text -> InteractionId -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= InteractionId
ii
, Text
"context" Text -> [ResponseContextEntry] -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= [ResponseContextEntry]
ctx
]
encodeTCM DisplayInfo
Info_Version = Text -> [TCM Pair] -> TCM Value
kind Text
"Version"
[ Text
"version" Text -> String -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= (String
versionWithCommitInfo :: String)
]
encodeTCM (Info_GoalSpecific InteractionId
ii GoalDisplayInfo_boot TCErr
info) = Text -> [TCM Pair] -> TCM Value
kind Text
"GoalSpecific"
[ Text
"interactionPoint" Text -> InteractionId -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= InteractionId
ii
, Text
"goalInfo" Text -> TCM Value -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= InteractionId -> TCM Value -> TCM Value
forall (m :: * -> *) a.
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
MonadTCEnv m, MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
ii (InteractionId -> GoalDisplayInfo_boot TCErr -> TCM Value
encodeGoalSpecific InteractionId
ii GoalDisplayInfo_boot TCErr
info)
]
instance EncodeTCM GoalTypeAux where
encodeTCM :: GoalTypeAux -> TCM Value
encodeTCM GoalTypeAux
GoalOnly = Text -> [TCM Pair] -> TCM Value
kind Text
"GoalOnly" []
encodeTCM (GoalAndHave Expr
expr [IPFace' Expr]
_) = Text -> [TCM Pair] -> TCM Value
kind Text
"GoalAndHave"
[ Text
"expr" Text -> TCM Value -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= Expr -> TCM Value
forall a. PrettyTCM a => a -> TCM Value
encodePrettyTCM Expr
expr ]
encodeTCM (GoalAndElaboration Term
term) = Text -> [TCM Pair] -> TCM Value
kind Text
"GoalAndElaboration"
[ Text
"term" Text -> TCM Value -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= Term -> TCM Value
forall a. PrettyTCM a => a -> TCM Value
encodePrettyTCM Term
term ]
encodeGoalSpecific :: InteractionId -> GoalDisplayInfo -> TCM Value
encodeGoalSpecific :: InteractionId -> GoalDisplayInfo_boot TCErr -> TCM Value
encodeGoalSpecific InteractionId
ii = GoalDisplayInfo_boot TCErr -> TCM Value
go
where
go :: GoalDisplayInfo_boot TCErr -> TCM Value
go (Goal_HelperFunction OutputConstraint' Expr Expr
helperType) = Text -> [TCM Pair] -> TCM Value
kind Text
"HelperFunction"
[ Text
"signature" Text -> TCMT IO Doc -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= TCMT IO Doc -> TCMT IO Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (OutputConstraint' Expr Expr -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyATop OutputConstraint' Expr Expr
helperType)
]
go (Goal_NormalForm ComputeMode
computeMode Expr
expr) = Text -> [TCM Pair] -> TCM Value
kind Text
"NormalForm"
[ Text
"computeMode" Text -> ComputeMode -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= ComputeMode
computeMode
, Text
"expr" Text -> TCMT IO Doc -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= ComputeMode -> Expr -> TCMT IO Doc
B.showComputed ComputeMode
computeMode Expr
expr
]
go (Goal_GoalType Rewrite
rewrite GoalTypeAux
goalType [ResponseContextEntry]
entries [IPFace' Expr]
boundary [OutputForm_boot TCErr Expr Expr]
outputForms) = Text -> [TCM Pair] -> TCM Value
kind Text
"GoalType"
[ Text
"rewrite" Text -> Rewrite -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= Rewrite
rewrite
, Text
"typeAux" Text -> GoalTypeAux -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= GoalTypeAux
goalType
, Text
"type" Text -> TCMT IO Doc -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= Rewrite -> InteractionId -> TCMT IO Doc
prettyTypeOfMeta Rewrite
rewrite InteractionId
ii
, Text
"entries" Text -> [ResponseContextEntry] -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= [ResponseContextEntry]
entries
, Text
"boundary" Text -> [Value] -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= (IPFace' Expr -> Value) -> [IPFace' Expr] -> [Value]
forall a b. (a -> b) -> [a] -> [b]
map IPFace' Expr -> Value
forall a. Pretty a => a -> Value
encodePretty [IPFace' Expr]
boundary
, Text
"outputForms" Text -> [Value] -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= (OutputForm_boot TCErr Expr Expr -> Value)
-> [OutputForm_boot TCErr Expr Expr] -> [Value]
forall a b. (a -> b) -> [a] -> [b]
map OutputForm_boot TCErr Expr Expr -> Value
forall a. Pretty a => a -> Value
encodePretty [OutputForm_boot TCErr Expr Expr]
outputForms
]
go (Goal_CurrentGoal Rewrite
rewrite) = Text -> [TCM Pair] -> TCM Value
kind Text
"CurrentGoal"
[ Text
"rewrite" Text -> Rewrite -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= Rewrite
rewrite
, Text
"type" Text -> TCMT IO Doc -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= Rewrite -> InteractionId -> TCMT IO Doc
prettyTypeOfMeta Rewrite
rewrite InteractionId
ii
]
go (Goal_InferredType Expr
expr) = Text -> [TCM Pair] -> TCM Value
kind Text
"InferredType"
[ Text
"expr" Text -> TCMT IO Doc -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= Expr -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyATop Expr
expr
]
instance EncodeTCM Info_Error where
encodeTCM :: Info_Error_boot TCErr TCWarning -> TCM Value
encodeTCM (Info_GenericError TCErr
err) = Text -> [TCM Pair] -> TCM Value
kind Text
"Error"
[ Text
"warnings" Text -> TCM Value -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= (TCErr -> TCM [TCWarning]
getAllWarningsOfTCErr TCErr
err
TCM [TCWarning] -> ([TCWarning] -> TCM Value) -> TCM Value
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [TCWarning] -> TCM Value
forall a. EncodeTCM a => a -> TCM Value
encodeTCM ([TCWarning] -> TCM Value)
-> ([TCWarning] -> [TCWarning]) -> [TCWarning] -> TCM Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [TCWarning] -> [TCWarning]
filterTCWarnings)
, Text
"error" Text -> TCM Value -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= TCErr -> TCM Value
forall a. EncodeTCM a => a -> TCM Value
encodeTCM TCErr
err
]
encodeTCM Info_Error_boot TCErr TCWarning
err = Text -> [TCM Pair] -> TCM Value
kind Text
"Error"
[ Text
"warnings" Text -> [String] -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= ([] :: [String])
, Text
"error" Text -> TCM Value -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= [TCM Pair] -> TCM Value
obj
[ Text
"message" Text -> TCM String -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= Info_Error_boot TCErr TCWarning -> TCM String
showInfoError Info_Error_boot TCErr TCWarning
err
]
]
instance EncodeTCM TCErr where
encodeTCM :: TCErr -> TCM Value
encodeTCM TCErr
err = [TCM Pair] -> TCM Value
obj
[ Text
"message" Text -> TCM Value -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= TCErr -> TCM Value
forall a. PrettyTCM a => a -> TCM Value
encodePrettyTCM TCErr
err
]
instance EncodeTCM TCWarning where
encodeTCM :: TCWarning -> TCM Value
encodeTCM TCWarning
w = [TCM Pair] -> TCM Value
obj
[ Text
"message" Text -> TCM String -> TCM Pair
forall a. ToJSON a => Text -> TCM a -> TCM Pair
#= (Doc -> String
forall a. Doc a -> String
P.render (Doc -> String) -> TCMT IO Doc -> TCM String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCWarning -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => TCWarning -> m Doc
prettyTCM TCWarning
w)
]
instance EncodeTCM Response where
encodeTCM :: Response -> TCM Value
encodeTCM (Resp_HighlightingInfo HighlightingInfo
info RemoveTokenBasedHighlighting
remove HighlightingMethod
method ModuleToSource
modFile) =
IO Value -> TCM Value
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Value -> TCM Value) -> IO Value -> TCM Value
forall a b. (a -> b) -> a -> b
$ HighlightingInfo
-> RemoveTokenBasedHighlighting
-> HighlightingMethod
-> ModuleToSource
-> IO Value
jsonifyHighlightingInfo HighlightingInfo
info RemoveTokenBasedHighlighting
remove HighlightingMethod
method ModuleToSource
modFile
encodeTCM (Resp_DisplayInfo DisplayInfo
info) = Text -> [TCM Pair] -> TCM Value
kind Text
"DisplayInfo"
[ Text
"info" Text -> DisplayInfo -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= DisplayInfo
info
]
encodeTCM (Resp_ClearHighlighting TokenBased
tokenBased) = Text -> [TCM Pair] -> TCM Value
kind Text
"ClearHighlighting"
[ Text
"tokenBased" Text -> TokenBased -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= TokenBased
tokenBased
]
encodeTCM Response
Resp_DoneAborting = Text -> [TCM Pair] -> TCM Value
kind Text
"DoneAborting" []
encodeTCM Response
Resp_DoneExiting = Text -> [TCM Pair] -> TCM Value
kind Text
"DoneExiting" []
encodeTCM Response
Resp_ClearRunningInfo = Text -> [TCM Pair] -> TCM Value
kind Text
"ClearRunningInfo" []
encodeTCM (Resp_RunningInfo Nat
debugLevel String
msg) = Text -> [TCM Pair] -> TCM Value
kind Text
"RunningInfo"
[ Text
"debugLevel" Text -> Nat -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= Nat
debugLevel
, Text
"message" Text -> String -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= String
msg
]
encodeTCM (Resp_Status Status
status) = Text -> [TCM Pair] -> TCM Value
kind Text
"Status"
[ Text
"status" Text -> Status -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= Status
status
]
encodeTCM (Resp_JumpToError String
filepath Int32
position) = Text -> [TCM Pair] -> TCM Value
kind Text
"JumpToError"
[ Text
"filepath" Text -> String -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= String
filepath
, Text
"position" Text -> Int32 -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= Int32
position
]
encodeTCM (Resp_InteractionPoints [InteractionId]
interactionPoints) = Text -> [TCM Pair] -> TCM Value
kind Text
"InteractionPoints"
[ Text
"interactionPoints" Text -> [InteractionId] -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= [InteractionId]
interactionPoints
]
encodeTCM (Resp_GiveAction InteractionId
i GiveResult
giveResult) = Text -> [TCM Pair] -> TCM Value
kind Text
"GiveAction"
[ Text
"interactionPoint" Text -> InteractionId -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= InteractionId
i
, Text
"giveResult" Text -> GiveResult -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= GiveResult
giveResult
]
encodeTCM (Resp_MakeCase InteractionId
id MakeCaseVariant
variant [String]
clauses) = Text -> [TCM Pair] -> TCM Value
kind Text
"MakeCase"
[ Text
"interactionPoint" Text -> InteractionId -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= InteractionId
id
, Text
"variant" Text -> MakeCaseVariant -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= MakeCaseVariant
variant
, Text
"clauses" Text -> [String] -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= [String]
clauses
]
encodeTCM (Resp_SolveAll [(InteractionId, Expr)]
solutions) = Text -> [TCM Pair] -> TCM Value
kind Text
"SolveAll"
[ Text
"solutions" Text -> [Value] -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= ((InteractionId, Expr) -> Value)
-> [(InteractionId, Expr)] -> [Value]
forall a b. (a -> b) -> [a] -> [b]
map (InteractionId, Expr) -> Value
forall {a} {a}. (ToJSON a, Pretty a) => (a, a) -> Value
encodeSolution [(InteractionId, Expr)]
solutions
]
where
encodeSolution :: (a, a) -> Value
encodeSolution (a
i, a
expr) = [Pair] -> Value
object
[ Text
"interactionPoint" Text -> a -> Pair
forall a. ToJSON a => Text -> a -> Pair
.= a
i
, Text
"expression" Text -> String -> Pair
forall a. ToJSON a => Text -> a -> Pair
.= a -> String
forall a. Pretty a => a -> String
P.prettyShow a
expr
]
encodeTCM (Resp_Mimer InteractionId
ii Maybe String
str) = Text -> [TCM Pair] -> TCM Value
kind Text
"Mimer"
[ Text
"solution" Text -> Maybe String -> TCM Pair
forall a. EncodeTCM a => Text -> a -> TCM Pair
@= Maybe String
str
]
jsonifyResponse :: Response -> TCM ByteString
jsonifyResponse :: Response -> TCMT IO ByteString
jsonifyResponse = ByteString -> TCMT IO ByteString
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ByteString -> TCMT IO ByteString)
-> (Value -> ByteString) -> Value -> TCMT IO ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value -> ByteString
forall a. ToJSON a => a -> ByteString
encode (Value -> TCMT IO ByteString)
-> (Response -> TCM Value) -> Response -> TCMT IO ByteString
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Response -> TCM Value
forall a. EncodeTCM a => a -> TCM Value
encodeTCM