def lex_atomic_value_source

qasim-bend-kit@0.1.0.2 · proof/JSON_SourceProof.bend:840

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_PrimitiveProof.bend as P
import qasim-bend-kit@0.1.0.2/proof/JSON_StringProof.bend as S
import qasim-bend-kit@0.1.0.2/proof/JSON_NumberLexProof.bend as Num
import qasim-bend-kit@0.1.0.2/proof/JSON_LexWhitespaceProof.bend as W

840def lex_atomic_value_source(+atom: AtomicValue) -> {J.lex_scan(J.stringify(atomic_value(atom)), J.Outside{}, SNil{}, Nil{}) == J.source(atomic_value(atom), False{}, Nil{}) : List<&2, J.Lexeme>}:
841    match atom:
842        case AtomicNull{}: {==}
843        case AtomicTrue{}: {==}
844        case AtomicFalse{}: {==}
845        case AtomicNumber{text, certificate}:
846            Equal.trans(List<&2, J.Lexeme>,
847                J.lex_scan(J.stringify(J.Number{text, certificate}), J.Outside{}, SNil{}, Nil{}),
848                J.lex_scan(text, J.Outside{}, SNil{}, Nil{}),
849                J.source(J.Number{text, certificate}, False{}, Nil{}),
850                Equal.cong(String, List<&2, J.Lexeme>, source => J.lex_scan(source, J.Outside{}, SNil{}, Nil{}),
851                    J.stringify(J.Number{text, certificate}), text, S.append_nil(text)),
852                Equal.trans(List<&2, J.Lexeme>, J.lex_scan(text, J.Outside{}, SNil{}, Nil{}),
853                    J.Payload{text} <> Nil{}, J.source(J.Number{text, certificate}, False{}, Nil{}),
854                    Num.lex_number_payload(text, P.cert_valid(text, certificate)), {==}))
855        case AtomicString{text}:
856            W.lex_rendered_string(text)