def atom_roundtrip

qasim-bend-kit@0.1.0.2 · proof/JSON_AssemblyProof.bend:72

import Base
import qasim-bend-kit@0.1.0.2/libs/JSON.bend as J

72def atom_roundtrip(+value: J.Value,
73                   +mode: Mode,
74                   -tail: List<J.Token>,
75                   +acc: List<&2, J.Value>,
76                   +fields: List<&2, Sigma<&2, &2, String, key => J.Value>>, +kont: J.ParserKont, +text: String, started: {start(value, mode, acc, fields, kont) == J.NeedValue{kont} : J.Assembly}, completed_value: {completed(value, mode, acc, fields) == value : J.Value}, tokenized: {tokens(value, mode, tail) == J.Atom{J.decode_payload(text)} <> tail : List<J.Token>}, decoded: {J.decode_payload(text) == Done{value} : Result<&1, &1, J.Error, J.Value>}) -> {J.assemble(tokens(value, mode, tail), start(value, mode, acc, fields, kont)) == J.assemble(tail, J.assembly_resume(kont, completed(value, mode, acc, fields))) : R()}:
77    Equal.trans(R(),
78        J.assemble(tokens(value, mode, tail), start(value, mode, acc, fields, kont)),
79        J.assemble(J.Atom{Done{value}} <> tail, J.NeedValue{kont}),
80        J.assemble(tail, J.assembly_resume(kont, completed(value, mode, acc, fields))),
81        Equal.trans(R(),
82            J.assemble(tokens(value, mode, tail), start(value, mode, acc, fields, kont)),
83            J.assemble(tokens(value, mode, tail), J.NeedValue{kont}),
84            J.assemble(J.Atom{Done{value}} <> tail, J.NeedValue{kont}),
85            Equal.cong(J.Assembly, R(), state => J.assemble(tokens(value, mode, tail), state),
86                start(value, mode, acc, fields, kont), J.NeedValue{kont}, started),
87            Equal.cong(List<J.Token>, R(), stream => J.assemble(stream, J.NeedValue{kont}),
88                tokens(value, mode, tail), J.Atom{Done{value}} <> tail,
89                Equal.trans(List<J.Token>, tokens(value, mode, tail), J.Atom{J.decode_payload(text)} <> tail,
90                    J.Atom{Done{value}} <> tail, tokenized,
91                    Equal.cong(Result<&1, &1, J.Error, J.Value>, List<J.Token>, result => J.Atom{result} <> tail,
92                        J.decode_payload(text), Done{value}, decoded)))),
93        Equal.cong(J.Value, R(), item => J.assemble(tail, J.assembly_resume(kont, item)),
94            value, completed(value, mode, acc, fields), Equal.sym(J.Value, completed(value, mode, acc, fields), value, completed_value)))