JSONSourceProof.source_tokens: def of qasim-bend-kit@0.1.0.2 Import: import qasim-bend-kit@0.1.0.2/proof/JSON_SourceProof.bend as JSONSourceProof Lines 1434-1515 of qasim-bend-kit@0.1.0.2/proof/JSON_SourceProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_SourceProof.bend&start_line=1434&end_line=1515 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 def source_tokens(+value: J.Value, +mode: A.Mode, +suffix: List<&2, J.Lexeme>, -tail: List) -> {token_source(J.source(value, to_bool(mode), suffix), tail) == canonical(value, mode, token_source(suffix, tail)) : List}: match value: case J.Null{}: {==} case J.Bool{truth}: match truth: case True{}: {==} case False{}: {==} case J.Number{lexeme, certificate}: {==} case J.Str{text}: {==} case J.Arr{values}: match values: case Nil{}: match mode: case A.Whole{}: {==} case A.Members{}: {==} case head <> rest: match mode: case A.Whole{}: Equal.trans(List, token_source(J.source(J.Arr{head <> rest}, False{}, suffix), tail), J.Delimiter{'['} <> canonical(head, A.Whole{}, token_source(J.source(J.Arr{rest}, True{}, suffix), tail)), canonical(J.Arr{head <> rest}, A.Whole{}, token_source(suffix, tail)), Equal.cong(List, List, xs => J.Delimiter{'['} <> xs, token_source(J.source(head, False{}, J.source(J.Arr{rest}, True{}, suffix)), tail), canonical(head, A.Whole{}, token_source(J.source(J.Arr{rest}, True{}, suffix), tail)), source_tokens(head, A.Whole{}, J.source(J.Arr{rest}, True{}, suffix), tail)), Equal.cong(List, List, xs => J.Delimiter{'['} <> canonical(head, A.Whole{}, xs), token_source(J.source(J.Arr{rest}, True{}, suffix), tail), canonical(J.Arr{rest}, A.Members{}, token_source(suffix, tail)), source_tokens(J.Arr{rest}, A.Members{}, suffix, tail))) case A.Members{}: Equal.trans(List, token_source(J.source(J.Arr{head <> rest}, True{}, suffix), tail), J.Delimiter{','} <> canonical(head, A.Whole{}, token_source(J.source(J.Arr{rest}, True{}, suffix), tail)), canonical(J.Arr{head <> rest}, A.Members{}, token_source(suffix, tail)), Equal.cong(List, List, xs => J.Delimiter{','} <> xs, token_source(J.source(head, False{}, J.source(J.Arr{rest}, True{}, suffix)), tail), canonical(head, A.Whole{}, token_source(J.source(J.Arr{rest}, True{}, suffix), tail)), source_tokens(head, A.Whole{}, J.source(J.Arr{rest}, True{}, suffix), tail)), Equal.cong(List, List, xs => J.Delimiter{','} <> canonical(head, A.Whole{}, xs), token_source(J.source(J.Arr{rest}, True{}, suffix), tail), canonical(J.Arr{rest}, A.Members{}, token_source(suffix, tail)), source_tokens(J.Arr{rest}, A.Members{}, suffix, tail))) case J.Obj{fields}: match fields: case Nil{}: match mode: case A.Whole{}: {==} case A.Members{}: {==} case (key, field_value) <> rest: match mode: case A.Whole{}: Equal.trans(List, token_source(J.source(J.Obj{(key, field_value) <> rest}, False{}, suffix), tail), J.Delimiter{'{'} <> token_string(key) <> J.Delimiter{':'} <> token_source(J.source(field_value, False{}, J.source(J.Obj{rest}, True{}, suffix)), tail), canonical(J.Obj{(key, field_value) <> rest}, A.Whole{}, token_source(suffix, tail)), source_object_key_prefix('{', key, J.Punctuation{':'} <> J.source(field_value, False{}, J.source(J.Obj{rest}, True{}, suffix)), tail), Equal.trans(List, J.Delimiter{'{'} <> token_string(key) <> J.Delimiter{':'} <> token_source(J.source(field_value, False{}, J.source(J.Obj{rest}, True{}, suffix)), tail), J.Delimiter{'{'} <> token_string(key) <> J.Delimiter{':'} <> canonical(field_value, A.Whole{}, token_source(J.source(J.Obj{rest}, True{}, suffix), tail)), canonical(J.Obj{(key, field_value) <> rest}, A.Whole{}, token_source(suffix, tail)), Equal.cong(List, List, xs => J.Delimiter{'{'} <> token_string(key) <> J.Delimiter{':'} <> xs, token_source(J.source(field_value, False{}, J.source(J.Obj{rest}, True{}, suffix)), tail), canonical(field_value, A.Whole{}, token_source(J.source(J.Obj{rest}, True{}, suffix), tail)), source_tokens(field_value, A.Whole{}, J.source(J.Obj{rest}, True{}, suffix), tail)), Equal.cong(List, List, xs => J.Delimiter{'{'} <> token_string(key) <> J.Delimiter{':'} <> canonical(field_value, A.Whole{}, xs), token_source(J.source(J.Obj{rest}, True{}, suffix), tail), canonical(J.Obj{rest}, A.Members{}, token_source(suffix, tail)), source_tokens(J.Obj{rest}, A.Members{}, suffix, tail)))) case A.Members{}: Equal.trans(List, token_source(J.source(J.Obj{(key, field_value) <> rest}, True{}, suffix), tail), J.Delimiter{','} <> token_string(key) <> J.Delimiter{':'} <> token_source(J.source(field_value, False{}, J.source(J.Obj{rest}, True{}, suffix)), tail), canonical(J.Obj{(key, field_value) <> rest}, A.Members{}, token_source(suffix, tail)), source_object_key_prefix(',', key, J.Punctuation{':'} <> J.source(field_value, False{}, J.source(J.Obj{rest}, True{}, suffix)), tail), Equal.trans(List, J.Delimiter{','} <> token_string(key) <> J.Delimiter{':'} <> token_source(J.source(field_value, False{}, J.source(J.Obj{rest}, True{}, suffix)), tail), J.Delimiter{','} <> token_string(key) <> J.Delimiter{':'} <> canonical(field_value, A.Whole{}, token_source(J.source(J.Obj{rest}, True{}, suffix), tail)), canonical(J.Obj{(key, field_value) <> rest}, A.Members{}, token_source(suffix, tail)), Equal.cong(List, List, xs => J.Delimiter{','} <> token_string(key) <> J.Delimiter{':'} <> xs, token_source(J.source(field_value, False{}, J.source(J.Obj{rest}, True{}, suffix)), tail), canonical(field_value, A.Whole{}, token_source(J.source(J.Obj{rest}, True{}, suffix), tail)), source_tokens(field_value, A.Whole{}, J.source(J.Obj{rest}, True{}, suffix), tail)), Equal.cong(List, List, xs => J.Delimiter{','} <> token_string(key) <> J.Delimiter{':'} <> canonical(field_value, A.Whole{}, xs), token_source(J.source(J.Obj{rest}, True{}, suffix), tail), canonical(J.Obj{rest}, A.Members{}, token_source(suffix, tail)), source_tokens(J.Obj{rest}, A.Members{}, suffix, tail)))) Uses (16): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Char https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=Lexeme https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=Token https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=Value https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=source https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_AssemblyProof.bend&name=Mode https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_SourceProof.bend&name=canonical https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_SourceProof.bend&name=source_object_key_prefix https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_SourceProof.bend&name=to_bool https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_SourceProof.bend&name=token_source https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_SourceProof.bend&name=token_string