def roundtrip
qasim-bend-kit@0.1.0.2 · proof/JSON_AssemblyProof.bend:137
import qasim-bend-kit@0.1.0.2/proof/JSON_AssemblyProof.bend as JSONAssemblyProof
import Base
import qasim-bend-kit@0.1.0.2/libs/JSON.bend as J
import qasim-bend-kit@0.1.0.2/proof/JSON_ListProof.bend as L
import qasim-bend-kit@0.1.0.2/proof/JSON_PrimitiveProof.bend as P
import qasim-bend-kit@0.1.0.2/proof/JSON_StringProof.bend as S
137def roundtrip(+value: J.Value,
138 +mode: Mode,
139 -tail: List<J.Token>,
140 +acc: List<&2, J.Value>,
141 +fields: List<&2, Sigma<&2, &2, String, key => J.Value>>, +kont: J.ParserKont) -> {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()}:
142 match value:
143 case J.Arr{Nil{}}:
144 match mode:
145 case Whole{}: {==}
146 case Members{}: {==}
147 case J.Arr{head <> rest}:
148 match mode:
149 case Whole{}:
150 %Equal.sym(R(), J.assemble(tokens(head, Whole{}, tokens(J.Arr{rest}, Members{}, tail)), J.ArrayFirst{kont}), J.assemble(tokens(head, Whole{}, tokens(J.Arr{rest}, Members{}, tail)), J.NeedValue{J.InArray{Nil{}, kont}}), array_first(head, tokens(J.Arr{rest}, Members{}, tail), Nil{}, kont)) : {_ == J.assemble(tail, J.assembly_resume(kont, completed(J.Arr{head <> rest}, Whole{}, acc, fields))) : R()}
151 %Equal.sym(R(), J.assemble(tokens(head, Whole{}, tokens(J.Arr{rest}, Members{}, tail)), J.NeedValue{J.InArray{Nil{}, kont}}), J.assemble(tokens(J.Arr{rest}, Members{}, tail), J.ArrayComma{head <> Nil{}, kont}), roundtrip(head, Whole{}, tokens(J.Arr{rest}, Members{}, tail), Nil{}, Nil{}, J.InArray{Nil{}, kont})) : {_ == J.assemble(tail, J.assembly_resume(kont, completed(J.Arr{head <> rest}, Whole{}, acc, fields))) : R()}
152 %Equal.sym(R(), J.assemble(tokens(J.Arr{rest}, Members{}, tail), J.ArrayComma{head <> Nil{}, kont}), J.assemble(tail, J.assembly_resume(kont, completed(J.Arr{rest}, Members{}, head <> Nil{}, Nil{}))), roundtrip(J.Arr{rest}, Members{}, tail, head <> Nil{}, Nil{}, kont)) : {_ == J.assemble(tail, J.assembly_resume(kont, completed(J.Arr{head <> rest}, Whole{}, acc, fields))) : R()}
153 Equal.cong(List<&2, J.Value>, R(), xs => J.assemble(tail, J.assembly_resume(kont, J.Arr{xs})), List.reverse(&2, J.Value, List.reverse(&2, J.Value, head <> rest)), head <> rest, L.reverse_twice(J.Value, head <> rest))
154 case Members{}:
155 %Equal.sym(R(), J.assemble(tokens(head, Whole{}, tokens(J.Arr{rest}, Members{}, tail)), J.ArrayNext{acc, kont}), J.assemble(tokens(head, Whole{}, tokens(J.Arr{rest}, Members{}, tail)), J.NeedValue{J.InArray{acc, kont}}), array_next(head, tokens(J.Arr{rest}, Members{}, tail), acc, kont)) : {_ == J.assemble(tail, J.assembly_resume(kont, completed(J.Arr{head <> rest}, Members{}, acc, fields))) : R()}
156 %Equal.sym(R(), J.assemble(tokens(head, Whole{}, tokens(J.Arr{rest}, Members{}, tail)), J.NeedValue{J.InArray{acc, kont}}), J.assemble(tokens(J.Arr{rest}, Members{}, tail), J.ArrayComma{head <> acc, kont}), roundtrip(head, Whole{}, tokens(J.Arr{rest}, Members{}, tail), Nil{}, Nil{}, J.InArray{acc, kont})) : {_ == J.assemble(tail, J.assembly_resume(kont, completed(J.Arr{head <> rest}, Members{}, acc, fields))) : R()}
157 roundtrip(J.Arr{rest}, Members{}, tail, head <> acc, Nil{}, kont)
158 case J.Obj{Nil{}}:
159 match mode:
160 case Whole{}: {==}
161 case Members{}: {==}
162 case J.Obj{(key, head) <> rest}:
163 match mode:
164 case Whole{}:
165 %Equal.sym(R(), J.assemble(tokens(head, Whole{}, tokens(J.Obj{rest}, Members{}, tail)), J.NeedValue{J.InObject{key, Nil{}, kont}}), J.assemble(tokens(J.Obj{rest}, Members{}, tail), J.ObjectComma{(key, head) <> Nil{}, kont}), roundtrip(head, Whole{}, tokens(J.Obj{rest}, Members{}, tail), Nil{}, Nil{}, J.InObject{key, Nil{}, kont})) : {_ == J.assemble(tail, J.assembly_resume(kont, completed(J.Obj{(key, head) <> rest}, Whole{}, acc, fields))) : R()}
166 %Equal.sym(R(), J.assemble(tokens(J.Obj{rest}, Members{}, tail), J.ObjectComma{(key, head) <> Nil{}, kont}), J.assemble(tail, J.assembly_resume(kont, completed(J.Obj{rest}, Members{}, Nil{}, (key, head) <> Nil{}))), roundtrip(J.Obj{rest}, Members{}, tail, Nil{}, (key, head) <> Nil{}, kont)) : {_ == J.assemble(tail, J.assembly_resume(kont, completed(J.Obj{(key, head) <> rest}, Whole{}, acc, fields))) : R()}
167 Equal.cong(List<&2, Sigma<&2, &2, String, key => J.Value>>, R(), xs => J.assemble(tail, J.assembly_resume(kont, J.Obj{xs})), List.reverse(&2, Sigma<&2, &2, String, key => J.Value>, List.reverse(&2, Sigma<&2, &2, String, key => J.Value>, (key, head) <> rest)), (key, head) <> rest, L.reverse_twice(Sigma<&2, &2, String, key => J.Value>, (key, head) <> rest))
168 case Members{}:
169 %Equal.sym(R(), J.assemble(tokens(head, Whole{}, tokens(J.Obj{rest}, Members{}, tail)), J.NeedValue{J.InObject{key, fields, kont}}), J.assemble(tokens(J.Obj{rest}, Members{}, tail), J.ObjectComma{(key, head) <> fields, kont}), roundtrip(head, Whole{}, tokens(J.Obj{rest}, Members{}, tail), Nil{}, Nil{}, J.InObject{key, fields, kont})) : {_ == J.assemble(tail, J.assembly_resume(kont, completed(J.Obj{(key, head) <> rest}, Members{}, acc, fields))) : R()}
170 roundtrip(J.Obj{rest}, Members{}, tail, Nil{}, (key, head) <> fields, kont)
171 case J.Null{}:
172 match mode:
173 case Whole{}: atom_roundtrip(J.Null{}, mode, tail, acc, fields, kont, "null", {==}, {==}, {==}, {==})
174 case Members{}: atom_roundtrip(J.Null{}, mode, tail, acc, fields, kont, "null", {==}, {==}, {==}, {==})
175 case J.Bool{True{}}:
176 match mode:
177 case Whole{}: atom_roundtrip(J.Bool{True{}}, mode, tail, acc, fields, kont, "true", {==}, {==}, {==}, {==})
178 case Members{}: atom_roundtrip(J.Bool{True{}}, mode, tail, acc, fields, kont, "true", {==}, {==}, {==}, {==})
179 case J.Bool{False{}}:
180 match mode:
181 case Whole{}: atom_roundtrip(J.Bool{False{}}, mode, tail, acc, fields, kont, "false", {==}, {==}, {==}, {==})
182 case Members{}: atom_roundtrip(J.Bool{False{}}, mode, tail, acc, fields, kont, "false", {==}, {==}, {==}, {==})
183 case J.Number{s, cert}:
184 match mode:
185 case Whole{}: atom_roundtrip(J.Number{s, cert}, mode, tail, acc, fields, kont, s, {==}, {==}, {==}, P.number_roundtrip(s, cert))
186 case Members{}: atom_roundtrip(J.Number{s, cert}, mode, tail, acc, fields, kont, s, {==}, {==}, {==}, P.number_roundtrip(s, cert))
187 case J.Str{s}:
188 match mode:
189 case Whole{}: atom_roundtrip(J.Str{s}, mode, tail, acc, fields, kont, "\"" ++ J.escape_string(s) ++ "\"", {==}, {==}, {==}, S.string_payload(s))
190 case Members{}: atom_roundtrip(J.Str{s}, mode, tail, acc, fields, kont, "\"" ++ J.escape_string(s) ++ "\"", {==}, {==}, {==}, S.string_payload(s))