One decode step: `Failed` is a fixed point; `Going` peels one byte (O(1) via
`bytes-head`/`bytes-tail`) at offset `offset` and dispatches on the pending
state. The peeled byte's position is `offset`; the next offset is `succ
offset`.
592def utf8MachineStep =
593 (lambda unrestricted machine : (family UTF8DecodeMachine) .
594 (eliminate
595 UTF8DecodeMachine
596 (lambda unrestricted current : (family UTF8DecodeMachine) . (family UTF8DecodeMachine))
597 machine
598 (branch
599 UTF8DecodeMachineGoing
600 remaining
601 offset
602 pending
603 reversed
604 .
605 (app
606 (lambda unrestricted b : Byte .
607 (lambda unrestricted rest : Bytes .
608 (eliminate
609 UTF8DecodePending
610 (lambda unrestricted current : (family UTF8DecodePending) .
611 (family UTF8DecodeMachine))
612 pending
613 (branch UTF8PendingReady . (utf8MachineReady b rest offset (succ offset) reversed))
614 (branch
615 UTF8PendingTwo
616 lead
617 .
618 (utf8MachineTwo lead b rest offset (succ offset) reversed))
619 (branch
620 UTF8PendingThreeA
621 lead
622 leadOffset
623 .
624 (utf8MachineThreeA lead leadOffset b rest offset (succ offset) reversed))
625 (branch
626 UTF8PendingThreeB
627 lead
628 byte1
629 .
630 (utf8MachineThreeB lead byte1 b rest offset (succ offset) reversed))
631 (branch
632 UTF8PendingFourA
633 lead
634 leadOffset
635 .
636 (utf8MachineFourA lead leadOffset b rest offset (succ offset) reversed))
637 (branch
638 UTF8PendingFourB
639 lead
640 byte1
641 .
642 (utf8MachineFourB lead byte1 b rest offset (succ offset) reversed))
643 (branch
644 UTF8PendingFourC
645 lead
646 byte1
647 byte2
648 .
649 (utf8MachineFourC lead byte1 byte2 b rest offset (succ offset) reversed)))))
650 (bytes-head remaining)
651 (bytes-tail remaining)))
652 (branch
653 UTF8DecodeMachineFailed
654 error
655 offset
656 .
657 (constructor UTF8DecodeMachine UTF8DecodeMachineFailed error 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.