def push_object

qasim-bend-kit@0.1.0.2 · proof/JSON_RenderLexProof.bend:81

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

81def push_object(+key: String,
82                +head: J.Value,
83                +tail: List<&2, Sigma<&2, &2, String, k => J.Value>>, +mode: SP.RenderMode, +acc: List<&2,
84                J.Lexeme>) -> {push(J.Obj{(key, head) <> tail}, mode, acc) == push(J.Obj{tail}, SP.RenderMembers{}, push(head, SP.RenderWhole{}, J.Punctuation{':'} <> J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> prefix_acc(ObjectKind{}, mode, acc))) : List<&2, J.Lexeme>}:
85    match mode:
86        case SP.RenderWhole{}: push_source(head, False{}, J.source(J.Obj{tail}, True{}, Nil{}), J.Punctuation{':'} <> J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> prefix_acc(ObjectKind{}, SP.RenderWhole{}, acc))
87        case SP.RenderMembers{}: push_source(head, False{}, J.source(J.Obj{tail}, True{}, Nil{}), J.Punctuation{':'} <> J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> prefix_acc(ObjectKind{}, SP.RenderMembers{}, acc))
88        case SP.RenderAfterSeparator{}: push_source(head, False{}, J.source(J.Obj{tail}, True{}, Nil{}), J.Punctuation{':'} <> J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> prefix_acc(ObjectKind{}, SP.RenderAfterSeparator{}, acc))