proof/JSON_NumberLexProof.bend
qasim-bend-kit@0.1.0.2 · 409 lines · 16 definitions
1import Base
2import qasim-bend-kit@0.1.0.2/libs/JSON.bend as J
3import qasim-bend-kit@0.1.0.2/proof/JSON_PrimitiveProof.bend as P
4import qasim-bend-kit@0.1.0.2/proof/JSON_StringProof.bend as S
5import qasim-bend-kit@0.1.0.2/proof/JSON_LexWhitespaceProof.bend as W
6
7def false_true(e: {False{} == True{} : Bool}) -> Empty:
8 %e : P.false_type(_)
9 Unit{}
10
11def number_valid_cons(+character: Char,
12 +tail: String,
13 +state: J.NumberState,
14 evidence: {J.number_valid_end(J.number_valid_step(SCon{character, tail}, state)) == True{} : Bool}) -> {J.number_valid_end(J.number_valid_step(tail, J.number_next(state, character))) == True{} : Bool}:
15 match state:
16 case J.NumberInvalid{}:
17 Empty.absurd({J.number_valid_end(J.number_valid_step(tail, J.NumberInvalid{})) == True{} : Bool}, false_true(evidence))
18 case J.NumberStart{}:
19 Equal.trans(Bool, J.number_valid_end(J.number_valid_step(tail, J.number_next(J.NumberStart{}, character))), J.number_valid_end(J.number_valid_step(SCon{character, tail}, J.NumberStart{})), True{}, {==}, evidence)
20 case J.NumberMinus{}:
21 Equal.trans(Bool, J.number_valid_end(J.number_valid_step(tail, J.number_next(J.NumberMinus{}, character))), J.number_valid_end(J.number_valid_step(SCon{character, tail}, J.NumberMinus{})), True{}, {==}, evidence)
22 case J.NumberZero{}:
23 Equal.trans(Bool, J.number_valid_end(J.number_valid_step(tail, J.number_next(J.NumberZero{}, character))), J.number_valid_end(J.number_valid_step(SCon{character, tail}, J.NumberZero{})), True{}, {==}, evidence)
24 case J.NumberInteger{}:
25 Equal.trans(Bool, J.number_valid_end(J.number_valid_step(tail, J.number_next(J.NumberInteger{}, character))), J.number_valid_end(J.number_valid_step(SCon{character, tail}, J.NumberInteger{})), True{}, {==}, evidence)
26 case J.NumberDot{}:
27 Equal.trans(Bool, J.number_valid_end(J.number_valid_step(tail, J.number_next(J.NumberDot{}, character))), J.number_valid_end(J.number_valid_step(SCon{character, tail}, J.NumberDot{})), True{}, {==}, evidence)
28 case J.NumberFraction{}:
29 Equal.trans(Bool, J.number_valid_end(J.number_valid_step(tail, J.number_next(J.NumberFraction{}, character))), J.number_valid_end(J.number_valid_step(SCon{character, tail}, J.NumberFraction{})), True{}, {==}, evidence)
30 case J.NumberExponent{}:
31 Equal.trans(Bool, J.number_valid_end(J.number_valid_step(tail, J.number_next(J.NumberExponent{}, character))), J.number_valid_end(J.number_valid_step(SCon{character, tail}, J.NumberExponent{})), True{}, {==}, evidence)
32 case J.NumberExponentSign{}:
33 Equal.trans(Bool, J.number_valid_end(J.number_valid_step(tail, J.number_next(J.NumberExponentSign{}, character))), J.number_valid_end(J.number_valid_step(SCon{character, tail}, J.NumberExponentSign{})), True{}, {==}, evidence)
34 case J.NumberExponentDigits{}:
35 Equal.trans(Bool, J.number_valid_end(J.number_valid_step(tail, J.number_next(J.NumberExponentDigits{}, character))), J.number_valid_end(J.number_valid_step(SCon{character, tail}, J.NumberExponentDigits{})), True{}, {==}, evidence)
36
37def number_other_invalid(state: J.NumberState) -> {J.number_step(J.NOther{}, state) == J.NumberInvalid{} : J.NumberState}:
38 match state:
39 case J.NumberStart{}: {==}
40 case J.NumberMinus{}: {==}
41 case J.NumberZero{}: {==}
42 case J.NumberInteger{}: {==}
43 case J.NumberDot{}: {==}
44 case J.NumberFraction{}: {==}
45 case J.NumberExponent{}: {==}
46 case J.NumberExponentSign{}: {==}
47 case J.NumberExponentDigits{}: {==}
48 case J.NumberInvalid{}: {==}
49
50def number_next_other(+character: Char,
51 +state: J.NumberState,
52 evidence: {J.number_char(character) == J.NOther{} : J.NumberChar}) -> {J.number_next(state, character) == J.NumberInvalid{} : J.NumberState}:
53 match state:
54 case J.NumberInvalid{}: {==}
55 case J.NumberStart{}:
56 Equal.trans(J.NumberState, J.number_next(J.NumberStart{}, character), J.number_step(J.NOther{}, J.NumberStart{}), J.NumberInvalid{},
57 Equal.cong(J.NumberChar, J.NumberState, c => J.number_step(c, J.NumberStart{}), J.number_char(character), J.NOther{}, evidence), number_other_invalid(J.NumberStart{}))
58 case J.NumberMinus{}:
59 Equal.trans(J.NumberState, J.number_next(J.NumberMinus{}, character), J.number_step(J.NOther{}, J.NumberMinus{}), J.NumberInvalid{},
60 Equal.cong(J.NumberChar, J.NumberState, c => J.number_step(c, J.NumberMinus{}), J.number_char(character), J.NOther{}, evidence), number_other_invalid(J.NumberMinus{}))
61 case J.NumberZero{}:
62 Equal.trans(J.NumberState, J.number_next(J.NumberZero{}, character), J.number_step(J.NOther{}, J.NumberZero{}), J.NumberInvalid{},
63 Equal.cong(J.NumberChar, J.NumberState, c => J.number_step(c, J.NumberZero{}), J.number_char(character), J.NOther{}, evidence), number_other_invalid(J.NumberZero{}))
64 case J.NumberInteger{}:
65 Equal.trans(J.NumberState, J.number_next(J.NumberInteger{}, character), J.number_step(J.NOther{}, J.NumberInteger{}), J.NumberInvalid{},
66 Equal.cong(J.NumberChar, J.NumberState, c => J.number_step(c, J.NumberInteger{}), J.number_char(character), J.NOther{}, evidence), number_other_invalid(J.NumberInteger{}))
67 case J.NumberDot{}:
68 Equal.trans(J.NumberState, J.number_next(J.NumberDot{}, character), J.number_step(J.NOther{}, J.NumberDot{}), J.NumberInvalid{},
69 Equal.cong(J.NumberChar, J.NumberState, c => J.number_step(c, J.NumberDot{}), J.number_char(character), J.NOther{}, evidence), number_other_invalid(J.NumberDot{}))
70 case J.NumberFraction{}:
71 Equal.trans(J.NumberState, J.number_next(J.NumberFraction{}, character), J.number_step(J.NOther{}, J.NumberFraction{}), J.NumberInvalid{},
72 Equal.cong(J.NumberChar, J.NumberState, c => J.number_step(c, J.NumberFraction{}), J.number_char(character), J.NOther{}, evidence), number_other_invalid(J.NumberFraction{}))
73 case J.NumberExponent{}:
74 Equal.trans(J.NumberState, J.number_next(J.NumberExponent{}, character), J.number_step(J.NOther{}, J.NumberExponent{}), J.NumberInvalid{},
75 Equal.cong(J.NumberChar, J.NumberState, c => J.number_step(c, J.NumberExponent{}), J.number_char(character), J.NOther{}, evidence), number_other_invalid(J.NumberExponent{}))
76 case J.NumberExponentSign{}:
77 Equal.trans(J.NumberState, J.number_next(J.NumberExponentSign{}, character), J.number_step(J.NOther{}, J.NumberExponentSign{}), J.NumberInvalid{},
78 Equal.cong(J.NumberChar, J.NumberState, c => J.number_step(c, J.NumberExponentSign{}), J.number_char(character), J.NOther{}, evidence), number_other_invalid(J.NumberExponentSign{}))
79 case J.NumberExponentDigits{}:
80 Equal.trans(J.NumberState, J.number_next(J.NumberExponentDigits{}, character), J.number_step(J.NOther{}, J.NumberExponentDigits{}), J.NumberInvalid{},
81 Equal.cong(J.NumberChar, J.NumberState, c => J.number_step(c, J.NumberExponentDigits{}), J.number_char(character), J.NOther{}, evidence), number_other_invalid(J.NumberExponentDigits{}))
82
83def invalid_valid_tail(+tail: String,
84 +state: J.NumberState,
85 +character: Char,
86 other: {J.number_char(character) == J.NOther{} : J.NumberChar},
87 evidence: {J.number_valid_end(J.number_valid_step(SCon{character, tail}, state)) == True{} : Bool}) -> Empty:
88 false_true(Equal.trans(Bool, False{},
89 J.number_valid_end(J.number_valid_step(tail, J.NumberInvalid{})), True{},
90 Equal.sym(Bool, J.number_valid_end(J.number_valid_step(tail, J.NumberInvalid{})), False{}, P.invalid_end(tail)),
91 Equal.trans(Bool,
92 J.number_valid_end(J.number_valid_step(tail, J.NumberInvalid{})),
93 J.number_valid_end(J.number_valid_step(tail, J.number_next(state, character))), True{},
94 Equal.sym(Bool,
95 J.number_valid_end(J.number_valid_step(tail, J.number_next(state, character))),
96 J.number_valid_end(J.number_valid_step(tail, J.NumberInvalid{})),
97 Equal.cong(J.NumberState, Bool, s => J.number_valid_end(J.number_valid_step(tail, s)),
98 J.number_next(state, character), J.NumberInvalid{}, number_next_other(character, state, other))),
99 number_valid_cons(character, tail, state, evidence))))
100
101def plain_lexemes(+text: String, reversed: String, acc: List<&2, J.Lexeme>) -> List<&2, J.Lexeme>:
102 match text:
103 case SNil{}: List.reverse(&2, J.Lexeme, J.flush_lexeme(reversed, acc))
104 case SCon{head, tail}: plain_lexemes(tail, SCon{head, reversed}, acc)
105
106def number_char_action(+character: Char,
107 +class: J.NumberChar,
108 class_eq: {J.number_char(character) == class : J.NumberChar},
109 +tail: String,
110 +state: J.NumberState,
111 evidence: {J.number_valid_end(J.number_valid_step(SCon{character, tail}, state)) == True{} : Bool}) -> {J.lex_outside_action(character, class) == J.LexRaw{} : J.LexAction}:
112 match class:
113 case J.NOther{}:
114 Empty.absurd({J.lex_outside_action(character, J.NOther{}) == J.LexRaw{} : J.LexAction},
115 invalid_valid_tail(tail, state, character, class_eq, evidence))
116 case J.NMinus{}: {==}
117 case J.NPlus{}: {==}
118 case J.NDot{}: {==}
119 case J.NExp{}: {==}
120 case J.NZero{}: {==}
121 case J.NDigit{}: {==}
122
123def number_prefix_mode(+text: String,
124 +state: J.NumberState,
125 +evidence: {J.number_valid_end(J.number_valid_step(text, state)) == True{} : Bool}) -> {W.prefix_mode(text, J.Outside{}) == J.Outside{} : J.LexMode}:
126 match text:
127 case SNil{}: {==}
128 case SCon{+head, +tail}:
129 Equal.trans(J.LexMode, W.prefix_mode(SCon{head, tail}, J.Outside{}),
130 W.prefix_mode(tail, W.after_mode(J.lex_seed_action(SCon{head, tail}, J.Outside{}), J.Outside{})), J.Outside{},
131 {==},
132 Equal.trans(J.LexMode,
133 W.prefix_mode(tail, W.after_mode(J.lex_seed_action(SCon{head, tail}, J.Outside{}), J.Outside{})),
134 W.prefix_mode(tail, J.Outside{}), J.Outside{},
135 Equal.cong(J.LexAction, J.LexMode, action => W.prefix_mode(tail, W.after_mode(action, J.Outside{})),
136 J.lex_seed_action(SCon{head, tail}, J.Outside{}), J.LexRaw{},
137 number_char_action(head, J.number_char(head), {==}, tail, state, evidence)),
138 number_prefix_mode(tail, J.number_next(state, head), number_valid_cons(head, tail, state, evidence))))
139
140def number_prefix_acc(+text: String,
141 +state: J.NumberState,
142 +reversed: String,
143 +acc: List<&2, J.Lexeme>,
144 +evidence: {J.number_valid_end(J.number_valid_step(text, state)) == True{} : Bool}) -> {W.prefix_acc(text, J.Outside{}, reversed, acc) == acc : List<&2, J.Lexeme>}:
145 match text:
146 case SNil{}: {==}
147 case SCon{+head, +tail}:
148 Equal.trans(List<&2, J.Lexeme>, W.prefix_acc(SCon{head, tail}, J.Outside{}, reversed, acc),
149 W.prefix_acc(tail, J.Outside{}, SCon{head, reversed}, acc), acc,
150 Equal.trans(List<&2, J.Lexeme>,
151 W.prefix_acc(SCon{head, tail}, J.Outside{}, reversed, acc),
152 W.prefix_acc(tail, W.after_mode(J.lex_seed_action(SCon{head, tail}, J.Outside{}), J.Outside{}),
153 W.after_reversed(J.lex_seed_action(SCon{head, tail}, J.Outside{}), head, reversed),
154 W.after_acc(J.lex_seed_action(SCon{head, tail}, J.Outside{}), head, reversed, acc)),
155 W.prefix_acc(tail, J.Outside{}, SCon{head, reversed}, acc),
156 {==},
157 Equal.cong(J.LexAction, List<&2, J.Lexeme>, action => W.prefix_acc(tail, W.after_mode(action, J.Outside{}),
158 W.after_reversed(action, head, reversed), W.after_acc(action, head, reversed, acc)),
159 J.lex_seed_action(SCon{head, tail}, J.Outside{}), J.LexRaw{},
160 number_char_action(head, J.number_char(head), {==}, tail, state, evidence))),
161 number_prefix_acc(tail, J.number_next(state, head), SCon{head, reversed}, acc,
162 number_valid_cons(head, tail, state, evidence)))
163
164def number_prefix_reversed(+text: String,
165 +state: J.NumberState,
166 +reversed: String,
167 +evidence: {J.number_valid_end(J.number_valid_step(text, state)) == True{} : Bool}) -> {W.prefix_reversed(text, J.Outside{}, reversed) == String.reverse(text) ++ reversed : String}:
168 match text:
169 case SNil{}: {==}
170 case SCon{+head, +tail}:
171 Equal.trans(String, W.prefix_reversed(SCon{head, tail}, J.Outside{}, reversed),
172 W.prefix_reversed(tail, J.Outside{}, SCon{head, reversed}),
173 String.reverse(SCon{head, tail}) ++ reversed,
174 Equal.trans(String,
175 W.prefix_reversed(SCon{head, tail}, J.Outside{}, reversed),
176 W.prefix_reversed(tail, W.after_mode(J.lex_seed_action(SCon{head, tail}, J.Outside{}), J.Outside{}),
177 W.after_reversed(J.lex_seed_action(SCon{head, tail}, J.Outside{}), head, reversed)),
178 W.prefix_reversed(tail, J.Outside{}, SCon{head, reversed}),
179 {==},
180 Equal.cong(J.LexAction, String, action => W.prefix_reversed(tail, W.after_mode(action, J.Outside{}),
181 W.after_reversed(action, head, reversed)),
182 J.lex_seed_action(SCon{head, tail}, J.Outside{}), J.LexRaw{},
183 number_char_action(head, J.number_char(head), {==}, tail, state, evidence))),
184 Equal.trans(String,
185 W.prefix_reversed(tail, J.Outside{}, SCon{head, reversed}),
186 String.reverse(tail) ++ SCon{head, reversed},
187 String.reverse(SCon{head, tail}) ++ reversed,
188 number_prefix_reversed(tail, J.number_next(state, head), SCon{head, reversed},
189 number_valid_cons(head, tail, state, evidence)),
190 Equal.trans(String,
191 String.reverse(tail) ++ SCon{head, reversed},
192 (String.reverse(tail) ++ SCon{head, SNil{}}) ++ reversed,
193 String.reverse(SCon{head, tail}) ++ reversed,
194 Equal.sym(String, (String.reverse(tail) ++ SCon{head, SNil{}}) ++ reversed,
195 String.reverse(tail) ++ SCon{head, reversed},
196 S.append_assoc(String.reverse(tail), SCon{head, SNil{}}, reversed)),
197 Equal.cong(String, String, value => value ++ reversed,
198 String.reverse(tail) ++ SCon{head, SNil{}}, String.reverse(SCon{head, tail}),
199 Equal.sym(String, String.reverse(SCon{head, tail}), String.reverse(tail) ++ SCon{head, SNil{}},
200 S.reverse_cons(head, tail))))))
201
202
203def lex_number_valid(+text: String,
204 +state: J.NumberState,
205 +reversed: String,
206 +acc: List<&2, J.Lexeme>,
207 +evidence: {J.number_valid_end(J.number_valid_step(text, state)) == True{} : Bool}) -> {J.lex_scan(text, J.Outside{}, reversed, acc) == plain_lexemes(text, reversed, acc) : List<&2, J.Lexeme>}:
208 match text:
209 case SNil{}: {==}
210 case SCon{+head, +tail}:
211 Equal.trans(List<&2, J.Lexeme>,
212 J.lex_scan(text, J.Outside{}, reversed, acc),
213 J.lexemes(text, J.Outside{}, reversed, acc, J.LexRaw{}),
214 plain_lexemes(text, reversed, acc),
215 Equal.cong(J.LexAction, List<&2, J.Lexeme>, action => J.lexemes(text, J.Outside{}, reversed, acc, action),
216 J.lex_seed_action(text, J.Outside{}), J.LexRaw{},
217 number_char_action(head, J.number_char(head), {==}, tail, state, evidence)),
218 Equal.trans(List<&2, J.Lexeme>,
219 J.lexemes(text, J.Outside{}, reversed, acc, J.LexRaw{}),
220 J.lexemes(tail, J.Outside{}, SCon{head, reversed}, acc, J.lex_seed_action(tail, J.Outside{})),
221 plain_lexemes(text, reversed, acc),
222 {==},
223 lex_number_valid(tail, J.number_next(state, head), SCon{head, reversed}, acc,
224 number_valid_cons(head, tail, state, evidence))))
225
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)))))
281
282def lex_number_payload(+text: String,
283 +evidence: {J.number_valid(text) == True{} : Bool}) -> {J.lex_scan(text, J.Outside{}, SNil{}, Nil{}) == (J.Payload{text} <> Nil{}) : List<&2, J.Lexeme>}:
284 match text:
285 case SNil{}:
286 Empty.absurd({J.lex_scan(SNil{}, J.Outside{}, SNil{}, Nil{}) == (J.Payload{SNil{}} <> Nil{}) : List<&2, J.Lexeme>},
287 false_true(Equal.trans(Bool, False{}, J.number_valid(SNil{}), True{}, {==}, evidence)))
288 case SCon{+head, +tail}:
289 Equal.trans(List<&2, J.Lexeme>,
290 J.lex_scan(text, J.Outside{}, SNil{}, Nil{}),
291 J.lexemes(text, J.Outside{}, SNil{}, Nil{}, J.LexRaw{}),
292 J.Payload{text} <> Nil{},
293 Equal.cong(J.LexAction, List<&2, J.Lexeme>, action => J.lexemes(text, J.Outside{}, SNil{}, Nil{}, action),
294 J.lex_seed_action(text, J.Outside{}), J.LexRaw{},
295 number_char_action(head, J.number_char(head), {==}, tail, J.NumberStart{}, evidence)),
296 Equal.trans(List<&2, J.Lexeme>,
297 J.lexemes(text, J.Outside{}, SNil{}, Nil{}, J.LexRaw{}),
298 J.lex_scan(tail, J.Outside{}, SCon{head, SNil{}}, Nil{}),
299 J.Payload{text} <> Nil{},
300 {==},
301 Equal.trans(List<&2, J.Lexeme>,
302 J.lex_scan(tail, J.Outside{}, SCon{head, SNil{}}, Nil{}),
303 J.Payload{SCon{head, SNil{}} ++ tail} <> Nil{},
304 J.Payload{text} <> Nil{},
305 lex_number_tail(tail, J.number_next(J.NumberStart{}, head), head, SNil{}, head, SNil{}, {==},
306 number_valid_cons(head, tail, J.NumberStart{}, evidence)),
307 Equal.cong(String, List<&2, J.Lexeme>, s => J.Payload{s} <> Nil{},
308 SCon{head, SNil{}} ++ tail, text, {==}))))
309
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))))
367
368def lex_number_before_punctuation(+first: Char,
369 +number_tail: String,
370 +punctuation: Char,
371 +suffix: String,
372 +acc: List<&2, J.Lexeme>,
373 action: {J.lex_seed_action(SCon{punctuation, suffix}, J.Outside{}) == J.LexPunctuation{punctuation} : J.LexAction},
374 +evidence: {J.number_valid(SCon{first, number_tail}) == True{} : Bool}) -> {J.lex_scan(SCon{first, number_tail} ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc) == J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Payload{SCon{first, number_tail}} <> acc) : List<&2, J.Lexeme>}:
375 Equal.trans(List<&2, J.Lexeme>,
376 J.lex_scan(SCon{first, number_tail} ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc),
377 J.lex_scan(number_tail ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SCon{first, SNil{}}, acc),
378 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Payload{SCon{first, number_tail}} <> acc),
379 Equal.trans(List<&2, J.Lexeme>,
380 J.lex_scan(SCon{first, number_tail} ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc),
381 J.lex_scan(number_tail ++ (SCon{punctuation, SNil{}} ++ suffix),
382 W.after_mode(J.lex_seed_action(SCon{first, number_tail ++ (SCon{punctuation, SNil{}} ++ suffix)}, J.Outside{}), J.Outside{}),
383 W.after_reversed(J.lex_seed_action(SCon{first, number_tail ++ (SCon{punctuation, SNil{}} ++ suffix)}, J.Outside{}), first, SNil{}),
384 W.after_acc(J.lex_seed_action(SCon{first, number_tail ++ (SCon{punctuation, SNil{}} ++ suffix)}, J.Outside{}), first, SNil{}, acc)),
385 J.lex_scan(number_tail ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SCon{first, SNil{}}, acc),
386 W.lex_scan_step(first, number_tail ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc),
387 Equal.cong(J.LexAction, List<&2, J.Lexeme>, lex_action => J.lex_scan(number_tail ++ (SCon{punctuation, SNil{}} ++ suffix),
388 W.after_mode(lex_action, J.Outside{}), W.after_reversed(lex_action, first, SNil{}), W.after_acc(lex_action, first, SNil{}, acc)),
389 J.lex_seed_action(SCon{first, number_tail ++ (SCon{punctuation, SNil{}} ++ suffix)}, J.Outside{}), J.LexRaw{},
390 number_char_action(first, J.number_char(first), {==}, number_tail, J.NumberStart{}, evidence))),
391 lex_number_delimited_tail(number_tail, J.number_next(J.NumberStart{}, first), first, SNil{}, SCon{first, SNil{}},
392 punctuation, suffix, acc,
393 Equal.trans(String, String.reverse(SCon{first, SNil{}}), String.reverse(SNil{}) ++ SCon{first, SNil{}}, SCon{first, SNil{}},
394 S.reverse_cons(first, SNil{}), S.append_nil(SCon{first, SNil{}})),
395 action, number_valid_cons(first, number_tail, J.NumberStart{}, evidence)))
396
397def lex_certified_number_before_punctuation(+text: String,
398 +certificate: J.NumberCert<text>,
399 +punctuation: Char,
400 +suffix: String,
401 +acc: List<&2, J.Lexeme>,
402 action: {J.lex_seed_action(SCon{punctuation, suffix}, J.Outside{}) == J.LexPunctuation{punctuation} : J.LexAction}) -> {J.lex_scan(text ++ (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>}:
403 match text:
404 case SNil{}:
405 Empty.absurd({J.lex_scan(SNil{} ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc) ==
406 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Payload{SNil{}} <> acc) : List<&2, J.Lexeme>},
407 false_true(Equal.trans(Bool, False{}, J.number_valid(SNil{}), True{}, {==}, P.cert_valid(SNil{}, certificate))))
408 case SCon{head, tail}:
409 lex_number_before_punctuation(head, tail, punctuation, suffix, acc, action, P.cert_valid(text, certificate))