Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.Interaction.JSONTop

Contents

- Orphan instances

Synopsis

- jsonREPL :: TCM () -> TCM ()

# Documentation

jsonREPL :: TCM () -> TCM () Source #

`jsonREPL` is a interpreter like `mimicGHCi`, but outputs JSON-encoded strings.

`jsonREPL` reads Haskell values (that starts from `IOTCM` ...) from stdin, interprets them, and outputs JSON-encoded strings. into stdout.

# Orphan instances

EncodeTCM CommandState Source # |
Instance details Methods encodeTCM :: CommandState -> TCM Value Source #
EncodeTCM ComputeMode Source # |
Instance details Methods encodeTCM :: ComputeMode -> TCM Value Source #
EncodeTCM CurrentFile Source # |
Instance details Methods encodeTCM :: CurrentFile -> TCM Value Source #
EncodeTCM Rewrite Source # |
Instance details Methods encodeTCM :: Rewrite -> TCM Value Source #
EncodeTCM DisplayInfo Source # |
Instance details Methods encodeTCM :: DisplayInfo -> TCM Value Source #
EncodeTCM Info_Error Source # |
Instance details Methods encodeTCM :: Info_Error -> TCM Value Source #
EncodeTCM Response Source # |
Instance details Methods encodeTCM :: Response -> TCM Value Source #
EncodeTCM GiveResult Source # |
Instance details Methods encodeTCM :: GiveResult -> TCM Value Source #
EncodeTCM GoalTypeAux Source # |
Instance details Methods encodeTCM :: GoalTypeAux -> TCM Value Source #
EncodeTCM MakeCaseVariant Source # |
Instance details Methods encodeTCM :: MakeCaseVariant -> TCM Value Source #
EncodeTCM ResponseContextEntry Source # |
Instance details Methods encodeTCM :: ResponseContextEntry -> TCM Value Source #
EncodeTCM Status Source # |
Instance details Methods encodeTCM :: Status -> TCM Value Source #
EncodeTCM InteractionId Source # |
Instance details Methods encodeTCM :: InteractionId -> TCM Value Source #
EncodeTCM MetaId Source # |
Instance details Methods encodeTCM :: MetaId -> TCM Value Source #
EncodeTCM ProblemId Source # |
Instance details Methods encodeTCM :: ProblemId -> TCM Value Source #
EncodeTCM NameInScope Source # |
Instance details Methods encodeTCM :: NameInScope -> TCM Value Source #
EncodeTCM Blocker Source # |
Instance details Methods encodeTCM :: Blocker -> TCM Value Source #
EncodeTCM Range Source # |
Instance details Methods encodeTCM :: Range -> TCM Value Source #
EncodeTCM TCErr Source # |
Instance details Methods encodeTCM :: TCErr -> TCM Value Source #
EncodeTCM TCWarning Source # |
Instance details Methods encodeTCM :: TCWarning -> TCM Value Source #
EncodeTCM NamedMeta Source # |
Instance details Methods encodeTCM :: NamedMeta -> TCM Value Source #
EncodeTCM CPUTime Source # |
Instance details Methods encodeTCM :: CPUTime -> TCM Value Source #
ToJSON CommandState Source # |
Instance details Methods toJSON :: CommandState -> Value Source # toEncoding :: CommandState -> Encoding Source # toJSONList :: [CommandState] -> Value Source # toEncodingList :: [CommandState] -> Encoding Source # omitField :: CommandState -> Bool Source #
ToJSON ComputeMode Source # |
Instance details Methods toJSON :: ComputeMode -> Value Source # toEncoding :: ComputeMode -> Encoding Source # toJSONList :: [ComputeMode] -> Value Source # toEncodingList :: [ComputeMode] -> Encoding Source # omitField :: ComputeMode -> Bool Source #
ToJSON CurrentFile Source # |
Instance details Methods toJSON :: CurrentFile -> Value Source # toEncoding :: CurrentFile -> Encoding Source # toJSONList :: [CurrentFile] -> Value Source # toEncodingList :: [CurrentFile] -> Encoding Source # omitField :: CurrentFile -> Bool Source #
ToJSON Rewrite Source # |
Instance details Methods toJSON :: Rewrite -> Value Source # toEncoding :: Rewrite -> Encoding Source # toJSONList :: [Rewrite] -> Value Source # toEncodingList :: [Rewrite] -> Encoding Source # omitField :: Rewrite -> Bool Source #
ToJSON GiveResult Source # |
Instance details Methods toJSON :: GiveResult -> Value Source # toEncoding :: GiveResult -> Encoding Source # toJSONList :: [GiveResult] -> Value Source # toEncodingList :: [GiveResult] -> Encoding Source # omitField :: GiveResult -> Bool Source #
ToJSON MakeCaseVariant Source # |
Instance details Methods toJSON :: MakeCaseVariant -> Value Source # toEncoding :: MakeCaseVariant -> Encoding Source # toJSONList :: [MakeCaseVariant] -> Value Source # toEncodingList :: [MakeCaseVariant] -> Encoding Source # omitField :: MakeCaseVariant -> Bool Source #
ToJSON Status Source # |
Instance details Methods toJSON :: Status -> Value Source # toEncoding :: Status -> Encoding Source # toJSONList :: [Status] -> Value Source # toEncodingList :: [Status] -> Encoding Source # omitField :: Status -> Bool Source #
ToJSON InteractionId Source # |
Instance details Methods toJSON :: InteractionId -> Value Source # toEncoding :: InteractionId -> Encoding Source # toJSONList :: [InteractionId] -> Value Source # toEncodingList :: [InteractionId] -> Encoding Source # omitField :: InteractionId -> Bool Source #
ToJSON MetaId Source # |
Instance details Methods toJSON :: MetaId -> Value Source # toEncoding :: MetaId -> Encoding Source # toJSONList :: [MetaId] -> Value Source # toEncodingList :: [MetaId] -> Encoding Source # omitField :: MetaId -> Bool Source #
ToJSON ProblemId Source # |
Instance details Methods toJSON :: ProblemId -> Value Source # toEncoding :: ProblemId -> Encoding Source # toJSONList :: [ProblemId] -> Value Source # toEncodingList :: [ProblemId] -> Encoding Source # omitField :: ProblemId -> Bool Source #
ToJSON NameInScope Source # |
Instance details Methods toJSON :: NameInScope -> Value Source # toEncoding :: NameInScope -> Encoding Source # toJSONList :: [NameInScope] -> Value Source # toEncodingList :: [NameInScope] -> Encoding Source # omitField :: NameInScope -> Bool Source #
ToJSON Range Source # |
Instance details Methods toJSON :: Range -> Value Source # toEncoding :: Range -> Encoding Source # toJSONList :: [Range] -> Value Source # toEncodingList :: [Range] -> Encoding Source # omitField :: Range -> Bool Source #
ToJSON ModuleNameHash Source # |
Instance details Methods toJSON :: ModuleNameHash -> Value Source # toEncoding :: ModuleNameHash -> Encoding Source # toJSONList :: [ModuleNameHash] -> Value Source # toEncodingList :: [ModuleNameHash] -> Encoding Source # omitField :: ModuleNameHash -> Bool Source #
ToJSON CPUTime Source # |
Instance details Methods toJSON :: CPUTime -> Value Source # toEncoding :: CPUTime -> Encoding Source # toJSONList :: [CPUTime] -> Value Source # toEncodingList :: [CPUTime] -> Encoding Source # omitField :: CPUTime -> Bool Source #
EncodeTCM (Position' ()) Source # |
Instance details Methods encodeTCM :: Position' () -> TCM Value Source #
ToJSON (Position' ()) Source # |
Instance details Methods toJSON :: Position' () -> Value Source # toEncoding :: Position' () -> Encoding Source # toJSONList :: [Position' ()] -> Value Source # toEncodingList :: [Position' ()] -> Encoding Source # omitField :: Position' () -> Bool Source #
EncodeTCM (OutputForm Expr Expr) Source # |
Instance details Methods encodeTCM :: OutputForm Expr Expr -> TCM Value Source #