def reverse_source_object_after_separator

qasim-bend-kit@0.1.0.2 · proof/JSON_SourceProof.bend:407

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 LP

407def reverse_source_object_after_separator(+key: String,
408                                          +value: J.Value,
409                                          +tail: List<&2, Sigma<&2, &2, String, key => J.Value>>) -> {reverse_source_task(J.Obj{(key, value) <> tail}, RenderAfterSeparator{}) == List.append(&2, J.Lexeme, reverse_source_task(J.Obj{tail}, RenderMembers{}), List.append(&2, J.Lexeme, reverse_source_task(value, RenderWhole{}), J.Punctuation{':'} <> J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> Nil{})) : List<&2, J.Lexeme>}:
410    Equal.trans(List<&2, J.Lexeme>,
411        reverse_source_task(J.Obj{(key, value) <> tail}, RenderAfterSeparator{}),
412        List.append(&2, J.Lexeme,
413            List.reverse(&2, J.Lexeme, J.Punctuation{':'} <> J.source(value, False{}, J.source(J.Obj{tail}, True{}, Nil{}))),
414            J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> Nil{}),
415        List.append(&2, J.Lexeme, reverse_source_task(J.Obj{tail}, RenderMembers{}),
416            List.append(&2, J.Lexeme, reverse_source_task(value, RenderWhole{}),
417                J.Punctuation{':'} <> J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> Nil{})),
418        reverse_source_text("\"" ++ J.escape_string(key) ++ "\"",
419            J.Punctuation{':'} <> J.source(value, False{}, J.source(J.Obj{tail}, True{}, Nil{}))),
420        Equal.trans(List<&2, J.Lexeme>,
421            List.append(&2, J.Lexeme,
422                List.reverse(&2, J.Lexeme, J.Punctuation{':'} <> J.source(value, False{}, J.source(J.Obj{tail}, True{}, Nil{}))),
423                J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> Nil{}),
424            List.append(&2, J.Lexeme,
425                List.append(&2, J.Lexeme, reverse_source_task(J.Obj{tail}, RenderMembers{}),
426                    List.append(&2, J.Lexeme, reverse_source_task(value, RenderWhole{}), J.Punctuation{':'} <> Nil{})),
427                J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> Nil{}),
428            List.append(&2, J.Lexeme, reverse_source_task(J.Obj{tail}, RenderMembers{}),
429                List.append(&2, J.Lexeme, reverse_source_task(value, RenderWhole{}),
430                    J.Punctuation{':'} <> J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> Nil{})),
431            Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, xs =>
432                List.append(&2, J.Lexeme, xs, J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> Nil{}),
433                List.reverse(&2, J.Lexeme, J.Punctuation{':'} <> J.source(value, False{}, J.source(J.Obj{tail}, True{}, Nil{}))),
434                List.append(&2, J.Lexeme, reverse_source_task(J.Obj{tail}, RenderMembers{}),
435                    List.append(&2, J.Lexeme, reverse_source_task(value, RenderWhole{}), J.Punctuation{':'} <> Nil{})),
436                reverse_source_colon_value_tail(value, tail)),
437            Equal.trans(List<&2, J.Lexeme>,
438                List.append(&2, J.Lexeme,
439                    List.append(&2, J.Lexeme, reverse_source_task(J.Obj{tail}, RenderMembers{}),
440                        List.append(&2, J.Lexeme, reverse_source_task(value, RenderWhole{}), J.Punctuation{':'} <> Nil{})),
441                    J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> Nil{}),
442                List.append(&2, J.Lexeme, reverse_source_task(J.Obj{tail}, RenderMembers{}),
443                    List.append(&2, J.Lexeme,
444                        List.append(&2, J.Lexeme, reverse_source_task(value, RenderWhole{}), J.Punctuation{':'} <> Nil{}),
445                        J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> Nil{})),
446                List.append(&2, J.Lexeme, reverse_source_task(J.Obj{tail}, RenderMembers{}),
447                    List.append(&2, J.Lexeme, reverse_source_task(value, RenderWhole{}),
448                        J.Punctuation{':'} <> J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> Nil{})),
449                LP.append_assoc(J.Lexeme, reverse_source_task(J.Obj{tail}, RenderMembers{}),
450                    List.append(&2, J.Lexeme, reverse_source_task(value, RenderWhole{}), J.Punctuation{':'} <> Nil{}),
451                    J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> Nil{}),
452                Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, xs =>
453                    List.append(&2, J.Lexeme, reverse_source_task(J.Obj{tail}, RenderMembers{}), xs),
454                    List.append(&2, J.Lexeme,
455                        List.append(&2, J.Lexeme, reverse_source_task(value, RenderWhole{}), J.Punctuation{':'} <> Nil{}),
456                        J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> Nil{}),
457                    List.append(&2, J.Lexeme, reverse_source_task(value, RenderWhole{}),
458                        List.append(&2, J.Lexeme, J.Punctuation{':'} <> Nil{}, J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> Nil{})),
459                    LP.append_assoc(J.Lexeme, reverse_source_task(value, RenderWhole{}), J.Punctuation{':'} <> Nil{},
460                        J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> Nil{})))))