1module Compiler.QuotedLiteral
2
3import Compiler.IntegerLiteral
4import Std.Natural
5import Data.UTF8
6import Model.Config
7import Model.Word32
8import Std.Byte
9import Std.Foundation
10
11family QuotedLiteralFailure : Type 0
12constructor QuotedInvalidPrefix
13constructor QuotedUnknownEscape
14constructor QuotedIncompleteEscape
15constructor QuotedBadHex
16constructor QuotedNonASCII
17constructor QuotedNewline
18constructor QuotedUnterminated
19constructor QuotedTrailingInput
20constructor QuotedUnicodeSyntax
21constructor QuotedInvalidScalar
22constructor QuotedInvalidUTF8
23
24end-family
25
26family QuotedLiteralResult : Type 0
27constructor QuotedLiteralDecoded
28field unrestricted quotedDecodedBytes : Bytes
29constructor QuotedLiteralFailed
30field unrestricted quotedFailure : (family QuotedLiteralFailure)
31field unrestricted quotedFailureByte : Nat
32field unrestricted quotedFailureEndByte : Nat
33
34end-family
35
36family QuotedByteState : Type 0
37constructor QuotedNormal
38constructor QuotedEscape
39field unrestricted escapeStart : Nat
40constructor QuotedHexHigh
41field unrestricted hexStart : Nat
42constructor QuotedHexLow
43field unrestricted lowHexStart : Nat
44field unrestricted highHexDigit : Nat
45constructor QuotedFailureTail
46field unrestricted failureTailKind : (family QuotedLiteralFailure)
47field unrestricted failureTailStart : Nat
48field unrestricted failureTailRemaining : Nat
49constructor QuotedClosed
50
51end-family
52
53family QuotedTextState : Type 0
54constructor QuotedTextNormal
55constructor QuotedTextEscape
56field unrestricted textEscapeStart : Nat
57constructor QuotedTextUnicodeOpen
58field unrestricted unicodeOpenStart : Nat
59constructor QuotedTextUnicodeDigits
60field unrestricted unicodeDigitsStart : Nat
61field unrestricted unicodeDigitCount : Nat
62field unrestricted unicodeAccumulator : (family ModelWord32)
63constructor QuotedTextClosed
64
65end-family
66
67-- Continuations are forced only for the selected transition.
68def quotedChoose =
69 (lambda unrestricted condition : Nat .
70 (lambda unrestricted yes : (pi unrestricted force : Nat . (family QuotedLiteralResult)) .
71 (lambda unrestricted no : (pi unrestricted force : Nat . (family QuotedLiteralResult)) .
72 (app
73 (nat-eliminate
74 (lambda unrestricted flag : Nat .
75 (pi unrestricted force : Nat . (family QuotedLiteralResult)))
76 no
77 (lambda unrestricted predecessor : Nat .
78 (lambda unrestricted unused : (pi unrestricted force : Nat . (family QuotedLiteralResult)) .
79 yes))
80 condition)
81 zero))))
82
83def quotedPrepend =
84 (lambda unrestricted head : Byte .
85 (lambda unrestricted result : (family QuotedLiteralResult) .
86 (eliminate
87 QuotedLiteralResult
88 (lambda unrestricted value : (family QuotedLiteralResult) . (family QuotedLiteralResult))
89 result
90 (branch
91 QuotedLiteralDecoded
92 bytes
93 .
94 (constructor QuotedLiteralResult QuotedLiteralDecoded (bytes-cons head bytes)))
95 (branch
96 QuotedLiteralFailed
97 failure
98 offset
99 endOffset
100 .
101 (constructor QuotedLiteralResult QuotedLiteralFailed failure offset endOffset)))))
102
103-- A quoted recovery fragment stops before a delimiter or physical newline.
104def quotedRecoveryBoundary =
105 (lambda unrestricted value : Byte .
106 (Std.Natural/naturalOr
107 (byte-equal value (byte 34))
108 (Std.Natural/naturalOr (byte-equal value (byte 10)) (byte-equal value (byte 13)))))
109
110def quotedByteStep =
111 (lambda unrestricted head : Byte .
112 (lambda unrestricted state : (family QuotedByteState) .
113 (lambda unrestricted offset : Nat .
114 (lambda unrestricted continue : (pi unrestricted state : (family QuotedByteState) . (pi unrestricted offset : Nat . (family QuotedLiteralResult))) .
115 (eliminate
116 QuotedByteState
117 (lambda unrestricted current : (family QuotedByteState) . (family QuotedLiteralResult))
118 state
119 (branch
120 QuotedNormal
121 .
122 (quotedChoose
123 (byte-equal head (byte 13))
124 (lambda unrestricted force : Nat .
125 (constructor
126 QuotedLiteralResult
127 QuotedLiteralFailed
128 (constructor QuotedLiteralFailure QuotedNewline)
129 offset
130 (succ offset)))
131 (lambda unrestricted force : Nat .
132 (quotedChoose
133 (byte-equal head (byte 10))
134 (lambda unrestricted force : Nat .
135 (constructor
136 QuotedLiteralResult
137 QuotedLiteralFailed
138 (constructor QuotedLiteralFailure QuotedNewline)
139 offset
140 (succ offset)))
141 (lambda unrestricted force : Nat .
142 (quotedChoose
143 (byte-equal head (byte 34))
144 (lambda unrestricted force : Nat .
145 (continue (constructor QuotedByteState QuotedClosed) (succ offset)))
146 (lambda unrestricted force : Nat .
147 (quotedChoose
148 (byte-equal head (byte 92))
149 (lambda unrestricted force : Nat .
150 (continue
151 (constructor QuotedByteState QuotedEscape offset)
152 (succ offset)))
153 (lambda unrestricted force : Nat .
154 (quotedChoose
155 (byte-less-than head (byte 128))
156 (lambda unrestricted force : Nat .
157 (quotedPrepend
158 head
159 (continue
160 (constructor QuotedByteState QuotedNormal)
161 (succ offset))))
162 (lambda unrestricted force : Nat .
163 (continue
164 (constructor
165 QuotedByteState
166 QuotedFailureTail
167 (constructor QuotedLiteralFailure QuotedNonASCII)
168 offset
169 zero)
170 (succ offset)))))))))))))
171 (branch
172 QuotedEscape
173 start
174 .
175 (quotedChoose
176 (byte-equal head (byte 13))
177 (lambda unrestricted force : Nat .
178 (constructor
179 QuotedLiteralResult
180 QuotedLiteralFailed
181 (constructor QuotedLiteralFailure QuotedNewline)
182 offset
183 (succ offset)))
184 (lambda unrestricted force : Nat .
185 (quotedChoose
186 (byte-equal head (byte 10))
187 (lambda unrestricted force : Nat .
188 (constructor
189 QuotedLiteralResult
190 QuotedLiteralFailed
191 (constructor QuotedLiteralFailure QuotedNewline)
192 offset
193 (succ offset)))
194 (lambda unrestricted force : Nat .
195 (quotedChoose
196 (byte-equal head (byte 92))
197 (lambda unrestricted force : Nat .
198 (quotedPrepend
199 (byte 92)
200 (continue (constructor QuotedByteState QuotedNormal) (succ offset))))
201 (lambda unrestricted force : Nat .
202 (quotedChoose
203 (byte-equal head (byte 34))
204 (lambda unrestricted force : Nat .
205 (quotedPrepend
206 (byte 34)
207 (continue (constructor QuotedByteState QuotedNormal) (succ offset))))
208 (lambda unrestricted force : Nat .
209 (quotedChoose
210 (byte-equal head (byte 114))
211 (lambda unrestricted force : Nat .
212 (quotedPrepend
213 (byte 13)
214 (continue
215 (constructor QuotedByteState QuotedNormal)
216 (succ offset))))
217 (lambda unrestricted force : Nat .
218 (quotedChoose
219 (byte-equal head (byte 116))
220 (lambda unrestricted force : Nat .
221 (quotedPrepend
222 (byte 9)
223 (continue
224 (constructor QuotedByteState QuotedNormal)
225 (succ offset))))
226 (lambda unrestricted force : Nat .
227 (quotedChoose
228 (byte-equal head (byte 110))
229 (lambda unrestricted force : Nat .
230 (quotedPrepend
231 (byte 10)
232 (continue
233 (constructor QuotedByteState QuotedNormal)
234 (succ offset))))
235 (lambda unrestricted force : Nat .
236 (quotedChoose
237 (byte-equal head (byte 120))
238 (lambda unrestricted force : Nat .
239 (continue
240 (constructor QuotedByteState QuotedHexHigh start)
241 (succ offset)))
242 (lambda unrestricted force : Nat .
243 (continue
244 (constructor
245 QuotedByteState
246 QuotedFailureTail
247 (constructor QuotedLiteralFailure QuotedUnknownEscape)
248 start
249 zero)
250 (succ offset)))))))))))))))))))
251 (branch
252 QuotedHexHigh
253 start
254 .
255 (eliminate
256 IntegerLiteralDigitResult
257 (lambda unrestricted decoded : (family IntegerLiteralDigitResult) .
258 (family QuotedLiteralResult))
259 (Compiler.IntegerLiteral/integerLiteralDecodeHex head)
260 (branch
261 IntegerLiteralDigitValue
262 digit
263 .
264 (continue (constructor QuotedByteState QuotedHexLow start digit) (succ offset)))
265 (branch
266 IntegerLiteralDigitFailed
267 failure
268 .
269 (quotedChoose
270 (quotedRecoveryBoundary head)
271 (lambda unrestricted force : Nat .
272 (constructor
273 QuotedLiteralResult
274 QuotedLiteralFailed
275 (constructor QuotedLiteralFailure QuotedBadHex)
276 start
277 offset))
278 (lambda unrestricted force : Nat .
279 (continue
280 (constructor
281 QuotedByteState
282 QuotedFailureTail
283 (constructor QuotedLiteralFailure QuotedBadHex)
284 start
285 (succ zero))
286 (succ offset)))))))
287 (branch
288 QuotedHexLow
289 start
290 high
291 .
292 (eliminate
293 IntegerLiteralDigitResult
294 (lambda unrestricted decoded : (family IntegerLiteralDigitResult) .
295 (family QuotedLiteralResult))
296 (Compiler.IntegerLiteral/integerLiteralDecodeHex head)
297 (branch
298 IntegerLiteralDigitValue
299 digit
300 .
301 (quotedPrepend
302 (nat-to-byte
303 (Std.Natural/naturalAdd
304 (Std.Natural/naturalMultiply high (byte-to-nat (byte 16)))
305 digit))
306 (continue (constructor QuotedByteState QuotedNormal) (succ offset))))
307 (branch
308 IntegerLiteralDigitFailed
309 failure
310 .
311 (quotedChoose
312 (quotedRecoveryBoundary head)
313 (lambda unrestricted force : Nat .
314 (constructor
315 QuotedLiteralResult
316 QuotedLiteralFailed
317 (constructor QuotedLiteralFailure QuotedBadHex)
318 start
319 offset))
320 (lambda unrestricted force : Nat .
321 (continue
322 (constructor
323 QuotedByteState
324 QuotedFailureTail
325 (constructor QuotedLiteralFailure QuotedBadHex)
326 start
327 zero)
328 (succ offset)))))))
329 (branch
330 QuotedFailureTail
331 failure
332 start
333 remaining
334 .
335 (quotedChoose
336 (Data.UTF8/utf8ContinuationValid head)
337 (lambda unrestricted force : Nat .
338 (continue
339 (constructor QuotedByteState QuotedFailureTail failure start remaining)
340 (succ offset)))
341 (lambda unrestricted force : Nat .
342 (quotedChoose
343 remaining
344 (lambda unrestricted force : Nat .
345 (quotedChoose
346 (quotedRecoveryBoundary head)
347 (lambda unrestricted force : Nat .
348 (constructor QuotedLiteralResult QuotedLiteralFailed failure start offset))
349 (lambda unrestricted force : Nat .
350 (continue
351 (constructor QuotedByteState QuotedFailureTail failure start zero)
352 (succ offset)))))
353 (lambda unrestricted force : Nat .
354 (constructor QuotedLiteralResult QuotedLiteralFailed failure start offset))))))
355 (branch
356 QuotedClosed
357 .
358 (constructor
359 QuotedLiteralResult
360 QuotedLiteralFailed
361 (constructor QuotedLiteralFailure QuotedTrailingInput)
362 offset
363 (succ offset))))))))
364
365def quotedByteFinish =
366 (lambda unrestricted state : (family QuotedByteState) .
367 (lambda unrestricted offset : Nat .
368 (eliminate
369 QuotedByteState
370 (lambda unrestricted current : (family QuotedByteState) . (family QuotedLiteralResult))
371 state
372 (branch
373 QuotedNormal
374 .
375 (constructor
376 QuotedLiteralResult
377 QuotedLiteralFailed
378 (constructor QuotedLiteralFailure QuotedUnterminated)
379 zero
380 offset))
381 (branch
382 QuotedEscape
383 start
384 .
385 (constructor
386 QuotedLiteralResult
387 QuotedLiteralFailed
388 (constructor QuotedLiteralFailure QuotedIncompleteEscape)
389 start
390 offset))
391 (branch
392 QuotedHexHigh
393 start
394 .
395 (constructor
396 QuotedLiteralResult
397 QuotedLiteralFailed
398 (constructor QuotedLiteralFailure QuotedBadHex)
399 start
400 offset))
401 (branch
402 QuotedHexLow
403 start
404 high
405 .
406 (constructor
407 QuotedLiteralResult
408 QuotedLiteralFailed
409 (constructor QuotedLiteralFailure QuotedBadHex)
410 start
411 offset))
412 (branch
413 QuotedFailureTail
414 failure
415 start
416 remaining
417 .
418 (constructor QuotedLiteralResult QuotedLiteralFailed failure start offset))
419 (branch QuotedClosed . (constructor QuotedLiteralResult QuotedLiteralDecoded b"")))))
420
421-- Input includes its closing quote; the full-spelling byte offset starts at2.
422def decodeByteLiteralBody =
423 (lambda unrestricted body : Bytes .
424 (app
425 (bytes-eliminate
426 (lambda unrestricted remaining : Bytes .
427 (pi unrestricted state : (family QuotedByteState) .
428 (pi unrestricted offset : Nat . (family QuotedLiteralResult))))
429 quotedByteFinish
430 (lambda unrestricted head : Byte .
431 (lambda unrestricted tail : Bytes .
432 (lambda unrestricted continue : (pi unrestricted state : (family QuotedByteState) . (pi unrestricted offset : Nat . (family QuotedLiteralResult))) .
433 (lambda unrestricted state : (family QuotedByteState) .
434 (lambda unrestricted offset : Nat . (quotedByteStep head state offset continue))))))
435 body)
436 (constructor QuotedByteState QuotedNormal)
437 (succ (succ zero))))
438
439def quotedDecodeByteLiteral =
440 (lambda unrestricted spelling : Bytes .
441 (quotedChoose
442 (byte-equal (bytes-head spelling) (byte 98))
443 (lambda unrestricted force : Nat .
444 (quotedChoose
445 (byte-equal (bytes-head (bytes-tail spelling)) (byte 34))
446 (lambda unrestricted force : Nat .
447 (decodeByteLiteralBody (bytes-tail (bytes-tail spelling))))
448 (lambda unrestricted force : Nat .
449 (constructor
450 QuotedLiteralResult
451 QuotedLiteralFailed
452 (constructor QuotedLiteralFailure QuotedInvalidPrefix)
453 zero
454 zero))))
455 (lambda unrestricted force : Nat .
456 (constructor
457 QuotedLiteralResult
458 QuotedLiteralFailed
459 (constructor QuotedLiteralFailure QuotedInvalidPrefix)
460 zero
461 zero))))
462
463-- Stable parser failure tags; the result above retains the exact byte offset.
464def quotedLiteralFailureCode =
465 (lambda unrestricted failure : (family QuotedLiteralFailure) .
466 (eliminate
467 QuotedLiteralFailure
468 (lambda unrestricted current : (family QuotedLiteralFailure) . Nat)
469 failure
470 (branch QuotedInvalidPrefix . (byte-to-nat (byte 91)))
471 (branch QuotedUnknownEscape . (byte-to-nat (byte 92)))
472 (branch QuotedIncompleteEscape . (byte-to-nat (byte 93)))
473 (branch QuotedBadHex . (byte-to-nat (byte 94)))
474 (branch QuotedNonASCII . (byte-to-nat (byte 95)))
475 (branch QuotedNewline . (byte-to-nat (byte 96)))
476 (branch QuotedUnterminated . (byte-to-nat (byte 97)))
477 (branch QuotedTrailingInput . (byte-to-nat (byte 98)))
478 (branch QuotedUnicodeSyntax . (byte-to-nat (byte 99)))
479 (branch QuotedInvalidScalar . (byte-to-nat (byte 100)))
480 (branch QuotedInvalidUTF8 . (byte-to-nat (byte 101)))))
481
482-- Prepend an encoded scalar without changing the following failure location.
483def quotedPrependBytes =
484 (lambda unrestricted prefix : Bytes .
485 (lambda unrestricted result : (family QuotedLiteralResult) .
486 (eliminate
487 QuotedLiteralResult
488 (lambda unrestricted current : (family QuotedLiteralResult) . (family QuotedLiteralResult))
489 result
490 (branch
491 QuotedLiteralDecoded
492 suffix
493 .
494 (constructor QuotedLiteralResult QuotedLiteralDecoded (bytes-append prefix suffix)))
495 (branch
496 QuotedLiteralFailed
497 failure
498 offset
499 endOffset
500 .
501 (constructor QuotedLiteralResult QuotedLiteralFailed failure offset endOffset)))))
502
503-- Each hex digit shifts four bits once; six digits fit in the 24 low bits.
504def quotedAppendHexDigit =
505 (lambda unrestricted word : (family ModelWord32) .
506 (lambda unrestricted digit : Nat .
507 (eliminate
508 ModelWord32
509 (lambda unrestricted current : (family ModelWord32) . (family ModelWord32))
510 word
511 (branch
512 ModelWord32Value
513 b0
514 b1
515 b2
516 b3
517 .
518 (constructor
519 ModelWord32
520 ModelWord32Value
521 (nat-to-byte
522 (Std.Natural/naturalAdd
523 (byte-to-nat (Std.Byte/byteShiftLeftTruncated b0 (byte-to-nat (byte 4))))
524 digit))
525 (Std.Byte/byteOr
526 (Std.Byte/byteShiftLeftTruncated b1 (byte-to-nat (byte 4)))
527 (Std.Byte/byteShiftRight b0 (byte-to-nat (byte 4))))
528 (Std.Byte/byteOr
529 (Std.Byte/byteShiftLeftTruncated b2 (byte-to-nat (byte 4)))
530 (Std.Byte/byteShiftRight b1 (byte-to-nat (byte 4))))
531 (Std.Byte/byteOr
532 (Std.Byte/byteShiftLeftTruncated b3 (byte-to-nat (byte 4)))
533 (Std.Byte/byteShiftRight b2 (byte-to-nat (byte 4)))))))))
534
535-- Keep scalar arithmetic bounded while consuming the complete malformed escape.
536def quotedAppendBoundedHexDigit =
537 (lambda unrestricted count : Nat .
538 (lambda unrestricted accumulator : (family ModelWord32) .
539 (lambda unrestricted digit : Nat .
540 (nat-eliminate
541 (lambda unrestricted condition : Nat . (family ModelWord32))
542 accumulator
543 (lambda unrestricted predecessor : Nat .
544 (lambda unrestricted unused : (family ModelWord32) .
545 (quotedAppendHexDigit accumulator digit)))
546 (nat-less-than count (byte-to-nat (byte 6)))))))
547
548-- This helper is used only after decodeUTF8 validates the full Text spelling.
549def quotedValidatedScalarEnd =
550 (lambda unrestricted head : Byte .
551 (lambda unrestricted offset : Nat .
552 (Std.Natural/naturalAdd
553 offset
554 (Std.Natural/naturalSelect
555 (Data.UTF8/utf8LeadFourValid head)
556 (byte-to-nat (byte 4))
557 (Std.Natural/naturalSelect
558 (Data.UTF8/utf8LeadThreeValid head)
559 (byte-to-nat (byte 3))
560 (Std.Natural/naturalSelect
561 (Data.UTF8/utf8LeadTwoValid head)
562 (byte-to-nat (byte 2))
563 (succ zero)))))))
564
565def quotedTextStep =
566 (lambda unrestricted head : Byte .
567 (lambda unrestricted state : (family QuotedTextState) .
568 (lambda unrestricted offset : Nat .
569 (lambda unrestricted continue : (pi unrestricted state : (family QuotedTextState) . (pi unrestricted offset : Nat . (family QuotedLiteralResult))) .
570 (quotedChoose
571 (byte-equal head (byte 13))
572 (lambda unrestricted force : Nat .
573 (constructor
574 QuotedLiteralResult
575 QuotedLiteralFailed
576 (constructor QuotedLiteralFailure QuotedNewline)
577 offset
578 (succ offset)))
579 (lambda unrestricted force : Nat .
580 (quotedChoose
581 (byte-equal head (byte 10))
582 (lambda unrestricted force : Nat .
583 (constructor
584 QuotedLiteralResult
585 QuotedLiteralFailed
586 (constructor QuotedLiteralFailure QuotedNewline)
587 offset
588 (succ offset)))
589 (lambda unrestricted force : Nat .
590 (eliminate
591 QuotedTextState
592 (lambda unrestricted current : (family QuotedTextState) .
593 (family QuotedLiteralResult))
594 state
595 (branch
596 QuotedTextNormal
597 .
598 (quotedChoose
599 (byte-equal head (byte 34))
600 (lambda unrestricted force : Nat .
601 (continue (constructor QuotedTextState QuotedTextClosed) (succ offset)))
602 (lambda unrestricted force : Nat .
603 (quotedChoose
604 (byte-equal head (byte 92))
605 (lambda unrestricted force : Nat .
606 (continue
607 (constructor QuotedTextState QuotedTextEscape offset)
608 (succ offset)))
609 (lambda unrestricted force : Nat .
610 (quotedPrepend
611 head
612 (continue
613 (constructor QuotedTextState QuotedTextNormal)
614 (succ offset))))))))
615 (branch
616 QuotedTextEscape
617 start
618 .
619 (quotedChoose
620 (byte-equal head (byte 92))
621 (lambda unrestricted force : Nat .
622 (quotedPrepend
623 (byte 92)
624 (continue (constructor QuotedTextState QuotedTextNormal) (succ offset))))
625 (lambda unrestricted force : Nat .
626 (quotedChoose
627 (byte-equal head (byte 34))
628 (lambda unrestricted force : Nat .
629 (quotedPrepend
630 (byte 34)
631 (continue
632 (constructor QuotedTextState QuotedTextNormal)
633 (succ offset))))
634 (lambda unrestricted force : Nat .
635 (quotedChoose
636 (byte-equal head (byte 114))
637 (lambda unrestricted force : Nat .
638 (quotedPrepend
639 (byte 13)
640 (continue
641 (constructor QuotedTextState QuotedTextNormal)
642 (succ offset))))
643 (lambda unrestricted force : Nat .
644 (quotedChoose
645 (byte-equal head (byte 116))
646 (lambda unrestricted force : Nat .
647 (quotedPrepend
648 (byte 9)
649 (continue
650 (constructor QuotedTextState QuotedTextNormal)
651 (succ offset))))
652 (lambda unrestricted force : Nat .
653 (quotedChoose
654 (byte-equal head (byte 110))
655 (lambda unrestricted force : Nat .
656 (quotedPrepend
657 (byte 10)
658 (continue
659 (constructor QuotedTextState QuotedTextNormal)
660 (succ offset))))
661 (lambda unrestricted force : Nat .
662 (quotedChoose
663 (byte-equal head (byte 117))
664 (lambda unrestricted force : Nat .
665 (continue
666 (constructor QuotedTextState QuotedTextUnicodeOpen start)
667 (succ offset)))
668 (lambda unrestricted force : Nat .
669 (constructor
670 QuotedLiteralResult
671 QuotedLiteralFailed
672 (constructor QuotedLiteralFailure QuotedUnknownEscape)
673 start
674 (quotedValidatedScalarEnd head offset)))))))))))))))
675 (branch
676 QuotedTextUnicodeOpen
677 start
678 .
679 (quotedChoose
680 (byte-equal head (byte 123))
681 (lambda unrestricted force : Nat .
682 (continue
683 (constructor
684 QuotedTextState
685 QuotedTextUnicodeDigits
686 start
687 zero
688 Model.Word32/modelWord32Zero)
689 (succ offset)))
690 (lambda unrestricted force : Nat .
691 (constructor
692 QuotedLiteralResult
693 QuotedLiteralFailed
694 (constructor QuotedLiteralFailure QuotedUnicodeSyntax)
695 start
696 offset))))
697 (branch
698 QuotedTextUnicodeDigits
699 start
700 count
701 accumulator
702 .
703 (quotedChoose
704 (byte-equal head (byte 125))
705 (lambda unrestricted force : Nat .
706 (quotedChoose
707 (Std.Natural/naturalAnd
708 count
709 (nat-less-than count (byte-to-nat (byte 7))))
710 (lambda unrestricted force : Nat .
711 (eliminate
712 UTF8CodepointEncodeResult
713 (lambda unrestricted encoded : (family UTF8CodepointEncodeResult) .
714 (family QuotedLiteralResult))
715 (Data.UTF8/utf8EncodeCodepoint
716 (constructor UTF8Codepoint UTF8CodepointValue accumulator))
717 (branch
718 UTF8CodepointEncoded
719 bytes
720 .
721 (quotedPrependBytes
722 bytes
723 (continue
724 (constructor QuotedTextState QuotedTextNormal)
725 (succ offset))))
726 (branch
727 UTF8CodepointRejected
728 failure
729 .
730 (constructor
731 QuotedLiteralResult
732 QuotedLiteralFailed
733 (constructor QuotedLiteralFailure QuotedInvalidScalar)
734 start
735 (succ offset)))))
736 (lambda unrestricted force : Nat .
737 (constructor
738 QuotedLiteralResult
739 QuotedLiteralFailed
740 (constructor QuotedLiteralFailure QuotedUnicodeSyntax)
741 start
742 (succ offset)))))
743 (lambda unrestricted force : Nat .
744 (eliminate
745 IntegerLiteralDigitResult
746 (lambda unrestricted decoded : (family IntegerLiteralDigitResult) .
747 (family QuotedLiteralResult))
748 (Compiler.IntegerLiteral/integerLiteralDecodeHex head)
749 (branch
750 IntegerLiteralDigitValue
751 digit
752 .
753 (continue
754 (constructor
755 QuotedTextState
756 QuotedTextUnicodeDigits
757 start
758 (succ count)
759 (quotedAppendBoundedHexDigit count accumulator digit))
760 (succ offset)))
761 (branch
762 IntegerLiteralDigitFailed
763 failure
764 .
765 (constructor
766 QuotedLiteralResult
767 QuotedLiteralFailed
768 (constructor QuotedLiteralFailure QuotedUnicodeSyntax)
769 start
770 offset))))))
771 (branch
772 QuotedTextClosed
773 .
774 (constructor
775 QuotedLiteralResult
776 QuotedLiteralFailed
777 (constructor QuotedLiteralFailure QuotedTrailingInput)
778 offset
779 (succ offset))))))))))))
780
781def quotedTextFinish =
782 (lambda unrestricted state : (family QuotedTextState) .
783 (lambda unrestricted offset : Nat .
784 (eliminate
785 QuotedTextState
786 (lambda unrestricted current : (family QuotedTextState) . (family QuotedLiteralResult))
787 state
788 (branch
789 QuotedTextNormal
790 .
791 (constructor
792 QuotedLiteralResult
793 QuotedLiteralFailed
794 (constructor QuotedLiteralFailure QuotedUnterminated)
795 zero
796 offset))
797 (branch
798 QuotedTextEscape
799 start
800 .
801 (constructor
802 QuotedLiteralResult
803 QuotedLiteralFailed
804 (constructor QuotedLiteralFailure QuotedIncompleteEscape)
805 start
806 offset))
807 (branch
808 QuotedTextUnicodeOpen
809 start
810 .
811 (constructor
812 QuotedLiteralResult
813 QuotedLiteralFailed
814 (constructor QuotedLiteralFailure QuotedUnicodeSyntax)
815 start
816 offset))
817 (branch
818 QuotedTextUnicodeDigits
819 start
820 count
821 accumulator
822 .
823 (constructor
824 QuotedLiteralResult
825 QuotedLiteralFailed
826 (constructor QuotedLiteralFailure QuotedUnicodeSyntax)
827 start
828 offset))
829 (branch QuotedTextClosed . (constructor QuotedLiteralResult QuotedLiteralDecoded b"")))))
830
831def quotedDecodeTextBody =
832 (lambda unrestricted body : Bytes .
833 (app
834 (bytes-eliminate
835 (lambda unrestricted remaining : Bytes .
836 (pi unrestricted state : (family QuotedTextState) .
837 (pi unrestricted offset : Nat . (family QuotedLiteralResult))))
838 quotedTextFinish
839 (lambda unrestricted head : Byte .
840 (lambda unrestricted tail : Bytes .
841 (lambda unrestricted continue : (pi unrestricted state : (family QuotedTextState) . (pi unrestricted offset : Nat . (family QuotedLiteralResult))) .
842 (lambda unrestricted state : (family QuotedTextState) .
843 (lambda unrestricted offset : Nat . (quotedTextStep head state offset continue))))))
844 body)
845 (constructor QuotedTextState QuotedTextNormal)
846 (succ zero)))
847
848def quotedDecodeTextLiteral =
849 (lambda unrestricted spelling : Bytes .
850 (eliminate
851 UTF8DecodeResult
852 (lambda unrestricted decoded : (family UTF8DecodeResult) . (family QuotedLiteralResult))
853 (Data.UTF8/decodeUTF8 spelling)
854 (branch
855 UTF8DecodeSucceeded
856 points
857 .
858 (quotedChoose
859 (byte-equal (bytes-head spelling) (byte 34))
860 (lambda unrestricted force : Nat . (quotedDecodeTextBody (bytes-tail spelling)))
861 (lambda unrestricted force : Nat .
862 (constructor
863 QuotedLiteralResult
864 QuotedLiteralFailed
865 (constructor QuotedLiteralFailure QuotedInvalidPrefix)
866 zero
867 zero))))
868 (branch
869 UTF8DecodeFailed
870 failure
871 offset
872 .
873 (constructor
874 QuotedLiteralResult
875 QuotedLiteralFailed
876 (constructor QuotedLiteralFailure QuotedInvalidUTF8)
877 (Model.Word32/modelWord32ToNatural offset)
878 (succ (Model.Word32/modelWord32ToNatural offset))))))
879
880-- Stable diagnostics for the closed literal failure vocabulary; other parser
881-- failures retain their caller-owned code.
882def quotedLiteralDiagnosticCode =
883 (lambda unrestricted code : Nat .
884 (lambda unrestricted fallback : Bytes .
885 (app
886 (nat-eliminate
887 (lambda unrestricted matched : Nat . (pi unrestricted force : Nat . Bytes))
888 (lambda unrestricted force : Nat .
889 (app
890 (nat-eliminate
891 (lambda unrestricted matched : Nat . (pi unrestricted force : Nat . Bytes))
892 (lambda unrestricted force : Nat .
893 (app
894 (nat-eliminate
895 (lambda unrestricted matched : Nat . (pi unrestricted force : Nat . Bytes))
896 (lambda unrestricted force : Nat .
897 (app
898 (nat-eliminate
899 (lambda unrestricted matched : Nat .
900 (pi unrestricted force : Nat . Bytes))
901 (lambda unrestricted force : Nat .
902 (app
903 (nat-eliminate
904 (lambda unrestricted matched : Nat .
905 (pi unrestricted force : Nat . Bytes))
906 (lambda unrestricted force : Nat .
907 (app
908 (nat-eliminate
909 (lambda unrestricted matched : Nat .
910 (pi unrestricted force : Nat . Bytes))
911 (lambda unrestricted force : Nat .
912 (app
913 (nat-eliminate
914 (lambda unrestricted matched : Nat .
915 (pi unrestricted force : Nat . Bytes))
916 (lambda unrestricted force : Nat .
917 (app
918 (nat-eliminate
919 (lambda unrestricted matched : Nat .
920 (pi unrestricted force : Nat . Bytes))
921 (lambda unrestricted force : Nat .
922 (app
923 (nat-eliminate
924 (lambda unrestricted matched : Nat .
925 (pi unrestricted force : Nat . Bytes))
926 (lambda unrestricted force : Nat . fallback)
927 (lambda unrestricted predecessor : Nat .
928 (lambda unrestricted unused : (pi unrestricted force : Nat . Bytes) .
929 (lambda unrestricted force : Nat .
930 b"ALPHA-SOURCE-INVALID-UTF8")))
931 (Std.Natural/naturalEqual
932 code
933 (quotedLiteralFailureCode
934 (constructor QuotedLiteralFailure QuotedInvalidUTF8))))
935 zero))
936 (lambda unrestricted predecessor : Nat .
937 (lambda unrestricted unused : (pi unrestricted force : Nat . Bytes) .
938 (lambda unrestricted force : Nat .
939 b"ALPHA-LITERAL-SCALAR")))
940 (Std.Natural/naturalEqual
941 code
942 (quotedLiteralFailureCode
943 (constructor QuotedLiteralFailure QuotedInvalidScalar))))
944 zero))
945 (lambda unrestricted predecessor : Nat .
946 (lambda unrestricted unused : (pi unrestricted force : Nat . Bytes) .
947 (lambda unrestricted force : Nat .
948 b"ALPHA-LITERAL-UNICODE-ESCAPE")))
949 (Std.Natural/naturalEqual
950 code
951 (quotedLiteralFailureCode
952 (constructor QuotedLiteralFailure QuotedUnicodeSyntax))))
953 zero))
954 (lambda unrestricted predecessor : Nat .
955 (lambda unrestricted unused : (pi unrestricted force : Nat . Bytes) .
956 (lambda unrestricted force : Nat .
957 b"ALPHA-LITERAL-UNTERMINATED")))
958 (Std.Natural/naturalEqual
959 code
960 (quotedLiteralFailureCode
961 (constructor QuotedLiteralFailure QuotedUnterminated))))
962 zero))
963 (lambda unrestricted predecessor : Nat .
964 (lambda unrestricted unused : (pi unrestricted force : Nat . Bytes) .
965 (lambda unrestricted force : Nat .
966 b"ALPHA-LITERAL-NEWLINE")))
967 (Std.Natural/naturalEqual
968 code
969 (quotedLiteralFailureCode
970 (constructor QuotedLiteralFailure QuotedNewline))))
971 zero))
972 (lambda unrestricted predecessor : Nat .
973 (lambda unrestricted unused : (pi unrestricted force : Nat . Bytes) .
974 (lambda unrestricted force : Nat .
975 b"ALPHA-LITERAL-BYTES-NON-ASCII")))
976 (Std.Natural/naturalEqual
977 code
978 (quotedLiteralFailureCode
979 (constructor QuotedLiteralFailure QuotedNonASCII))))
980 zero))
981 (lambda unrestricted predecessor : Nat .
982 (lambda unrestricted unused : (pi unrestricted force : Nat . Bytes) .
983 (lambda unrestricted force : Nat .
984 b"ALPHA-LITERAL-BYTE-ESCAPE")))
985 (Std.Natural/naturalEqual
986 code
987 (quotedLiteralFailureCode (constructor QuotedLiteralFailure QuotedBadHex))))
988 zero))
989 (lambda unrestricted predecessor : Nat .
990 (lambda unrestricted unused : (pi unrestricted force : Nat . Bytes) .
991 (lambda unrestricted force : Nat .
992 b"ALPHA-LITERAL-INCOMPLETE-ESCAPE")))
993 (Std.Natural/naturalEqual
994 code
995 (quotedLiteralFailureCode
996 (constructor QuotedLiteralFailure QuotedIncompleteEscape))))
997 zero))
998 (lambda unrestricted predecessor : Nat .
999 (lambda unrestricted unused : (pi unrestricted force : Nat . Bytes) .
1000 (lambda unrestricted force : Nat .
1001 b"ALPHA-LITERAL-UNKNOWN-ESCAPE")))
1002 (Std.Natural/naturalEqual
1003 code
1004 (quotedLiteralFailureCode (constructor QuotedLiteralFailure QuotedUnknownEscape))))
1005 zero)))
1006
1007-- Structural lexing validates only quoted atoms; unquoted spelling is unchanged.
1008def quotedValidateSourceAtom =
1009 (lambda unrestricted spelling : Bytes .
1010 (quotedChoose
1011 (byte-equal (bytes-head spelling) (byte 34))
1012 (lambda unrestricted force : Nat . (quotedDecodeTextLiteral spelling))
1013 (lambda unrestricted force : Nat .
1014 (quotedChoose
1015 (Std.Natural/naturalAnd
1016 (byte-equal (bytes-head spelling) (byte 98))
1017 (byte-equal (bytes-head (bytes-tail spelling)) (byte 34)))
1018 (lambda unrestricted force : Nat . (quotedDecodeByteLiteral spelling))
1019 (lambda unrestricted force : Nat .
1020 (constructor QuotedLiteralResult QuotedLiteralDecoded spelling))))))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.