proof/JSON_RenderLexProof.bend source
proof/JSON_RenderLexProof.bend on the hub · documented module
# Lexer/renderer bridge. All recursion follows the JSON value structure.import Baseimport ../libs/JSON.bend as Jimport ./JSON_SourceProof.bend as SPimport ./JSON_NumberLexProof.bend as Numimport ./JSON_PrimitiveProof.bend as Pimport ./JSON_ListProof.bend as LPimport ./JSON_StringProof.bend as Simport ./JSON_LexWhitespaceProof.bend as Wdef reverse_concat(+xs: List<&2, J.Lexeme>, +ys: List<&2, J.Lexeme>, +acc: List<&2, J.Lexeme>) -> {List.reverse.go(&2, J.Lexeme, List.append(&2, J.Lexeme, xs, ys), acc) == List.reverse.go(&2, J.Lexeme, ys, List.reverse.go(&2, J.Lexeme, xs, acc)) : List<&2, J.Lexeme>}: match xs: case Nil{}: {==} case h <> t: reverse_concat(t, ys, h <> acc)def push(value: J.Value, mode: SP.RenderMode, acc: List<&2, J.Lexeme>) -> List<&2, J.Lexeme>: List.reverse.go(&2, J.Lexeme, SP.source_task(value, mode, Nil{}), acc)def push_append(+value: J.Value, +mode: SP.RenderMode, +acc: List<&2, J.Lexeme>) -> {push(value, mode, acc) == List.append(&2, J.Lexeme, SP.reverse_source_task(value, mode), acc) : List<&2, J.Lexeme>}: LP.reverse_go_append(J.Lexeme, SP.source_task(value, mode, Nil{}), Nil{}, acc)def push_source(+value: J.Value, +members: Bool, +suffix: List<&2, J.Lexeme>, +acc: List<&2, J.Lexeme>) -> {List.reverse.go(&2, J.Lexeme, J.source(value, members, suffix), acc) == List.reverse.go(&2, J.Lexeme, suffix, List.reverse.go(&2, J.Lexeme, J.source(value, members, Nil{}), acc)) : List<&2, J.Lexeme>}: Equal.trans(List<&2, J.Lexeme>, List.reverse.go(&2, J.Lexeme, J.source(value, members, suffix), acc), List.reverse.go(&2, J.Lexeme, List.append(&2, J.Lexeme, J.source(value, members, Nil{}), suffix), acc), List.reverse.go(&2, J.Lexeme, suffix, List.reverse.go(&2, J.Lexeme, J.source(value, members, Nil{}), acc)), Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, x => List.reverse.go(&2, J.Lexeme, x, acc), J.source(value, members, suffix), List.append(&2, J.Lexeme, J.source(value, members, Nil{}), suffix), SP.source_append(value, members, Nil{}, suffix)), reverse_concat(J.source(value, members, Nil{}), suffix, acc))type Container is Data: ArrayKind{} ObjectKind{}def opening(kind: Container) -> Char: match kind: case ArrayKind{}: '[' case ObjectKind{}: '{'def prefix_text(kind: Container, mode: SP.RenderMode, text: String) -> String: match mode: case SP.RenderWhole{}: SCon{opening(kind), text} case SP.RenderMembers{}: SCon{',', text} case SP.RenderAfterSeparator{}: textdef prefix_acc(kind: Container, mode: SP.RenderMode, acc: List<&2, J.Lexeme>) -> List<&2, J.Lexeme>: match mode: case SP.RenderWhole{}: J.Punctuation{opening(kind)} <> acc case SP.RenderMembers{}: J.Punctuation{','} <> acc case SP.RenderAfterSeparator{}: accdef scan_prefix(+kind: Container, +mode: SP.RenderMode, +text: String, +acc: List<&2, J.Lexeme>) -> {J.lex_scan(prefix_text(kind, mode, text), J.Outside{}, SNil{}, acc) == J.lex_scan(text, J.Outside{}, SNil{}, prefix_acc(kind, mode, acc)) : List<&2, J.Lexeme>}: match kind mode: case ArrayKind{} SP.RenderWhole{}: W.scan_punctuation_char('[', text, SNil{}, acc, {==}) case ObjectKind{} SP.RenderWhole{}: W.scan_punctuation_char('{', text, SNil{}, acc, {==}) case _ SP.RenderMembers{}: W.scan_punctuation_char(',', text, SNil{}, acc, {==}) case _ SP.RenderAfterSeparator{}: {==}def push_array(+head: J.Value, +tail: List<&2, J.Value>, +mode: SP.RenderMode, +acc: List<&2, J.Lexeme>) -> {push(J.Arr{head <> tail}, mode, acc) == push(J.Arr{tail}, SP.RenderMembers{}, push(head, SP.RenderWhole{}, prefix_acc(ArrayKind{}, mode, acc))) : List<&2, J.Lexeme>}: match mode: case SP.RenderWhole{}: push_source(head, False{}, J.source(J.Arr{tail}, True{}, Nil{}), prefix_acc(ArrayKind{}, SP.RenderWhole{}, acc)) case SP.RenderMembers{}: push_source(head, False{}, J.source(J.Arr{tail}, True{}, Nil{}), prefix_acc(ArrayKind{}, SP.RenderMembers{}, acc)) case SP.RenderAfterSeparator{}: push_source(head, False{}, J.source(J.Arr{tail}, True{}, Nil{}), prefix_acc(ArrayKind{}, SP.RenderAfterSeparator{}, acc))def push_object(+key: String, +head: J.Value, +tail: List<&2, Sigma<&2, &2, String, k => J.Value>>, +mode: SP.RenderMode, +acc: List<&2, 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>}: match mode: 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)) 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)) 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))def number_tail_acc(+text: String, +state: J.NumberState, +rev_head: Char, +rev_tail: String, +first: Char, +prefix_tail: String, +acc: List<&2, J.Lexeme>, +reverse_prefix: {String.reverse(SCon{rev_head, rev_tail}) == SCon{first, prefix_tail} : String}, +evidence: {J.number_valid_end(J.number_valid_step(text, state)) == True{} : Bool}) -> {J.lex_scan(text, J.Outside{}, SCon{rev_head, rev_tail}, acc) == (List.reverse(&2, J.Lexeme, J.Payload{SCon{first, prefix_tail} ++ text} <> acc)) : List<&2, J.Lexeme>}: match text: case SNil{}: Equal.trans(List<&2, J.Lexeme>, J.lex_scan(SNil{}, J.Outside{}, SCon{rev_head, rev_tail}, acc), List.reverse(&2, J.Lexeme, J.Payload{String.reverse(SCon{rev_head, rev_tail})} <> acc), List.reverse(&2, J.Lexeme, J.Payload{SCon{first, prefix_tail} ++ SNil{}} <> acc), {==}, Equal.trans(List<&2, J.Lexeme>, List.reverse(&2, J.Lexeme, J.Payload{String.reverse(SCon{rev_head, rev_tail})} <> acc), List.reverse(&2, J.Lexeme, J.Payload{SCon{first, prefix_tail}} <> acc), List.reverse(&2, J.Lexeme, J.Payload{SCon{first, prefix_tail} ++ SNil{}} <> acc), Equal.cong(String, List<&2, J.Lexeme>, s => List.reverse(&2, J.Lexeme, J.Payload{s} <> acc), String.reverse(SCon{rev_head, rev_tail}), SCon{first, prefix_tail}, reverse_prefix), Equal.cong(String, List<&2, J.Lexeme>, s => List.reverse(&2, J.Lexeme, J.Payload{s} <> acc), SCon{first, prefix_tail}, SCon{first, prefix_tail} ++ SNil{}, Equal.sym(String, SCon{first, prefix_tail} ++ SNil{}, SCon{first, prefix_tail}, S.append_nil(SCon{first, prefix_tail}))))) case SCon{+head, +tail}: Equal.trans(List<&2, J.Lexeme>, J.lex_scan(text, J.Outside{}, SCon{rev_head, rev_tail}, acc), J.lexemes(text, J.Outside{}, SCon{rev_head, rev_tail}, acc, J.LexRaw{}), List.reverse(&2, J.Lexeme, J.Payload{SCon{first, prefix_tail} ++ text} <> acc), Equal.cong(J.LexAction, List<&2, J.Lexeme>, action => J.lexemes(text, J.Outside{}, SCon{rev_head, rev_tail}, acc, action), J.lex_seed_action(text, J.Outside{}), J.LexRaw{}, Num.number_char_action(head, J.number_char(head), {==}, tail, state, evidence)), Equal.trans(List<&2, J.Lexeme>, J.lexemes(text, J.Outside{}, SCon{rev_head, rev_tail}, acc, J.LexRaw{}), J.lex_scan(tail, J.Outside{}, SCon{head, SCon{rev_head, rev_tail}}, acc), List.reverse(&2, J.Lexeme, J.Payload{SCon{first, prefix_tail} ++ text} <> acc), {==}, Equal.trans(List<&2, J.Lexeme>, J.lex_scan(tail, J.Outside{}, SCon{head, SCon{rev_head, rev_tail}}, acc), List.reverse(&2, J.Lexeme, J.Payload{(SCon{first, prefix_tail} ++ SCon{head, SNil{}}) ++ tail} <> acc), List.reverse(&2, J.Lexeme, J.Payload{SCon{first, prefix_tail} ++ text} <> acc), number_tail_acc(tail, J.number_next(state, head), head, SCon{rev_head, rev_tail}, first, prefix_tail ++ SCon{head, SNil{}}, acc, Equal.trans(String, String.reverse(SCon{head, SCon{rev_head, rev_tail}}), String.reverse(SCon{rev_head, rev_tail}) ++ SCon{head, SNil{}}, SCon{first, prefix_tail} ++ SCon{head, SNil{}}, S.reverse_cons(head, SCon{rev_head, rev_tail}), Equal.cong(String, String, x => x ++ SCon{head, SNil{}}, String.reverse(SCon{rev_head, rev_tail}), SCon{first, prefix_tail}, reverse_prefix)), Num.number_valid_cons(head, tail, state, evidence)), Equal.cong(String, List<&2, J.Lexeme>, s => List.reverse(&2, J.Lexeme, J.Payload{s} <> acc), (SCon{first, prefix_tail} ++ SCon{head, SNil{}}) ++ tail, SCon{first, prefix_tail} ++ text, S.append_assoc(SCon{first, prefix_tail}, SCon{head, SNil{}}, tail)))))def number_end(+text: String, +acc: List<&2, J.Lexeme>, +evidence: {J.number_valid(text) == True{} : Bool}) -> {J.lex_scan(text, J.Outside{}, SNil{}, acc) == (List.reverse(&2, J.Lexeme, J.Payload{text} <> acc)) : List<&2, J.Lexeme>}: match text: case SNil{}: Empty.absurd({J.lex_scan(SNil{}, J.Outside{}, SNil{}, acc) == (List.reverse(&2, J.Lexeme, J.Payload{SNil{}} <> acc)) : List<&2, J.Lexeme>}, Num.false_true(Equal.trans(Bool, False{}, J.number_valid(SNil{}), True{}, {==}, evidence))) case SCon{+head, +tail}: Equal.trans(List<&2, J.Lexeme>, J.lex_scan(text, J.Outside{}, SNil{}, acc), J.lexemes(text, J.Outside{}, SNil{}, acc, J.LexRaw{}), List.reverse(&2, J.Lexeme, J.Payload{text} <> acc), Equal.cong(J.LexAction, List<&2, J.Lexeme>, action => J.lexemes(text, J.Outside{}, SNil{}, acc, action), J.lex_seed_action(text, J.Outside{}), J.LexRaw{}, Num.number_char_action(head, J.number_char(head), {==}, tail, J.NumberStart{}, evidence)), Equal.trans(List<&2, J.Lexeme>, J.lexemes(text, J.Outside{}, SNil{}, acc, J.LexRaw{}), J.lex_scan(tail, J.Outside{}, SCon{head, SNil{}}, acc), List.reverse(&2, J.Lexeme, J.Payload{text} <> acc), {==}, Equal.trans(List<&2, J.Lexeme>, J.lex_scan(tail, J.Outside{}, SCon{head, SNil{}}, acc), List.reverse(&2, J.Lexeme, J.Payload{SCon{head, SNil{}} ++ tail} <> acc), List.reverse(&2, J.Lexeme, J.Payload{text} <> acc), number_tail_acc(tail, J.number_next(J.NumberStart{}, head), head, SNil{}, head, SNil{}, acc, {==}, Num.number_valid_cons(head, tail, J.NumberStart{}, evidence)), Equal.cong(String, List<&2, J.Lexeme>, s => List.reverse(&2, J.Lexeme, J.Payload{s} <> acc), SCon{head, SNil{}} ++ tail, text, {==}))))# A rendered value is followed either by end of input or a JSON delimiter.type Boundary is Data: End{} Delimited{mark: SP.JsonPunctuation, suffix: String}def boundary_text(boundary: Boundary) -> String: match boundary: case End{}: SNil{} case Delimited{mark, suffix}: SCon{SP.punctuation_char(mark), suffix}def finish(boundary: Boundary, acc: List<&2, J.Lexeme>) -> List<&2, J.Lexeme>: match boundary: case End{}: J.lex_scan(SNil{}, J.Outside{}, SNil{}, acc) case Delimited{mark, suffix}: J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{SP.punctuation_char(mark)} <> acc)def scan_boundary(+boundary: Boundary, +acc: List<&2, J.Lexeme>) -> {J.lex_scan(boundary_text(boundary), J.Outside{}, SNil{}, acc) == finish(boundary, acc) : List<&2, J.Lexeme>}: match boundary: case End{}: {==} case Delimited{mark, suffix}: W.scan_punctuation_char(SP.punctuation_char(mark), suffix, SNil{}, acc, SP.punctuation_action(mark, suffix))def atomic_end(+atom: SP.AtomicValue, +acc: List<&2, J.Lexeme>) -> {J.lex_scan(J.render(SP.atomic_value(atom), False{}, SNil{}), J.Outside{}, SNil{}, acc) == finish(End{}, push(SP.atomic_value(atom), SP.RenderWhole{}, acc)) : List<&2, J.Lexeme>}: match atom: case SP.AtomicNull{}: {==} case SP.AtomicTrue{}: {==} case SP.AtomicFalse{}: {==} case SP.AtomicNumber{text, certificate}: Equal.trans(List<&2, J.Lexeme>, J.lex_scan(J.render(J.Number{text, certificate}, False{}, SNil{}), J.Outside{}, SNil{}, acc), J.lex_scan(text, J.Outside{}, SNil{}, acc), finish(End{}, push(J.Number{text, certificate}, SP.RenderWhole{}, acc)), Equal.cong(String, List<&2, J.Lexeme>, x => J.lex_scan(x, J.Outside{}, SNil{}, acc), text ++ SNil{}, text, S.append_nil(text)), number_end(text, acc, P.cert_valid(text, certificate))) case SP.AtomicString{text}: Equal.trans(List<&2, J.Lexeme>, J.lex_scan(J.render(J.Str{text}, False{}, SNil{}), J.Outside{}, SNil{}, acc), J.lex_scan(J.render(J.Str{text}, False{}, SNil{}) ++ SNil{}, J.Outside{}, SNil{}, acc), finish(End{}, push(J.Str{text}, SP.RenderWhole{}, acc)), Equal.cong(String, List<&2, J.Lexeme>, x => J.lex_scan(x, J.Outside{}, SNil{}, acc), J.render(J.Str{text}, False{}, SNil{}), J.render(J.Str{text}, False{}, SNil{}) ++ SNil{}, Equal.sym(String, J.render(J.Str{text}, False{}, SNil{}) ++ SNil{}, J.render(J.Str{text}, False{}, SNil{}), S.append_nil(J.render(J.Str{text}, False{}, SNil{})))), W.lex_rendered_string_suffix(text, SNil{}, acc))def atomic_mode_end(+atom: SP.AtomicValue, +mode: SP.RenderMode, +acc: List<&2, J.Lexeme>) -> {J.lex_scan(SP.render_task(SP.atomic_value(atom), mode, SNil{}), J.Outside{}, SNil{}, acc) == finish(End{}, push(SP.atomic_value(atom), mode, acc)) : List<&2, J.Lexeme>}: match atom mode: case SP.AtomicNull{} SP.RenderWhole{}: atomic_end(SP.AtomicNull{}, acc) case SP.AtomicNull{} SP.RenderMembers{}: atomic_end(SP.AtomicNull{}, acc) case SP.AtomicNull{} SP.RenderAfterSeparator{}: atomic_end(SP.AtomicNull{}, acc) case SP.AtomicTrue{} SP.RenderWhole{}: atomic_end(SP.AtomicTrue{}, acc) case SP.AtomicTrue{} SP.RenderMembers{}: atomic_end(SP.AtomicTrue{}, acc) case SP.AtomicTrue{} SP.RenderAfterSeparator{}: atomic_end(SP.AtomicTrue{}, acc) case SP.AtomicFalse{} SP.RenderWhole{}: atomic_end(SP.AtomicFalse{}, acc) case SP.AtomicFalse{} SP.RenderMembers{}: atomic_end(SP.AtomicFalse{}, acc) case SP.AtomicFalse{} SP.RenderAfterSeparator{}: atomic_end(SP.AtomicFalse{}, acc) case SP.AtomicNumber{text, certificate} SP.RenderWhole{}: atomic_end(SP.AtomicNumber{text, certificate}, acc) case SP.AtomicNumber{text, certificate} SP.RenderMembers{}: atomic_end(SP.AtomicNumber{text, certificate}, acc) case SP.AtomicNumber{text, certificate} SP.RenderAfterSeparator{}: atomic_end(SP.AtomicNumber{text, certificate}, acc) case SP.AtomicString{text} SP.RenderWhole{}: atomic_end(SP.AtomicString{text}, acc) case SP.AtomicString{text} SP.RenderMembers{}: atomic_end(SP.AtomicString{text}, acc) case SP.AtomicString{text} SP.RenderAfterSeparator{}: atomic_end(SP.AtomicString{text}, acc)def atomic_lex(+atom: SP.AtomicValue, +mode: SP.RenderMode, +boundary: Boundary, +acc: List<&2, J.Lexeme>) -> {J.lex_scan(SP.render_task(SP.atomic_value(atom), mode, boundary_text(boundary)), J.Outside{}, SNil{}, acc) == finish(boundary, push(SP.atomic_value(atom), mode, acc)) : List<&2, J.Lexeme>}: match boundary: case End{}: atomic_mode_end(atom, mode, acc) case Delimited{mark, suffix}: Equal.trans(List<&2, J.Lexeme>, J.lex_scan(SP.render_task(SP.atomic_value(atom), mode, boundary_text(Delimited{mark, suffix})), J.Outside{}, SNil{}, acc), J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{SP.punctuation_char(mark)} <> List.append(&2, J.Lexeme, SP.reverse_source_task(SP.atomic_value(atom), mode), acc)), finish(Delimited{mark, suffix}, push(SP.atomic_value(atom), mode, acc)), SP.lex_simple_task_suffix_before_punctuation(SP.SimpleAtom{atom}, mode, SP.punctuation_char(mark), suffix, acc, SP.punctuation_action(mark, suffix)), Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, x => finish(Delimited{mark, suffix}, x), List.append(&2, J.Lexeme, SP.reverse_source_task(SP.atomic_value(atom), mode), acc), push(SP.atomic_value(atom), mode, acc), Equal.sym(List<&2, J.Lexeme>, push(SP.atomic_value(atom), mode, acc), List.append(&2, J.Lexeme, SP.reverse_source_task(SP.atomic_value(atom), mode), acc), push_append(SP.atomic_value(atom), mode, acc))))def array_continuation(values: List<&2, J.Value>, boundary: Boundary) -> Boundary: match values: case Nil{}: Delimited{SP.ArrayEnd{}, boundary_text(boundary)} case head <> tail: Delimited{SP.MemberComma{}, SP.render_task(J.Arr{values}, SP.RenderAfterSeparator{}, boundary_text(boundary))}def array_continuation_text(+values: List<&2, J.Value>, +boundary: Boundary) -> {SP.render_task(J.Arr{values}, SP.RenderMembers{}, boundary_text(boundary)) == boundary_text(array_continuation(values, boundary)) : String}: match values: case Nil{}: {==} case head <> tail: {==}def array_resume(+values: List<&2, J.Value>, +boundary: Boundary, +acc: List<&2, J.Lexeme>, tail_lex: {J.lex_scan(SP.render_task(J.Arr{values}, SP.RenderAfterSeparator{}, boundary_text(boundary)), J.Outside{}, SNil{}, J.Punctuation{','} <> acc) == finish(boundary, push(J.Arr{values}, SP.RenderAfterSeparator{}, J.Punctuation{','} <> acc)) : List<&2, J.Lexeme>}) -> {finish(array_continuation(values, boundary), acc) == finish(boundary, push(J.Arr{values}, SP.RenderMembers{}, acc)) : List<&2, J.Lexeme>}: match values: case Nil{}: scan_boundary(boundary, J.Punctuation{']'} <> acc) case head <> tail: tail_lexdef object_continuation(values: List<&2, Sigma<&2, &2, String, k => J.Value>>, boundary: Boundary) -> Boundary: match values: case Nil{}: Delimited{SP.ObjectEnd{}, boundary_text(boundary)} case (key, head) <> tail: Delimited{SP.MemberComma{}, SP.render_task(J.Obj{values}, SP.RenderAfterSeparator{}, boundary_text(boundary))}def object_continuation_text(+values: List<&2, Sigma<&2, &2, String, k => J.Value>>, +boundary: Boundary) -> {SP.render_task(J.Obj{values}, SP.RenderMembers{}, boundary_text(boundary)) == boundary_text(object_continuation(values, boundary)) : String}: match values: case Nil{}: {==} case (key, head) <> tail: {==}def object_resume(+values: List<&2, Sigma<&2, &2, String, k => J.Value>>, +boundary: Boundary, +acc: List<&2, J.Lexeme>, tail_lex: {J.lex_scan(SP.render_task(J.Obj{values}, SP.RenderAfterSeparator{}, boundary_text(boundary)), J.Outside{}, SNil{}, J.Punctuation{','} <> acc) == finish(boundary, push(J.Obj{values}, SP.RenderAfterSeparator{}, J.Punctuation{','} <> acc)) : List<&2, J.Lexeme>}) -> {finish(object_continuation(values, boundary), acc) == finish(boundary, push(J.Obj{values}, SP.RenderMembers{}, acc)) : List<&2, J.Lexeme>}: match values: case Nil{}: scan_boundary(boundary, J.Punctuation{'}'} <> acc) case (key, head) <> tail: tail_lexdef field_text(+key: String, +text: String) -> {J.render_object_field(SNil{}, key, text) == ("\"" ++ J.escape_string(key) ++ "\"") ++ (":" ++ text) : String}: Equal.trans(String, J.render_object_field(SNil{}, key, text), SCon{'"', J.escape_string(key) ++ ("\":" ++ text)}, ("\"" ++ J.escape_string(key) ++ "\"") ++ (":" ++ text), Equal.cong(String, String, x => SCon{'"', x}, (J.escape_string(key) ++ "\":") ++ text, J.escape_string(key) ++ ("\":" ++ text), S.append_assoc(J.escape_string(key), "\":", text)), Equal.sym(String, ("\"" ++ J.escape_string(key) ++ "\"") ++ (":" ++ text), SCon{'"', J.escape_string(key) ++ ("\":" ++ text)}, Equal.cong(String, String, x => SCon{'"', x}, (J.escape_string(key) ++ "\"") ++ (":" ++ text), J.escape_string(key) ++ ("\"" ++ (":" ++ text)), S.append_assoc(J.escape_string(key), "\"", ":" ++ text))))def scan_field(+key: String, +text: String, +acc: List<&2, J.Lexeme>) -> {J.lex_scan(J.render_object_field(SNil{}, key, text), J.Outside{}, SNil{}, acc) == J.lex_scan(text, J.Outside{}, SNil{}, J.Punctuation{':'} <> J.Payload{("\"" ++ J.escape_string(key) ++ "\"")} <> acc) : List<&2, J.Lexeme>}: Equal.trans(List<&2, J.Lexeme>, J.lex_scan(J.render_object_field(SNil{}, key, text), J.Outside{}, SNil{}, acc), J.lex_scan(("\"" ++ J.escape_string(key) ++ "\"") ++ (":" ++ text), J.Outside{}, SNil{}, acc), J.lex_scan(text, J.Outside{}, SNil{}, J.Punctuation{':'} <> J.Payload{("\"" ++ J.escape_string(key) ++ "\"")} <> acc), Equal.cong(String, List<&2, J.Lexeme>, x => J.lex_scan(x, J.Outside{}, SNil{}, acc), J.render_object_field(SNil{}, key, text), ("\"" ++ J.escape_string(key) ++ "\"") ++ (":" ++ text), field_text(key, text)), SP.lex_object_key_before_colon(key, text, acc))def empty_array_end(+mode: SP.RenderMode, +acc: List<&2, J.Lexeme>) -> {J.lex_scan(SP.render_task(J.Arr{Nil{}}, mode, SNil{}), J.Outside{}, SNil{}, acc) == finish(End{}, push(J.Arr{Nil{}}, mode, acc)) : List<&2, J.Lexeme>}: match mode: case SP.RenderWhole{}: {==} case SP.RenderMembers{}: {==} case SP.RenderAfterSeparator{}: {==}def empty_array_lex(+mode: SP.RenderMode, +boundary: Boundary, +acc: List<&2, J.Lexeme>) -> {J.lex_scan(SP.render_task(J.Arr{Nil{}}, mode, boundary_text(boundary)), J.Outside{}, SNil{}, acc) == finish(boundary, push(J.Arr{Nil{}}, mode, acc)) : List<&2, J.Lexeme>}: match boundary: case End{}: empty_array_end(mode, acc) case Delimited{mark, suffix}: Equal.trans(List<&2, J.Lexeme>, J.lex_scan(SP.render_task(J.Arr{Nil{}}, mode, boundary_text(Delimited{mark, suffix})), J.Outside{}, SNil{}, acc), finish(Delimited{mark, suffix}, List.append(&2, J.Lexeme, SP.reverse_source_task(J.Arr{Nil{}}, mode), acc)), finish(Delimited{mark, suffix}, push(J.Arr{Nil{}}, mode, acc)), SP.lex_simple_task_suffix_before_punctuation(SP.SimpleEmptyArray{}, mode, SP.punctuation_char(mark), suffix, acc, SP.punctuation_action(mark, suffix)), Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, x => finish(Delimited{mark, suffix}, x), List.append(&2, J.Lexeme, SP.reverse_source_task(J.Arr{Nil{}}, mode), acc), push(J.Arr{Nil{}}, mode, acc), Equal.sym(List<&2, J.Lexeme>, push(J.Arr{Nil{}}, mode, acc), List.append(&2, J.Lexeme, SP.reverse_source_task(J.Arr{Nil{}}, mode), acc), push_append(J.Arr{Nil{}}, mode, acc))))def empty_object_end(+mode: SP.RenderMode, +acc: List<&2, J.Lexeme>) -> {J.lex_scan(SP.render_task(J.Obj{Nil{}}, mode, SNil{}), J.Outside{}, SNil{}, acc) == finish(End{}, push(J.Obj{Nil{}}, mode, acc)) : List<&2, J.Lexeme>}: match mode: case SP.RenderWhole{}: {==} case SP.RenderMembers{}: {==} case SP.RenderAfterSeparator{}: {==}def empty_object_lex(+mode: SP.RenderMode, +boundary: Boundary, +acc: List<&2, J.Lexeme>) -> {J.lex_scan(SP.render_task(J.Obj{Nil{}}, mode, boundary_text(boundary)), J.Outside{}, SNil{}, acc) == finish(boundary, push(J.Obj{Nil{}}, mode, acc)) : List<&2, J.Lexeme>}: match boundary: case End{}: empty_object_end(mode, acc) case Delimited{mark, suffix}: Equal.trans(List<&2, J.Lexeme>, J.lex_scan(SP.render_task(J.Obj{Nil{}}, mode, boundary_text(Delimited{mark, suffix})), J.Outside{}, SNil{}, acc), finish(Delimited{mark, suffix}, List.append(&2, J.Lexeme, SP.reverse_source_task(J.Obj{Nil{}}, mode), acc)), finish(Delimited{mark, suffix}, push(J.Obj{Nil{}}, mode, acc)), SP.lex_simple_task_suffix_before_punctuation(SP.SimpleEmptyObject{}, mode, SP.punctuation_char(mark), suffix, acc, SP.punctuation_action(mark, suffix)), Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, x => finish(Delimited{mark, suffix}, x), List.append(&2, J.Lexeme, SP.reverse_source_task(J.Obj{Nil{}}, mode), acc), push(J.Obj{Nil{}}, mode, acc), Equal.sym(List<&2, J.Lexeme>, push(J.Obj{Nil{}}, mode, acc), List.append(&2, J.Lexeme, SP.reverse_source_task(J.Obj{Nil{}}, mode), acc), push_append(J.Obj{Nil{}}, mode, acc))))def render_array(+head: J.Value, +tail: List<&2, J.Value>, +mode: SP.RenderMode, +boundary: Boundary, +acc: List<&2, J.Lexeme>) -> {SP.render_task(J.Arr{head <> tail}, mode, boundary_text(boundary)) == prefix_text(ArrayKind{}, mode, SP.render_task(head, SP.RenderWhole{}, boundary_text(array_continuation(tail, boundary)))) : String}: match mode: case SP.RenderWhole{}: Equal.cong(String, String, x => prefix_text(ArrayKind{}, SP.RenderWhole{}, SP.render_task(head, SP.RenderWhole{}, x)), SP.render_task(J.Arr{tail}, SP.RenderMembers{}, boundary_text(boundary)), boundary_text(array_continuation(tail, boundary)), array_continuation_text(tail, boundary)) case SP.RenderMembers{}: Equal.cong(String, String, x => prefix_text(ArrayKind{}, SP.RenderMembers{}, SP.render_task(head, SP.RenderWhole{}, x)), SP.render_task(J.Arr{tail}, SP.RenderMembers{}, boundary_text(boundary)), boundary_text(array_continuation(tail, boundary)), array_continuation_text(tail, boundary)) case SP.RenderAfterSeparator{}: Equal.cong(String, String, x => prefix_text(ArrayKind{}, SP.RenderAfterSeparator{}, SP.render_task(head, SP.RenderWhole{}, x)), SP.render_task(J.Arr{tail}, SP.RenderMembers{}, boundary_text(boundary)), boundary_text(array_continuation(tail, boundary)), array_continuation_text(tail, boundary))def lex_array(+head: J.Value, +tail: List<&2, J.Value>, +mode: SP.RenderMode, +boundary: Boundary, +acc: List<&2, J.Lexeme>, head_lex: {J.lex_scan(SP.render_task(head, SP.RenderWhole{}, boundary_text(array_continuation(tail, boundary))), J.Outside{}, SNil{}, prefix_acc(ArrayKind{}, mode, acc)) == finish(array_continuation(tail, boundary), push(head, SP.RenderWhole{}, prefix_acc(ArrayKind{}, mode, acc))) : List<&2, J.Lexeme>}, tail_lex: {J.lex_scan(SP.render_task(J.Arr{tail}, SP.RenderAfterSeparator{}, boundary_text(boundary)), J.Outside{}, SNil{}, J.Punctuation{','} <> push(head, SP.RenderWhole{}, prefix_acc(ArrayKind{}, mode, acc))) == finish(boundary, push(J.Arr{tail}, SP.RenderAfterSeparator{}, J.Punctuation{','} <> push(head, SP.RenderWhole{}, prefix_acc(ArrayKind{}, mode, acc)))) : List<&2, J.Lexeme>}) -> {J.lex_scan(SP.render_task(J.Arr{head <> tail}, mode, boundary_text(boundary)), J.Outside{}, SNil{}, acc) == finish(boundary, push(J.Arr{head <> tail}, mode, acc)) : List<&2, J.Lexeme>}: Equal.trans(List<&2, J.Lexeme>, J.lex_scan(SP.render_task(J.Arr{head <> tail}, mode, boundary_text(boundary)), J.Outside{}, SNil{}, acc), J.lex_scan(prefix_text(ArrayKind{}, mode, SP.render_task(head, SP.RenderWhole{}, boundary_text(array_continuation(tail, boundary)))), J.Outside{}, SNil{}, acc), finish(boundary, push(J.Arr{head <> tail}, mode, acc)), Equal.cong(String, List<&2, J.Lexeme>, x => J.lex_scan(x, J.Outside{}, SNil{}, acc), SP.render_task(J.Arr{head <> tail}, mode, boundary_text(boundary)), prefix_text(ArrayKind{}, mode, SP.render_task(head, SP.RenderWhole{}, boundary_text(array_continuation(tail, boundary)))), render_array(head, tail, mode, boundary, acc)), Equal.trans(List<&2, J.Lexeme>, J.lex_scan(prefix_text(ArrayKind{}, mode, SP.render_task(head, SP.RenderWhole{}, boundary_text(array_continuation(tail, boundary)))), J.Outside{}, SNil{}, acc), J.lex_scan(SP.render_task(head, SP.RenderWhole{}, boundary_text(array_continuation(tail, boundary))), J.Outside{}, SNil{}, prefix_acc(ArrayKind{}, mode, acc)), finish(boundary, push(J.Arr{head <> tail}, mode, acc)), scan_prefix(ArrayKind{}, mode, SP.render_task(head, SP.RenderWhole{}, boundary_text(array_continuation(tail, boundary))), acc), Equal.trans(List<&2, J.Lexeme>, J.lex_scan(SP.render_task(head, SP.RenderWhole{}, boundary_text(array_continuation(tail, boundary))), J.Outside{}, SNil{}, prefix_acc(ArrayKind{}, mode, acc)), finish(array_continuation(tail, boundary), push(head, SP.RenderWhole{}, prefix_acc(ArrayKind{}, mode, acc))), finish(boundary, push(J.Arr{head <> tail}, mode, acc)), head_lex, Equal.trans(List<&2, J.Lexeme>, finish(array_continuation(tail, boundary), push(head, SP.RenderWhole{}, prefix_acc(ArrayKind{}, mode, acc))), finish(boundary, push(J.Arr{tail}, SP.RenderMembers{}, push(head, SP.RenderWhole{}, prefix_acc(ArrayKind{}, mode, acc)))), finish(boundary, push(J.Arr{head <> tail}, mode, acc)), array_resume(tail, boundary, push(head, SP.RenderWhole{}, prefix_acc(ArrayKind{}, mode, acc)), tail_lex), Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, x => finish(boundary, x), push(J.Arr{tail}, SP.RenderMembers{}, push(head, SP.RenderWhole{}, prefix_acc(ArrayKind{}, mode, acc))), push(J.Arr{head <> tail}, mode, acc), Equal.sym(List<&2, J.Lexeme>, push(J.Arr{head <> tail}, mode, acc), push(J.Arr{tail}, SP.RenderMembers{}, push(head, SP.RenderWhole{}, prefix_acc(ArrayKind{}, mode, acc))), push_array(head, tail, mode, acc)))))))def render_object(+key: String, +head: J.Value, +tail: List<&2, Sigma<&2, &2, String, k => J.Value>>, +mode: SP.RenderMode, +boundary: Boundary, +acc: List<&2, J.Lexeme>) -> {SP.render_task(J.Obj{(key, head) <> tail}, mode, boundary_text(boundary)) == prefix_text(ObjectKind{}, mode, J.render_object_field(SNil{}, key, SP.render_task(head, SP.RenderWhole{}, boundary_text(object_continuation(tail, boundary))))) : String}: match mode: case SP.RenderWhole{}: Equal.cong(String, String, x => prefix_text(ObjectKind{}, SP.RenderWhole{}, J.render_object_field(SNil{}, key, SP.render_task(head, SP.RenderWhole{}, x))), SP.render_task(J.Obj{tail}, SP.RenderMembers{}, boundary_text(boundary)), boundary_text(object_continuation(tail, boundary)), object_continuation_text(tail, boundary)) case SP.RenderMembers{}: Equal.cong(String, String, x => prefix_text(ObjectKind{}, SP.RenderMembers{}, J.render_object_field(SNil{}, key, SP.render_task(head, SP.RenderWhole{}, x))), SP.render_task(J.Obj{tail}, SP.RenderMembers{}, boundary_text(boundary)), boundary_text(object_continuation(tail, boundary)), object_continuation_text(tail, boundary)) case SP.RenderAfterSeparator{}: Equal.cong(String, String, x => prefix_text(ObjectKind{}, SP.RenderAfterSeparator{}, J.render_object_field(SNil{}, key, SP.render_task(head, SP.RenderWhole{}, x))), SP.render_task(J.Obj{tail}, SP.RenderMembers{}, boundary_text(boundary)), boundary_text(object_continuation(tail, boundary)), object_continuation_text(tail, boundary))def lex_object(+key: String, +head: J.Value, +tail: List<&2, Sigma<&2, &2, String, k => J.Value>>, +mode: SP.RenderMode, +boundary: Boundary, +acc: List<&2, 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>}: Equal.trans(List<&2, J.Lexeme>, J.lex_scan(SP.render_task(J.Obj{(key, head) <> tail}, mode, boundary_text(boundary)), J.Outside{}, SNil{}, acc), 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), finish(boundary, push(J.Obj{(key, head) <> tail}, mode, acc)), Equal.cong(String, List<&2, J.Lexeme>, x => J.lex_scan(x, J.Outside{}, SNil{}, acc), SP.render_task(J.Obj{(key, head) <> tail}, mode, boundary_text(boundary)), prefix_text(ObjectKind{}, mode, J.render_object_field(SNil{}, key, SP.render_task(head, SP.RenderWhole{}, boundary_text(object_continuation(tail, boundary))))), render_object(key, head, tail, mode, boundary, acc)), Equal.trans(List<&2, J.Lexeme>, 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), 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)), finish(boundary, push(J.Obj{(key, head) <> tail}, mode, acc)), scan_prefix(ObjectKind{}, mode, J.render_object_field(SNil{}, key, SP.render_task(head, SP.RenderWhole{}, boundary_text(object_continuation(tail, boundary)))), acc), Equal.trans(List<&2, J.Lexeme>, 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)), 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(boundary, push(J.Obj{(key, head) <> tail}, mode, acc)), scan_field(key, SP.render_task(head, SP.RenderWhole{}, boundary_text(object_continuation(tail, boundary))), prefix_acc(ObjectKind{}, mode, acc)), Equal.trans(List<&2, J.Lexeme>, 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))), finish(boundary, push(J.Obj{(key, head) <> tail}, mode, acc)), head_lex, Equal.trans(List<&2, J.Lexeme>, finish(object_continuation(tail, boundary), push(head, SP.RenderWhole{}, J.Punctuation{':'} <> J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> prefix_acc(ObjectKind{}, mode, acc))), 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)))), finish(boundary, push(J.Obj{(key, head) <> tail}, mode, acc)), object_resume(tail, boundary, push(head, SP.RenderWhole{}, J.Punctuation{':'} <> J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> prefix_acc(ObjectKind{}, mode, acc)), tail_lex), Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, x => finish(boundary, x), push(J.Obj{tail}, SP.RenderMembers{}, push(head, SP.RenderWhole{}, J.Punctuation{':'} <> J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> prefix_acc(ObjectKind{}, mode, acc))), push(J.Obj{(key, head) <> tail}, mode, acc), Equal.sym(List<&2, 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))), push_object(key, head, tail, mode, acc))))))))def lex_value(+value: J.Value, +mode: SP.RenderMode, +boundary: Boundary, +acc: List<&2, J.Lexeme>) -> {J.lex_scan(SP.render_task(value, mode, boundary_text(boundary)), J.Outside{}, SNil{}, acc) == finish(boundary, push(value, mode, acc)) : List<&2, J.Lexeme>}: match value: case J.Null{}: atomic_lex(SP.AtomicNull{}, mode, boundary, acc) case J.Bool{truth}: match truth: case True{}: atomic_lex(SP.AtomicTrue{}, mode, boundary, acc) case False{}: atomic_lex(SP.AtomicFalse{}, mode, boundary, acc) case J.Number{text, certificate}: atomic_lex(SP.AtomicNumber{text, certificate}, mode, boundary, acc) case J.Str{text}: atomic_lex(SP.AtomicString{text}, mode, boundary, acc) case J.Arr{Nil{}}: empty_array_lex(mode, boundary, acc) case J.Obj{Nil{}}: empty_object_lex(mode, boundary, acc) case J.Arr{head <> tail}: lex_array(head, tail, mode, boundary, acc, lex_value(head, SP.RenderWhole{}, array_continuation(tail, boundary), prefix_acc(ArrayKind{}, mode, acc)), lex_value(J.Arr{tail}, SP.RenderAfterSeparator{}, boundary, J.Punctuation{','} <> push(head, SP.RenderWhole{}, prefix_acc(ArrayKind{}, mode, acc)))) case J.Obj{(key, head) <> tail}: lex_object(key, head, tail, mode, boundary, acc, lex_value(head, SP.RenderWhole{}, object_continuation(tail, boundary), J.Punctuation{':'} <> J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> prefix_acc(ObjectKind{}, mode, acc)), lex_value(J.Obj{tail}, SP.RenderAfterSeparator{}, boundary, J.Punctuation{','} <> push(head, SP.RenderWhole{}, J.Punctuation{':'} <> J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> prefix_acc(ObjectKind{}, mode, acc))))def lex_source(+value: J.Value) -> {J.lex_scan(J.stringify(value), J.Outside{}, SNil{}, Nil{}) == J.source(value, False{}, Nil{}) : List<&2, J.Lexeme>}: Equal.trans(List<&2, J.Lexeme>, J.lex_scan(J.stringify(value), J.Outside{}, SNil{}, Nil{}), finish(End{}, push(value, SP.RenderWhole{}, Nil{})), J.source(value, False{}, Nil{}), lex_value(value, SP.RenderWhole{}, End{}, Nil{}), LP.reverse_twice(J.Lexeme, J.source(value, False{}, Nil{})))