Safe Haskell	None
Language	Haskell2010

Agda.Interaction.JSON

Contents

Orphan instances

Description

Encoding stuff into JSON values in TCM

Synopsis

class EncodeTCM a where
- encodeTCM :: a -> TCM Value
obj :: [TCM Pair] -> TCM Value
kind :: Text -> [TCM Pair] -> TCM Value
kind' :: Text -> [Pair] -> Value
(@=) :: EncodeTCM a => Text -> a -> TCM Pair
(#=) :: ToJSON a => Text -> TCM a -> TCM Pair
(>=>) :: Monad m => (a -> m b) -> (b -> m c) -> a -> m c
(<=<) :: Monad m => (b -> m c) -> (a -> m b) -> a -> m c

Documentation

class EncodeTCM a where Source #

The JSON version ofPrettyTCM, for encoding JSON value in TCM

Minimal complete definition

Nothing

Methods

encodeTCM :: a -> TCM Value Source #

default encodeTCM :: ToJSON a => a -> TCM Value Source #

Instances

Instances details

EncodeTCM Bool Source #
Instance details Defined in Agda.Interaction.JSON Methods encodeTCM :: Bool -> TCM Value Source #
EncodeTCM Int Source #
Instance details Defined in Agda.Interaction.JSON Methods encodeTCM :: Int -> TCM Value Source #
EncodeTCM Int32 Source #
Instance details Defined in Agda.Interaction.JSON Methods encodeTCM :: Int32 -> TCM Value Source #
EncodeTCM String Source #
Instance details Defined in Agda.Interaction.JSON Methods encodeTCM :: String -> TCM Value Source #
EncodeTCM Doc Source #
Instance details Defined in Agda.Interaction.JSON Methods encodeTCM :: Doc -> TCM Value Source #
EncodeTCM CPUTime Source #
Instance details Defined in Agda.Interaction.JSONTop Methods encodeTCM :: CPUTime -> TCM Value Source #
EncodeTCM Range Source #
Instance details Defined in Agda.Interaction.JSONTop Methods encodeTCM :: Range -> TCM Value Source #
EncodeTCM InteractionId Source #
Instance details Defined in Agda.Interaction.JSONTop Methods encodeTCM :: InteractionId -> TCM Value Source #
EncodeTCM NameInScope Source #
Instance details Defined in Agda.Interaction.JSONTop Methods encodeTCM :: NameInScope -> TCM Value Source #
EncodeTCM ProblemId Source #
Instance details Defined in Agda.Interaction.JSONTop Methods encodeTCM :: ProblemId -> TCM Value Source #
EncodeTCM TokenBased Source #
Instance details Defined in Agda.Interaction.Highlighting.JSON Methods encodeTCM :: TokenBased -> TCM Value Source #
EncodeTCM Status Source #
Instance details Defined in Agda.Interaction.JSONTop Methods encodeTCM :: Status -> TCM Value Source #
EncodeTCM GiveResult Source #
Instance details Defined in Agda.Interaction.JSONTop Methods encodeTCM :: GiveResult -> TCM Value Source #
EncodeTCM DisplayInfo Source #
Instance details Defined in Agda.Interaction.JSONTop Methods encodeTCM :: DisplayInfo -> TCM Value Source #
EncodeTCM MakeCaseVariant Source #
Instance details Defined in Agda.Interaction.JSONTop Methods encodeTCM :: MakeCaseVariant -> TCM Value Source #
EncodeTCM Response Source #
Instance details Defined in Agda.Interaction.JSONTop Methods encodeTCM :: Response -> TCM Value Source #
EncodeTCM ComputeMode Source #
Instance details Defined in Agda.Interaction.JSONTop Methods encodeTCM :: ComputeMode -> TCM Value Source #
EncodeTCM Rewrite Source #
Instance details Defined in Agda.Interaction.JSONTop Methods encodeTCM :: Rewrite -> TCM Value Source #
EncodeTCM CommandState Source #
Instance details Defined in Agda.Interaction.JSONTop Methods encodeTCM :: CommandState -> TCM Value Source #
EncodeTCM ResponseContextEntry Source #
Instance details Defined in Agda.Interaction.JSONTop Methods encodeTCM :: ResponseContextEntry -> TCM Value Source #
EncodeTCM GoalTypeAux Source #
Instance details Defined in Agda.Interaction.JSONTop Methods encodeTCM :: GoalTypeAux -> TCM Value Source #
EncodeTCM Value Source #
Instance details Defined in Agda.Interaction.JSON Methods encodeTCM :: Value -> TCM Value Source #
EncodeTCM a => EncodeTCM [a] Source #
Instance details Defined in Agda.Interaction.JSON Methods encodeTCM :: [a] -> TCM Value Source #
EncodeTCM a => EncodeTCM (Maybe a) Source #
Instance details Defined in Agda.Interaction.JSON Methods encodeTCM :: Maybe a -> TCM Value Source #
EncodeTCM (Position' ()) Source #
Instance details Defined in Agda.Interaction.JSONTop Methods encodeTCM :: Position' () -> TCM Value Source #
EncodeTCM (OutputForm Expr Expr) Source #
Instance details Defined in Agda.Interaction.JSONTop Methods encodeTCM :: OutputForm Expr Expr -> TCM Value Source #

obj :: [TCM Pair] -> TCM Value Source #

TCM monadic version of object

kind :: Text -> [TCM Pair] -> TCM Value Source #

A handy alternative of obj with kind specified

kind' :: Text -> [Pair] -> Value Source #

A handy alternative of object with kind specified

(@=) :: EncodeTCM a => Text -> a -> TCM Pair Source #

Abbreviation of `_ #= encodeTCM _`

(#=) :: ToJSON a => Text -> TCM a -> TCM Pair Source #

Pairs a key with a value wrapped in TCM

(>=>) :: Monad m => (a -> m b) -> (b -> m c) -> a -> m c infixr 1 #

Left-to-right composition of Kleisli arrows.

'(bs >=> cs) a' can be understood as the do expression

do b <- bs a
   cs b

(<=<) :: Monad m => (b -> m c) -> (a -> m b) -> a -> m c infixr 1 #

Right-to-left composition of Kleisli arrows. (>=>), with the arguments flipped.

Note how this operator resembles function composition (.):

(.)   ::            (b ->   c) -> (a ->   b) -> a ->   c
(<=<) :: Monad m => (b -> m c) -> (a -> m b) -> a -> m c

Orphan instances

ToJSON Doc Source #
Instance details Methods toJSON :: Doc -> Value toEncoding :: Doc -> Encoding toJSONList :: [Doc] -> Value toEncodingList :: [Doc] -> Encoding
ToJSON AbsolutePath Source #
Instance details Methods toJSON :: AbsolutePath -> Value toEncoding :: AbsolutePath -> Encoding toJSONList :: [AbsolutePath] -> Value toEncodingList :: [AbsolutePath] -> Encoding
ToJSON a => ToJSON (Maybe a) Source #
Instance details Methods toJSON :: Maybe a -> Value toEncoding :: Maybe a -> Encoding toJSONList :: [Maybe a] -> Value toEncodingList :: [Maybe a] -> Encoding