def lex_number_delimited_tail
qasim-bend-kit@0.1.0.2 · proof/JSON_NumberLexProof.bend:310
import qasim-bend-kit@0.1.0.2/proof/JSON_NumberLexProof.bend as JSONNumberLexProof
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
310def lex_number_delimited_tail(+text: String,
311 +state: J.NumberState,
312 +rev_head: Char,
313 +rev_tail: String,
314 +payload: String,
315 +punctuation: Char,
316 +suffix: String,
317 +acc: List<&2, J.Lexeme>,
318 reverse_buffer: {String.reverse(SCon{rev_head, rev_tail}) == payload : String},
319 action: {J.lex_seed_action(SCon{punctuation, suffix}, J.Outside{}) == J.LexPunctuation{punctuation} : J.LexAction},
320 +evidence: {J.number_valid_end(J.number_valid_step(text, state)) == True{} : Bool}) -> {J.lex_scan(text ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SCon{rev_head, rev_tail}, acc) == J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Payload{payload ++ text} <> acc) : List<&2, J.Lexeme>}:
321 match text:
322 case SNil{}:
323 Equal.trans(List<&2, J.Lexeme>, J.lex_scan(SCon{punctuation, SNil{}} ++ suffix, J.Outside{}, SCon{rev_head, rev_tail}, acc),
324 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Payload{payload} <> acc),
325 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Payload{payload ++ SNil{}} <> acc),
326 Equal.trans(List<&2, J.Lexeme>, J.lex_scan(SCon{punctuation, SNil{}} ++ suffix, J.Outside{}, SCon{rev_head, rev_tail}, acc),
327 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.flush_lexeme(SCon{rev_head, rev_tail}, acc)),
328 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Payload{payload} <> acc),
329 W.scan_punctuation_char(punctuation, suffix, SCon{rev_head, rev_tail}, acc, action),
330 Equal.trans(List<&2, J.Lexeme>, J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.flush_lexeme(SCon{rev_head, rev_tail}, acc)),
331 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Payload{String.reverse(SCon{rev_head, rev_tail})} <> acc),
332 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Payload{payload} <> acc),
333 {==},
334 Equal.cong(String, List<&2, J.Lexeme>, value => J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Payload{value} <> acc),
335 String.reverse(SCon{rev_head, rev_tail}), payload, reverse_buffer))),
336 Equal.cong(String, List<&2, J.Lexeme>, value => J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Payload{value} <> acc),
337 payload, payload ++ SNil{}, Equal.sym(String, payload ++ SNil{}, payload, S.append_nil(payload))))
338 case SCon{+head, +tail}:
339 Equal.trans(List<&2, J.Lexeme>, J.lex_scan(SCon{head, tail} ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SCon{rev_head, rev_tail}, acc),
340 J.lex_scan(tail ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SCon{head, SCon{rev_head, rev_tail}}, acc),
341 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Payload{payload ++ SCon{head, tail}} <> acc),
342 Equal.trans(List<&2, J.Lexeme>, J.lex_scan(SCon{head, tail} ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SCon{rev_head, rev_tail}, acc),
343 J.lex_scan(tail ++ (SCon{punctuation, SNil{}} ++ suffix),
344 W.after_mode(J.lex_seed_action(SCon{head, tail ++ (SCon{punctuation, SNil{}} ++ suffix)}, J.Outside{}), J.Outside{}),
345 W.after_reversed(J.lex_seed_action(SCon{head, tail ++ (SCon{punctuation, SNil{}} ++ suffix)}, J.Outside{}), head, SCon{rev_head, rev_tail}),
346 W.after_acc(J.lex_seed_action(SCon{head, tail ++ (SCon{punctuation, SNil{}} ++ suffix)}, J.Outside{}), head, SCon{rev_head, rev_tail}, acc)),
347 J.lex_scan(tail ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SCon{head, SCon{rev_head, rev_tail}}, acc),
348 W.lex_scan_step(head, tail ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SCon{rev_head, rev_tail}, acc),
349 Equal.cong(J.LexAction, List<&2, J.Lexeme>, lex_action => J.lex_scan(tail ++ (SCon{punctuation, SNil{}} ++ suffix),
350 W.after_mode(lex_action, J.Outside{}), W.after_reversed(lex_action, head, SCon{rev_head, rev_tail}),
351 W.after_acc(lex_action, head, SCon{rev_head, rev_tail}, acc)),
352 J.lex_seed_action(SCon{head, tail ++ (SCon{punctuation, SNil{}} ++ suffix)}, J.Outside{}), J.LexRaw{},
353 number_char_action(head, J.number_char(head), {==}, tail, state, evidence))),
354 Equal.trans(List<&2, J.Lexeme>, J.lex_scan(tail ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SCon{head, SCon{rev_head, rev_tail}}, acc),
355 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Payload{(payload ++ SCon{head, SNil{}}) ++ tail} <> acc),
356 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Payload{payload ++ SCon{head, tail}} <> acc),
357 lex_number_delimited_tail(tail, J.number_next(state, head), head, SCon{rev_head, rev_tail}, payload ++ SCon{head, SNil{}},
358 punctuation, suffix, acc,
359 Equal.trans(String, String.reverse(SCon{head, SCon{rev_head, rev_tail}}),
360 String.reverse(SCon{rev_head, rev_tail}) ++ SCon{head, SNil{}}, payload ++ SCon{head, SNil{}},
361 S.reverse_cons(head, SCon{rev_head, rev_tail}),
362 Equal.cong(String, String, value => value ++ SCon{head, SNil{}}, String.reverse(SCon{rev_head, rev_tail}), payload, reverse_buffer)),
363 action, number_valid_cons(head, tail, state, evidence)),
364 Equal.cong(String, List<&2, J.Lexeme>, value => J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Payload{value} <> acc),
365 (payload ++ SCon{head, SNil{}}) ++ tail, payload ++ SCon{head, tail},
366 S.append_assoc(payload, SCon{head, SNil{}}, tail))))