def lex_object
qasim-bend-kit@0.1.0.2 · proof/JSON_RenderLexProof.bend:486
import qasim-bend-kit@0.1.0.2/proof/JSON_RenderLexProof.bend as JSONRenderLexProof
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_SourceProof.bend as SP
486def lex_object(+key: String,
487 +head: J.Value,
488 +tail: List<&2, Sigma<&2, &2, String, k => J.Value>>, +mode: SP.RenderMode, +boundary: Boundary, +acc: List<&2,
489 J.Lexeme>, head_lex: {J.lex_scan(SP.render_task(head, SP.RenderWhole{}, boundary_text(object_continuation(tail, boundary))), J.Outside{}, SNil{}, J.Punctuation{':'} <> J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> prefix_acc(ObjectKind{}, mode, acc)) == finish(object_continuation(tail, boundary), push(head, SP.RenderWhole{}, J.Punctuation{':'} <> J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> prefix_acc(ObjectKind{}, mode, acc))) : List<&2, J.Lexeme>}, tail_lex: {J.lex_scan(SP.render_task(J.Obj{tail}, SP.RenderAfterSeparator{}, boundary_text(boundary)), J.Outside{}, SNil{}, J.Punctuation{','} <> push(head, SP.RenderWhole{}, J.Punctuation{':'} <> J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> prefix_acc(ObjectKind{}, mode, acc))) == finish(boundary, push(J.Obj{tail}, SP.RenderAfterSeparator{}, J.Punctuation{','} <> push(head, SP.RenderWhole{}, J.Punctuation{':'} <> J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> prefix_acc(ObjectKind{}, mode, acc)))) : List<&2, J.Lexeme>}) -> {J.lex_scan(SP.render_task(J.Obj{(key, head) <> tail}, mode, boundary_text(boundary)), J.Outside{}, SNil{}, acc) == finish(boundary, push(J.Obj{(key, head) <> tail}, mode, acc)) : List<&2, J.Lexeme>}:
490 Equal.trans(List<&2, J.Lexeme>,
491 J.lex_scan(SP.render_task(J.Obj{(key, head) <> tail}, mode, boundary_text(boundary)), J.Outside{}, SNil{}, acc),
492 J.lex_scan(prefix_text(ObjectKind{}, mode, J.render_object_field(SNil{}, key, SP.render_task(head, SP.RenderWhole{}, boundary_text(object_continuation(tail, boundary))))), J.Outside{}, SNil{}, acc),
493 finish(boundary, push(J.Obj{(key, head) <> tail}, mode, acc)),
494 Equal.cong(String, List<&2, J.Lexeme>,
495 x => J.lex_scan(x, J.Outside{}, SNil{}, acc),
496 SP.render_task(J.Obj{(key, head) <> tail}, mode, boundary_text(boundary)),
497 prefix_text(ObjectKind{}, mode, J.render_object_field(SNil{}, key, SP.render_task(head, SP.RenderWhole{}, boundary_text(object_continuation(tail, boundary))))),
498 render_object(key, head, tail, mode, boundary, acc)),
499 Equal.trans(List<&2, J.Lexeme>,
500 J.lex_scan(prefix_text(ObjectKind{}, mode, J.render_object_field(SNil{}, key, SP.render_task(head, SP.RenderWhole{}, boundary_text(object_continuation(tail, boundary))))), J.Outside{}, SNil{}, acc),
501 J.lex_scan(J.render_object_field(SNil{}, key, SP.render_task(head, SP.RenderWhole{}, boundary_text(object_continuation(tail, boundary)))), J.Outside{}, SNil{}, prefix_acc(ObjectKind{}, mode, acc)),
502 finish(boundary, push(J.Obj{(key, head) <> tail}, mode, acc)),
503 scan_prefix(ObjectKind{}, mode, J.render_object_field(SNil{}, key, SP.render_task(head, SP.RenderWhole{}, boundary_text(object_continuation(tail, boundary)))), acc),
504 Equal.trans(List<&2, J.Lexeme>,
505 J.lex_scan(J.render_object_field(SNil{}, key, SP.render_task(head, SP.RenderWhole{}, boundary_text(object_continuation(tail, boundary)))), J.Outside{}, SNil{}, prefix_acc(ObjectKind{}, mode, acc)),
506 J.lex_scan(SP.render_task(head, SP.RenderWhole{}, boundary_text(object_continuation(tail, boundary))), J.Outside{}, SNil{}, J.Punctuation{':'} <> J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> prefix_acc(ObjectKind{}, mode, acc)),
507 finish(boundary, push(J.Obj{(key, head) <> tail}, mode, acc)),
508 scan_field(key, SP.render_task(head, SP.RenderWhole{}, boundary_text(object_continuation(tail, boundary))), prefix_acc(ObjectKind{}, mode, acc)),
509 Equal.trans(List<&2, J.Lexeme>,
510 J.lex_scan(SP.render_task(head, SP.RenderWhole{}, boundary_text(object_continuation(tail, boundary))), J.Outside{}, SNil{}, J.Punctuation{':'} <> J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> prefix_acc(ObjectKind{}, mode, acc)),
511 finish(object_continuation(tail, boundary), push(head, SP.RenderWhole{}, J.Punctuation{':'} <> J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> prefix_acc(ObjectKind{}, mode, acc))),
512 finish(boundary, push(J.Obj{(key, head) <> tail}, mode, acc)),
513 head_lex,
514 Equal.trans(List<&2, J.Lexeme>,
515 finish(object_continuation(tail, boundary), push(head, SP.RenderWhole{}, J.Punctuation{':'} <> J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> prefix_acc(ObjectKind{}, mode, acc))),
516 finish(boundary, push(J.Obj{tail}, SP.RenderMembers{}, push(head, SP.RenderWhole{}, J.Punctuation{':'} <> J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> prefix_acc(ObjectKind{}, mode, acc)))),
517 finish(boundary, push(J.Obj{(key, head) <> tail}, mode, acc)),
518 object_resume(tail, boundary, push(head, SP.RenderWhole{}, J.Punctuation{':'} <> J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> prefix_acc(ObjectKind{}, mode, acc)), tail_lex),
519 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>,
520 x => finish(boundary, x),
521 push(J.Obj{tail}, SP.RenderMembers{}, push(head, SP.RenderWhole{}, J.Punctuation{':'} <> J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> prefix_acc(ObjectKind{}, mode, acc))),
522 push(J.Obj{(key, head) <> tail}, mode, acc),
523 Equal.sym(List<&2, J.Lexeme>,
524 push(J.Obj{(key, head) <> tail}, mode, acc),
525 push(J.Obj{tail}, SP.RenderMembers{}, push(head, SP.RenderWhole{}, J.Punctuation{':'} <> J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> prefix_acc(ObjectKind{}, mode, acc))),
526 push_object(key, head, tail, mode, acc))))))))