Agda-2.6.1.3: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.Interaction.JSON

Description

Encoding stuff into JSON values in TCM

Synopsis

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