def reverse_source_array_members

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

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

505def reverse_source_array_members(+head: J.Value,
506                                 +tail: List<&2, J.Value>) -> {reverse_source_task(J.Arr{head <> tail}, RenderMembers{}) == List.append(&2, J.Lexeme, reverse_source_task(J.Arr{tail}, RenderMembers{}), List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), J.Punctuation{','} <> Nil{})) : List<&2, J.Lexeme>}:
507    Equal.trans(List<&2, J.Lexeme>,
508        reverse_source_task(J.Arr{head <> tail}, RenderMembers{}),
509        List.reverse(&2, J.Lexeme, List.append(&2, J.Lexeme,
510            J.Punctuation{','} <> J.source(head, False{}, Nil{}), J.source(J.Arr{tail}, True{}, Nil{}))),
511        List.append(&2, J.Lexeme, reverse_source_task(J.Arr{tail}, RenderMembers{}),
512            List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), J.Punctuation{','} <> Nil{})),
513        Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, items => List.reverse(&2, J.Lexeme, items),
514            J.source(J.Arr{head <> tail}, True{}, Nil{}),
515            List.append(&2, J.Lexeme, J.Punctuation{','} <> J.source(head, False{}, Nil{}), J.source(J.Arr{tail}, True{}, Nil{})),
516            Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, items => J.Punctuation{','} <> items,
517                J.source(head, False{}, J.source(J.Arr{tail}, True{}, Nil{})),
518                List.append(&2, J.Lexeme, J.source(head, False{}, Nil{}), J.source(J.Arr{tail}, True{}, Nil{})),
519                source_append(head, False{}, Nil{}, J.source(J.Arr{tail}, True{}, Nil{})))),
520        Equal.trans(List<&2, J.Lexeme>,
521            List.reverse(&2, J.Lexeme, List.append(&2, J.Lexeme,
522                J.Punctuation{','} <> J.source(head, False{}, Nil{}), J.source(J.Arr{tail}, True{}, Nil{}))),
523            List.append(&2, J.Lexeme,
524                List.reverse(&2, J.Lexeme, J.source(J.Arr{tail}, True{}, Nil{})),
525                List.reverse(&2, J.Lexeme, J.Punctuation{','} <> J.source(head, False{}, Nil{}))),
526            List.append(&2, J.Lexeme, reverse_source_task(J.Arr{tail}, RenderMembers{}),
527                List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), J.Punctuation{','} <> Nil{})),
528            LP.reverse_append(J.Lexeme, J.Punctuation{','} <> J.source(head, False{}, Nil{}), J.source(J.Arr{tail}, True{}, Nil{})),
529            Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, items => List.append(&2, J.Lexeme, reverse_source_task(J.Arr{tail}, RenderMembers{}), items),
530                List.reverse(&2, J.Lexeme, J.Punctuation{','} <> J.source(head, False{}, Nil{})),
531                List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), J.Punctuation{','} <> Nil{}),
532                LP.reverse_cons(J.Lexeme, J.Punctuation{','}, J.source(head, False{}, Nil{})))))