JSONAssemblyProof.roundtrip: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/JSON_AssemblyProof.bend as JSONAssemblyProof
Lines 137-190 of qasim-bend-kit@0.1.0.2/proof/JSON_AssemblyProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_AssemblyProof.bend&start_line=137&end_line=190

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

def roundtrip(+value: J.Value,
              +mode: Mode,
              -tail: List<J.Token>,
              +acc: List<&2, J.Value>,
              +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()}:
    match value:
        case J.Arr{Nil{}}:
            match mode:
                case Whole{}: {==}
                case Members{}: {==}
        case J.Arr{head <> rest}:
            match mode:
                case Whole{}:
                    %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()}
                    %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()}
                    %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()}
                    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))
                case Members{}:
                    %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()}
                    %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()}
                    roundtrip(J.Arr{rest}, Members{}, tail, head <> acc, Nil{}, kont)
        case J.Obj{Nil{}}:
            match mode:
                case Whole{}: {==}
                case Members{}: {==}
        case J.Obj{(key, head) <> rest}:
            match mode:
                case Whole{}:
                    %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()}
                    %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()}
                    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))
                case Members{}:
                    %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()}
                    roundtrip(J.Obj{rest}, Members{}, tail, Nil{}, (key, head) <> fields, kont)
        case J.Null{}:
            match mode:
                case Whole{}: atom_roundtrip(J.Null{}, mode, tail, acc, fields, kont, "null", {==}, {==}, {==}, {==})
                case Members{}: atom_roundtrip(J.Null{}, mode, tail, acc, fields, kont, "null", {==}, {==}, {==}, {==})
        case J.Bool{True{}}:
            match mode:
                case Whole{}: atom_roundtrip(J.Bool{True{}}, mode, tail, acc, fields, kont, "true", {==}, {==}, {==}, {==})
                case Members{}: atom_roundtrip(J.Bool{True{}}, mode, tail, acc, fields, kont, "true", {==}, {==}, {==}, {==})
        case J.Bool{False{}}:
            match mode:
                case Whole{}: atom_roundtrip(J.Bool{False{}}, mode, tail, acc, fields, kont, "false", {==}, {==}, {==}, {==})
                case Members{}: atom_roundtrip(J.Bool{False{}}, mode, tail, acc, fields, kont, "false", {==}, {==}, {==}, {==})
        case J.Number{s, cert}:
            match mode:
                case Whole{}: atom_roundtrip(J.Number{s, cert}, mode, tail, acc, fields, kont, s, {==}, {==}, {==}, P.number_roundtrip(s, cert))
                case Members{}: atom_roundtrip(J.Number{s, cert}, mode, tail, acc, fields, kont, s, {==}, {==}, {==}, P.number_roundtrip(s, cert))
        case J.Str{s}:
            match mode:
                case Whole{}: atom_roundtrip(J.Str{s}, mode, tail, acc, fields, kont, "\"" ++ J.escape_string(s) ++ "\"", {==}, {==}, {==}, S.string_payload(s))
                case Members{}: atom_roundtrip(J.Str{s}, mode, tail, acc, fields, kont, "\"" ++ J.escape_string(s) ++ "\"", {==}, {==}, {==}, S.string_payload(s))

Uses (26):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.reverse
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String.append
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=Assembly
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=ParserKont
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=Token
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=Value
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=assemble
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=assembly_resume
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=escape_string
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_AssemblyProof.bend&name=Mode
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_AssemblyProof.bend&name=R
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_AssemblyProof.bend&name=array_first
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_AssemblyProof.bend&name=array_next
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_AssemblyProof.bend&name=atom_roundtrip
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_AssemblyProof.bend&name=completed
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_AssemblyProof.bend&name=start
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_AssemblyProof.bend&name=tokens
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_ListProof.bend&name=reverse_twice
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_PrimitiveProof.bend&name=number_roundtrip
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_StringProof.bend&name=string_payload