def lex_number_tail

qasim-bend-kit@0.1.0.2 · proof/JSON_NumberLexProof.bend:226

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

226def lex_number_tail(+text: String,
227                    +state: J.NumberState,
228                    +rev_head: Char,
229                    +rev_tail: String,
230                    +first: Char,
231                    +prefix_tail: String,
232                    +reverse_prefix: {String.reverse(SCon{rev_head, rev_tail}) == SCon{first, prefix_tail} : String},
233                    +evidence: {J.number_valid_end(J.number_valid_step(text, state)) == True{} : Bool}) -> {J.lex_scan(text, J.Outside{}, SCon{rev_head, rev_tail}, Nil{}) == (J.Payload{SCon{first, prefix_tail} ++ text} <> Nil{}) : List<&2, J.Lexeme>}:
234    match text:
235        case SNil{}:
236            Equal.trans(List<&2, J.Lexeme>,
237                J.lex_scan(SNil{}, J.Outside{}, SCon{rev_head, rev_tail}, Nil{}),
238                J.Payload{String.reverse(SCon{rev_head, rev_tail})} <> Nil{},
239                J.Payload{SCon{first, prefix_tail} ++ SNil{}} <> Nil{},
240                {==},
241                Equal.trans(List<&2, J.Lexeme>,
242                    J.Payload{String.reverse(SCon{rev_head, rev_tail})} <> Nil{},
243                    J.Payload{SCon{first, prefix_tail}} <> Nil{},
244                    J.Payload{SCon{first, prefix_tail} ++ SNil{}} <> Nil{},
245                    Equal.cong(String, List<&2, J.Lexeme>, s => J.Payload{s} <> Nil{},
246                        String.reverse(SCon{rev_head, rev_tail}), SCon{first, prefix_tail}, reverse_prefix),
247                    Equal.cong(String, List<&2, J.Lexeme>, s => J.Payload{s} <> Nil{},
248                        SCon{first, prefix_tail}, SCon{first, prefix_tail} ++ SNil{},
249                        Equal.sym(String, SCon{first, prefix_tail} ++ SNil{}, SCon{first, prefix_tail}, S.append_nil(SCon{first, prefix_tail})))))
250        case SCon{+head, +tail}:
251            Equal.trans(List<&2, J.Lexeme>,
252                J.lex_scan(text, J.Outside{}, SCon{rev_head, rev_tail}, Nil{}),
253                J.lexemes(text, J.Outside{}, SCon{rev_head, rev_tail}, Nil{}, J.LexRaw{}),
254                J.Payload{SCon{first, prefix_tail} ++ text} <> Nil{},
255                Equal.cong(J.LexAction, List<&2, J.Lexeme>, action => J.lexemes(text, J.Outside{}, SCon{rev_head, rev_tail}, Nil{}, action),
256                    J.lex_seed_action(text, J.Outside{}), J.LexRaw{},
257                    number_char_action(head, J.number_char(head), {==}, tail, state, evidence)),
258                Equal.trans(List<&2, J.Lexeme>,
259                    J.lexemes(text, J.Outside{}, SCon{rev_head, rev_tail}, Nil{}, J.LexRaw{}),
260                    J.lex_scan(tail, J.Outside{}, SCon{head, SCon{rev_head, rev_tail}}, Nil{}),
261                    J.Payload{SCon{first, prefix_tail} ++ text} <> Nil{},
262                    {==},
263                    Equal.trans(List<&2, J.Lexeme>,
264                        J.lex_scan(tail, J.Outside{}, SCon{head, SCon{rev_head, rev_tail}}, Nil{}),
265                        J.Payload{(SCon{first, prefix_tail} ++ SCon{head, SNil{}}) ++ tail} <> Nil{},
266                        J.Payload{SCon{first, prefix_tail} ++ text} <> Nil{},
267                        lex_number_tail(tail, J.number_next(state, head), head, SCon{rev_head, rev_tail}, first,
268                            prefix_tail ++ SCon{head, SNil{}},
269                            Equal.trans(String,
270                                String.reverse(SCon{head, SCon{rev_head, rev_tail}}),
271                                String.reverse(SCon{rev_head, rev_tail}) ++ SCon{head, SNil{}},
272                                SCon{first, prefix_tail} ++ SCon{head, SNil{}},
273                                S.reverse_cons(head, SCon{rev_head, rev_tail}),
274                                Equal.cong(String, String, x => x ++ SCon{head, SNil{}},
275                                    String.reverse(SCon{rev_head, rev_tail}), SCon{first, prefix_tail}, reverse_prefix)),
276                            number_valid_cons(head, tail, state, evidence)),
277                        Equal.cong(String, List<&2, J.Lexeme>, s => J.Payload{s} <> Nil{},
278                            (SCon{first, prefix_tail} ++ SCon{head, SNil{}}) ++ tail,
279                            SCon{first, prefix_tail} ++ text,
280                            S.append_assoc(SCon{first, prefix_tail}, SCon{head, SNil{}}, tail)))))