def escape_reverse_shape

qasim-bend-kit@0.1.0.2 · proof/JSON_LexWhitespaceProof.bend:271

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_StringProof.bend as S

271def escape_reverse_shape(+text: String,
272                         +reversed: String) -> {String.reverse(escape_reverse(text, reversed)) == String.reverse(reversed) ++ J.escape_string(text) : String}:
273    match text:
274        case SNil{}: Equal.sym(String, String.reverse(reversed) ++ J.escape_string(SNil{}), String.reverse(reversed), S.append_nil(String.reverse(reversed)))
275        case SCon{head, tail}:
276            Equal.trans(String,
277                String.reverse(escape_reverse(tail, String.reverse(J.escape_char(head)) ++ reversed)),
278                String.reverse(String.reverse(J.escape_char(head)) ++ reversed) ++ J.escape_string(tail),
279                String.reverse(reversed) ++ J.escape_string(SCon{head, tail}),
280                escape_reverse_shape(tail, String.reverse(J.escape_char(head)) ++ reversed),
281                Equal.trans(String,
282                    String.reverse(String.reverse(J.escape_char(head)) ++ reversed) ++ J.escape_string(tail),
283                    (String.reverse(reversed) ++ String.reverse(String.reverse(J.escape_char(head)))) ++ J.escape_string(tail),
284                    String.reverse(reversed) ++ (J.escape_char(head) ++ J.escape_string(tail)),
285                    Equal.cong(String, String, value => value ++ J.escape_string(tail),
286                        String.reverse(String.reverse(J.escape_char(head)) ++ reversed),
287                        String.reverse(reversed) ++ String.reverse(String.reverse(J.escape_char(head))),
288                        S.reverse_append(String.reverse(J.escape_char(head)), reversed)),
289                    Equal.trans(String,
290                        (String.reverse(reversed) ++ String.reverse(String.reverse(J.escape_char(head)))) ++ J.escape_string(tail),
291                        String.reverse(reversed) ++ (String.reverse(String.reverse(J.escape_char(head))) ++ J.escape_string(tail)),
292                        String.reverse(reversed) ++ (J.escape_char(head) ++ J.escape_string(tail)),
293                        S.append_assoc(String.reverse(reversed), String.reverse(String.reverse(J.escape_char(head))), J.escape_string(tail)),
294                        Equal.cong(String, String, value => String.reverse(reversed) ++ (value ++ J.escape_string(tail)),
295                            String.reverse(String.reverse(J.escape_char(head))), J.escape_char(head), S.reverse_twice(J.escape_char(head))))))