module Data.UTF8 import Model.Config import Model.Word32 import Std.Byte import Std.Natural import Std.Foundation import Std.Flag family UTF8Codepoint : Type 0 constructor UTF8CodepointValue field unrestricted utf8CodepointWord : (family ModelWord32) end-family family UTF8Codepoints : Type 0 constructor UTF8CodepointsEnd constructor UTF8CodepointsNext field unrestricted utf8CodepointHead : (family UTF8Codepoint) recursive unrestricted utf8CodepointTail end-family family UTF8DecoderState : Type 0 constructor UTF8DecoderReady constructor UTF8DecoderNeedOne field unrestricted utf8DecoderOneLead : Byte constructor UTF8DecoderNeedTwo field unrestricted utf8DecoderTwoLead : Byte field unrestricted utf8DecoderTwoByte1 : Byte constructor UTF8DecoderNeedThree field unrestricted utf8DecoderThreeLead : Byte field unrestricted utf8DecoderThreeByte1 : Byte field unrestricted utf8DecoderThreeByte2 : Byte end-family family UTF8ErrorCode : Type 0 constructor UTF8UnexpectedContinuation constructor UTF8InvalidLeadingByte constructor UTF8ContinuationMissing constructor UTF8ContinuationInvalid constructor UTF8TwoByteOverlong constructor UTF8ThreeByteOverlong constructor UTF8FourByteOverlong constructor UTF8SurrogateCodepoint constructor UTF8CodepointOutOfRange constructor UTF8SequenceTruncated end-family family UTF8DecodeResult : Type 0 constructor UTF8DecodeSucceeded field unrestricted utf8DecodedCodepoints : (family UTF8Codepoints) constructor UTF8DecodeFailed field unrestricted utf8DecodeError : (family UTF8ErrorCode) field unrestricted utf8DecodeOffset : (family ModelWord32) end-family family UTF8EncodeResult : Type 0 constructor UTF8EncodeSucceeded field unrestricted utf8EncodedBytes : Bytes constructor UTF8EncodeFailed field unrestricted utf8EncodeError : (family UTF8ErrorCode) field unrestricted utf8EncodeOffset : (family ModelWord32) end-family family UTF8CodepointEncodeResult : Type 0 constructor UTF8CodepointEncoded field unrestricted utf8CodepointEncodedBytes : Bytes constructor UTF8CodepointRejected field unrestricted utf8CodepointEncodeError : (family UTF8ErrorCode) end-family family UTF8EncodeBuilderResult : Type 0 constructor UTF8EncodeBuilderSucceeded field unrestricted utf8EncodedBuilder : BytesBuilder constructor UTF8EncodeBuilderFailed field unrestricted utf8EncodeBuilderError : (family UTF8ErrorCode) field unrestricted utf8EncodeBuilderOffset : Nat end-family family UTF8DecodeTelemetry : Type 0 constructor UTF8DecodeTelemetryValue field unrestricted utf8DecodeTelemetryInputBytes : Nat field unrestricted utf8DecodeTelemetryInspectedBytes : Nat field unrestricted utf8DecodeTelemetryCodepoints : Nat field unrestricted utf8DecodeTelemetryASCII : Nat field unrestricted utf8DecodeTelemetryTwoByte : Nat field unrestricted utf8DecodeTelemetryThreeByte : Nat field unrestricted utf8DecodeTelemetryFourByte : Nat field unrestricted utf8DecodeTelemetryContinuationBytes : Nat field unrestricted utf8DecodeTelemetryIllegalBytes : Nat field unrestricted utf8DecodeTelemetryFailurePresent : Nat field unrestricted utf8DecodeTelemetryFailureOffset : Nat end-family family UTF8EncodeTelemetry : Type 0 constructor UTF8EncodeTelemetryValue field unrestricted utf8EncodeTelemetryInputCodepoints : Nat field unrestricted utf8EncodeTelemetryProcessedCodepoints : Nat field unrestricted utf8EncodeTelemetryOutputBytes : Nat field unrestricted utf8EncodeTelemetryASCII : Nat field unrestricted utf8EncodeTelemetryTwoByte : Nat field unrestricted utf8EncodeTelemetryThreeByte : Nat field unrestricted utf8EncodeTelemetryFourByte : Nat field unrestricted utf8EncodeTelemetryInvalidScalars : Nat field unrestricted utf8EncodeTelemetryFailurePresent : Nat field unrestricted utf8EncodeTelemetryFailureOrdinal : Nat end-family family UTF8DecodeExecutionResult : Type 0 constructor UTF8DecodeExecutionSucceeded field unrestricted utf8DecodeExecutionCodepoints : (family UTF8Codepoints) field unrestricted utf8DecodeExecutionTelemetry : (family UTF8DecodeTelemetry) constructor UTF8DecodeExecutionFailed field unrestricted utf8DecodeExecutionError : (family UTF8ErrorCode) field unrestricted utf8DecodeExecutionOffset : (family ModelWord32) field unrestricted utf8DecodeExecutionStableError : Bytes field unrestricted utf8DecodeExecutionTelemetryBeforeFailure : (family UTF8DecodeTelemetry) end-family family UTF8EncodeExecutionResult : Type 0 constructor UTF8EncodeExecutionSucceeded field unrestricted utf8EncodeExecutionBytes : Bytes field unrestricted utf8EncodeExecutionTelemetry : (family UTF8EncodeTelemetry) constructor UTF8EncodeExecutionFailed field unrestricted utf8EncodeExecutionError : (family UTF8ErrorCode) field unrestricted utf8EncodeExecutionOffset : (family ModelWord32) field unrestricted utf8EncodeExecutionStableError : Bytes field unrestricted utf8EncodeExecutionTelemetryBeforeFailure : (family UTF8EncodeTelemetry) end-family -- Pending multi-byte context for the byte-at-a-time decoder (see `decodeUTF8`). -- `Ready` is a codepoint boundary; the others hold the lead byte and the -- continuation bytes collected so far while more are awaited. `ThreeA`/`FourA` -- also carry the lead's byte offset, the only states whose error (overlong / -- surrogate / out-of-range) is reported AT the lead rather than at the byte -- being read. family UTF8DecodePending : Type 0 constructor UTF8PendingReady constructor UTF8PendingTwo field unrestricted utf8PendingTwoLead : Byte constructor UTF8PendingThreeA field unrestricted utf8PendingThreeALead : Byte field unrestricted utf8PendingThreeAOffset : Nat constructor UTF8PendingThreeB field unrestricted utf8PendingThreeBLead : Byte field unrestricted utf8PendingThreeBByte1 : Byte constructor UTF8PendingFourA field unrestricted utf8PendingFourALead : Byte field unrestricted utf8PendingFourAOffset : Nat constructor UTF8PendingFourB field unrestricted utf8PendingFourBLead : Byte field unrestricted utf8PendingFourBByte1 : Byte constructor UTF8PendingFourC field unrestricted utf8PendingFourCLead : Byte field unrestricted utf8PendingFourCByte1 : Byte field unrestricted utf8PendingFourCByte2 : Byte end-family -- Byte-at-a-time decoder accumulator threaded by a `nat-eliminate` over the -- input length. Every step is O(1): it peels one byte with `bytes-head` / -- `bytes-tail` (both O(1) on the `[Word8]` representation), advances the offset -- with `succ` (O(1)), and either prepends a completed codepoint onto -- `utf8MachineReversed` or updates `utf8MachinePending`. It must avoid -- `bytes-eliminate`, `bytes-length` and `naturalAdd` in the loop: the reference -- machine folds the ENTIRE tail to build a (here unused) induction for those, so -- one call is O(remaining) and per-step use would be O(length^2). Fuel equals -- the byte count exactly, so a step never reads past the end (no empty test is -- needed). `Failed` is a fixed point that absorbs any surplus fuel. family UTF8DecodeMachine : Type 0 constructor UTF8DecodeMachineGoing field unrestricted utf8MachineRemaining : Bytes field unrestricted utf8MachineOffset : Nat field unrestricted utf8MachinePending : (family UTF8DecodePending) field unrestricted utf8MachineReversed : (family UTF8Codepoints) constructor UTF8DecodeMachineFailed field unrestricted utf8MachineError : (family UTF8ErrorCode) field unrestricted utf8MachineErrorOffset : Nat end-family -- First-order reversal accumulator: `utf8ReverseRemaining` is the list still to -- move, `utf8ReverseAccumulated` is the reversed prefix already built. family UTF8CodepointsReverseState : Type 0 constructor UTF8CodepointsReverseStateValue field unrestricted utf8ReverseRemaining : (family UTF8Codepoints) field unrestricted utf8ReverseAccumulated : (family UTF8Codepoints) end-family def utf8MaximumCodepoint = (constructor ModelWord32 ModelWord32Value (byte 255) (byte 255) (byte 16) (byte 0)) def utf8SurrogateMinimum = (constructor ModelWord32 ModelWord32Value (byte 0) (byte 216) (byte 0) (byte 0)) def utf8SurrogateMaximum = (constructor ModelWord32 ModelWord32Value (byte 255) (byte 223) (byte 0) (byte 0)) def utf8NaturalOne = (succ zero) def utf8NaturalTwo = (succ utf8NaturalOne) def utf8NaturalThree = (succ utf8NaturalTwo) def utf8NaturalSix = (byte-to-nat (byte 6)) def utf8NaturalTwelve = (byte-to-nat (byte 12)) def utf8NaturalEighteen = (byte-to-nat (byte 18)) def utf8NaturalSixtyFour = (byte-to-nat (byte 64)) def utf8NaturalOneHundredTwentyEight = (naturalPowerOfTwo (byte-to-nat (byte 7))) def utf8NaturalTwoThousandFortyEight = (naturalPowerOfTwo (byte-to-nat (byte 11))) def utf8NaturalFiftyFiveThousandTwoHundredNinetySix = (naturalMultiply (byte-to-nat (byte 216)) byteNaturalTwoHundredFiftySix) def utf8NaturalFiftySevenThousandThreeHundredFortyFour = (naturalMultiply (byte-to-nat (byte 224)) byteNaturalTwoHundredFiftySix) def utf8NaturalSixtyFiveThousandFiveHundredThirtySix = (naturalPowerOfTwo (byte-to-nat (byte 16))) def utf8NaturalOneMillionOneHundredFourteenThousandOneHundredTwelve = (naturalMultiply (byte-to-nat (byte 17)) utf8NaturalSixtyFiveThousandFiveHundredThirtySix) -- Delegates to the one owner (Std.Flag): this body is alpha-equivalent to -- Std.Flag.inferenceFlagNot (binder renamed value<->flag, otherwise -- identical) -- missed by `alpha-ast duplicates`' exact (binder-name- -- sensitive) shape digest, found by manual inspection after that tool -- grouped it with Std.Natural.naturalIsZero instead (also alpha-equivalent -- to inferenceFlagNot, coincidentally under the same binder name "value"). def utf8FlagNot = inferenceFlagNot -- Delegates to the one owner (Std.Flag), which this file already had a -- byte-for-byte copy of before `alpha-ast duplicates` found it (L24d). def utf8FlagAnd = inferenceFlagAnd def utf8ByteAtLeast = (lambda unrestricted value : Byte . (lambda unrestricted minimum : Byte . (utf8FlagNot (byte-less-than value minimum)))) def utf8ByteInHalfOpenRange = (lambda unrestricted value : Byte . (lambda unrestricted minimum : Byte . (lambda unrestricted maximum : Byte . (utf8FlagAnd (utf8ByteAtLeast value minimum) (byte-less-than value maximum))))) def utf8ContinuationValid = (lambda unrestricted value : Byte . (utf8ByteInHalfOpenRange value (byte 128) (byte 192))) def utf8LeadTwoValid = (lambda unrestricted value : Byte . (utf8ByteInHalfOpenRange value (byte 194) (byte 224))) def utf8LeadThreeValid = (lambda unrestricted value : Byte . (utf8ByteInHalfOpenRange value (byte 224) (byte 240))) def utf8LeadFourValid = (lambda unrestricted value : Byte . (utf8ByteInHalfOpenRange value (byte 240) (byte 245))) def utf8OffsetWord = (lambda unrestricted offset : Nat . (modelWord32FromNaturalTruncated offset)) -- Build a failed machine at byte offset `offset` (a `Nat` already threaded via -- `succ`; converted to the public ModelWord32 offset once, in `decodeUTF8`). def utf8MachineFailAt = (lambda unrestricted code : (family UTF8ErrorCode) . (lambda unrestricted offset : Nat . (constructor UTF8DecodeMachine UTF8DecodeMachineFailed code offset))) -- Build a still-going machine. def utf8MachineGoing = (lambda unrestricted remaining : Bytes . (lambda unrestricted offset : Nat . (lambda unrestricted pending : (family UTF8DecodePending) . (lambda unrestricted reversed : (family UTF8Codepoints) . (constructor UTF8DecodeMachine UTF8DecodeMachineGoing remaining offset pending reversed))))) -- Complete a codepoint: return to `Ready` with the codepoint prepended onto the -- reversed accumulator (O(1)). def utf8MachineEmit = (lambda unrestricted codepoint : (family UTF8Codepoint) . (lambda unrestricted remaining : Bytes . (lambda unrestricted offset : Nat . (lambda unrestricted reversed : (family UTF8Codepoints) . (utf8MachineGoing remaining offset (constructor UTF8DecodePending UTF8PendingReady) (constructor UTF8Codepoints UTF8CodepointsNext codepoint reversed)))))) -- Codepoint words are composed from the byte bits directly (D17): no natural -- arithmetic, so a decoded character costs a handful of byte operations -- instead of a fold over the codepoint's value. def utf8CodepointWord = (lambda unrestricted b0 : Byte . (lambda unrestricted b1 : Byte . (lambda unrestricted b2 : Byte . (constructor UTF8Codepoint UTF8CodepointValue (constructor ModelWord32 ModelWord32Value b0 b1 b2 (byte 0)))))) def utf8CodepointFromOne = (lambda unrestricted lead : Byte . (utf8CodepointWord lead (byte 0) (byte 0))) -- (lead & 0x1F) << 6 | (b1 & 0x3F) def utf8CodepointFromTwo = (lambda unrestricted lead : Byte . (lambda unrestricted b1 : Byte . (utf8CodepointWord (byteOr (byteShiftLeftTruncated (byteAnd lead (byte 3)) utf8NaturalSix) (byteAnd b1 (byte 63))) (byteShiftRight (byteAnd lead (byte 31)) utf8NaturalTwo) (byte 0)))) -- (lead & 0x0F) << 12 | (b1 & 0x3F) << 6 | (b2 & 0x3F) def utf8CodepointFromThree = (lambda unrestricted lead : Byte . (lambda unrestricted b1 : Byte . (lambda unrestricted b2 : Byte . (utf8CodepointWord (byteOr (byteShiftLeftTruncated (byteAnd b1 (byte 3)) utf8NaturalSix) (byteAnd b2 (byte 63))) (byteOr (byteShiftLeftTruncated (byteAnd lead (byte 15)) (byte-to-nat (byte 4))) (byteShiftRight (byteAnd b1 (byte 63)) utf8NaturalTwo)) (byte 0))))) -- (lead & 0x07) << 18 | (b1 & 0x3F) << 12 | (b2 & 0x3F) << 6 | (b3 & 0x3F) def utf8CodepointFromFour = (lambda unrestricted lead : Byte . (lambda unrestricted b1 : Byte . (lambda unrestricted b2 : Byte . (lambda unrestricted b3 : Byte . (utf8CodepointWord (byteOr (byteShiftLeftTruncated (byteAnd b2 (byte 3)) utf8NaturalSix) (byteAnd b3 (byte 63))) (byteOr (byteShiftLeftTruncated (byteAnd b1 (byte 15)) (byte-to-nat (byte 4))) (byteShiftRight (byteAnd b2 (byte 63)) utf8NaturalTwo)) (byteOr (byteShiftLeftTruncated (byteAnd lead (byte 7)) utf8NaturalTwo) (byteShiftRight (byteAnd b1 (byte 63)) (byte-to-nat (byte 4))))))))) -- Ready-state byte: `b` is a codepoint start at byte offset `pos`; `rest` is the -- suffix after it and `nextOffset` = succ pos. Dispatch by class exactly as the -- original: ASCII emits; a 2/3/4-byte lead moves to the matching pending state; -- a bare continuation, a 0xC0/0xC1 lead, or any other byte fails AT `pos`. def utf8MachineReady = (lambda unrestricted b : Byte . (lambda unrestricted rest : Bytes . (lambda unrestricted pos : Nat . (lambda unrestricted nextOffset : Nat . (lambda unrestricted reversed : (family UTF8Codepoints) . (nat-eliminate (lambda unrestricted ascii : Nat . (family UTF8DecodeMachine)) (nat-eliminate (lambda unrestricted leadTwo : Nat . (family UTF8DecodeMachine)) (nat-eliminate (lambda unrestricted leadThree : Nat . (family UTF8DecodeMachine)) (nat-eliminate (lambda unrestricted leadFour : Nat . (family UTF8DecodeMachine)) (nat-eliminate (lambda unrestricted continuationByte : Nat . (family UTF8DecodeMachine)) (nat-eliminate (lambda unrestricted overlongTwo : Nat . (family UTF8DecodeMachine)) (utf8MachineFailAt (constructor UTF8ErrorCode UTF8InvalidLeadingByte) pos) (lambda unrestricted overlongPredecessor : Nat . (lambda unrestricted overlongInduction : (family UTF8DecodeMachine) . (utf8MachineFailAt (constructor UTF8ErrorCode UTF8TwoByteOverlong) pos))) (utf8FlagAnd (utf8ByteAtLeast b (byte 192)) (byte-less-than b (byte 194)))) (lambda unrestricted continuationPredecessor : Nat . (lambda unrestricted continuationInduction : (family UTF8DecodeMachine) . (utf8MachineFailAt (constructor UTF8ErrorCode UTF8UnexpectedContinuation) pos))) (utf8ContinuationValid b)) (lambda unrestricted fourPredecessor : Nat . (lambda unrestricted fourInduction : (family UTF8DecodeMachine) . (utf8MachineGoing rest nextOffset (constructor UTF8DecodePending UTF8PendingFourA b pos) reversed))) (utf8LeadFourValid b)) (lambda unrestricted threePredecessor : Nat . (lambda unrestricted threeInduction : (family UTF8DecodeMachine) . (utf8MachineGoing rest nextOffset (constructor UTF8DecodePending UTF8PendingThreeA b pos) reversed))) (utf8LeadThreeValid b)) (lambda unrestricted twoPredecessor : Nat . (lambda unrestricted twoInduction : (family UTF8DecodeMachine) . (utf8MachineGoing rest nextOffset (constructor UTF8DecodePending UTF8PendingTwo b) reversed))) (utf8LeadTwoValid b)) (lambda unrestricted asciiPredecessor : Nat . (lambda unrestricted asciiInduction : (family UTF8DecodeMachine) . (utf8MachineEmit (utf8CodepointFromOne b) rest nextOffset reversed))) (byte-less-than b (byte 128)))))))) -- Second byte of a two-byte sequence at offset `pos`. def utf8MachineTwo = (lambda unrestricted lead : Byte . (lambda unrestricted b : Byte . (lambda unrestricted rest : Bytes . (lambda unrestricted pos : Nat . (lambda unrestricted nextOffset : Nat . (lambda unrestricted reversed : (family UTF8Codepoints) . (nat-eliminate (lambda unrestricted valid : Nat . (family UTF8DecodeMachine)) (utf8MachineFailAt (constructor UTF8ErrorCode UTF8ContinuationInvalid) pos) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family UTF8DecodeMachine) . (utf8MachineEmit (utf8CodepointFromTwo lead b) rest nextOffset reversed))) (utf8ContinuationValid b)))))))) -- First continuation of a three-byte sequence. `leadOffset` is the lead's byte -- offset (overlong and surrogate are reported there); `pos` is this byte's. def utf8MachineThreeA = (lambda unrestricted lead : Byte . (lambda unrestricted leadOffset : Nat . (lambda unrestricted b : Byte . (lambda unrestricted rest : Bytes . (lambda unrestricted pos : Nat . (lambda unrestricted nextOffset : Nat . (lambda unrestricted reversed : (family UTF8Codepoints) . (nat-eliminate (lambda unrestricted valid : Nat . (family UTF8DecodeMachine)) (utf8MachineFailAt (constructor UTF8ErrorCode UTF8ContinuationInvalid) pos) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family UTF8DecodeMachine) . (nat-eliminate (lambda unrestricted overlong : Nat . (family UTF8DecodeMachine)) (nat-eliminate (lambda unrestricted surrogate : Nat . (family UTF8DecodeMachine)) (utf8MachineGoing rest nextOffset (constructor UTF8DecodePending UTF8PendingThreeB lead b) reversed) (lambda unrestricted surrogatePredecessor : Nat . (lambda unrestricted surrogateInduction : (family UTF8DecodeMachine) . (utf8MachineFailAt (constructor UTF8ErrorCode UTF8SurrogateCodepoint) leadOffset))) (utf8FlagAnd (byte-equal lead (byte 237)) (utf8ByteAtLeast b (byte 160)))) (lambda unrestricted overlongPredecessor : Nat . (lambda unrestricted overlongInduction : (family UTF8DecodeMachine) . (utf8MachineFailAt (constructor UTF8ErrorCode UTF8ThreeByteOverlong) leadOffset))) (utf8FlagAnd (byte-equal lead (byte 224)) (byte-less-than b (byte 160)))))) (utf8ContinuationValid b))))))))) -- Second continuation of a three-byte sequence, completing the codepoint. def utf8MachineThreeB = (lambda unrestricted lead : Byte . (lambda unrestricted b1 : Byte . (lambda unrestricted b : Byte . (lambda unrestricted rest : Bytes . (lambda unrestricted pos : Nat . (lambda unrestricted nextOffset : Nat . (lambda unrestricted reversed : (family UTF8Codepoints) . (nat-eliminate (lambda unrestricted valid : Nat . (family UTF8DecodeMachine)) (utf8MachineFailAt (constructor UTF8ErrorCode UTF8ContinuationInvalid) pos) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family UTF8DecodeMachine) . (utf8MachineEmit (utf8CodepointFromThree lead b1 b) rest nextOffset reversed))) (utf8ContinuationValid b))))))))) -- First continuation of a four-byte sequence. `leadOffset` carries the lead's -- offset for the overlong and out-of-range reports. def utf8MachineFourA = (lambda unrestricted lead : Byte . (lambda unrestricted leadOffset : Nat . (lambda unrestricted b : Byte . (lambda unrestricted rest : Bytes . (lambda unrestricted pos : Nat . (lambda unrestricted nextOffset : Nat . (lambda unrestricted reversed : (family UTF8Codepoints) . (nat-eliminate (lambda unrestricted valid : Nat . (family UTF8DecodeMachine)) (utf8MachineFailAt (constructor UTF8ErrorCode UTF8ContinuationInvalid) pos) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family UTF8DecodeMachine) . (nat-eliminate (lambda unrestricted overlong : Nat . (family UTF8DecodeMachine)) (nat-eliminate (lambda unrestricted outOfRange : Nat . (family UTF8DecodeMachine)) (utf8MachineGoing rest nextOffset (constructor UTF8DecodePending UTF8PendingFourB lead b) reversed) (lambda unrestricted rangePredecessor : Nat . (lambda unrestricted rangeInduction : (family UTF8DecodeMachine) . (utf8MachineFailAt (constructor UTF8ErrorCode UTF8CodepointOutOfRange) leadOffset))) (utf8FlagAnd (byte-equal lead (byte 244)) (utf8ByteAtLeast b (byte 144)))) (lambda unrestricted overlongPredecessor : Nat . (lambda unrestricted overlongInduction : (family UTF8DecodeMachine) . (utf8MachineFailAt (constructor UTF8ErrorCode UTF8FourByteOverlong) leadOffset))) (utf8FlagAnd (byte-equal lead (byte 240)) (byte-less-than b (byte 144)))))) (utf8ContinuationValid b))))))))) -- Second continuation of a four-byte sequence. def utf8MachineFourB = (lambda unrestricted lead : Byte . (lambda unrestricted b1 : Byte . (lambda unrestricted b : Byte . (lambda unrestricted rest : Bytes . (lambda unrestricted pos : Nat . (lambda unrestricted nextOffset : Nat . (lambda unrestricted reversed : (family UTF8Codepoints) . (nat-eliminate (lambda unrestricted valid : Nat . (family UTF8DecodeMachine)) (utf8MachineFailAt (constructor UTF8ErrorCode UTF8ContinuationInvalid) pos) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family UTF8DecodeMachine) . (utf8MachineGoing rest nextOffset (constructor UTF8DecodePending UTF8PendingFourC lead b1 b) reversed))) (utf8ContinuationValid b))))))))) -- Third continuation of a four-byte sequence, completing the codepoint. def utf8MachineFourC = (lambda unrestricted lead : Byte . (lambda unrestricted b1 : Byte . (lambda unrestricted b2 : Byte . (lambda unrestricted b : Byte . (lambda unrestricted rest : Bytes . (lambda unrestricted pos : Nat . (lambda unrestricted nextOffset : Nat . (lambda unrestricted reversed : (family UTF8Codepoints) . (nat-eliminate (lambda unrestricted valid : Nat . (family UTF8DecodeMachine)) (utf8MachineFailAt (constructor UTF8ErrorCode UTF8ContinuationInvalid) pos) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family UTF8DecodeMachine) . (utf8MachineEmit (utf8CodepointFromFour lead b1 b2 b) rest nextOffset reversed))) (utf8ContinuationValid b)))))))))) -- 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`. def utf8MachineStep = (lambda unrestricted machine : (family UTF8DecodeMachine) . (eliminate UTF8DecodeMachine (lambda unrestricted current : (family UTF8DecodeMachine) . (family UTF8DecodeMachine)) machine (branch UTF8DecodeMachineGoing remaining offset pending reversed . (app (lambda unrestricted b : Byte . (lambda unrestricted rest : Bytes . (eliminate UTF8DecodePending (lambda unrestricted current : (family UTF8DecodePending) . (family UTF8DecodeMachine)) pending (branch UTF8PendingReady . (utf8MachineReady b rest offset (succ offset) reversed)) (branch UTF8PendingTwo lead . (utf8MachineTwo lead b rest offset (succ offset) reversed)) (branch UTF8PendingThreeA lead leadOffset . (utf8MachineThreeA lead leadOffset b rest offset (succ offset) reversed)) (branch UTF8PendingThreeB lead byte1 . (utf8MachineThreeB lead byte1 b rest offset (succ offset) reversed)) (branch UTF8PendingFourA lead leadOffset . (utf8MachineFourA lead leadOffset b rest offset (succ offset) reversed)) (branch UTF8PendingFourB lead byte1 . (utf8MachineFourB lead byte1 b rest offset (succ offset) reversed)) (branch UTF8PendingFourC lead byte1 byte2 . (utf8MachineFourC lead byte1 byte2 b rest offset (succ offset) reversed))))) (bytes-head remaining) (bytes-tail remaining))) (branch UTF8DecodeMachineFailed error offset . (constructor UTF8DecodeMachine UTF8DecodeMachineFailed error offset)))) -- One step of an in-place list reversal driven by a first-order state VALUE: -- move the head of `remaining` onto `accumulated`. Empty `remaining` is a fixed -- point, so surplus fuel is harmless. The `eliminate` ignores its induction, so -- the reference machine does not fold the tail: each step is O(1). def utf8CodepointsReverseStep = (lambda unrestricted state : (family UTF8CodepointsReverseState) . (eliminate UTF8CodepointsReverseState (lambda unrestricted current : (family UTF8CodepointsReverseState) . (family UTF8CodepointsReverseState)) state (branch UTF8CodepointsReverseStateValue remaining accumulated . (eliminate UTF8Codepoints (lambda unrestricted current : (family UTF8Codepoints) . (family UTF8CodepointsReverseState)) remaining (branch UTF8CodepointsEnd . (constructor UTF8CodepointsReverseState UTF8CodepointsReverseStateValue (constructor UTF8Codepoints UTF8CodepointsEnd) accumulated)) (branch UTF8CodepointsNext head tail nodeInduction . (constructor UTF8CodepointsReverseState UTF8CodepointsReverseStateValue tail (constructor UTF8Codepoints UTF8CodepointsNext head accumulated))))))) -- Reverse a codepoint list in O(length). `fuel` need only be an upper bound on -- the list length (the caller passes the input byte count, always >= the -- codepoint count); once the list is exhausted the state stops changing. def utf8CodepointsReverse = (lambda unrestricted fuel : Nat . (lambda unrestricted list : (family UTF8Codepoints) . (eliminate UTF8CodepointsReverseState (lambda unrestricted current : (family UTF8CodepointsReverseState) . (family UTF8Codepoints)) (nat-eliminate (lambda unrestricted step : Nat . (family UTF8CodepointsReverseState)) (constructor UTF8CodepointsReverseState UTF8CodepointsReverseStateValue list (constructor UTF8Codepoints UTF8CodepointsEnd)) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family UTF8CodepointsReverseState) . (utf8CodepointsReverseStep induction))) fuel) (branch UTF8CodepointsReverseStateValue remaining accumulated . accumulated)))) -- A truncation failure carrying its byte offset (already a threaded `Nat`). def utf8DecodeTruncatedAt = (lambda unrestricted code : (family UTF8ErrorCode) . (lambda unrestricted offset : Nat . (constructor UTF8DecodeResult UTF8DecodeFailed code (utf8OffsetWord offset)))) -- 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. def decodeUTF8 = (lambda unrestricted input : Bytes . (eliminate UTF8DecodeMachine (lambda unrestricted current : (family UTF8DecodeMachine) . (family UTF8DecodeResult)) (nat-eliminate (lambda unrestricted step : Nat . (family UTF8DecodeMachine)) (utf8MachineGoing input zero (constructor UTF8DecodePending UTF8PendingReady) (constructor UTF8Codepoints UTF8CodepointsEnd)) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family UTF8DecodeMachine) . (utf8MachineStep induction))) (bytes-length input)) (branch UTF8DecodeMachineGoing remaining offset pending reversed . (eliminate UTF8DecodePending (lambda unrestricted current : (family UTF8DecodePending) . (family UTF8DecodeResult)) pending (branch UTF8PendingReady . (constructor UTF8DecodeResult UTF8DecodeSucceeded (utf8CodepointsReverse (bytes-length input) reversed))) (branch UTF8PendingTwo lead . (utf8DecodeTruncatedAt (constructor UTF8ErrorCode UTF8ContinuationMissing) offset)) (branch UTF8PendingThreeA lead leadOffset . (utf8DecodeTruncatedAt (constructor UTF8ErrorCode UTF8ContinuationMissing) offset)) (branch UTF8PendingThreeB lead byte1 . (utf8DecodeTruncatedAt (constructor UTF8ErrorCode UTF8SequenceTruncated) offset)) (branch UTF8PendingFourA lead leadOffset . (utf8DecodeTruncatedAt (constructor UTF8ErrorCode UTF8ContinuationMissing) offset)) (branch UTF8PendingFourB lead byte1 . (utf8DecodeTruncatedAt (constructor UTF8ErrorCode UTF8SequenceTruncated) offset)) (branch UTF8PendingFourC lead byte1 byte2 . (utf8DecodeTruncatedAt (constructor UTF8ErrorCode UTF8SequenceTruncated) offset)))) (branch UTF8DecodeMachineFailed error offset . (constructor UTF8DecodeResult UTF8DecodeFailed error (utf8OffsetWord offset))))) -- Scalar encoding is bounded by the four stored octets, never unary scalar -- magnitude. Masks/shifts form the exact Unicode UTF8 bit fields. def utf8ChooseEncoded = (lambda unrestricted condition : Nat . (lambda unrestricted yes : (pi unrestricted force : Nat . (family UTF8CodepointEncodeResult)) . (lambda unrestricted no : (pi unrestricted force : Nat . (family UTF8CodepointEncodeResult)) . (app (nat-eliminate (lambda unrestricted flag : Nat . (pi unrestricted force : Nat . (family UTF8CodepointEncodeResult))) no (lambda unrestricted predecessor : Nat . (lambda unrestricted unused : (pi unrestricted force : Nat . (family UTF8CodepointEncodeResult)) . yes)) condition) zero)))) def utf8EncodeCodepoint = (lambda unrestricted codepoint : (family UTF8Codepoint) . (eliminate UTF8Codepoint (lambda unrestricted current : (family UTF8Codepoint) . (family UTF8CodepointEncodeResult)) codepoint (branch UTF8CodepointValue word . (eliminate ModelWord32 (lambda unrestricted current : (family ModelWord32) . (family UTF8CodepointEncodeResult)) word (branch ModelWord32Value b0 b1 b2 b3 . (utf8ChooseEncoded (utf8FlagAnd (byte-equal b3 (byte 0)) (byte-less-than b2 (byte 17))) (lambda unrestricted force : Nat . (utf8ChooseEncoded (byte-equal b2 (byte 0)) (lambda unrestricted force : Nat . (utf8ChooseEncoded (utf8FlagAnd (byte-less-than (byte 215) b1) (byte-less-than b1 (byte 224))) (lambda unrestricted force : Nat . (constructor UTF8CodepointEncodeResult UTF8CodepointRejected (constructor UTF8ErrorCode UTF8SurrogateCodepoint))) (lambda unrestricted force : Nat . (utf8ChooseEncoded (utf8FlagAnd (byte-equal b1 (byte 0)) (byte-less-than b0 (byte 128))) (lambda unrestricted force : Nat . (constructor UTF8CodepointEncodeResult UTF8CodepointEncoded (bytes-cons b0 b""))) (lambda unrestricted force : Nat . (utf8ChooseEncoded (byte-less-than b1 (byte 8)) (lambda unrestricted force : Nat . (constructor UTF8CodepointEncodeResult UTF8CodepointEncoded (bytes-cons (Std.Byte/byteOr (byte 192) (Std.Byte/byteOr (Std.Byte/byteShiftRight b0 (byte-to-nat (byte 6))) (Std.Byte/byteShiftLeftTruncated b1 (byte-to-nat (byte 2))))) (bytes-cons (Std.Byte/byteOr (byte 128) (Std.Byte/byteAnd b0 (byte 63))) b"")))) (lambda unrestricted force : Nat . (constructor UTF8CodepointEncodeResult UTF8CodepointEncoded (bytes-cons (Std.Byte/byteOr (byte 224) (Std.Byte/byteShiftRight b1 (byte-to-nat (byte 4)))) (bytes-cons (Std.Byte/byteOr (byte 128) (Std.Byte/byteOr (Std.Byte/byteShiftRight b0 (byte-to-nat (byte 6))) (Std.Byte/byteShiftLeftTruncated (Std.Byte/byteAnd b1 (byte 15)) (byte-to-nat (byte 2))))) (bytes-cons (Std.Byte/byteOr (byte 128) (Std.Byte/byteAnd b0 (byte 63))) b""))))))))))) (lambda unrestricted force : Nat . (constructor UTF8CodepointEncodeResult UTF8CodepointEncoded (bytes-cons (Std.Byte/byteOr (byte 240) (Std.Byte/byteShiftRight b2 (byte-to-nat (byte 2)))) (bytes-cons (Std.Byte/byteOr (byte 128) (Std.Byte/byteOr (Std.Byte/byteShiftRight b1 (byte-to-nat (byte 4))) (Std.Byte/byteShiftLeftTruncated (Std.Byte/byteAnd b2 (byte 3)) (byte-to-nat (byte 4))))) (bytes-cons (Std.Byte/byteOr (byte 128) (Std.Byte/byteOr (Std.Byte/byteShiftRight b0 (byte-to-nat (byte 6))) (Std.Byte/byteShiftLeftTruncated (Std.Byte/byteAnd b1 (byte 15)) (byte-to-nat (byte 2))))) (bytes-cons (Std.Byte/byteOr (byte 128) (Std.Byte/byteAnd b0 (byte 63))) b"")))))))) (lambda unrestricted force : Nat . (constructor UTF8CodepointEncodeResult UTF8CodepointRejected (constructor UTF8ErrorCode UTF8CodepointOutOfRange))))))))) def utf8EncodeBuilderFold = (lambda unrestricted codepoints : (family UTF8Codepoints) . (eliminate UTF8Codepoints (lambda unrestricted current : (family UTF8Codepoints) . (family UTF8EncodeBuilderResult)) codepoints (branch UTF8CodepointsEnd . (constructor UTF8EncodeBuilderResult UTF8EncodeBuilderSucceeded (bytes-builder-empty))) (branch UTF8CodepointsNext head tail induction . (eliminate UTF8CodepointEncodeResult (lambda unrestricted current : (family UTF8CodepointEncodeResult) . (family UTF8EncodeBuilderResult)) (utf8EncodeCodepoint head) (branch UTF8CodepointEncoded encoded . (eliminate UTF8EncodeBuilderResult (lambda unrestricted current : (family UTF8EncodeBuilderResult) . (family UTF8EncodeBuilderResult)) induction (branch UTF8EncodeBuilderSucceeded suffix . (constructor UTF8EncodeBuilderResult UTF8EncodeBuilderSucceeded (bytes-builder-append (bytes-builder-chunk encoded) suffix))) (branch UTF8EncodeBuilderFailed code offset . (constructor UTF8EncodeBuilderResult UTF8EncodeBuilderFailed code (succ offset))))) (branch UTF8CodepointRejected code . (constructor UTF8EncodeBuilderResult UTF8EncodeBuilderFailed code zero)))))) def encodeUTF8 = (lambda unrestricted codepoints : (family UTF8Codepoints) . (eliminate UTF8EncodeBuilderResult (lambda unrestricted current : (family UTF8EncodeBuilderResult) . (family UTF8EncodeResult)) (utf8EncodeBuilderFold codepoints) (branch UTF8EncodeBuilderSucceeded builder . (constructor UTF8EncodeResult UTF8EncodeSucceeded (bytes-builder-build builder))) (branch UTF8EncodeBuilderFailed code offset . (constructor UTF8EncodeResult UTF8EncodeFailed code (utf8OffsetWord offset))))) -- Delegates to the one owner (Std.Flag), which this file already had a -- byte-for-byte copy of before `alpha-ast duplicates` found it (L24d). def utf8FlagOr = inferenceFlagOr def utf8ErrorStableCode = (lambda unrestricted code : (family UTF8ErrorCode) . (eliminate UTF8ErrorCode (lambda unrestricted current : (family UTF8ErrorCode) . Bytes) code (branch UTF8UnexpectedContinuation . b"UTF8-E001") (branch UTF8InvalidLeadingByte . b"UTF8-E002") (branch UTF8ContinuationMissing . b"UTF8-E003") (branch UTF8ContinuationInvalid . b"UTF8-E004") (branch UTF8TwoByteOverlong . b"UTF8-E005") (branch UTF8ThreeByteOverlong . b"UTF8-E006") (branch UTF8FourByteOverlong . b"UTF8-E007") (branch UTF8SurrogateCodepoint . b"UTF8-E008") (branch UTF8CodepointOutOfRange . b"UTF8-E009") (branch UTF8SequenceTruncated . b"UTF8-E010"))) def utf8WordScalarValid = (lambda unrestricted word : (family ModelWord32) . (app (lambda unrestricted value : Nat . (utf8FlagAnd (nat-less-than value utf8NaturalOneMillionOneHundredFourteenThousandOneHundredTwelve) (utf8FlagNot (utf8FlagAnd (utf8FlagNot (nat-less-than value utf8NaturalFiftyFiveThousandTwoHundredNinetySix)) (nat-less-than value utf8NaturalFiftySevenThousandThreeHundredFortyFour))))) (modelWord32ToNatural word))) def utf8CodepointScalarValid = (lambda unrestricted codepoint : (family UTF8Codepoint) . (eliminate UTF8Codepoint (lambda unrestricted current : (family UTF8Codepoint) . Nat) codepoint (branch UTF8CodepointValue word . (utf8WordScalarValid word)))) def utf8CodepointWidth = (lambda unrestricted codepoint : (family UTF8Codepoint) . (eliminate UTF8Codepoint (lambda unrestricted current : (family UTF8Codepoint) . Nat) codepoint (branch UTF8CodepointValue word . (app (lambda unrestricted value : Nat . (nat-eliminate (lambda unrestricted valid : Nat . Nat) zero (lambda unrestricted validPredecessor : Nat . (lambda unrestricted validInduction : Nat . (nat-eliminate (lambda unrestricted ascii : Nat . Nat) (nat-eliminate (lambda unrestricted twoByte : Nat . Nat) (nat-eliminate (lambda unrestricted threeByte : Nat . Nat) (byte-to-nat (byte 4)) (lambda unrestricted threePredecessor : Nat . (lambda unrestricted threeInduction : Nat . utf8NaturalThree)) (nat-less-than value utf8NaturalSixtyFiveThousandFiveHundredThirtySix)) (lambda unrestricted twoPredecessor : Nat . (lambda unrestricted twoInduction : Nat . utf8NaturalTwo)) (nat-less-than value utf8NaturalTwoThousandFortyEight)) (lambda unrestricted asciiPredecessor : Nat . (lambda unrestricted asciiInduction : Nat . utf8NaturalOne)) (nat-less-than value utf8NaturalOneHundredTwentyEight)))) (utf8WordScalarValid word))) (modelWord32ToNatural word))))) def utf8CodepointsLength = (lambda unrestricted codepoints : (family UTF8Codepoints) . (eliminate UTF8Codepoints (lambda unrestricted current : (family UTF8Codepoints) . Nat) codepoints (branch UTF8CodepointsEnd . zero) (branch UTF8CodepointsNext head tail induction . (succ induction)))) def utf8CodepointsWidthCount = (lambda unrestricted expected : Nat . (lambda unrestricted codepoints : (family UTF8Codepoints) . (eliminate UTF8Codepoints (lambda unrestricted current : (family UTF8Codepoints) . Nat) codepoints (branch UTF8CodepointsEnd . zero) (branch UTF8CodepointsNext head tail induction . (nat-eliminate (lambda unrestricted matches : Nat . Nat) induction (lambda unrestricted predecessor : Nat . (lambda unrestricted matchInduction : Nat . (succ induction))) (naturalEqual (utf8CodepointWidth head) expected)))))) def utf8CodepointsInvalidCount = (lambda unrestricted codepoints : (family UTF8Codepoints) . (eliminate UTF8Codepoints (lambda unrestricted current : (family UTF8Codepoints) . Nat) codepoints (branch UTF8CodepointsEnd . zero) (branch UTF8CodepointsNext head tail induction . (nat-eliminate (lambda unrestricted valid : Nat . Nat) (succ induction) (lambda unrestricted predecessor : Nat . (lambda unrestricted validInduction : Nat . induction)) (utf8CodepointScalarValid head))))) def utf8BytesCountWhere = (lambda unrestricted predicate : (pi unrestricted value : Byte . Nat) . (lambda unrestricted input : Bytes . (bytes-eliminate (lambda unrestricted current : Bytes . Nat) zero (lambda unrestricted head : Byte . (lambda unrestricted tail : Bytes . (lambda unrestricted induction : Nat . (nat-eliminate (lambda unrestricted matches : Nat . Nat) induction (lambda unrestricted predecessor : Nat . (lambda unrestricted matchInduction : Nat . (succ induction))) (predicate head))))) input))) def utf8ByteIllegal = (lambda unrestricted value : Byte . (utf8FlagNot (utf8FlagOr (byte-less-than value (byte 128)) (utf8FlagOr (utf8ContinuationValid value) (utf8FlagOr (utf8LeadTwoValid value) (utf8FlagOr (utf8LeadThreeValid value) (utf8LeadFourValid value))))))) def utf8DecodeTelemetryFor = (lambda unrestricted input : Bytes . (lambda unrestricted inspected : Nat . (lambda unrestricted codepoints : (family UTF8Codepoints) . (lambda unrestricted failurePresent : Nat . (lambda unrestricted failureOffset : Nat . (constructor UTF8DecodeTelemetry UTF8DecodeTelemetryValue (bytes-length input) inspected (utf8CodepointsLength codepoints) (utf8CodepointsWidthCount utf8NaturalOne codepoints) (utf8CodepointsWidthCount utf8NaturalTwo codepoints) (utf8CodepointsWidthCount utf8NaturalThree codepoints) (utf8CodepointsWidthCount (byte-to-nat (byte 4)) codepoints) (utf8BytesCountWhere utf8ContinuationValid input) (utf8BytesCountWhere utf8ByteIllegal input) failurePresent failureOffset)))))) def utf8EncodeTelemetryFor = (lambda unrestricted codepoints : (family UTF8Codepoints) . (lambda unrestricted processed : Nat . (lambda unrestricted outputBytes : Nat . (lambda unrestricted failurePresent : Nat . (lambda unrestricted failureOrdinal : Nat . (constructor UTF8EncodeTelemetry UTF8EncodeTelemetryValue (utf8CodepointsLength codepoints) processed outputBytes (utf8CodepointsWidthCount utf8NaturalOne codepoints) (utf8CodepointsWidthCount utf8NaturalTwo codepoints) (utf8CodepointsWidthCount utf8NaturalThree codepoints) (utf8CodepointsWidthCount (byte-to-nat (byte 4)) codepoints) (utf8CodepointsInvalidCount codepoints) failurePresent failureOrdinal)))))) def decodeUTF8WithTelemetry = (lambda unrestricted input : Bytes . (eliminate UTF8DecodeResult (lambda unrestricted current : (family UTF8DecodeResult) . (family UTF8DecodeExecutionResult)) (decodeUTF8 input) (branch UTF8DecodeSucceeded codepoints . (constructor UTF8DecodeExecutionResult UTF8DecodeExecutionSucceeded codepoints (utf8DecodeTelemetryFor input (bytes-length input) codepoints zero zero))) (branch UTF8DecodeFailed code offset . (app (lambda unrestricted exactOffset : Nat . (constructor UTF8DecodeExecutionResult UTF8DecodeExecutionFailed code offset (utf8ErrorStableCode code) (utf8DecodeTelemetryFor input exactOffset (constructor UTF8Codepoints UTF8CodepointsEnd) (succ zero) exactOffset))) (modelWord32ToNatural offset))))) def encodeUTF8WithTelemetry = (lambda unrestricted codepoints : (family UTF8Codepoints) . (eliminate UTF8EncodeResult (lambda unrestricted current : (family UTF8EncodeResult) . (family UTF8EncodeExecutionResult)) (encodeUTF8 codepoints) (branch UTF8EncodeSucceeded encoded . (constructor UTF8EncodeExecutionResult UTF8EncodeExecutionSucceeded encoded (utf8EncodeTelemetryFor codepoints (utf8CodepointsLength codepoints) (bytes-length encoded) zero zero))) (branch UTF8EncodeFailed code offset . (app (lambda unrestricted exactOffset : Nat . (constructor UTF8EncodeExecutionResult UTF8EncodeExecutionFailed code offset (utf8ErrorStableCode code) (utf8EncodeTelemetryFor codepoints exactOffset zero (succ zero) exactOffset))) (modelWord32ToNatural offset))))) -- Text and the compiler share this validity decision with the existing decoder. -- No replacement character, normalization or second validation machine. def stdUtf8Valid : (pi unrestricted input : Bytes . (family StdBool)) = (lambda unrestricted input : Bytes . (eliminate UTF8DecodeResult (lambda unrestricted result : (family UTF8DecodeResult) . (family StdBool)) (decodeUTF8 input) (branch UTF8DecodeSucceeded codepoints . (constructor StdBool StdTrue)) (branch UTF8DecodeFailed error offset . (constructor StdBool StdFalse))))