def parse_string_payload

qasim-bend-kit@0.1.0.2 · PROOF.bend:100

import Base
import qasim-bend-kit@0.1.0.2/libs/JSON.bend as Json
import qasim-bend-kit@0.1.0.2/proof/JSON_LexWhitespaceProof.bend as LexWhitespaceProof

100def parse_string_payload(+text: String) -> {Json.parse_normalized("\"" ++ Json.escape_string(text) ++ "\"") == Done{Json.Str{text}} : ResultValue()}:
101    Equal.trans(ResultValue(), Json.parse_normalized("\"" ++ Json.escape_string(text) ++ "\""),
102        Json.assemble(Json.token_list(Json.decode_tree(Json.lex_tree(Json.Payload{"\"" ++ Json.escape_string(text) ++ "\""} <> Nil{})), Nil{}), Json.NeedValue{Json.Top{}}),
103        Done{Json.Str{text}},
104        Equal.cong(List<&2, Json.Lexeme>, ResultValue(), items => Json.assemble(Json.token_list(Json.decode_tree(Json.lex_tree(items)), Nil{}), Json.NeedValue{Json.Top{}}),
105            Json.lex_scan("\"" ++ Json.escape_string(text) ++ "\"", Json.Outside{}, SNil{}, Nil{}),
106            Json.Payload{"\"" ++ Json.escape_string(text) ++ "\""} <> Nil{},
107            LexWhitespaceProof.lex_rendered_string(text)),
108        Equal.trans(ResultValue(),
109            Json.assemble(Json.token_list(Json.decode_tree(Json.lex_tree(Json.Payload{"\"" ++ Json.escape_string(text) ++ "\""} <> Nil{})), Nil{}), Json.NeedValue{Json.Top{}}),
110            Json.assemble(Json.decode_lexeme(Json.Payload{"\"" ++ Json.escape_string(text) ++ "\""}) <> Nil{}, Json.NeedValue{Json.Top{}}),
111            Done{Json.Str{text}},
112            Equal.cong(List<Json.Token>, ResultValue(), tokens => Json.assemble(tokens, Json.NeedValue{Json.Top{}}),
113                Json.token_list(Json.decode_tree(Json.lex_tree(Json.Payload{"\"" ++ Json.escape_string(text) ++ "\""} <> Nil{})), Nil{}),
114                Json.decode_lexeme(Json.Payload{"\"" ++ Json.escape_string(text) ++ "\""}) <> Nil{},
115                parallel_single("\"" ++ Json.escape_string(text) ++ "\"")),
116            assembled_string_payload(text)))