Decode UTF-8 to a codepoint list, FIRST-ORDER, byte-at-a-time, LINEAR.
The old driver `utf8DecodeWithFuel` was a `nat-eliminate` whose motive was a
`pi` (Bytes -> Nat -> Result): the "fuel-as-function" pattern `f n = step
(n-1) (f (n-1))`, which the reference machine runs unshared as `T(n) =
2*T(n-1)` -- exponential per byte (docs/ALPHA-ER-RUNPOD-TRAINING-TARGET.md
3.11) -- and which the direct lane refuses outright.
This driver's `nat-eliminate` motive is a first-order VALUE, `UTF8Decode
Machine`, and it runs exactly `bytes-length input` steps, one input byte
each. Every step is O(1) -- `bytes-head`/`bytes-tail` peel a byte, `succ`
advances the offset, a completed codepoint is prepended -- because the loop
never calls the reference machine's tail-folding eliminators (`bytes-
eliminate`, `bytes-length`) or `naturalAdd`, each of which is O(remaining).
So decode is O(length). Fuel equals the byte count exactly, so no step reads
past the end. At the end the pending state decides the outcome: `Ready` is a
clean success (reversed back to source order); a pending multi-byte state is a
truncation whose offset is the final position (`ContinuationMissing` with no
continuation collected, else `SequenceTruncated`). Success/error codes and
offsets are identical to the original by construction.
749def decodeUTF8 =
750 (lambda unrestricted input : Bytes .
751 (eliminate
752 UTF8DecodeMachine
753 (lambda unrestricted current : (family UTF8DecodeMachine) . (family UTF8DecodeResult))
754 (nat-eliminate
755 (lambda unrestricted step : Nat . (family UTF8DecodeMachine))
756 (utf8MachineGoing
757 input
758 zero
759 (constructor UTF8DecodePending UTF8PendingReady)
760 (constructor UTF8Codepoints UTF8CodepointsEnd))
761 (lambda unrestricted predecessor : Nat .
762 (lambda unrestricted induction : (family UTF8DecodeMachine) . (utf8MachineStep induction)))
763 (bytes-length input))
764 (branch
765 UTF8DecodeMachineGoing
766 remaining
767 offset
768 pending
769 reversed
770 .
771 (eliminate
772 UTF8DecodePending
773 (lambda unrestricted current : (family UTF8DecodePending) . (family UTF8DecodeResult))
774 pending
775 (branch
776 UTF8PendingReady
777 .
778 (constructor
779 UTF8DecodeResult
780 UTF8DecodeSucceeded
781 (utf8CodepointsReverse (bytes-length input) reversed)))
782 (branch
783 UTF8PendingTwo
784 lead
785 .
786 (utf8DecodeTruncatedAt (constructor UTF8ErrorCode UTF8ContinuationMissing) offset))
787 (branch
788 UTF8PendingThreeA
789 lead
790 leadOffset
791 .
792 (utf8DecodeTruncatedAt (constructor UTF8ErrorCode UTF8ContinuationMissing) offset))
793 (branch
794 UTF8PendingThreeB
795 lead
796 byte1
797 .
798 (utf8DecodeTruncatedAt (constructor UTF8ErrorCode UTF8SequenceTruncated) offset))
799 (branch
800 UTF8PendingFourA
801 lead
802 leadOffset
803 .
804 (utf8DecodeTruncatedAt (constructor UTF8ErrorCode UTF8ContinuationMissing) offset))
805 (branch
806 UTF8PendingFourB
807 lead
808 byte1
809 .
810 (utf8DecodeTruncatedAt (constructor UTF8ErrorCode UTF8SequenceTruncated) offset))
811 (branch
812 UTF8PendingFourC
813 lead
814 byte1
815 byte2
816 .
817 (utf8DecodeTruncatedAt (constructor UTF8ErrorCode UTF8SequenceTruncated) offset))))
818 (branch
819 UTF8DecodeMachineFailed
820 error
821 offset
822 .
823 (constructor UTF8DecodeResult UTF8DecodeFailed error (utf8OffsetWord 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.