def lex_source_number_before_punctuation

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

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_StringProof.bend as S
import qasim-bend-kit@0.1.0.2/proof/JSON_NumberLexProof.bend as Num

173def lex_source_number_before_punctuation(+text: String,
174                                         +certificate: J.NumberCert<text>,
175                                         +punctuation: Char,
176                                         +suffix: String,
177                                         +acc: List<&2, J.Lexeme>,
178                                         action: {J.lex_seed_action(SCon{punctuation, suffix}, J.Outside{}) == J.LexPunctuation{punctuation} : J.LexAction}) -> {J.lex_scan(J.render(J.Number{text, certificate}, False{}, SNil{}) ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc) == J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Payload{text} <> acc) : List<&2, J.Lexeme>}:
179    Equal.trans(List<&2, J.Lexeme>,
180        J.lex_scan(J.render(J.Number{text, certificate}, False{}, SNil{}) ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc),
181        J.lex_scan(text ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc),
182        J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Payload{text} <> acc),
183        Equal.cong(String, List<&2, J.Lexeme>, source => J.lex_scan(source ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc),
184            J.render(J.Number{text, certificate}, False{}, SNil{}), text,
185            S.append_nil(text)),
186        Num.lex_certified_number_before_punctuation(text, certificate, punctuation, suffix, acc, action))