def source_tokens
qasim-bend-kit@0.1.0.2 · proof/JSON_SourceProof.bend:1434
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_AssemblyProof.bend as A
1434def source_tokens(+value: J.Value,
1435 +mode: A.Mode,
1436 +suffix: List<&2, J.Lexeme>,
1437 -tail: List<J.Token>) -> {token_source(J.source(value, to_bool(mode), suffix), tail) == canonical(value, mode, token_source(suffix, tail)) : List<J.Token>}:
1438 match value:
1439 case J.Null{}: {==}
1440 case J.Bool{truth}:
1441 match truth:
1442 case True{}: {==}
1443 case False{}: {==}
1444 case J.Number{lexeme, certificate}: {==}
1445 case J.Str{text}: {==}
1446 case J.Arr{values}:
1447 match values:
1448 case Nil{}:
1449 match mode:
1450 case A.Whole{}: {==}
1451 case A.Members{}: {==}
1452 case head <> rest:
1453 match mode:
1454 case A.Whole{}:
1455 Equal.trans(List<J.Token>, token_source(J.source(J.Arr{head <> rest}, False{}, suffix), tail),
1456 J.Delimiter{'['} <> canonical(head, A.Whole{}, token_source(J.source(J.Arr{rest}, True{}, suffix), tail)),
1457 canonical(J.Arr{head <> rest}, A.Whole{}, token_source(suffix, tail)),
1458 Equal.cong(List<J.Token>, List<J.Token>, xs => J.Delimiter{'['} <> xs,
1459 token_source(J.source(head, False{}, J.source(J.Arr{rest}, True{}, suffix)), tail),
1460 canonical(head, A.Whole{}, token_source(J.source(J.Arr{rest}, True{}, suffix), tail)),
1461 source_tokens(head, A.Whole{}, J.source(J.Arr{rest}, True{}, suffix), tail)),
1462 Equal.cong(List<J.Token>, List<J.Token>, xs => J.Delimiter{'['} <> canonical(head, A.Whole{}, xs),
1463 token_source(J.source(J.Arr{rest}, True{}, suffix), tail), canonical(J.Arr{rest}, A.Members{}, token_source(suffix, tail)),
1464 source_tokens(J.Arr{rest}, A.Members{}, suffix, tail)))
1465 case A.Members{}:
1466 Equal.trans(List<J.Token>, token_source(J.source(J.Arr{head <> rest}, True{}, suffix), tail),
1467 J.Delimiter{','} <> canonical(head, A.Whole{}, token_source(J.source(J.Arr{rest}, True{}, suffix), tail)),
1468 canonical(J.Arr{head <> rest}, A.Members{}, token_source(suffix, tail)),
1469 Equal.cong(List<J.Token>, List<J.Token>, xs => J.Delimiter{','} <> xs,
1470 token_source(J.source(head, False{}, J.source(J.Arr{rest}, True{}, suffix)), tail),
1471 canonical(head, A.Whole{}, token_source(J.source(J.Arr{rest}, True{}, suffix), tail)),
1472 source_tokens(head, A.Whole{}, J.source(J.Arr{rest}, True{}, suffix), tail)),
1473 Equal.cong(List<J.Token>, List<J.Token>, xs => J.Delimiter{','} <> canonical(head, A.Whole{}, xs),
1474 token_source(J.source(J.Arr{rest}, True{}, suffix), tail), canonical(J.Arr{rest}, A.Members{}, token_source(suffix, tail)),
1475 source_tokens(J.Arr{rest}, A.Members{}, suffix, tail)))
1476 case J.Obj{fields}:
1477 match fields:
1478 case Nil{}:
1479 match mode:
1480 case A.Whole{}: {==}
1481 case A.Members{}: {==}
1482 case (key, field_value) <> rest:
1483 match mode:
1484 case A.Whole{}:
1485 Equal.trans(List<J.Token>, token_source(J.source(J.Obj{(key, field_value) <> rest}, False{}, suffix), tail),
1486 J.Delimiter{'{'} <> token_string(key) <> J.Delimiter{':'} <> token_source(J.source(field_value, False{}, J.source(J.Obj{rest}, True{}, suffix)), tail),
1487 canonical(J.Obj{(key, field_value) <> rest}, A.Whole{}, token_source(suffix, tail)),
1488 source_object_key_prefix('{', key, J.Punctuation{':'} <> J.source(field_value, False{}, J.source(J.Obj{rest}, True{}, suffix)), tail),
1489 Equal.trans(List<J.Token>,
1490 J.Delimiter{'{'} <> token_string(key) <> J.Delimiter{':'} <> token_source(J.source(field_value, False{}, J.source(J.Obj{rest}, True{}, suffix)), tail),
1491 J.Delimiter{'{'} <> token_string(key) <> J.Delimiter{':'} <> canonical(field_value, A.Whole{}, token_source(J.source(J.Obj{rest}, True{}, suffix), tail)),
1492 canonical(J.Obj{(key, field_value) <> rest}, A.Whole{}, token_source(suffix, tail)),
1493 Equal.cong(List<J.Token>, List<J.Token>, xs => J.Delimiter{'{'} <> token_string(key) <> J.Delimiter{':'} <> xs,
1494 token_source(J.source(field_value, False{}, J.source(J.Obj{rest}, True{}, suffix)), tail),
1495 canonical(field_value, A.Whole{}, token_source(J.source(J.Obj{rest}, True{}, suffix), tail)),
1496 source_tokens(field_value, A.Whole{}, J.source(J.Obj{rest}, True{}, suffix), tail)),
1497 Equal.cong(List<J.Token>, List<J.Token>, xs => J.Delimiter{'{'} <> token_string(key) <> J.Delimiter{':'} <> canonical(field_value, A.Whole{}, xs),
1498 token_source(J.source(J.Obj{rest}, True{}, suffix), tail), canonical(J.Obj{rest}, A.Members{}, token_source(suffix, tail)),
1499 source_tokens(J.Obj{rest}, A.Members{}, suffix, tail))))
1500 case A.Members{}:
1501 Equal.trans(List<J.Token>, token_source(J.source(J.Obj{(key, field_value) <> rest}, True{}, suffix), tail),
1502 J.Delimiter{','} <> token_string(key) <> J.Delimiter{':'} <> token_source(J.source(field_value, False{}, J.source(J.Obj{rest}, True{}, suffix)), tail),
1503 canonical(J.Obj{(key, field_value) <> rest}, A.Members{}, token_source(suffix, tail)),
1504 source_object_key_prefix(',', key, J.Punctuation{':'} <> J.source(field_value, False{}, J.source(J.Obj{rest}, True{}, suffix)), tail),
1505 Equal.trans(List<J.Token>,
1506 J.Delimiter{','} <> token_string(key) <> J.Delimiter{':'} <> token_source(J.source(field_value, False{}, J.source(J.Obj{rest}, True{}, suffix)), tail),
1507 J.Delimiter{','} <> token_string(key) <> J.Delimiter{':'} <> canonical(field_value, A.Whole{}, token_source(J.source(J.Obj{rest}, True{}, suffix), tail)),
1508 canonical(J.Obj{(key, field_value) <> rest}, A.Members{}, token_source(suffix, tail)),
1509 Equal.cong(List<J.Token>, List<J.Token>, xs => J.Delimiter{','} <> token_string(key) <> J.Delimiter{':'} <> xs,
1510 token_source(J.source(field_value, False{}, J.source(J.Obj{rest}, True{}, suffix)), tail),
1511 canonical(field_value, A.Whole{}, token_source(J.source(J.Obj{rest}, True{}, suffix), tail)),
1512 source_tokens(field_value, A.Whole{}, J.source(J.Obj{rest}, True{}, suffix), tail)),
1513 Equal.cong(List<J.Token>, List<J.Token>, xs => J.Delimiter{','} <> token_string(key) <> J.Delimiter{':'} <> canonical(field_value, A.Whole{}, xs),
1514 token_source(J.source(J.Obj{rest}, True{}, suffix), tail), canonical(J.Obj{rest}, A.Members{}, token_source(suffix, tail)),
1515 source_tokens(J.Obj{rest}, A.Members{}, suffix, tail))))