def source_append
qasim-bend-kit@0.1.0.2 · proof/JSON_SourceProof.bend:279
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
279def source_append(+value: J.Value,
280 +members: Bool,
281 +first: List<&2, J.Lexeme>,
282 +second: List<&2, J.Lexeme>) -> {J.source(value, members, List.append(&2, J.Lexeme, first, second)) == List.append(&2, J.Lexeme, J.source(value, members, first), second) : List<&2, J.Lexeme>}:
283 match value:
284 case J.Null{}: source_text_append("null", first, second)
285 case J.Bool{truth}:
286 match truth:
287 case True{}: source_text_append("true", first, second)
288 case False{}: source_text_append("false", first, second)
289 case J.Number{lexeme, certificate}: source_text_append(lexeme, first, second)
290 case J.Str{text}: source_text_append("\"" ++ J.escape_string(text) ++ "\"", first, second)
291 case J.Arr{Nil{}}:
292 match members:
293 case False{}: {==}
294 case True{}: {==}
295 case J.Arr{head <> tail}:
296 match members:
297 case False{}:
298 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, xs => J.Punctuation{'['} <> xs,
299 J.source(head, False{}, J.source(J.Arr{tail}, True{}, List.append(&2, J.Lexeme, first, second))),
300 List.append(&2, J.Lexeme, J.source(head, False{}, J.source(J.Arr{tail}, True{}, first)), second),
301 Equal.trans(List<&2, J.Lexeme>,
302 J.source(head, False{}, J.source(J.Arr{tail}, True{}, List.append(&2, J.Lexeme, first, second))),
303 J.source(head, False{}, List.append(&2, J.Lexeme, J.source(J.Arr{tail}, True{}, first), second)),
304 List.append(&2, J.Lexeme, J.source(head, False{}, J.source(J.Arr{tail}, True{}, first)), second),
305 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, xs => J.source(head, False{}, xs),
306 J.source(J.Arr{tail}, True{}, List.append(&2, J.Lexeme, first, second)),
307 List.append(&2, J.Lexeme, J.source(J.Arr{tail}, True{}, first), second),
308 source_append(J.Arr{tail}, True{}, first, second)),
309 source_append(head, False{}, J.source(J.Arr{tail}, True{}, first), second)))
310 case True{}:
311 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, xs => J.Punctuation{','} <> xs,
312 J.source(head, False{}, J.source(J.Arr{tail}, True{}, List.append(&2, J.Lexeme, first, second))),
313 List.append(&2, J.Lexeme, J.source(head, False{}, J.source(J.Arr{tail}, True{}, first)), second),
314 Equal.trans(List<&2, J.Lexeme>,
315 J.source(head, False{}, J.source(J.Arr{tail}, True{}, List.append(&2, J.Lexeme, first, second))),
316 J.source(head, False{}, List.append(&2, J.Lexeme, J.source(J.Arr{tail}, True{}, first), second)),
317 List.append(&2, J.Lexeme, J.source(head, False{}, J.source(J.Arr{tail}, True{}, first)), second),
318 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, xs => J.source(head, False{}, xs),
319 J.source(J.Arr{tail}, True{}, List.append(&2, J.Lexeme, first, second)),
320 List.append(&2, J.Lexeme, J.source(J.Arr{tail}, True{}, first), second),
321 source_append(J.Arr{tail}, True{}, first, second)),
322 source_append(head, False{}, J.source(J.Arr{tail}, True{}, first), second)))
323 case J.Obj{Nil{}}:
324 match members:
325 case False{}: {==}
326 case True{}: {==}
327 case J.Obj{(key, field_value) <> tail}:
328 match members:
329 case False{}:
330 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, xs => J.Punctuation{'{'} <> xs,
331 J.source_text("\"" ++ J.escape_string(key) ++ "\"", J.Punctuation{':'} <> J.source(field_value, False{}, J.source(J.Obj{tail}, True{}, List.append(&2, J.Lexeme, first, second)))),
332 List.append(&2, J.Lexeme, J.source_text("\"" ++ J.escape_string(key) ++ "\"", J.Punctuation{':'} <> J.source(field_value, False{}, J.source(J.Obj{tail}, True{}, first))), second),
333 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, xs => J.source_text("\"" ++ J.escape_string(key) ++ "\"", J.Punctuation{':'} <> xs),
334 J.source(field_value, False{}, J.source(J.Obj{tail}, True{}, List.append(&2, J.Lexeme, first, second))),
335 List.append(&2, J.Lexeme, J.source(field_value, False{}, J.source(J.Obj{tail}, True{}, first)), second),
336 Equal.trans(List<&2, J.Lexeme>,
337 J.source(field_value, False{}, J.source(J.Obj{tail}, True{}, List.append(&2, J.Lexeme, first, second))),
338 J.source(field_value, False{}, List.append(&2, J.Lexeme, J.source(J.Obj{tail}, True{}, first), second)),
339 List.append(&2, J.Lexeme, J.source(field_value, False{}, J.source(J.Obj{tail}, True{}, first)), second),
340 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, xs => J.source(field_value, False{}, xs),
341 J.source(J.Obj{tail}, True{}, List.append(&2, J.Lexeme, first, second)),
342 List.append(&2, J.Lexeme, J.source(J.Obj{tail}, True{}, first), second),
343 source_append(J.Obj{tail}, True{}, first, second)),
344 source_append(field_value, False{}, J.source(J.Obj{tail}, True{}, first), second))))
345 case True{}:
346 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, xs => J.Punctuation{','} <> xs,
347 J.source_text("\"" ++ J.escape_string(key) ++ "\"", J.Punctuation{':'} <> J.source(field_value, False{}, J.source(J.Obj{tail}, True{}, List.append(&2, J.Lexeme, first, second)))),
348 List.append(&2, J.Lexeme, J.source_text("\"" ++ J.escape_string(key) ++ "\"", J.Punctuation{':'} <> J.source(field_value, False{}, J.source(J.Obj{tail}, True{}, first))), second),
349 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, xs => J.source_text("\"" ++ J.escape_string(key) ++ "\"", J.Punctuation{':'} <> xs),
350 J.source(field_value, False{}, J.source(J.Obj{tail}, True{}, List.append(&2, J.Lexeme, first, second))),
351 List.append(&2, J.Lexeme, J.source(field_value, False{}, J.source(J.Obj{tail}, True{}, first)), second),
352 Equal.trans(List<&2, J.Lexeme>,
353 J.source(field_value, False{}, J.source(J.Obj{tail}, True{}, List.append(&2, J.Lexeme, first, second))),
354 J.source(field_value, False{}, List.append(&2, J.Lexeme, J.source(J.Obj{tail}, True{}, first), second)),
355 List.append(&2, J.Lexeme, J.source(field_value, False{}, J.source(J.Obj{tail}, True{}, first)), second),
356 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, xs => J.source(field_value, False{}, xs),
357 J.source(J.Obj{tail}, True{}, List.append(&2, J.Lexeme, first, second)),
358 List.append(&2, J.Lexeme, J.source(J.Obj{tail}, True{}, first), second),
359 source_append(J.Obj{tail}, True{}, first, second)),
360 source_append(field_value, False{}, J.source(J.Obj{tail}, True{}, first), second))))