Agda.Interaction.JSONTop
Contents
jsonREPL :: TCM () -> TCM () Source #
jsonREPL is a interpreter like mimicGHCi, but outputs JSON-encoded strings.
jsonREPL
mimicGHCi
jsonREPL reads Haskell values (that starts from IOTCM ...) from stdin, interprets them, and outputs JSON-encoded strings. into stdout.
IOTCM
Methods
encodeTCM :: CommandState -> TCM Value Source #
encodeTCM :: ComputeMode -> TCM Value Source #
encodeTCM :: CurrentFile -> TCM Value Source #
encodeTCM :: Rewrite -> TCM Value Source #
encodeTCM :: DisplayInfo -> TCM Value Source #
encodeTCM :: GiveResult -> TCM Value Source #
encodeTCM :: GoalTypeAux -> TCM Value Source #
encodeTCM :: Info_Error -> TCM Value Source #
encodeTCM :: MakeCaseVariant -> TCM Value Source #
encodeTCM :: Response -> TCM Value Source #
encodeTCM :: ResponseContextEntry -> TCM Value Source #
encodeTCM :: Status -> TCM Value Source #
encodeTCM :: InteractionId -> TCM Value Source #
encodeTCM :: MetaId -> TCM Value Source #
encodeTCM :: ProblemId -> TCM Value Source #
encodeTCM :: NameInScope -> TCM Value Source #
encodeTCM :: Blocker -> TCM Value Source #
encodeTCM :: Range -> TCM Value Source #
encodeTCM :: NamedMeta -> TCM Value Source #
encodeTCM :: TCErr -> TCM Value Source #
encodeTCM :: TCWarning -> TCM Value Source #
encodeTCM :: CPUTime -> TCM Value Source #
toJSON :: CommandState -> Value #
toEncoding :: CommandState -> Encoding #
toJSONList :: [CommandState] -> Value #
toEncodingList :: [CommandState] -> Encoding #
omitField :: CommandState -> Bool #
toJSON :: ComputeMode -> Value #
toEncoding :: ComputeMode -> Encoding #
toJSONList :: [ComputeMode] -> Value #
toEncodingList :: [ComputeMode] -> Encoding #
omitField :: ComputeMode -> Bool #
toJSON :: CurrentFile -> Value #
toEncoding :: CurrentFile -> Encoding #
toJSONList :: [CurrentFile] -> Value #
toEncodingList :: [CurrentFile] -> Encoding #
omitField :: CurrentFile -> Bool #
toJSON :: Rewrite -> Value #
toEncoding :: Rewrite -> Encoding #
toJSONList :: [Rewrite] -> Value #
toEncodingList :: [Rewrite] -> Encoding #
omitField :: Rewrite -> Bool #
toJSON :: GiveResult -> Value #
toEncoding :: GiveResult -> Encoding #
toJSONList :: [GiveResult] -> Value #
toEncodingList :: [GiveResult] -> Encoding #
omitField :: GiveResult -> Bool #
toJSON :: MakeCaseVariant -> Value #
toEncoding :: MakeCaseVariant -> Encoding #
toJSONList :: [MakeCaseVariant] -> Value #
toEncodingList :: [MakeCaseVariant] -> Encoding #
omitField :: MakeCaseVariant -> Bool #
toJSON :: Status -> Value #
toEncoding :: Status -> Encoding #
toJSONList :: [Status] -> Value #
toEncodingList :: [Status] -> Encoding #
omitField :: Status -> Bool #
toJSON :: InteractionId -> Value #
toEncoding :: InteractionId -> Encoding #
toJSONList :: [InteractionId] -> Value #
toEncodingList :: [InteractionId] -> Encoding #
omitField :: InteractionId -> Bool #
toJSON :: MetaId -> Value #
toEncoding :: MetaId -> Encoding #
toJSONList :: [MetaId] -> Value #
toEncodingList :: [MetaId] -> Encoding #
omitField :: MetaId -> Bool #
toJSON :: ModuleNameHash -> Value #
toEncoding :: ModuleNameHash -> Encoding #
toJSONList :: [ModuleNameHash] -> Value #
toEncodingList :: [ModuleNameHash] -> Encoding #
omitField :: ModuleNameHash -> Bool #
toJSON :: ProblemId -> Value #
toEncoding :: ProblemId -> Encoding #
toJSONList :: [ProblemId] -> Value #
toEncodingList :: [ProblemId] -> Encoding #
omitField :: ProblemId -> Bool #
toJSON :: NameInScope -> Value #
toEncoding :: NameInScope -> Encoding #
toJSONList :: [NameInScope] -> Value #
toEncodingList :: [NameInScope] -> Encoding #
omitField :: NameInScope -> Bool #
toJSON :: Range -> Value #
toEncoding :: Range -> Encoding #
toJSONList :: [Range] -> Value #
toEncodingList :: [Range] -> Encoding #
omitField :: Range -> Bool #
toJSON :: CPUTime -> Value #
toEncoding :: CPUTime -> Encoding #
toJSONList :: [CPUTime] -> Value #
toEncodingList :: [CPUTime] -> Encoding #
omitField :: CPUTime -> Bool #
encodeTCM :: Position' () -> TCM Value Source #
toJSON :: Position' () -> Value #
toEncoding :: Position' () -> Encoding #
toJSONList :: [Position' ()] -> Value #
toEncodingList :: [Position' ()] -> Encoding #
omitField :: Position' () -> Bool #
encodeTCM :: OutputForm Expr Expr -> TCM Value Source #