1module Compiler.IntegerLiteral
2
3import Std.Byte
4import Std.Word
5import Std.Natural
6import Data.Bytes
7import Model.Parameter
8import Model.Word64
9
10-- The compiler owns literal syntax and its failures. Std.Word owns arithmetic
11-- and codecs; this module deliberately does not expose those diagnostics.
12family IntegerLiteralRadix : Type 0
13constructor IntegerLiteralDecimal
14constructor IntegerLiteralBinary
15constructor IntegerLiteralHexadecimal
16
17end-family
18
19family IntegerLiteralSign : Type 0
20constructor IntegerLiteralPositive
21constructor IntegerLiteralNegative
22
23end-family
24
25family IntegerLiteralKind : Type 0
26constructor IntegerLiteralUnsigned
27constructor IntegerLiteralSigned
28
29end-family
30
31family IntegerLiteralWidth : Type 0
32constructor IntegerLiteralWidth8
33constructor IntegerLiteralWidth16
34constructor IntegerLiteralWidth32
35constructor IntegerLiteralWidth64
36
37end-family
38
39family IntegerLiteralFailure : Type 0
40constructor IntegerLiteralMissingDigits
41constructor IntegerLiteralBadDigit
42constructor IntegerLiteralBadSeparator
43constructor IntegerLiteralOutOfRange
44
45end-family
46
47family IntegerLiteralResult : Type 0
48constructor IntegerLiteralWord
49field unrestricted integerLiteralWidth : (family IntegerLiteralWidth)
50field unrestricted integerLiteralSign : (family IntegerLiteralSign)
51field unrestricted integerLiteralBytesLE : Bytes
52constructor IntegerLiteralFailed
53field unrestricted integerLiteralFailure : (family IntegerLiteralFailure)
54
55end-family
56
57family IntegerLiteralDigitResult : Type 0
58constructor IntegerLiteralDigitValue
59field unrestricted integerLiteralDigit : Nat
60constructor IntegerLiteralDigitFailed
61field unrestricted integerLiteralDigitFailure : (family IntegerLiteralFailure)
62
63end-family
64
65family IntegerLiteralFoldResult : Type 0
66constructor IntegerLiteralFoldValue
67field unrestricted integerLiteralFoldAccumulator : (family ModelWord64)
68constructor IntegerLiteralFoldFailed
69field unrestricted integerLiteralFoldFailure : (family IntegerLiteralFailure)
70
71end-family
72
73family IntegerLiteralU64StepResult : Type 0
74constructor IntegerLiteralU64StepSucceeded
75field unrestricted integerLiteralU64StepValue : (family ModelWord64)
76constructor IntegerLiteralU64StepFailed
77
78end-family
79
80family IntegerLiteralSyntaxResult : Type 0
81constructor IntegerLiteralSyntaxAccepted
82constructor IntegerLiteralSyntaxFailed
83field unrestricted integerLiteralSyntaxFailure : (family IntegerLiteralFailure)
84
85end-family
86
87def integerLiteralZero =
88 (constructor
89 ModelWord64
90 ModelWord64Value
91 (byte 0)
92 (byte 0)
93 (byte 0)
94 (byte 0)
95 (byte 0)
96 (byte 0)
97 (byte 0)
98 (byte 0))
99
100def integerLiteralOne =
101 (constructor
102 ModelWord64
103 ModelWord64Value
104 (byte 1)
105 (byte 0)
106 (byte 0)
107 (byte 0)
108 (byte 0)
109 (byte 0)
110 (byte 0)
111 (byte 0))
112
113def integerLiteralTwo =
114 (constructor
115 ModelWord64
116 ModelWord64Value
117 (byte 2)
118 (byte 0)
119 (byte 0)
120 (byte 0)
121 (byte 0)
122 (byte 0)
123 (byte 0)
124 (byte 0))
125
126def integerLiteralTen =
127 (constructor
128 ModelWord64
129 ModelWord64Value
130 (byte 10)
131 (byte 0)
132 (byte 0)
133 (byte 0)
134 (byte 0)
135 (byte 0)
136 (byte 0)
137 (byte 0))
138
139def integerLiteralSixteen =
140 (constructor
141 ModelWord64
142 ModelWord64Value
143 (byte 16)
144 (byte 0)
145 (byte 0)
146 (byte 0)
147 (byte 0)
148 (byte 0)
149 (byte 0)
150 (byte 0))
151
152def integerLiteralMaxU8 =
153 (constructor
154 ModelWord64
155 ModelWord64Value
156 (byte 255)
157 (byte 0)
158 (byte 0)
159 (byte 0)
160 (byte 0)
161 (byte 0)
162 (byte 0)
163 (byte 0))
164
165def integerLiteralMaxU16 =
166 (constructor
167 ModelWord64
168 ModelWord64Value
169 (byte 255)
170 (byte 255)
171 (byte 0)
172 (byte 0)
173 (byte 0)
174 (byte 0)
175 (byte 0)
176 (byte 0))
177
178def integerLiteralMaxU32 =
179 (constructor
180 ModelWord64
181 ModelWord64Value
182 (byte 255)
183 (byte 255)
184 (byte 255)
185 (byte 255)
186 (byte 0)
187 (byte 0)
188 (byte 0)
189 (byte 0))
190
191def integerLiteralMaxU64 =
192 (constructor
193 ModelWord64
194 ModelWord64Value
195 (byte 255)
196 (byte 255)
197 (byte 255)
198 (byte 255)
199 (byte 255)
200 (byte 255)
201 (byte 255)
202 (byte 255))
203
204def integerLiteralMaxI8 =
205 (constructor
206 ModelWord64
207 ModelWord64Value
208 (byte 127)
209 (byte 0)
210 (byte 0)
211 (byte 0)
212 (byte 0)
213 (byte 0)
214 (byte 0)
215 (byte 0))
216
217def integerLiteralMaxI16 =
218 (constructor
219 ModelWord64
220 ModelWord64Value
221 (byte 255)
222 (byte 127)
223 (byte 0)
224 (byte 0)
225 (byte 0)
226 (byte 0)
227 (byte 0)
228 (byte 0))
229
230def integerLiteralMaxI32 =
231 (constructor
232 ModelWord64
233 ModelWord64Value
234 (byte 255)
235 (byte 255)
236 (byte 255)
237 (byte 127)
238 (byte 0)
239 (byte 0)
240 (byte 0)
241 (byte 0))
242
243def integerLiteralMaxI64 =
244 (constructor
245 ModelWord64
246 ModelWord64Value
247 (byte 255)
248 (byte 255)
249 (byte 255)
250 (byte 255)
251 (byte 255)
252 (byte 255)
253 (byte 255)
254 (byte 127))
255
256def integerLiteralMinMagnitudeI8 =
257 (constructor
258 ModelWord64
259 ModelWord64Value
260 (byte 128)
261 (byte 0)
262 (byte 0)
263 (byte 0)
264 (byte 0)
265 (byte 0)
266 (byte 0)
267 (byte 0))
268
269def integerLiteralMinMagnitudeI16 =
270 (constructor
271 ModelWord64
272 ModelWord64Value
273 (byte 0)
274 (byte 128)
275 (byte 0)
276 (byte 0)
277 (byte 0)
278 (byte 0)
279 (byte 0)
280 (byte 0))
281
282def integerLiteralMinMagnitudeI32 =
283 (constructor
284 ModelWord64
285 ModelWord64Value
286 (byte 0)
287 (byte 0)
288 (byte 0)
289 (byte 128)
290 (byte 0)
291 (byte 0)
292 (byte 0)
293 (byte 0))
294
295def integerLiteralMinMagnitudeI64 =
296 (constructor
297 ModelWord64
298 ModelWord64Value
299 (byte 0)
300 (byte 0)
301 (byte 0)
302 (byte 0)
303 (byte 0)
304 (byte 0)
305 (byte 0)
306 (byte 128))
307
308def integerLiteralDigitWord =
309 (lambda unrestricted digit : Byte .
310 (constructor
311 ModelWord64
312 ModelWord64Value
313 digit
314 (byte 0)
315 (byte 0)
316 (byte 0)
317 (byte 0)
318 (byte 0)
319 (byte 0)
320 (byte 0)))
321
322def integerLiteralFailureResult =
323 (lambda unrestricted failure : (family IntegerLiteralFailure) .
324 (constructor IntegerLiteralResult IntegerLiteralFailed failure))
325
326def integerLiteralBadDigitResult =
327 (constructor
328 IntegerLiteralDigitResult
329 IntegerLiteralDigitFailed
330 (constructor IntegerLiteralFailure IntegerLiteralBadDigit))
331
332def integerLiteralChoose =
333 (lambda unrestricted condition : Nat .
334 (lambda unrestricted whenTrue : (family IntegerLiteralDigitResult) .
335 (lambda unrestricted whenFalse : (family IntegerLiteralDigitResult) .
336 (nat-eliminate
337 (lambda unrestricted current : Nat . (family IntegerLiteralDigitResult))
338 whenFalse
339 (lambda unrestricted predecessor : Nat .
340 (lambda unrestricted induction : (family IntegerLiteralDigitResult) . whenTrue))
341 condition))))
342
343def integerLiteralDecodeDecimal =
344 (lambda unrestricted value : Byte .
345 (nat-eliminate
346 (lambda unrestricted current : Nat . (family IntegerLiteralDigitResult))
347 integerLiteralBadDigitResult
348 (lambda unrestricted predecessor : Nat .
349 (lambda unrestricted induction : (family IntegerLiteralDigitResult) .
350 (nat-eliminate
351 (lambda unrestricted current : Nat . (family IntegerLiteralDigitResult))
352 integerLiteralBadDigitResult
353 (lambda unrestricted predecessorAgain : Nat .
354 (lambda unrestricted inductionAgain : (family IntegerLiteralDigitResult) .
355 (constructor
356 IntegerLiteralDigitResult
357 IntegerLiteralDigitValue
358 (naturalSaturatingSubtract (byte-to-nat value) (byte-to-nat (byte 48))))))
359 (byte-less-than value (byte 58)))))
360 (byte-less-than (byte 47) value)))
361
362def integerLiteralDecodeBinary =
363 (lambda unrestricted value : Byte .
364 (nat-eliminate
365 (lambda unrestricted current : Nat . (family IntegerLiteralDigitResult))
366 integerLiteralBadDigitResult
367 (lambda unrestricted predecessor : Nat .
368 (lambda unrestricted induction : (family IntegerLiteralDigitResult) .
369 (nat-eliminate
370 (lambda unrestricted current : Nat . (family IntegerLiteralDigitResult))
371 integerLiteralBadDigitResult
372 (lambda unrestricted predecessorAgain : Nat .
373 (lambda unrestricted inductionAgain : (family IntegerLiteralDigitResult) .
374 (constructor
375 IntegerLiteralDigitResult
376 IntegerLiteralDigitValue
377 (naturalSaturatingSubtract (byte-to-nat value) (byte-to-nat (byte 48))))))
378 (byte-less-than value (byte 50)))))
379 (byte-less-than (byte 47) value)))
380
381def integerLiteralDecodeHexLetter =
382 (lambda unrestricted value : Byte .
383 (integerLiteralChoose
384 (stdFlagAnd (byte-less-than (byte 64) value) (byte-less-than value (byte 71)))
385 (constructor
386 IntegerLiteralDigitResult
387 IntegerLiteralDigitValue
388 (naturalSaturatingSubtract (byte-to-nat value) (byte-to-nat (byte 55))))
389 (integerLiteralChoose
390 (stdFlagAnd (byte-less-than (byte 96) value) (byte-less-than value (byte 103)))
391 (constructor
392 IntegerLiteralDigitResult
393 IntegerLiteralDigitValue
394 (naturalSaturatingSubtract (byte-to-nat value) (byte-to-nat (byte 87))))
395 integerLiteralBadDigitResult)))
396
397def integerLiteralDecodeHex =
398 (lambda unrestricted value : Byte .
399 (eliminate
400 IntegerLiteralDigitResult
401 (lambda unrestricted current : (family IntegerLiteralDigitResult) .
402 (family IntegerLiteralDigitResult))
403 (integerLiteralDecodeDecimal value)
404 (branch
405 IntegerLiteralDigitValue
406 digit
407 .
408 (constructor IntegerLiteralDigitResult IntegerLiteralDigitValue digit))
409 (branch IntegerLiteralDigitFailed failure . (integerLiteralDecodeHexLetter value))))
410
411def integerLiteralDecodeDigit =
412 (lambda unrestricted radix : (family IntegerLiteralRadix) .
413 (lambda unrestricted value : Byte .
414 (eliminate
415 IntegerLiteralRadix
416 (lambda unrestricted current : (family IntegerLiteralRadix) .
417 (family IntegerLiteralDigitResult))
418 radix
419 (branch IntegerLiteralDecimal . (integerLiteralDecodeDecimal value))
420 (branch IntegerLiteralBinary . (integerLiteralDecodeBinary value))
421 (branch IntegerLiteralHexadecimal . (integerLiteralDecodeHex value)))))
422
423def integerLiteralRadixWord =
424 (lambda unrestricted radix : (family IntegerLiteralRadix) .
425 (eliminate
426 IntegerLiteralRadix
427 (lambda unrestricted current : (family IntegerLiteralRadix) . (family ModelWord64))
428 radix
429 (branch IntegerLiteralDecimal . integerLiteralTen)
430 (branch IntegerLiteralBinary . integerLiteralTwo)
431 (branch IntegerLiteralHexadecimal . integerLiteralSixteen)))
432
433-- Source radices are fixed by the grammar. Checked addition chains avoid
434-- a general 64-step multiply per digit, while Std.Word remains the arithmetic
435-- owner. Every intermediate fits whenever the final nonnegative product fits;
436-- an intermediate overflow therefore proves the literal cannot fit U64.
437def integerLiteralCheckedAdd =
438 (lambda unrestricted left : (family ModelWord64) .
439 (lambda unrestricted right : (family ModelWord64) .
440 (eliminate
441 ModelWord64CheckedResult
442 (lambda unrestricted current : (family ModelWord64CheckedResult) .
443 (family IntegerLiteralU64StepResult))
444 (stdU64AddChecked left right)
445 (branch
446 ModelWord64CheckedSucceeded
447 value
448 .
449 (constructor IntegerLiteralU64StepResult IntegerLiteralU64StepSucceeded value))
450 (branch
451 ModelWord64CheckedFailed
452 error
453 .
454 (constructor IntegerLiteralU64StepResult IntegerLiteralU64StepFailed)))))
455
456def integerLiteralThen =
457 (lambda unrestricted step : (family IntegerLiteralU64StepResult) .
458 (lambda unrestricted continue : (pi unrestricted value : (family ModelWord64) . (family IntegerLiteralU64StepResult)) .
459 (eliminate
460 IntegerLiteralU64StepResult
461 (lambda unrestricted current : (family IntegerLiteralU64StepResult) .
462 (family IntegerLiteralU64StepResult))
463 step
464 (branch IntegerLiteralU64StepSucceeded value . (continue value))
465 (branch
466 IntegerLiteralU64StepFailed
467 .
468 (constructor IntegerLiteralU64StepResult IntegerLiteralU64StepFailed)))))
469
470def integerLiteralScale =
471 (lambda unrestricted radix : (family IntegerLiteralRadix) .
472 (lambda unrestricted accumulator : (family ModelWord64) .
473 (eliminate
474 IntegerLiteralRadix
475 (lambda unrestricted current : (family IntegerLiteralRadix) .
476 (family IntegerLiteralU64StepResult))
477 radix
478 (branch
479 IntegerLiteralDecimal
480 .
481 (integerLiteralThen
482 (integerLiteralCheckedAdd accumulator accumulator)
483 (lambda unrestricted twice : (family ModelWord64) .
484 (integerLiteralThen
485 (integerLiteralCheckedAdd twice twice)
486 (lambda unrestricted four : (family ModelWord64) .
487 (integerLiteralThen
488 (integerLiteralCheckedAdd four four)
489 (lambda unrestricted eight : (family ModelWord64) .
490 (integerLiteralCheckedAdd eight twice))))))))
491 (branch IntegerLiteralBinary . (integerLiteralCheckedAdd accumulator accumulator))
492 (branch
493 IntegerLiteralHexadecimal
494 .
495 (integerLiteralThen
496 (integerLiteralCheckedAdd accumulator accumulator)
497 (lambda unrestricted twice : (family ModelWord64) .
498 (integerLiteralThen
499 (integerLiteralCheckedAdd twice twice)
500 (lambda unrestricted four : (family ModelWord64) .
501 (integerLiteralThen
502 (integerLiteralCheckedAdd four four)
503 (lambda unrestricted eight : (family ModelWord64) .
504 (integerLiteralCheckedAdd eight eight)))))))))))
505
506def integerLiteralStep =
507 (lambda unrestricted radix : (family IntegerLiteralRadix) .
508 (lambda unrestricted accumulator : (family ModelWord64) .
509 (lambda unrestricted digit : Byte .
510 (integerLiteralThen
511 (integerLiteralScale radix accumulator)
512 (lambda unrestricted scaled : (family ModelWord64) .
513 (integerLiteralCheckedAdd scaled (integerLiteralDigitWord digit)))))))
514
515def integerLiteralStepBytes =
516 (lambda unrestricted radix : (family IntegerLiteralRadix) .
517 (lambda unrestricted accumulator : (family ModelWord64) .
518 (lambda unrestricted digit : Byte .
519 (eliminate
520 IntegerLiteralU64StepResult
521 (lambda unrestricted current : (family IntegerLiteralU64StepResult) . Bytes)
522 (integerLiteralStep radix accumulator digit)
523 (branch IntegerLiteralU64StepSucceeded value . (Std.Word/stdU64EncodeLE value))
524 (branch IntegerLiteralU64StepFailed . b"")))))
525
526-- Branches are suspended: the evaluator is strict in application arguments.
527-- Calling the continuation in both value arguments would double the remaining
528-- validation work at each byte, even when only one branch is selected.
529def integerLiteralChooseSyntax =
530 (lambda unrestricted condition : Nat .
531 (lambda unrestricted whenTrue : (pi unrestricted ignored : Nat . (family IntegerLiteralSyntaxResult)) .
532 (lambda unrestricted whenFalse : (pi unrestricted ignored : Nat . (family IntegerLiteralSyntaxResult)) .
533 (app
534 (nat-eliminate
535 (lambda unrestricted current : Nat .
536 (pi unrestricted ignored : Nat . (family IntegerLiteralSyntaxResult)))
537 whenFalse
538 (lambda unrestricted predecessor : Nat .
539 (lambda unrestricted induction : (pi unrestricted ignored : Nat . (family IntegerLiteralSyntaxResult)) .
540 whenTrue))
541 condition)
542 zero))))
543
544-- A separator has a valid radix digit on both sides. The continuation
545-- carries only that preceding-digit fact; arithmetic starts after validation.
546def integerLiteralDigitValid =
547 (lambda unrestricted radix : (family IntegerLiteralRadix) .
548 (lambda unrestricted value : Byte .
549 (eliminate
550 IntegerLiteralDigitResult
551 (lambda unrestricted current : (family IntegerLiteralDigitResult) . Nat)
552 (integerLiteralDecodeDigit radix value)
553 (branch IntegerLiteralDigitValue digit . (succ zero))
554 (branch IntegerLiteralDigitFailed failure . zero))))
555
556def integerLiteralSeparatorStep =
557 (lambda unrestricted radix : (family IntegerLiteralRadix) .
558 (lambda unrestricted head : Byte .
559 (lambda unrestricted tail : Bytes .
560 (lambda unrestricted continue : (pi unrestricted previousWasDigit : Nat . (family IntegerLiteralSyntaxResult)) .
561 (lambda unrestricted previousWasDigit : Nat .
562 (integerLiteralChooseSyntax
563 (byte-equal head (byte 95))
564 (lambda unrestricted ignored : Nat .
565 (integerLiteralChooseSyntax
566 (stdFlagAnd previousWasDigit (integerLiteralDigitValid radix (bytes-head tail)))
567 (lambda unrestricted ignored : Nat . (continue zero))
568 (lambda unrestricted ignored : Nat .
569 (constructor
570 IntegerLiteralSyntaxResult
571 IntegerLiteralSyntaxFailed
572 (constructor IntegerLiteralFailure IntegerLiteralBadSeparator)))))
573 (lambda unrestricted ignored : Nat .
574 (eliminate
575 IntegerLiteralDigitResult
576 (lambda unrestricted current : (family IntegerLiteralDigitResult) .
577 (family IntegerLiteralSyntaxResult))
578 (integerLiteralDecodeDigit radix head)
579 (branch IntegerLiteralDigitValue digit . (continue (succ zero)))
580 (branch
581 IntegerLiteralDigitFailed
582 failure
583 .
584 (constructor IntegerLiteralSyntaxResult IntegerLiteralSyntaxFailed failure))))))))))
585
586def integerLiteralValidateSeparators =
587 (lambda unrestricted radix : (family IntegerLiteralRadix) .
588 (lambda unrestricted digits : Bytes .
589 (app
590 (bytes-eliminate
591 (lambda unrestricted remaining : Bytes .
592 (pi unrestricted previousWasDigit : Nat . (family IntegerLiteralSyntaxResult)))
593 (lambda unrestricted previousWasDigit : Nat .
594 (integerLiteralChooseSyntax
595 previousWasDigit
596 (lambda unrestricted ignored : Nat .
597 (constructor IntegerLiteralSyntaxResult IntegerLiteralSyntaxAccepted))
598 (lambda unrestricted ignored : Nat .
599 (constructor
600 IntegerLiteralSyntaxResult
601 IntegerLiteralSyntaxFailed
602 (constructor IntegerLiteralFailure IntegerLiteralBadSeparator)))))
603 (integerLiteralSeparatorStep radix)
604 digits)
605 zero)))
606
607def integerLiteralStripSeparators =
608 (lambda unrestricted digits : Bytes .
609 (bytes-eliminate
610 (lambda unrestricted remaining : Bytes . Bytes)
611 b""
612 (lambda unrestricted head : Byte .
613 (lambda unrestricted tail : Bytes .
614 (lambda unrestricted slots : Bytes .
615 (nat-eliminate
616 (lambda unrestricted current : Nat . Bytes)
617 (bytes-cons head slots)
618 (lambda unrestricted predecessor : Nat .
619 (lambda unrestricted induction : Bytes . slots))
620 (byte-equal head (byte 95))))))
621 digits))
622
623def integerLiteralFoldDigits =
624 (lambda unrestricted radix : (family IntegerLiteralRadix) .
625 (lambda unrestricted digits : Bytes .
626 (app
627 (bytes-eliminate
628 (lambda unrestricted remaining : Bytes .
629 (pi unrestricted accumulator : (family ModelWord64) . (family IntegerLiteralFoldResult)))
630 (lambda unrestricted accumulator : (family ModelWord64) .
631 (constructor IntegerLiteralFoldResult IntegerLiteralFoldValue accumulator))
632 (lambda unrestricted head : Byte .
633 (lambda unrestricted tail : Bytes .
634 (lambda unrestricted continue : (pi unrestricted accumulator : (family ModelWord64) . (family IntegerLiteralFoldResult)) .
635 (lambda unrestricted accumulator : (family ModelWord64) .
636 (eliminate
637 IntegerLiteralDigitResult
638 (lambda unrestricted current : (family IntegerLiteralDigitResult) .
639 (family IntegerLiteralFoldResult))
640 (integerLiteralDecodeDigit radix head)
641 (branch
642 IntegerLiteralDigitValue
643 digit
644 .
645 (eliminate
646 IntegerLiteralU64StepResult
647 (lambda unrestricted current : (family IntegerLiteralU64StepResult) .
648 (family IntegerLiteralFoldResult))
649 (integerLiteralStep radix accumulator (nat-to-byte digit))
650 (branch IntegerLiteralU64StepSucceeded next . (continue next))
651 (branch
652 IntegerLiteralU64StepFailed
653 .
654 (constructor
655 IntegerLiteralFoldResult
656 IntegerLiteralFoldFailed
657 (constructor IntegerLiteralFailure IntegerLiteralOutOfRange)))))
658 (branch
659 IntegerLiteralDigitFailed
660 failure
661 .
662 (constructor IntegerLiteralFoldResult IntegerLiteralFoldFailed failure)))))))
663 digits)
664 integerLiteralZero)))
665
666def integerLiteralLessOrEqual =
667 (lambda unrestricted left : (family ModelWord64) .
668 (lambda unrestricted right : (family ModelWord64) .
669 -- Unsigned words form a total order. Negating the reverse comparison
670 -- avoids the general XOR-based equality implementation at this boundary.
671 (stdFlagNot (stdU64LessThan right left))))
672
673def integerLiteralUnsignedBound =
674 (lambda unrestricted width : (family IntegerLiteralWidth) .
675 (eliminate
676 IntegerLiteralWidth
677 (lambda unrestricted current : (family IntegerLiteralWidth) . (family ModelWord64))
678 width
679 (branch IntegerLiteralWidth8 . integerLiteralMaxU8)
680 (branch IntegerLiteralWidth16 . integerLiteralMaxU16)
681 (branch IntegerLiteralWidth32 . integerLiteralMaxU32)
682 (branch IntegerLiteralWidth64 . integerLiteralMaxU64)))
683
684def integerLiteralSignedPositiveBound =
685 (lambda unrestricted width : (family IntegerLiteralWidth) .
686 (eliminate
687 IntegerLiteralWidth
688 (lambda unrestricted current : (family IntegerLiteralWidth) . (family ModelWord64))
689 width
690 (branch IntegerLiteralWidth8 . integerLiteralMaxI8)
691 (branch IntegerLiteralWidth16 . integerLiteralMaxI16)
692 (branch IntegerLiteralWidth32 . integerLiteralMaxI32)
693 (branch IntegerLiteralWidth64 . integerLiteralMaxI64)))
694
695def integerLiteralSignedNegativeBound =
696 (lambda unrestricted width : (family IntegerLiteralWidth) .
697 (eliminate
698 IntegerLiteralWidth
699 (lambda unrestricted current : (family IntegerLiteralWidth) . (family ModelWord64))
700 width
701 (branch IntegerLiteralWidth8 . integerLiteralMinMagnitudeI8)
702 (branch IntegerLiteralWidth16 . integerLiteralMinMagnitudeI16)
703 (branch IntegerLiteralWidth32 . integerLiteralMinMagnitudeI32)
704 (branch IntegerLiteralWidth64 . integerLiteralMinMagnitudeI64)))
705
706def integerLiteralEncodeWidth =
707 (lambda unrestricted width : (family IntegerLiteralWidth) .
708 (lambda unrestricted value : (family ModelWord64) .
709 (eliminate
710 ModelWord64
711 (lambda unrestricted current : (family ModelWord64) . Bytes)
712 value
713 (branch
714 ModelWord64Value
715 b0
716 b1
717 b2
718 b3
719 b4
720 b5
721 b6
722 b7
723 .
724 (eliminate
725 IntegerLiteralWidth
726 (lambda unrestricted current : (family IntegerLiteralWidth) . Bytes)
727 width
728 (branch IntegerLiteralWidth8 . (bytes b0))
729 (branch IntegerLiteralWidth16 . (bytes b0 b1))
730 (branch IntegerLiteralWidth32 . (bytes b0 b1 b2 b3))
731 (branch IntegerLiteralWidth64 . (bytes b0 b1 b2 b3 b4 b5 b6 b7)))))))
732
733def integerLiteralFinish =
734 (lambda unrestricted kind : (family IntegerLiteralKind) .
735 (lambda unrestricted sign : (family IntegerLiteralSign) .
736 (lambda unrestricted width : (family IntegerLiteralWidth) .
737 (lambda unrestricted folded : (family IntegerLiteralFoldResult) .
738 (eliminate
739 IntegerLiteralFoldResult
740 (lambda unrestricted current : (family IntegerLiteralFoldResult) .
741 (family IntegerLiteralResult))
742 folded
743 (branch
744 IntegerLiteralFoldValue
745 magnitude
746 .
747 (eliminate
748 IntegerLiteralSign
749 (lambda unrestricted current : (family IntegerLiteralSign) .
750 (family IntegerLiteralResult))
751 sign
752 (branch
753 IntegerLiteralPositive
754 .
755 (nat-eliminate
756 (lambda unrestricted current : Nat . (family IntegerLiteralResult))
757 (constructor
758 IntegerLiteralResult
759 IntegerLiteralFailed
760 (constructor IntegerLiteralFailure IntegerLiteralOutOfRange))
761 (lambda unrestricted predecessor : Nat .
762 (lambda unrestricted induction : (family IntegerLiteralResult) .
763 (constructor
764 IntegerLiteralResult
765 IntegerLiteralWord
766 width
767 sign
768 (integerLiteralEncodeWidth width magnitude))))
769 (integerLiteralLessOrEqual
770 magnitude
771 (eliminate
772 IntegerLiteralKind
773 (lambda unrestricted current : (family IntegerLiteralKind) .
774 (family ModelWord64))
775 kind
776 (branch IntegerLiteralUnsigned . (integerLiteralUnsignedBound width))
777 (branch IntegerLiteralSigned . (integerLiteralSignedPositiveBound width))))))
778 (branch
779 IntegerLiteralNegative
780 .
781 (eliminate
782 IntegerLiteralKind
783 (lambda unrestricted current : (family IntegerLiteralKind) .
784 (family IntegerLiteralResult))
785 kind
786 (branch
787 IntegerLiteralUnsigned
788 .
789 (constructor
790 IntegerLiteralResult
791 IntegerLiteralFailed
792 (constructor IntegerLiteralFailure IntegerLiteralOutOfRange)))
793 (branch
794 IntegerLiteralSigned
795 .
796 (nat-eliminate
797 (lambda unrestricted current : Nat . (family IntegerLiteralResult))
798 (constructor
799 IntegerLiteralResult
800 IntegerLiteralFailed
801 (constructor IntegerLiteralFailure IntegerLiteralOutOfRange))
802 (lambda unrestricted predecessor : Nat .
803 (lambda unrestricted induction : (family IntegerLiteralResult) .
804 (constructor
805 IntegerLiteralResult
806 IntegerLiteralWord
807 width
808 sign
809 (integerLiteralEncodeWidth
810 width
811 (stdU64SubtractWrapping integerLiteralZero magnitude)))))
812 (integerLiteralLessOrEqual
813 magnitude
814 (integerLiteralSignedNegativeBound width))))))))
815 (branch
816 IntegerLiteralFoldFailed
817 failure
818 .
819 (constructor IntegerLiteralResult IntegerLiteralFailed failure)))))))
820
821-- Inspect only the first byte. This keeps the empty/nonempty decision
822-- bounded instead of materializing bytes-length as a second unary traversal
823-- before the checked digit fold.
824def integerLiteralHasDigits =
825 (lambda unrestricted digits : Bytes .
826 (bytes-eliminate
827 (lambda unrestricted remaining : Bytes . Nat)
828 zero
829 (lambda unrestricted head : Byte .
830 (lambda unrestricted tail : Bytes . (lambda unrestricted continue : Nat . (succ zero))))
831 digits))
832
833def integerLiteralParse =
834 (lambda unrestricted radix : (family IntegerLiteralRadix) .
835 (lambda unrestricted kind : (family IntegerLiteralKind) .
836 (lambda unrestricted sign : (family IntegerLiteralSign) .
837 (lambda unrestricted width : (family IntegerLiteralWidth) .
838 (lambda unrestricted digits : Bytes .
839 (nat-eliminate
840 (lambda unrestricted current : Nat . (family IntegerLiteralResult))
841 (integerLiteralFailureResult
842 (constructor IntegerLiteralFailure IntegerLiteralMissingDigits))
843 (lambda unrestricted predecessor : Nat .
844 (lambda unrestricted induction : (family IntegerLiteralResult) .
845 (eliminate
846 IntegerLiteralSyntaxResult
847 (lambda unrestricted current : (family IntegerLiteralSyntaxResult) .
848 (family IntegerLiteralResult))
849 (integerLiteralValidateSeparators radix digits)
850 (branch
851 IntegerLiteralSyntaxAccepted
852 .
853 (integerLiteralFinish
854 kind
855 sign
856 width
857 (integerLiteralFoldDigits radix (integerLiteralStripSeparators digits))))
858 (branch
859 IntegerLiteralSyntaxFailed
860 failure
861 .
862 (integerLiteralFailureResult failure)))))
863 (integerLiteralHasDigits digits)))))))
864
865-- The public parser is intentionally continuation-shaped: bytes-eliminate
866-- visits source bytes in order, so malformed syntax is observed before any
867-- later arithmetic result can be accepted. The radix-specific digit checker
868-- is kept as a separate owner for the future lexer bridge.
869def integerLiteralParseEmpty =
870 (lambda unrestricted radix : (family IntegerLiteralRadix) .
871 (lambda unrestricted sign : (family IntegerLiteralSign) .
872 (lambda unrestricted width : (family IntegerLiteralWidth) .
873 (integerLiteralFailureResult
874 (constructor IntegerLiteralFailure IntegerLiteralMissingDigits)))))
875
876def integerLiteralFailureTag =
877 (lambda unrestricted failure : (family IntegerLiteralFailure) .
878 (eliminate
879 IntegerLiteralFailure
880 (lambda unrestricted current : (family IntegerLiteralFailure) . Nat)
881 failure
882 (branch IntegerLiteralMissingDigits . (succ zero))
883 (branch IntegerLiteralBadDigit . (succ (succ zero)))
884 (branch IntegerLiteralBadSeparator . (succ (succ (succ zero))))
885 (branch IntegerLiteralOutOfRange . (succ (succ (succ (succ zero)))))))
886
887def integerLiteralResultBytes =
888 (lambda unrestricted result : (family IntegerLiteralResult) .
889 (eliminate
890 IntegerLiteralResult
891 (lambda unrestricted current : (family IntegerLiteralResult) . Bytes)
892 result
893 (branch IntegerLiteralWord width sign bytes . bytes)
894 (branch IntegerLiteralFailed failure . b"")))
895
896def integerLiteralResultFailureTag =
897 (lambda unrestricted result : (family IntegerLiteralResult) .
898 (eliminate
899 IntegerLiteralResult
900 (lambda unrestricted current : (family IntegerLiteralResult) . Nat)
901 result
902 (branch IntegerLiteralWord width sign bytes . zero)
903 (branch IntegerLiteralFailed failure . (integerLiteralFailureTag failure))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.