proof/JSON_RenderLexProof.bend
qasim-bend-kit@0.1.0.1 · 557 lines · 0 definitions
1# Lexer/renderer bridge. All recursion follows the JSON value structure.
2import Base
3import qasim-bend-kit@0.1.0.1/libs/JSON.bend as J
4import qasim-bend-kit@0.1.0.1/proof/JSON_SourceProof.bend as SP
5import qasim-bend-kit@0.1.0.1/proof/JSON_NumberLexProof.bend as Num
6import qasim-bend-kit@0.1.0.1/proof/JSON_PrimitiveProof.bend as P
7import qasim-bend-kit@0.1.0.1/proof/JSON_ListProof.bend as LP
8import qasim-bend-kit@0.1.0.1/proof/JSON_StringProof.bend as S
9import qasim-bend-kit@0.1.0.1/proof/JSON_LexWhitespaceProof.bend as W
10
11def reverse_concat(+xs: List<&2, J.Lexeme>,
12 +ys: List<&2, J.Lexeme>,
13 +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>}:
14 match xs:
15 case Nil{}: {==}
16 case h <> t: reverse_concat(t, ys, h <> acc)
17
18def push(value: J.Value, mode: SP.RenderMode, acc: List<&2, J.Lexeme>) -> List<&2, J.Lexeme>:
19 List.reverse.go(&2, J.Lexeme, SP.source_task(value, mode, Nil{}), acc)
20
21def push_append(+value: J.Value,
22 +mode: SP.RenderMode,
23 +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>}:
24 LP.reverse_go_append(J.Lexeme, SP.source_task(value, mode, Nil{}), Nil{}, acc)
25
26def push_source(+value: J.Value,
27 +members: Bool,
28 +suffix: List<&2, J.Lexeme>,
29 +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>}:
30 Equal.trans(List<&2, J.Lexeme>,
31 List.reverse.go(&2, J.Lexeme, J.source(value, members, suffix), acc),
32 List.reverse.go(&2, J.Lexeme, List.append(&2, J.Lexeme, J.source(value, members, Nil{}), suffix), acc),
33 List.reverse.go(&2, J.Lexeme, suffix, List.reverse.go(&2, J.Lexeme, J.source(value, members, Nil{}), acc)),
34 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>,
35 x => List.reverse.go(&2, J.Lexeme, x, acc),
36 J.source(value, members, suffix),
37 List.append(&2, J.Lexeme, J.source(value, members, Nil{}), suffix),
38 SP.source_append(value, members, Nil{}, suffix)),
39 reverse_concat(J.source(value, members, Nil{}), suffix, acc))
40
41type Container is Data:
42 ArrayKind{}
43 ObjectKind{}
44
45def opening(kind: Container) -> Char:
46 match kind:
47 case ArrayKind{}: '['
48 case ObjectKind{}: '{'
49
50def prefix_text(kind: Container, mode: SP.RenderMode, text: String) -> String:
51 match mode:
52 case SP.RenderWhole{}: SCon{opening(kind), text}
53 case SP.RenderMembers{}: SCon{',', text}
54 case SP.RenderAfterSeparator{}: text
55
56def prefix_acc(kind: Container, mode: SP.RenderMode, acc: List<&2, J.Lexeme>) -> List<&2, J.Lexeme>:
57 match mode:
58 case SP.RenderWhole{}: J.Punctuation{opening(kind)} <> acc
59 case SP.RenderMembers{}: J.Punctuation{','} <> acc
60 case SP.RenderAfterSeparator{}: acc
61
62def scan_prefix(+kind: Container,
63 +mode: SP.RenderMode,
64 +text: String,
65 +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>}:
66 match kind mode:
67 case ArrayKind{} SP.RenderWhole{}: W.scan_punctuation_char('[', text, SNil{}, acc, {==})
68 case ObjectKind{} SP.RenderWhole{}: W.scan_punctuation_char('{', text, SNil{}, acc, {==})
69 case _ SP.RenderMembers{}: W.scan_punctuation_char(',', text, SNil{}, acc, {==})
70 case _ SP.RenderAfterSeparator{}: {==}
71
72def push_array(+head: J.Value,
73 +tail: List<&2, J.Value>,
74 +mode: SP.RenderMode,
75 +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>}:
76 match mode:
77 case SP.RenderWhole{}: push_source(head, False{}, J.source(J.Arr{tail}, True{}, Nil{}), prefix_acc(ArrayKind{}, SP.RenderWhole{}, acc))
78 case SP.RenderMembers{}: push_source(head, False{}, J.source(J.Arr{tail}, True{}, Nil{}), prefix_acc(ArrayKind{}, SP.RenderMembers{}, acc))
79 case SP.RenderAfterSeparator{}: push_source(head, False{}, J.source(J.Arr{tail}, True{}, Nil{}), prefix_acc(ArrayKind{}, SP.RenderAfterSeparator{}, acc))
80
81def push_object(+key: String,
82 +head: J.Value,
83 +tail: List<&2, Sigma<&2, &2, String, k => J.Value>>, +mode: SP.RenderMode, +acc: List<&2,
84 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>}:
85 match mode:
86 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))
87 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))
88 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))
89
90def number_tail_acc(+text: String,
91 +state: J.NumberState,
92 +rev_head: Char,
93 +rev_tail: String,
94 +first: Char,
95 +prefix_tail: String,
96 +acc: List<&2, J.Lexeme>,
97 +reverse_prefix: {String.reverse(SCon{rev_head, rev_tail}) == SCon{first, prefix_tail} : String},
98 +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>}:
99 match text:
100 case SNil{}:
101 Equal.trans(List<&2, J.Lexeme>,
102 J.lex_scan(SNil{}, J.Outside{}, SCon{rev_head, rev_tail}, acc),
103 List.reverse(&2, J.Lexeme, J.Payload{String.reverse(SCon{rev_head, rev_tail})} <> acc),
104 List.reverse(&2, J.Lexeme, J.Payload{SCon{first, prefix_tail} ++ SNil{}} <> acc),
105 {==},
106 Equal.trans(List<&2, J.Lexeme>,
107 List.reverse(&2, J.Lexeme, J.Payload{String.reverse(SCon{rev_head, rev_tail})} <> acc),
108 List.reverse(&2, J.Lexeme, J.Payload{SCon{first, prefix_tail}} <> acc),
109 List.reverse(&2, J.Lexeme, J.Payload{SCon{first, prefix_tail} ++ SNil{}} <> acc),
110 Equal.cong(String, List<&2, J.Lexeme>, s => List.reverse(&2, J.Lexeme, J.Payload{s} <> acc),
111 String.reverse(SCon{rev_head, rev_tail}), SCon{first, prefix_tail}, reverse_prefix),
112 Equal.cong(String, List<&2, J.Lexeme>, s => List.reverse(&2, J.Lexeme, J.Payload{s} <> acc),
113 SCon{first, prefix_tail}, SCon{first, prefix_tail} ++ SNil{},
114 Equal.sym(String, SCon{first, prefix_tail} ++ SNil{}, SCon{first, prefix_tail}, S.append_nil(SCon{first, prefix_tail})))))
115 case SCon{+head, +tail}:
116 Equal.trans(List<&2, J.Lexeme>,
117 J.lex_scan(text, J.Outside{}, SCon{rev_head, rev_tail}, acc),
118 J.lexemes(text, J.Outside{}, SCon{rev_head, rev_tail}, acc, J.LexRaw{}),
119 List.reverse(&2, J.Lexeme, J.Payload{SCon{first, prefix_tail} ++ text} <> acc),
120 Equal.cong(J.LexAction, List<&2, J.Lexeme>, action => J.lexemes(text, J.Outside{}, SCon{rev_head, rev_tail}, acc, action),
121 J.lex_seed_action(text, J.Outside{}), J.LexRaw{},
122 Num.number_char_action(head, J.number_char(head), {==}, tail, state, evidence)),
123 Equal.trans(List<&2, J.Lexeme>,
124 J.lexemes(text, J.Outside{}, SCon{rev_head, rev_tail}, acc, J.LexRaw{}),
125 J.lex_scan(tail, J.Outside{}, SCon{head, SCon{rev_head, rev_tail}}, acc),
126 List.reverse(&2, J.Lexeme, J.Payload{SCon{first, prefix_tail} ++ text} <> acc),
127 {==},
128 Equal.trans(List<&2, J.Lexeme>,
129 J.lex_scan(tail, J.Outside{}, SCon{head, SCon{rev_head, rev_tail}}, acc),
130 List.reverse(&2, J.Lexeme, J.Payload{(SCon{first, prefix_tail} ++ SCon{head, SNil{}}) ++ tail} <> acc),
131 List.reverse(&2, J.Lexeme, J.Payload{SCon{first, prefix_tail} ++ text} <> acc),
132 number_tail_acc(tail, J.number_next(state, head), head, SCon{rev_head, rev_tail}, first,
133 prefix_tail ++ SCon{head, SNil{}}, acc,
134 Equal.trans(String,
135 String.reverse(SCon{head, SCon{rev_head, rev_tail}}),
136 String.reverse(SCon{rev_head, rev_tail}) ++ SCon{head, SNil{}},
137 SCon{first, prefix_tail} ++ SCon{head, SNil{}},
138 S.reverse_cons(head, SCon{rev_head, rev_tail}),
139 Equal.cong(String, String, x => x ++ SCon{head, SNil{}},
140 String.reverse(SCon{rev_head, rev_tail}), SCon{first, prefix_tail}, reverse_prefix)),
141 Num.number_valid_cons(head, tail, state, evidence)),
142 Equal.cong(String, List<&2, J.Lexeme>, s => List.reverse(&2, J.Lexeme, J.Payload{s} <> acc),
143 (SCon{first, prefix_tail} ++ SCon{head, SNil{}}) ++ tail,
144 SCon{first, prefix_tail} ++ text,
145 S.append_assoc(SCon{first, prefix_tail}, SCon{head, SNil{}}, tail)))))
146
147def number_end(+text: String,
148 +acc: List<&2, J.Lexeme>,
149 +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>}:
150 match text:
151 case SNil{}:
152 Empty.absurd({J.lex_scan(SNil{}, J.Outside{}, SNil{}, acc) == (List.reverse(&2, J.Lexeme, J.Payload{SNil{}} <> acc)) : List<&2, J.Lexeme>},
153 Num.false_true(Equal.trans(Bool, False{}, J.number_valid(SNil{}), True{}, {==}, evidence)))
154 case SCon{+head, +tail}:
155 Equal.trans(List<&2, J.Lexeme>,
156 J.lex_scan(text, J.Outside{}, SNil{}, acc),
157 J.lexemes(text, J.Outside{}, SNil{}, acc, J.LexRaw{}),
158 List.reverse(&2, J.Lexeme, J.Payload{text} <> acc),
159 Equal.cong(J.LexAction, List<&2, J.Lexeme>, action => J.lexemes(text, J.Outside{}, SNil{}, acc, action),
160 J.lex_seed_action(text, J.Outside{}), J.LexRaw{},
161 Num.number_char_action(head, J.number_char(head), {==}, tail, J.NumberStart{}, evidence)),
162 Equal.trans(List<&2, J.Lexeme>,
163 J.lexemes(text, J.Outside{}, SNil{}, acc, J.LexRaw{}),
164 J.lex_scan(tail, J.Outside{}, SCon{head, SNil{}}, acc),
165 List.reverse(&2, J.Lexeme, J.Payload{text} <> acc),
166 {==},
167 Equal.trans(List<&2, J.Lexeme>,
168 J.lex_scan(tail, J.Outside{}, SCon{head, SNil{}}, acc),
169 List.reverse(&2, J.Lexeme, J.Payload{SCon{head, SNil{}} ++ tail} <> acc),
170 List.reverse(&2, J.Lexeme, J.Payload{text} <> acc),
171 number_tail_acc(tail, J.number_next(J.NumberStart{}, head), head, SNil{}, head, SNil{}, acc, {==},
172 Num.number_valid_cons(head, tail, J.NumberStart{}, evidence)),
173 Equal.cong(String, List<&2, J.Lexeme>, s => List.reverse(&2, J.Lexeme, J.Payload{s} <> acc),
174 SCon{head, SNil{}} ++ tail, text, {==}))))
175
176# A rendered value is followed either by end of input or a JSON delimiter.
177type Boundary is Data:
178 End{}
179 Delimited{mark: SP.JsonPunctuation, suffix: String}
180
181def boundary_text(boundary: Boundary) -> String:
182 match boundary:
183 case End{}: SNil{}
184 case Delimited{mark, suffix}: SCon{SP.punctuation_char(mark), suffix}
185
186def finish(boundary: Boundary, acc: List<&2, J.Lexeme>) -> List<&2, J.Lexeme>:
187 match boundary:
188 case End{}: J.lex_scan(SNil{}, J.Outside{}, SNil{}, acc)
189 case Delimited{mark, suffix}:
190 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{SP.punctuation_char(mark)} <> acc)
191
192def scan_boundary(+boundary: Boundary,
193 +acc: List<&2, J.Lexeme>) -> {J.lex_scan(boundary_text(boundary), J.Outside{}, SNil{}, acc) == finish(boundary, acc) : List<&2, J.Lexeme>}:
194 match boundary:
195 case End{}: {==}
196 case Delimited{mark, suffix}:
197 W.scan_punctuation_char(SP.punctuation_char(mark), suffix, SNil{}, acc, SP.punctuation_action(mark, suffix))
198
199def atomic_end(+atom: SP.AtomicValue,
200 +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>}:
201 match atom:
202 case SP.AtomicNull{}: {==}
203 case SP.AtomicTrue{}: {==}
204 case SP.AtomicFalse{}: {==}
205 case SP.AtomicNumber{text, certificate}:
206 Equal.trans(List<&2, J.Lexeme>,
207 J.lex_scan(J.render(J.Number{text, certificate}, False{}, SNil{}), J.Outside{}, SNil{}, acc),
208 J.lex_scan(text, J.Outside{}, SNil{}, acc),
209 finish(End{}, push(J.Number{text, certificate}, SP.RenderWhole{}, acc)),
210 Equal.cong(String, List<&2, J.Lexeme>,
211 x => J.lex_scan(x, J.Outside{}, SNil{}, acc),
212 text ++ SNil{},
213 text,
214 S.append_nil(text)),
215 number_end(text, acc, P.cert_valid(text, certificate)))
216 case SP.AtomicString{text}:
217 Equal.trans(List<&2, J.Lexeme>,
218 J.lex_scan(J.render(J.Str{text}, False{}, SNil{}), J.Outside{}, SNil{}, acc),
219 J.lex_scan(J.render(J.Str{text}, False{}, SNil{}) ++ SNil{}, J.Outside{}, SNil{}, acc),
220 finish(End{}, push(J.Str{text}, SP.RenderWhole{}, acc)),
221 Equal.cong(String, List<&2, J.Lexeme>,
222 x => J.lex_scan(x, J.Outside{}, SNil{}, acc),
223 J.render(J.Str{text}, False{}, SNil{}),
224 J.render(J.Str{text}, False{}, SNil{}) ++ SNil{},
225 Equal.sym(String,
226 J.render(J.Str{text}, False{}, SNil{}) ++ SNil{},
227 J.render(J.Str{text}, False{}, SNil{}),
228 S.append_nil(J.render(J.Str{text}, False{}, SNil{})))),
229 W.lex_rendered_string_suffix(text, SNil{}, acc))
230
231def atomic_mode_end(+atom: SP.AtomicValue,
232 +mode: SP.RenderMode,
233 +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>}:
234 match atom mode:
235 case SP.AtomicNull{} SP.RenderWhole{}: atomic_end(SP.AtomicNull{}, acc)
236 case SP.AtomicNull{} SP.RenderMembers{}: atomic_end(SP.AtomicNull{}, acc)
237 case SP.AtomicNull{} SP.RenderAfterSeparator{}: atomic_end(SP.AtomicNull{}, acc)
238 case SP.AtomicTrue{} SP.RenderWhole{}: atomic_end(SP.AtomicTrue{}, acc)
239 case SP.AtomicTrue{} SP.RenderMembers{}: atomic_end(SP.AtomicTrue{}, acc)
240 case SP.AtomicTrue{} SP.RenderAfterSeparator{}: atomic_end(SP.AtomicTrue{}, acc)
241 case SP.AtomicFalse{} SP.RenderWhole{}: atomic_end(SP.AtomicFalse{}, acc)
242 case SP.AtomicFalse{} SP.RenderMembers{}: atomic_end(SP.AtomicFalse{}, acc)
243 case SP.AtomicFalse{} SP.RenderAfterSeparator{}: atomic_end(SP.AtomicFalse{}, acc)
244 case SP.AtomicNumber{text, certificate} SP.RenderWhole{}: atomic_end(SP.AtomicNumber{text, certificate}, acc)
245 case SP.AtomicNumber{text, certificate} SP.RenderMembers{}: atomic_end(SP.AtomicNumber{text, certificate}, acc)
246 case SP.AtomicNumber{text, certificate} SP.RenderAfterSeparator{}: atomic_end(SP.AtomicNumber{text, certificate}, acc)
247 case SP.AtomicString{text} SP.RenderWhole{}: atomic_end(SP.AtomicString{text}, acc)
248 case SP.AtomicString{text} SP.RenderMembers{}: atomic_end(SP.AtomicString{text}, acc)
249 case SP.AtomicString{text} SP.RenderAfterSeparator{}: atomic_end(SP.AtomicString{text}, acc)
250
251def atomic_lex(+atom: SP.AtomicValue,
252 +mode: SP.RenderMode,
253 +boundary: Boundary,
254 +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>}:
255 match boundary:
256 case End{}: atomic_mode_end(atom, mode, acc)
257 case Delimited{mark, suffix}:
258 Equal.trans(List<&2, J.Lexeme>,
259 J.lex_scan(SP.render_task(SP.atomic_value(atom), mode, boundary_text(Delimited{mark, suffix})), J.Outside{}, SNil{}, acc),
260 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)),
261 finish(Delimited{mark, suffix}, push(SP.atomic_value(atom), mode, acc)),
262 SP.lex_simple_task_suffix_before_punctuation(SP.SimpleAtom{atom}, mode, SP.punctuation_char(mark), suffix, acc, SP.punctuation_action(mark, suffix)),
263 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>,
264 x => finish(Delimited{mark, suffix}, x),
265 List.append(&2, J.Lexeme, SP.reverse_source_task(SP.atomic_value(atom), mode), acc),
266 push(SP.atomic_value(atom), mode, acc),
267 Equal.sym(List<&2, J.Lexeme>,
268 push(SP.atomic_value(atom), mode, acc),
269 List.append(&2, J.Lexeme, SP.reverse_source_task(SP.atomic_value(atom), mode), acc),
270 push_append(SP.atomic_value(atom), mode, acc))))
271
272def array_continuation(values: List<&2, J.Value>, boundary: Boundary) -> Boundary:
273 match values:
274 case Nil{}: Delimited{SP.ArrayEnd{}, boundary_text(boundary)}
275 case head <> tail:
276 Delimited{SP.MemberComma{}, SP.render_task(J.Arr{values}, SP.RenderAfterSeparator{}, boundary_text(boundary))}
277
278def array_continuation_text(+values: List<&2, J.Value>,
279 +boundary: Boundary) -> {SP.render_task(J.Arr{values}, SP.RenderMembers{}, boundary_text(boundary)) == boundary_text(array_continuation(values, boundary)) : String}:
280 match values:
281 case Nil{}: {==}
282 case head <> tail: {==}
283
284def array_resume(+values: List<&2, J.Value>,
285 +boundary: Boundary,
286 +acc: List<&2, J.Lexeme>,
287 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>}:
288 match values:
289 case Nil{}: scan_boundary(boundary, J.Punctuation{']'} <> acc)
290 case head <> tail: tail_lex
291
292def object_continuation(values: List<&2, Sigma<&2, &2, String, k => J.Value>>, boundary: Boundary) -> Boundary:
293 match values:
294 case Nil{}: Delimited{SP.ObjectEnd{}, boundary_text(boundary)}
295 case (key, head) <> tail:
296 Delimited{SP.MemberComma{}, SP.render_task(J.Obj{values}, SP.RenderAfterSeparator{}, boundary_text(boundary))}
297
298def 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}:
299 match values:
300 case Nil{}: {==}
301 case (key, head) <> tail: {==}
302
303def object_resume(+values: List<&2, Sigma<&2, &2, String, k => J.Value>>, +boundary: Boundary, +acc: List<&2,
304 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>}:
305 match values:
306 case Nil{}: scan_boundary(boundary, J.Punctuation{'}'} <> acc)
307 case (key, head) <> tail: tail_lex
308
309def field_text(+key: String,
310 +text: String) -> {J.render_object_field(SNil{}, key, text) == ("\"" ++ J.escape_string(key) ++ "\"") ++ (":" ++ text) : String}:
311 Equal.trans(String,
312 J.render_object_field(SNil{}, key, text),
313 SCon{'"', J.escape_string(key) ++ ("\":" ++ text)},
314 ("\"" ++ J.escape_string(key) ++ "\"") ++ (":" ++ text),
315 Equal.cong(String, String,
316 x => SCon{'"', x},
317 (J.escape_string(key) ++ "\":") ++ text,
318 J.escape_string(key) ++ ("\":" ++ text),
319 S.append_assoc(J.escape_string(key), "\":", text)),
320 Equal.sym(String,
321 ("\"" ++ J.escape_string(key) ++ "\"") ++ (":" ++ text),
322 SCon{'"', J.escape_string(key) ++ ("\":" ++ text)},
323 Equal.cong(String, String,
324 x => SCon{'"', x},
325 (J.escape_string(key) ++ "\"") ++ (":" ++ text),
326 J.escape_string(key) ++ ("\"" ++ (":" ++ text)),
327 S.append_assoc(J.escape_string(key), "\"", ":" ++ text))))
328
329def scan_field(+key: String,
330 +text: String,
331 +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>}:
332 Equal.trans(List<&2, J.Lexeme>,
333 J.lex_scan(J.render_object_field(SNil{}, key, text), J.Outside{}, SNil{}, acc),
334 J.lex_scan(("\"" ++ J.escape_string(key) ++ "\"") ++ (":" ++ text), J.Outside{}, SNil{}, acc),
335 J.lex_scan(text, J.Outside{}, SNil{}, J.Punctuation{':'} <> J.Payload{("\"" ++ J.escape_string(key) ++ "\"")} <> acc),
336 Equal.cong(String, List<&2, J.Lexeme>,
337 x => J.lex_scan(x, J.Outside{}, SNil{}, acc),
338 J.render_object_field(SNil{}, key, text),
339 ("\"" ++ J.escape_string(key) ++ "\"") ++ (":" ++ text),
340 field_text(key, text)),
341 SP.lex_object_key_before_colon(key, text, acc))
342
343def empty_array_end(+mode: SP.RenderMode,
344 +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>}:
345 match mode:
346 case SP.RenderWhole{}: {==}
347 case SP.RenderMembers{}: {==}
348 case SP.RenderAfterSeparator{}: {==}
349
350def empty_array_lex(+mode: SP.RenderMode,
351 +boundary: Boundary,
352 +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>}:
353 match boundary:
354 case End{}: empty_array_end(mode, acc)
355 case Delimited{mark, suffix}:
356 Equal.trans(List<&2, J.Lexeme>,
357 J.lex_scan(SP.render_task(J.Arr{Nil{}}, mode, boundary_text(Delimited{mark, suffix})), J.Outside{}, SNil{}, acc),
358 finish(Delimited{mark, suffix}, List.append(&2, J.Lexeme, SP.reverse_source_task(J.Arr{Nil{}}, mode), acc)),
359 finish(Delimited{mark, suffix}, push(J.Arr{Nil{}}, mode, acc)),
360 SP.lex_simple_task_suffix_before_punctuation(SP.SimpleEmptyArray{}, mode, SP.punctuation_char(mark), suffix, acc, SP.punctuation_action(mark, suffix)),
361 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>,
362 x => finish(Delimited{mark, suffix}, x),
363 List.append(&2, J.Lexeme, SP.reverse_source_task(J.Arr{Nil{}}, mode), acc),
364 push(J.Arr{Nil{}}, mode, acc),
365 Equal.sym(List<&2, J.Lexeme>,
366 push(J.Arr{Nil{}}, mode, acc),
367 List.append(&2, J.Lexeme, SP.reverse_source_task(J.Arr{Nil{}}, mode), acc),
368 push_append(J.Arr{Nil{}}, mode, acc))))
369
370def empty_object_end(+mode: SP.RenderMode,
371 +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>}:
372 match mode:
373 case SP.RenderWhole{}: {==}
374 case SP.RenderMembers{}: {==}
375 case SP.RenderAfterSeparator{}: {==}
376
377def empty_object_lex(+mode: SP.RenderMode,
378 +boundary: Boundary,
379 +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>}:
380 match boundary:
381 case End{}: empty_object_end(mode, acc)
382 case Delimited{mark, suffix}:
383 Equal.trans(List<&2, J.Lexeme>,
384 J.lex_scan(SP.render_task(J.Obj{Nil{}}, mode, boundary_text(Delimited{mark, suffix})), J.Outside{}, SNil{}, acc),
385 finish(Delimited{mark, suffix}, List.append(&2, J.Lexeme, SP.reverse_source_task(J.Obj{Nil{}}, mode), acc)),
386 finish(Delimited{mark, suffix}, push(J.Obj{Nil{}}, mode, acc)),
387 SP.lex_simple_task_suffix_before_punctuation(SP.SimpleEmptyObject{}, mode, SP.punctuation_char(mark), suffix, acc, SP.punctuation_action(mark, suffix)),
388 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>,
389 x => finish(Delimited{mark, suffix}, x),
390 List.append(&2, J.Lexeme, SP.reverse_source_task(J.Obj{Nil{}}, mode), acc),
391 push(J.Obj{Nil{}}, mode, acc),
392 Equal.sym(List<&2, J.Lexeme>,
393 push(J.Obj{Nil{}}, mode, acc),
394 List.append(&2, J.Lexeme, SP.reverse_source_task(J.Obj{Nil{}}, mode), acc),
395 push_append(J.Obj{Nil{}}, mode, acc))))
396
397def render_array(+head: J.Value,
398 +tail: List<&2, J.Value>,
399 +mode: SP.RenderMode,
400 +boundary: Boundary,
401 +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}:
402 match mode:
403 case SP.RenderWhole{}:
404 Equal.cong(String, String,
405 x => prefix_text(ArrayKind{}, SP.RenderWhole{}, SP.render_task(head, SP.RenderWhole{}, x)),
406 SP.render_task(J.Arr{tail}, SP.RenderMembers{}, boundary_text(boundary)),
407 boundary_text(array_continuation(tail, boundary)),
408 array_continuation_text(tail, boundary))
409 case SP.RenderMembers{}:
410 Equal.cong(String, String,
411 x => prefix_text(ArrayKind{}, SP.RenderMembers{}, SP.render_task(head, SP.RenderWhole{}, x)),
412 SP.render_task(J.Arr{tail}, SP.RenderMembers{}, boundary_text(boundary)),
413 boundary_text(array_continuation(tail, boundary)),
414 array_continuation_text(tail, boundary))
415 case SP.RenderAfterSeparator{}:
416 Equal.cong(String, String,
417 x => prefix_text(ArrayKind{}, SP.RenderAfterSeparator{}, SP.render_task(head, SP.RenderWhole{}, x)),
418 SP.render_task(J.Arr{tail}, SP.RenderMembers{}, boundary_text(boundary)),
419 boundary_text(array_continuation(tail, boundary)),
420 array_continuation_text(tail, boundary))
421
422def lex_array(+head: J.Value,
423 +tail: List<&2, J.Value>,
424 +mode: SP.RenderMode,
425 +boundary: Boundary,
426 +acc: List<&2, J.Lexeme>,
427 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>},
428 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>}:
429 Equal.trans(List<&2, J.Lexeme>,
430 J.lex_scan(SP.render_task(J.Arr{head <> tail}, mode, boundary_text(boundary)), J.Outside{}, SNil{}, acc),
431 J.lex_scan(prefix_text(ArrayKind{}, mode, SP.render_task(head, SP.RenderWhole{}, boundary_text(array_continuation(tail, boundary)))), J.Outside{}, SNil{}, acc),
432 finish(boundary, push(J.Arr{head <> tail}, mode, acc)),
433 Equal.cong(String, List<&2, J.Lexeme>,
434 x => J.lex_scan(x, J.Outside{}, SNil{}, acc),
435 SP.render_task(J.Arr{head <> tail}, mode, boundary_text(boundary)),
436 prefix_text(ArrayKind{}, mode, SP.render_task(head, SP.RenderWhole{}, boundary_text(array_continuation(tail, boundary)))),
437 render_array(head, tail, mode, boundary, acc)),
438 Equal.trans(List<&2, J.Lexeme>,
439 J.lex_scan(prefix_text(ArrayKind{}, mode, SP.render_task(head, SP.RenderWhole{}, boundary_text(array_continuation(tail, boundary)))), J.Outside{}, SNil{}, acc),
440 J.lex_scan(SP.render_task(head, SP.RenderWhole{}, boundary_text(array_continuation(tail, boundary))), J.Outside{}, SNil{}, prefix_acc(ArrayKind{}, mode, acc)),
441 finish(boundary, push(J.Arr{head <> tail}, mode, acc)),
442 scan_prefix(ArrayKind{}, mode, SP.render_task(head, SP.RenderWhole{}, boundary_text(array_continuation(tail, boundary))), acc),
443 Equal.trans(List<&2, J.Lexeme>,
444 J.lex_scan(SP.render_task(head, SP.RenderWhole{}, boundary_text(array_continuation(tail, boundary))), J.Outside{}, SNil{}, prefix_acc(ArrayKind{}, mode, acc)),
445 finish(array_continuation(tail, boundary), push(head, SP.RenderWhole{}, prefix_acc(ArrayKind{}, mode, acc))),
446 finish(boundary, push(J.Arr{head <> tail}, mode, acc)),
447 head_lex,
448 Equal.trans(List<&2, J.Lexeme>,
449 finish(array_continuation(tail, boundary), push(head, SP.RenderWhole{}, prefix_acc(ArrayKind{}, mode, acc))),
450 finish(boundary, push(J.Arr{tail}, SP.RenderMembers{}, push(head, SP.RenderWhole{}, prefix_acc(ArrayKind{}, mode, acc)))),
451 finish(boundary, push(J.Arr{head <> tail}, mode, acc)),
452 array_resume(tail, boundary, push(head, SP.RenderWhole{}, prefix_acc(ArrayKind{}, mode, acc)), tail_lex),
453 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>,
454 x => finish(boundary, x),
455 push(J.Arr{tail}, SP.RenderMembers{}, push(head, SP.RenderWhole{}, prefix_acc(ArrayKind{}, mode, acc))),
456 push(J.Arr{head <> tail}, mode, acc),
457 Equal.sym(List<&2, J.Lexeme>,
458 push(J.Arr{head <> tail}, mode, acc),
459 push(J.Arr{tail}, SP.RenderMembers{}, push(head, SP.RenderWhole{}, prefix_acc(ArrayKind{}, mode, acc))),
460 push_array(head, tail, mode, acc)))))))
461
462def render_object(+key: String,
463 +head: J.Value,
464 +tail: List<&2, Sigma<&2, &2, String, k => J.Value>>, +mode: SP.RenderMode, +boundary: Boundary, +acc: List<&2,
465 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}:
466 match mode:
467 case SP.RenderWhole{}:
468 Equal.cong(String, String,
469 x => prefix_text(ObjectKind{}, SP.RenderWhole{}, J.render_object_field(SNil{}, key, SP.render_task(head, SP.RenderWhole{}, x))),
470 SP.render_task(J.Obj{tail}, SP.RenderMembers{}, boundary_text(boundary)),
471 boundary_text(object_continuation(tail, boundary)),
472 object_continuation_text(tail, boundary))
473 case SP.RenderMembers{}:
474 Equal.cong(String, String,
475 x => prefix_text(ObjectKind{}, SP.RenderMembers{}, J.render_object_field(SNil{}, key, SP.render_task(head, SP.RenderWhole{}, x))),
476 SP.render_task(J.Obj{tail}, SP.RenderMembers{}, boundary_text(boundary)),
477 boundary_text(object_continuation(tail, boundary)),
478 object_continuation_text(tail, boundary))
479 case SP.RenderAfterSeparator{}:
480 Equal.cong(String, String,
481 x => prefix_text(ObjectKind{}, SP.RenderAfterSeparator{}, J.render_object_field(SNil{}, key, SP.render_task(head, SP.RenderWhole{}, x))),
482 SP.render_task(J.Obj{tail}, SP.RenderMembers{}, boundary_text(boundary)),
483 boundary_text(object_continuation(tail, boundary)),
484 object_continuation_text(tail, boundary))
485
486def lex_object(+key: String,
487 +head: J.Value,
488 +tail: List<&2, Sigma<&2, &2, String, k => J.Value>>, +mode: SP.RenderMode, +boundary: Boundary, +acc: List<&2,
489 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>}:
490 Equal.trans(List<&2, J.Lexeme>,
491 J.lex_scan(SP.render_task(J.Obj{(key, head) <> tail}, mode, boundary_text(boundary)), J.Outside{}, SNil{}, acc),
492 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),
493 finish(boundary, push(J.Obj{(key, head) <> tail}, mode, acc)),
494 Equal.cong(String, List<&2, J.Lexeme>,
495 x => J.lex_scan(x, J.Outside{}, SNil{}, acc),
496 SP.render_task(J.Obj{(key, head) <> tail}, mode, boundary_text(boundary)),
497 prefix_text(ObjectKind{}, mode, J.render_object_field(SNil{}, key, SP.render_task(head, SP.RenderWhole{}, boundary_text(object_continuation(tail, boundary))))),
498 render_object(key, head, tail, mode, boundary, acc)),
499 Equal.trans(List<&2, J.Lexeme>,
500 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),
501 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)),
502 finish(boundary, push(J.Obj{(key, head) <> tail}, mode, acc)),
503 scan_prefix(ObjectKind{}, mode, J.render_object_field(SNil{}, key, SP.render_task(head, SP.RenderWhole{}, boundary_text(object_continuation(tail, boundary)))), acc),
504 Equal.trans(List<&2, J.Lexeme>,
505 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)),
506 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)),
507 finish(boundary, push(J.Obj{(key, head) <> tail}, mode, acc)),
508 scan_field(key, SP.render_task(head, SP.RenderWhole{}, boundary_text(object_continuation(tail, boundary))), prefix_acc(ObjectKind{}, mode, acc)),
509 Equal.trans(List<&2, J.Lexeme>,
510 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)),
511 finish(object_continuation(tail, boundary), push(head, SP.RenderWhole{}, J.Punctuation{':'} <> J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> prefix_acc(ObjectKind{}, mode, acc))),
512 finish(boundary, push(J.Obj{(key, head) <> tail}, mode, acc)),
513 head_lex,
514 Equal.trans(List<&2, J.Lexeme>,
515 finish(object_continuation(tail, boundary), push(head, SP.RenderWhole{}, J.Punctuation{':'} <> J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> prefix_acc(ObjectKind{}, mode, acc))),
516 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)))),
517 finish(boundary, push(J.Obj{(key, head) <> tail}, mode, acc)),
518 object_resume(tail, boundary, push(head, SP.RenderWhole{}, J.Punctuation{':'} <> J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> prefix_acc(ObjectKind{}, mode, acc)), tail_lex),
519 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>,
520 x => finish(boundary, x),
521 push(J.Obj{tail}, SP.RenderMembers{}, push(head, SP.RenderWhole{}, J.Punctuation{':'} <> J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> prefix_acc(ObjectKind{}, mode, acc))),
522 push(J.Obj{(key, head) <> tail}, mode, acc),
523 Equal.sym(List<&2, J.Lexeme>,
524 push(J.Obj{(key, head) <> tail}, mode, acc),
525 push(J.Obj{tail}, SP.RenderMembers{}, push(head, SP.RenderWhole{}, J.Punctuation{':'} <> J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> prefix_acc(ObjectKind{}, mode, acc))),
526 push_object(key, head, tail, mode, acc))))))))
527
528def lex_value(+value: J.Value,
529 +mode: SP.RenderMode,
530 +boundary: Boundary,
531 +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>}:
532 match value:
533 case J.Null{}: atomic_lex(SP.AtomicNull{}, mode, boundary, acc)
534 case J.Bool{truth}:
535 match truth:
536 case True{}: atomic_lex(SP.AtomicTrue{}, mode, boundary, acc)
537 case False{}: atomic_lex(SP.AtomicFalse{}, mode, boundary, acc)
538 case J.Number{text, certificate}: atomic_lex(SP.AtomicNumber{text, certificate}, mode, boundary, acc)
539 case J.Str{text}: atomic_lex(SP.AtomicString{text}, mode, boundary, acc)
540 case J.Arr{Nil{}}: empty_array_lex(mode, boundary, acc)
541 case J.Obj{Nil{}}: empty_object_lex(mode, boundary, acc)
542 case J.Arr{head <> tail}:
543 lex_array(head, tail, mode, boundary, acc,
544 lex_value(head, SP.RenderWhole{}, array_continuation(tail, boundary), prefix_acc(ArrayKind{}, mode, acc)),
545 lex_value(J.Arr{tail}, SP.RenderAfterSeparator{}, boundary, J.Punctuation{','} <> push(head, SP.RenderWhole{}, prefix_acc(ArrayKind{}, mode, acc))))
546 case J.Obj{(key, head) <> tail}:
547 lex_object(key, head, tail, mode, boundary, acc,
548 lex_value(head, SP.RenderWhole{}, object_continuation(tail, boundary), J.Punctuation{':'} <> J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> prefix_acc(ObjectKind{}, mode, acc)),
549 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))))
550
551def lex_source(+value: J.Value) -> {J.lex_scan(J.stringify(value), J.Outside{}, SNil{}, Nil{}) == J.source(value, False{}, Nil{}) : List<&2, J.Lexeme>}:
552 Equal.trans(List<&2, J.Lexeme>,
553 J.lex_scan(J.stringify(value), J.Outside{}, SNil{}, Nil{}),
554 finish(End{}, push(value, SP.RenderWhole{}, Nil{})),
555 J.source(value, False{}, Nil{}),
556 lex_value(value, SP.RenderWhole{}, End{}, Nil{}),
557 LP.reverse_twice(J.Lexeme, J.source(value, False{}, Nil{})))