def parse_number_payload

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

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_PrimitiveProof.bend as PrimitiveProof
import qasim-bend-kit@0.1.0.2/proof/JSON_NumberLexProof.bend as NumberLexProof

71def parse_number_payload(+text: String,
72                         +certificate: Json.NumberCert<text>) -> {Json.parse_normalized(text) == Done{Json.Number{text, certificate}} : ResultValue()}:
73    Equal.trans(ResultValue(), Json.parse_normalized(text),
74        Json.assemble(Json.token_list(Json.decode_tree(Json.lex_tree(Json.Payload{text} <> Nil{})), Nil{}), Json.NeedValue{Json.Top{}}),
75        Done{Json.Number{text, certificate}},
76        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{}}),
77            Json.lex_scan(text, Json.Outside{}, SNil{}, Nil{}), Json.Payload{text} <> Nil{},
78            NumberLexProof.lex_number_payload(text, PrimitiveProof.cert_valid(text, certificate))),
79        Equal.trans(ResultValue(),
80            Json.assemble(Json.token_list(Json.decode_tree(Json.lex_tree(Json.Payload{text} <> Nil{})), Nil{}), Json.NeedValue{Json.Top{}}),
81            Json.decode_payload(text), Done{Json.Number{text, certificate}},
82            Equal.trans(ResultValue(),
83                Json.assemble(Json.token_list(Json.decode_tree(Json.lex_tree(Json.Payload{text} <> Nil{})), Nil{}), Json.NeedValue{Json.Top{}}),
84                Json.assemble(Json.decode_lexeme(Json.Payload{text}) <> Nil{}, Json.NeedValue{Json.Top{}}),
85                Json.decode_payload(text),
86                Equal.cong(List<Json.Token>, ResultValue(), tokens => Json.assemble(tokens, Json.NeedValue{Json.Top{}}),
87                    Json.token_list(Json.decode_tree(Json.lex_tree(Json.Payload{text} <> Nil{})), Nil{}),
88                    Json.decode_lexeme(Json.Payload{text}) <> Nil{},
89                    parallel_single(text)),
90                Equal.trans(ResultValue(),
91                    Json.assemble(Json.decode_lexeme(Json.Payload{text}) <> Nil{}, Json.NeedValue{Json.Top{}}),
92                    Json.decode_payload(text), Json.decode_payload(text),
93                    assemble_atom(Json.decode_payload(text)), {==})),
94            PrimitiveProof.number_roundtrip(text, certificate)))