576def jsonParseUnicodeEscape =
577 (lambda unrestricted continuation : (pi unrestricted input : Bytes . (family JSONStringParseResult)) .
578 (lambda unrestricted input : Bytes .
579 (eliminate
580 JSONHexQuadResult
581 (lambda unrestricted current : (family JSONHexQuadResult) . (family JSONStringParseResult))
582 (jsonParseHexQuad input)
583 (branch
584 JSONHexQuadParsed
585 high
586 remaining
587 .
588 (nat-eliminate
589 (lambda unrestricted highSurrogate : Nat . (family JSONStringParseResult))
590 (nat-eliminate
591 (lambda unrestricted lowSurrogate : Nat . (family JSONStringParseResult))
592 (jsonEncodeCodepointThen continuation high remaining)
593 (lambda unrestricted predecessor : Nat .
594 (lambda unrestricted induction : (family JSONStringParseResult) .
595 (jsonStringFailure
596 (constructor JSONErrorCode JSONUnicodeLowWithoutHigh)
597 remaining)))
598 (jsonFlagAnd
599 (jsonFlagNot (nat-less-than high jsonNaturalFiftySixThousandThreeHundredTwenty))
600 (nat-less-than high jsonNaturalFiftySevenThousandThreeHundredFortyFour)))
601 (lambda unrestricted predecessor : Nat .
602 (lambda unrestricted induction : (family JSONStringParseResult) .
603 (eliminate
604 JSONLiteralResult
605 (lambda unrestricted current : (family JSONLiteralResult) .
606 (family JSONStringParseResult))
607 (jsonConsumeLiteral b"\\u" remaining)
608 (branch
609 JSONLiteralConsumed
610 afterPrefix
611 .
612 (eliminate
613 JSONHexQuadResult
614 (lambda unrestricted current : (family JSONHexQuadResult) .
615 (family JSONStringParseResult))
616 (jsonParseHexQuad afterPrefix)
617 (branch
618 JSONHexQuadParsed
619 low
620 afterLow
621 .
622 (nat-eliminate
623 (lambda unrestricted validLow : Nat . (family JSONStringParseResult))
624 (jsonStringFailure
625 (constructor JSONErrorCode JSONUnicodeHighWithoutLow)
626 afterLow)
627 (lambda unrestricted validPredecessor : Nat .
628 (lambda unrestricted validInduction : (family JSONStringParseResult) .
629 (jsonEncodeCodepointThen
630 continuation
631 (naturalAdd
632 jsonNaturalSixtyFiveThousandFiveHundredThirtySix
633 (naturalAdd
634 (naturalMultiply
635 (naturalSaturatingSubtract
636 high
637 jsonNaturalFiftyFiveThousandTwoHundredNinetySix)
638 jsonNaturalOneThousandTwentyFour)
639 (naturalSaturatingSubtract
640 low
641 jsonNaturalFiftySixThousandThreeHundredTwenty)))
642 afterLow)))
643 (jsonFlagAnd
644 (jsonFlagNot
645 (nat-less-than low jsonNaturalFiftySixThousandThreeHundredTwenty))
646 (nat-less-than low jsonNaturalFiftySevenThousandThreeHundredFortyFour))))
647 (branch
648 JSONHexQuadFailed
649 failureRemaining
650 .
651 (jsonStringFailure
652 (constructor JSONErrorCode JSONUnicodeHighWithoutLow)
653 failureRemaining))))
654 (branch
655 JSONLiteralFailed
656 failureRemaining
657 .
658 (jsonStringFailure
659 (constructor JSONErrorCode JSONUnicodeHighWithoutLow)
660 failureRemaining)))))
661 (jsonFlagAnd
662 (jsonFlagNot (nat-less-than high jsonNaturalFiftyFiveThousandTwoHundredNinetySix))
663 (nat-less-than high jsonNaturalFiftySixThousandThreeHundredTwenty))))
664 (branch
665 JSONHexQuadFailed
666 remaining
667 .
668 (jsonStringFailure (constructor JSONErrorCode JSONUnicodeEscapeInvalid) remaining)))))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.