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))))))))))))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.