JSONSourceProof.lex_atomic_source_before_punctuation: 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 784-823 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=784&end_line=823

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

def lex_atomic_source_before_punctuation(+atom: AtomicValue,
                                         +punctuation: Char,
                                         +suffix: String,
                                         +acc: List<&2, J.Lexeme>,
                                         action: {J.lex_seed_action(SCon{punctuation, suffix}, J.Outside{}) == J.LexPunctuation{punctuation} : J.LexAction}) -> {J.lex_scan(J.render(atomic_value(atom), False{}, SNil{}) ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc) == J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> List.append(&2, J.Lexeme, atomic_source(atom), acc)) : List<&2, J.Lexeme>}:
    match atom:
        case AtomicNull{}:
            Equal.trans(List<&2, J.Lexeme>,
                J.lex_scan(J.render(J.Null{}, False{}, SNil{}) ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc),
                J.lex_scan("null" ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc),
                J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> List.append(&2, J.Lexeme, atomic_source(AtomicNull{}), acc)),
                Equal.cong(String, List<&2, J.Lexeme>, source => J.lex_scan(source ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc),
                    J.render(J.Null{}, False{}, SNil{}), "null", S.append_nil("null")),
                W.lex_null_before_punctuation(punctuation, suffix, acc, action))
        case AtomicTrue{}:
            Equal.trans(List<&2, J.Lexeme>,
                J.lex_scan(J.render(J.Bool{True{}}, False{}, SNil{}) ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc),
                J.lex_scan("true" ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc),
                J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> List.append(&2, J.Lexeme, atomic_source(AtomicTrue{}), acc)),
                Equal.cong(String, List<&2, J.Lexeme>, source => J.lex_scan(source ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc),
                    J.render(J.Bool{True{}}, False{}, SNil{}), "true", S.append_nil("true")),
                W.lex_true_before_punctuation(punctuation, suffix, acc, action))
        case AtomicFalse{}:
            Equal.trans(List<&2, J.Lexeme>,
                J.lex_scan(J.render(J.Bool{False{}}, False{}, SNil{}) ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc),
                J.lex_scan("false" ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc),
                J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> List.append(&2, J.Lexeme, atomic_source(AtomicFalse{}), acc)),
                Equal.cong(String, List<&2, J.Lexeme>, source => J.lex_scan(source ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc),
                    J.render(J.Bool{False{}}, False{}, SNil{}), "false", S.append_nil("false")),
                W.lex_false_before_punctuation(punctuation, suffix, acc, action))
        case AtomicNumber{text, certificate}:
            lex_source_number_before_punctuation(text, certificate, punctuation, suffix, acc, action)
        case AtomicString{text}:
            Equal.trans(List<&2, J.Lexeme>,
                J.lex_scan(J.render(J.Str{text}, False{}, SNil{}) ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc),
                J.lex_scan((SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}) ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc),
                J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> List.append(&2, J.Lexeme, atomic_source(AtomicString{text}), acc)),
                Equal.cong(String, List<&2, J.Lexeme>, source => J.lex_scan(source ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc),
                    J.render(J.Str{text}, False{}, SNil{}), SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}, {==}),
                W.lex_string_before_punctuation(text, punctuation, suffix, acc, action))

Uses (25):
  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=List.append
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String.append
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=LexAction
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=LexMode
  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=Value
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=escape_string
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=lex_scan
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=lex_seed_action
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=render
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_LexWhitespaceProof.bend&name=lex_false_before_punctuation
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_LexWhitespaceProof.bend&name=lex_null_before_punctuation
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_LexWhitespaceProof.bend&name=lex_string_before_punctuation
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_LexWhitespaceProof.bend&name=lex_true_before_punctuation
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_SourceProof.bend&name=AtomicValue
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_SourceProof.bend&name=atomic_source
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_SourceProof.bend&name=atomic_value
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_SourceProof.bend&name=lex_source_number_before_punctuation
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_StringProof.bend&name=append_nil