def render_append
qasim-bend-kit@0.1.0.2 · proof/JSON_SourceProof.bend:56
import qasim-bend-kit@0.1.0.2/proof/JSON_SourceProof.bend as JSONSourceProof
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
56def render_append(+value: J.Value,
57 +members: Bool,
58 +prefix: String,
59 +suffix: String) -> {J.render(value, members, prefix) ++ suffix == J.render(value, members, prefix ++ suffix) : String}:
60 match value:
61 case J.Null{}: S.append_assoc("null", prefix, suffix)
62 case J.Bool{truth}:
63 match truth:
64 case True{}: S.append_assoc("true", prefix, suffix)
65 case False{}: S.append_assoc("false", prefix, suffix)
66 case J.Number{lexeme, certificate}: S.append_assoc(lexeme, prefix, suffix)
67 case J.Str{text}:
68 Equal.cong(String, String, rest => SCon{'"', rest},
69 (J.escape_string(text) ++ (SCon{'"', SNil{}} ++ prefix)) ++ suffix,
70 J.escape_string(text) ++ (SCon{'"', SNil{}} ++ (prefix ++ suffix)),
71 Equal.trans(String,
72 (J.escape_string(text) ++ (SCon{'"', SNil{}} ++ prefix)) ++ suffix,
73 J.escape_string(text) ++ ((SCon{'"', SNil{}} ++ prefix) ++ suffix),
74 J.escape_string(text) ++ (SCon{'"', SNil{}} ++ (prefix ++ suffix)),
75 S.append_assoc(J.escape_string(text), SCon{'"', SNil{}} ++ prefix, suffix),
76 Equal.cong(String, String, value => J.escape_string(text) ++ value,
77 (SCon{'"', SNil{}} ++ prefix) ++ suffix,
78 SCon{'"', SNil{}} ++ (prefix ++ suffix),
79 S.append_assoc(SCon{'"', SNil{}}, prefix, suffix))))
80 case J.Arr{Nil{}}:
81 match members:
82 case False{}: S.append_assoc("[]", prefix, suffix)
83 case True{}: S.append_assoc("]", prefix, suffix)
84 case J.Arr{head <> tail}:
85 match members:
86 case False{}:
87 Equal.trans(String, ("[" ++ J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix))) ++ suffix,
88 "[" ++ (J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix)) ++ suffix),
89 "[" ++ J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix ++ suffix)),
90 S.append_assoc("[", J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix)), suffix),
91 Equal.trans(String, "[" ++ (J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix)) ++ suffix),
92 "[" ++ J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix) ++ suffix),
93 "[" ++ J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix ++ suffix)),
94 Equal.cong(String, String, text => "[" ++ text,
95 J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix)) ++ suffix,
96 J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix) ++ suffix),
97 render_append(head, False{}, J.render(J.Arr{tail}, True{}, prefix), suffix)),
98 Equal.cong(String, String, text => "[" ++ J.render(head, False{}, text),
99 J.render(J.Arr{tail}, True{}, prefix) ++ suffix,
100 J.render(J.Arr{tail}, True{}, prefix ++ suffix),
101 render_append(J.Arr{tail}, True{}, prefix, suffix))))
102 case True{}:
103 Equal.trans(String, ("," ++ J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix))) ++ suffix,
104 "," ++ (J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix)) ++ suffix),
105 "," ++ J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix ++ suffix)),
106 S.append_assoc(",", J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix)), suffix),
107 Equal.trans(String, "," ++ (J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix)) ++ suffix),
108 "," ++ J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix) ++ suffix),
109 "," ++ J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix ++ suffix)),
110 Equal.cong(String, String, text => "," ++ text,
111 J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix)) ++ suffix,
112 J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix) ++ suffix),
113 render_append(head, False{}, J.render(J.Arr{tail}, True{}, prefix), suffix)),
114 Equal.cong(String, String, text => "," ++ J.render(head, False{}, text),
115 J.render(J.Arr{tail}, True{}, prefix) ++ suffix,
116 J.render(J.Arr{tail}, True{}, prefix ++ suffix),
117 render_append(J.Arr{tail}, True{}, prefix, suffix))))
118 case J.Obj{Nil{}}:
119 match members:
120 case False{}: S.append_assoc("{}", prefix, suffix)
121 case True{}: S.append_assoc("}", prefix, suffix)
122 case J.Obj{(key, field_value) <> tail}:
123 match members:
124 case False{}:
125 Equal.trans(String,
126 J.render_object_field("{", key, J.render(field_value, False{}, J.render(J.Obj{tail}, True{}, prefix))) ++ suffix,
127 J.render_object_field("{", key, J.render(field_value, False{}, J.render(J.Obj{tail}, True{}, prefix)) ++ suffix),
128 J.render_object_field("{", key, J.render(field_value, False{}, J.render(J.Obj{tail}, True{}, prefix ++ suffix))),
129 render_object_field_append("{", key, J.render(field_value, False{}, J.render(J.Obj{tail}, True{}, prefix)), suffix),
130 Equal.cong(String, String, text => J.render_object_field("{", key, text),
131 J.render(field_value, False{}, J.render(J.Obj{tail}, True{}, prefix)) ++ suffix,
132 J.render(field_value, False{}, J.render(J.Obj{tail}, True{}, prefix ++ suffix)),
133 nested_render_append(field_value, J.Obj{tail}, True{}, prefix, suffix,
134 render_append(field_value, False{}, J.render(J.Obj{tail}, True{}, prefix), suffix),
135 render_append(J.Obj{tail}, True{}, prefix, suffix))))
136 case True{}:
137 Equal.trans(String,
138 J.render_object_field(",", key, J.render(field_value, False{}, J.render(J.Obj{tail}, True{}, prefix))) ++ suffix,
139 J.render_object_field(",", key, J.render(field_value, False{}, J.render(J.Obj{tail}, True{}, prefix)) ++ suffix),
140 J.render_object_field(",", key, J.render(field_value, False{}, J.render(J.Obj{tail}, True{}, prefix ++ suffix))),
141 render_object_field_append(",", key, J.render(field_value, False{}, J.render(J.Obj{tail}, True{}, prefix)), suffix),
142 Equal.cong(String, String, text => J.render_object_field(",", key, text),
143 J.render(field_value, False{}, J.render(J.Obj{tail}, True{}, prefix)) ++ suffix,
144 J.render(field_value, False{}, J.render(J.Obj{tail}, True{}, prefix ++ suffix)),
145 nested_render_append(field_value, J.Obj{tail}, True{}, prefix, suffix,
146 render_append(field_value, False{}, J.render(J.Obj{tail}, True{}, prefix), suffix),
147 render_append(J.Obj{tail}, True{}, prefix, suffix))))