One first-order string-body step over the `JSONStringLoop` accumulator.
`Going builder remaining` peeks the head with the O(1) `bytes-head` view
(never the tail-forcing `bytes-eliminate`): a closing quote absorbs to `Done`,
a control byte to `Failed`, `\` decodes exactly one escape via `jsonParseEscape`
(given a trivial continuation that just packages the position after the escape,
so the existing CPS escape decoder is reused unchanged), and any other byte is
appended to the decoded-prefix builder. `Done`/`Failed` are fixed points. Bytes
are appended front-to-back, matching the original's head-first prepend, so the
decoded string is byte-for-byte identical.
754def jsonParseStringBodyStep =
755 (lambda unrestricted acc : (family JSONStringLoop) .
756 (eliminate
757 JSONStringLoop
758 (lambda unrestricted current : (family JSONStringLoop) . (family JSONStringLoop))
759 acc
760 (branch
761 JSONStringLoopGoing
762 builder
763 remaining
764 .
765 (nat-eliminate
766 (lambda unrestricted nonEmpty : Nat . (family JSONStringLoop))
767 (app
768 (lambda unrestricted head : Byte .
769 (nat-eliminate
770 (lambda unrestricted quote : Nat . (family JSONStringLoop))
771 (nat-eliminate
772 (lambda unrestricted escape : Nat . (family JSONStringLoop))
773 (nat-eliminate
774 (lambda unrestricted control : Nat . (family JSONStringLoop))
775 (constructor
776 JSONStringLoop
777 JSONStringLoopGoing
778 (bytes-builder-append builder (bytes-builder-chunk (bytes-cons head b"")))
779 (bytes-tail remaining))
780 (lambda unrestricted controlPredecessor : Nat .
781 (lambda unrestricted controlInduction : (family JSONStringLoop) .
782 (constructor
783 JSONStringLoop
784 JSONStringLoopFailed
785 (constructor JSONErrorCode JSONStringControlCharacter)
786 remaining)))
787 (byte-less-than head (byte 32)))
788 (lambda unrestricted escapePredecessor : Nat .
789 (lambda unrestricted escapeInduction : (family JSONStringLoop) .
790 (eliminate
791 JSONStringParseResult
792 (lambda unrestricted current : (family JSONStringParseResult) .
793 (family JSONStringLoop))
794 (jsonParseEscape
795 (lambda unrestricted escRemaining : Bytes .
796 (constructor
797 JSONStringParseResult
798 JSONStringParsed
799 (bytes-builder-empty)
800 escRemaining))
801 (bytes-tail remaining))
802 (branch
803 JSONStringParsed
804 escBuilder
805 afterEsc
806 .
807 (constructor
808 JSONStringLoop
809 JSONStringLoopGoing
810 (bytes-builder-append builder escBuilder)
811 afterEsc))
812 (branch
813 JSONStringParseFailed
814 code
815 failRemaining
816 .
817 (constructor JSONStringLoop JSONStringLoopFailed code failRemaining)))))
818 (byte-equal head (byte 92)))
819 (lambda unrestricted quotePredecessor : Nat .
820 (lambda unrestricted quoteInduction : (family JSONStringLoop) .
821 (constructor JSONStringLoop JSONStringLoopDone builder (bytes-tail remaining))))
822 (byte-equal head (byte 34))))
823 (bytes-head remaining))
824 (lambda unrestricted emptyPredecessor : Nat .
825 (lambda unrestricted emptyInduction : (family JSONStringLoop) .
826 (constructor
827 JSONStringLoop
828 JSONStringLoopFailed
829 (constructor JSONErrorCode JSONStringUnterminated)
830 remaining)))
831 (naturalIsZero (bytes-length remaining))))
832 (branch JSONStringLoopDone doneBuilder doneRemaining . acc)
833 (branch JSONStringLoopFailed failError failRemaining . acc)))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.