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

Safe Haskell | Safe-Inferred
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 GiveResult Source # |
Instance details Methods encodeTCM :: GiveResult -> TCM Value Source #
EncodeTCM GoalTypeAux Source # |
Instance details Methods encodeTCM :: GoalTypeAux -> TCM Value Source #
EncodeTCM Info_Error Source # |
Instance details Methods encodeTCM :: Info_Error -> TCM Value Source #
EncodeTCM MakeCaseVariant Source # |
Instance details Methods encodeTCM :: MakeCaseVariant -> TCM Value Source #
EncodeTCM Response Source # |
Instance details Methods encodeTCM :: Response -> 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 NamedMeta Source # |
Instance details Methods encodeTCM :: NamedMeta -> 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 CPUTime Source # |
Instance details Methods encodeTCM :: CPUTime -> TCM Value Source #
ToJSON CommandState Source # |
Instance details Methods toJSON :: CommandState -> Value # toEncoding :: CommandState -> Encoding # toJSONList :: [CommandState] -> Value # toEncodingList :: [CommandState] -> Encoding #
ToJSON ComputeMode Source # |
Instance details Methods toJSON :: ComputeMode -> Value # toEncoding :: ComputeMode -> Encoding # toJSONList :: [ComputeMode] -> Value # toEncodingList :: [ComputeMode] -> Encoding #
ToJSON CurrentFile Source # |
Instance details Methods toJSON :: CurrentFile -> Value # toEncoding :: CurrentFile -> Encoding # toJSONList :: [CurrentFile] -> Value # toEncodingList :: [CurrentFile] -> Encoding #
ToJSON Rewrite Source # |
Instance details Methods toJSON :: Rewrite -> Value # toEncoding :: Rewrite -> Encoding # toJSONList :: [Rewrite] -> Value # toEncodingList :: [Rewrite] -> Encoding #
ToJSON GiveResult Source # |
Instance details Methods toJSON :: GiveResult -> Value # toEncoding :: GiveResult -> Encoding # toJSONList :: [GiveResult] -> Value # toEncodingList :: [GiveResult] -> Encoding #
ToJSON MakeCaseVariant Source # |
Instance details Methods toJSON :: MakeCaseVariant -> Value # toEncoding :: MakeCaseVariant -> Encoding # toJSONList :: [MakeCaseVariant] -> Value # toEncodingList :: [MakeCaseVariant] -> Encoding #
ToJSON Status Source # |
Instance details Methods toJSON :: Status -> Value # toEncoding :: Status -> Encoding # toJSONList :: [Status] -> Value # toEncodingList :: [Status] -> Encoding #
ToJSON InteractionId Source # |
Instance details Methods toJSON :: InteractionId -> Value # toEncoding :: InteractionId -> Encoding # toJSONList :: [InteractionId] -> Value # toEncodingList :: [InteractionId] -> Encoding #
ToJSON MetaId Source # |
Instance details Methods toJSON :: MetaId -> Value # toEncoding :: MetaId -> Encoding # toJSONList :: [MetaId] -> Value # toEncodingList :: [MetaId] -> Encoding #
ToJSON ProblemId Source # |
Instance details Methods toJSON :: ProblemId -> Value # toEncoding :: ProblemId -> Encoding # toJSONList :: [ProblemId] -> Value # toEncodingList :: [ProblemId] -> Encoding #
ToJSON NameInScope Source # |
Instance details Methods toJSON :: NameInScope -> Value # toEncoding :: NameInScope -> Encoding # toJSONList :: [NameInScope] -> Value # toEncodingList :: [NameInScope] -> Encoding #
ToJSON Range Source # |
Instance details Methods toJSON :: Range -> Value # toEncoding :: Range -> Encoding # toJSONList :: [Range] -> Value # toEncodingList :: [Range] -> Encoding #
ToJSON CPUTime Source # |
Instance details Methods toJSON :: CPUTime -> Value # toEncoding :: CPUTime -> Encoding # toJSONList :: [CPUTime] -> Value # toEncodingList :: [CPUTime] -> Encoding #
EncodeTCM (Position' ()) Source # |
Instance details Methods encodeTCM :: Position' () -> TCM Value Source #
ToJSON (Position' ()) Source # |
Instance details Methods toJSON :: Position' () -> Value # toEncoding :: Position' () -> Encoding # toJSONList :: [Position' ()] -> Value # toEncodingList :: [Position' ()] -> Encoding #
EncodeTCM (OutputForm Expr Expr) Source # |
Instance details Methods encodeTCM :: OutputForm Expr Expr -> TCM Value Source #