def atomic_end

qasim-bend-kit@0.1.0.2 · proof/JSON_RenderLexProof.bend:199

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_SourceProof.bend as SP
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_LexWhitespaceProof.bend as W

199def atomic_end(+atom: SP.AtomicValue,
200               +acc: List<&2, J.Lexeme>) -> {J.lex_scan(J.render(SP.atomic_value(atom), False{}, SNil{}), J.Outside{}, SNil{}, acc) == finish(End{}, push(SP.atomic_value(atom), SP.RenderWhole{}, acc)) : List<&2, J.Lexeme>}:
201    match atom:
202        case SP.AtomicNull{}: {==}
203        case SP.AtomicTrue{}: {==}
204        case SP.AtomicFalse{}: {==}
205        case SP.AtomicNumber{text, certificate}:
206            Equal.trans(List<&2, J.Lexeme>,
207                J.lex_scan(J.render(J.Number{text, certificate}, False{}, SNil{}), J.Outside{}, SNil{}, acc),
208                J.lex_scan(text, J.Outside{}, SNil{}, acc),
209                finish(End{}, push(J.Number{text, certificate}, SP.RenderWhole{}, acc)),
210                Equal.cong(String, List<&2, J.Lexeme>,
211                    x => J.lex_scan(x, J.Outside{}, SNil{}, acc),
212                    text ++ SNil{},
213                    text,
214                    S.append_nil(text)),
215                number_end(text, acc, P.cert_valid(text, certificate)))
216        case SP.AtomicString{text}:
217            Equal.trans(List<&2, J.Lexeme>,
218                J.lex_scan(J.render(J.Str{text}, False{}, SNil{}), J.Outside{}, SNil{}, acc),
219                J.lex_scan(J.render(J.Str{text}, False{}, SNil{}) ++ SNil{}, J.Outside{}, SNil{}, acc),
220                finish(End{}, push(J.Str{text}, SP.RenderWhole{}, acc)),
221                Equal.cong(String, List<&2, J.Lexeme>,
222                    x => J.lex_scan(x, J.Outside{}, SNil{}, acc),
223                    J.render(J.Str{text}, False{}, SNil{}),
224                    J.render(J.Str{text}, False{}, SNil{}) ++ SNil{},
225                    Equal.sym(String,
226                        J.render(J.Str{text}, False{}, SNil{}) ++ SNil{},
227                        J.render(J.Str{text}, False{}, SNil{}),
228                        S.append_nil(J.render(J.Str{text}, False{}, SNil{})))),
229                W.lex_rendered_string_suffix(text, SNil{}, acc))