1module Data.UTF8
2
3import Model.Config
4import Model.Word32
5import Std.Byte
6import Std.Natural
7import Std.Foundation
8import Std.Flag
9
10family UTF8Codepoint : Type 0
11constructor UTF8CodepointValue
12field unrestricted utf8CodepointWord : (family ModelWord32)
13
14end-family
15
16family UTF8Codepoints : Type 0
17constructor UTF8CodepointsEnd
18constructor UTF8CodepointsNext
19field unrestricted utf8CodepointHead : (family UTF8Codepoint)
20recursive unrestricted utf8CodepointTail
21
22end-family
23
24family UTF8DecoderState : Type 0
25constructor UTF8DecoderReady
26constructor UTF8DecoderNeedOne
27field unrestricted utf8DecoderOneLead : Byte
28constructor UTF8DecoderNeedTwo
29field unrestricted utf8DecoderTwoLead : Byte
30field unrestricted utf8DecoderTwoByte1 : Byte
31constructor UTF8DecoderNeedThree
32field unrestricted utf8DecoderThreeLead : Byte
33field unrestricted utf8DecoderThreeByte1 : Byte
34field unrestricted utf8DecoderThreeByte2 : Byte
35
36end-family
37
38family UTF8ErrorCode : Type 0
39constructor UTF8UnexpectedContinuation
40constructor UTF8InvalidLeadingByte
41constructor UTF8ContinuationMissing
42constructor UTF8ContinuationInvalid
43constructor UTF8TwoByteOverlong
44constructor UTF8ThreeByteOverlong
45constructor UTF8FourByteOverlong
46constructor UTF8SurrogateCodepoint
47constructor UTF8CodepointOutOfRange
48constructor UTF8SequenceTruncated
49
50end-family
51
52family UTF8DecodeResult : Type 0
53constructor UTF8DecodeSucceeded
54field unrestricted utf8DecodedCodepoints : (family UTF8Codepoints)
55constructor UTF8DecodeFailed
56field unrestricted utf8DecodeError : (family UTF8ErrorCode)
57field unrestricted utf8DecodeOffset : (family ModelWord32)
58
59end-family
60
61family UTF8EncodeResult : Type 0
62constructor UTF8EncodeSucceeded
63field unrestricted utf8EncodedBytes : Bytes
64constructor UTF8EncodeFailed
65field unrestricted utf8EncodeError : (family UTF8ErrorCode)
66field unrestricted utf8EncodeOffset : (family ModelWord32)
67
68end-family
69
70family UTF8CodepointEncodeResult : Type 0
71constructor UTF8CodepointEncoded
72field unrestricted utf8CodepointEncodedBytes : Bytes
73constructor UTF8CodepointRejected
74field unrestricted utf8CodepointEncodeError : (family UTF8ErrorCode)
75
76end-family
77
78family UTF8EncodeBuilderResult : Type 0
79constructor UTF8EncodeBuilderSucceeded
80field unrestricted utf8EncodedBuilder : BytesBuilder
81constructor UTF8EncodeBuilderFailed
82field unrestricted utf8EncodeBuilderError : (family UTF8ErrorCode)
83field unrestricted utf8EncodeBuilderOffset : Nat
84
85end-family
86
87family UTF8DecodeTelemetry : Type 0
88constructor UTF8DecodeTelemetryValue
89field unrestricted utf8DecodeTelemetryInputBytes : Nat
90field unrestricted utf8DecodeTelemetryInspectedBytes : Nat
91field unrestricted utf8DecodeTelemetryCodepoints : Nat
92field unrestricted utf8DecodeTelemetryASCII : Nat
93field unrestricted utf8DecodeTelemetryTwoByte : Nat
94field unrestricted utf8DecodeTelemetryThreeByte : Nat
95field unrestricted utf8DecodeTelemetryFourByte : Nat
96field unrestricted utf8DecodeTelemetryContinuationBytes : Nat
97field unrestricted utf8DecodeTelemetryIllegalBytes : Nat
98field unrestricted utf8DecodeTelemetryFailurePresent : Nat
99field unrestricted utf8DecodeTelemetryFailureOffset : Nat
100
101end-family
102
103family UTF8EncodeTelemetry : Type 0
104constructor UTF8EncodeTelemetryValue
105field unrestricted utf8EncodeTelemetryInputCodepoints : Nat
106field unrestricted utf8EncodeTelemetryProcessedCodepoints : Nat
107field unrestricted utf8EncodeTelemetryOutputBytes : Nat
108field unrestricted utf8EncodeTelemetryASCII : Nat
109field unrestricted utf8EncodeTelemetryTwoByte : Nat
110field unrestricted utf8EncodeTelemetryThreeByte : Nat
111field unrestricted utf8EncodeTelemetryFourByte : Nat
112field unrestricted utf8EncodeTelemetryInvalidScalars : Nat
113field unrestricted utf8EncodeTelemetryFailurePresent : Nat
114field unrestricted utf8EncodeTelemetryFailureOrdinal : Nat
115
116end-family
117
118family UTF8DecodeExecutionResult : Type 0
119constructor UTF8DecodeExecutionSucceeded
120field unrestricted utf8DecodeExecutionCodepoints : (family UTF8Codepoints)
121field unrestricted utf8DecodeExecutionTelemetry : (family UTF8DecodeTelemetry)
122constructor UTF8DecodeExecutionFailed
123field unrestricted utf8DecodeExecutionError : (family UTF8ErrorCode)
124field unrestricted utf8DecodeExecutionOffset : (family ModelWord32)
125field unrestricted utf8DecodeExecutionStableError : Bytes
126field unrestricted utf8DecodeExecutionTelemetryBeforeFailure : (family UTF8DecodeTelemetry)
127
128end-family
129
130family UTF8EncodeExecutionResult : Type 0
131constructor UTF8EncodeExecutionSucceeded
132field unrestricted utf8EncodeExecutionBytes : Bytes
133field unrestricted utf8EncodeExecutionTelemetry : (family UTF8EncodeTelemetry)
134constructor UTF8EncodeExecutionFailed
135field unrestricted utf8EncodeExecutionError : (family UTF8ErrorCode)
136field unrestricted utf8EncodeExecutionOffset : (family ModelWord32)
137field unrestricted utf8EncodeExecutionStableError : Bytes
138field unrestricted utf8EncodeExecutionTelemetryBeforeFailure : (family UTF8EncodeTelemetry)
139
140end-family
141
142-- Pending multi-byte context for the byte-at-a-time decoder (see `decodeUTF8`).
143-- `Ready` is a codepoint boundary; the others hold the lead byte and the
144-- continuation bytes collected so far while more are awaited. `ThreeA`/`FourA`
145-- also carry the lead's byte offset, the only states whose error (overlong /
146-- surrogate / out-of-range) is reported AT the lead rather than at the byte
147-- being read.
148family UTF8DecodePending : Type 0
149constructor UTF8PendingReady
150constructor UTF8PendingTwo
151field unrestricted utf8PendingTwoLead : Byte
152constructor UTF8PendingThreeA
153field unrestricted utf8PendingThreeALead : Byte
154field unrestricted utf8PendingThreeAOffset : Nat
155constructor UTF8PendingThreeB
156field unrestricted utf8PendingThreeBLead : Byte
157field unrestricted utf8PendingThreeBByte1 : Byte
158constructor UTF8PendingFourA
159field unrestricted utf8PendingFourALead : Byte
160field unrestricted utf8PendingFourAOffset : Nat
161constructor UTF8PendingFourB
162field unrestricted utf8PendingFourBLead : Byte
163field unrestricted utf8PendingFourBByte1 : Byte
164constructor UTF8PendingFourC
165field unrestricted utf8PendingFourCLead : Byte
166field unrestricted utf8PendingFourCByte1 : Byte
167field unrestricted utf8PendingFourCByte2 : Byte
168
169end-family
170
171-- Byte-at-a-time decoder accumulator threaded by a `nat-eliminate` over the
172-- input length. Every step is O(1): it peels one byte with `bytes-head` /
173-- `bytes-tail` (both O(1) on the `[Word8]` representation), advances the offset
174-- with `succ` (O(1)), and either prepends a completed codepoint onto
175-- `utf8MachineReversed` or updates `utf8MachinePending`. It must avoid
176-- `bytes-eliminate`, `bytes-length` and `naturalAdd` in the loop: the reference
177-- machine folds the ENTIRE tail to build a (here unused) induction for those, so
178-- one call is O(remaining) and per-step use would be O(length^2). Fuel equals
179-- the byte count exactly, so a step never reads past the end (no empty test is
180-- needed). `Failed` is a fixed point that absorbs any surplus fuel.
181family UTF8DecodeMachine : Type 0
182constructor UTF8DecodeMachineGoing
183field unrestricted utf8MachineRemaining : Bytes
184field unrestricted utf8MachineOffset : Nat
185field unrestricted utf8MachinePending : (family UTF8DecodePending)
186field unrestricted utf8MachineReversed : (family UTF8Codepoints)
187constructor UTF8DecodeMachineFailed
188field unrestricted utf8MachineError : (family UTF8ErrorCode)
189field unrestricted utf8MachineErrorOffset : Nat
190
191end-family
192
193-- First-order reversal accumulator: `utf8ReverseRemaining` is the list still to
194-- move, `utf8ReverseAccumulated` is the reversed prefix already built.
195family UTF8CodepointsReverseState : Type 0
196constructor UTF8CodepointsReverseStateValue
197field unrestricted utf8ReverseRemaining : (family UTF8Codepoints)
198field unrestricted utf8ReverseAccumulated : (family UTF8Codepoints)
199
200end-family
201
202def utf8MaximumCodepoint =
203 (constructor ModelWord32 ModelWord32Value (byte 255) (byte 255) (byte 16) (byte 0))
204
205def utf8SurrogateMinimum =
206 (constructor ModelWord32 ModelWord32Value (byte 0) (byte 216) (byte 0) (byte 0))
207
208def utf8SurrogateMaximum =
209 (constructor ModelWord32 ModelWord32Value (byte 255) (byte 223) (byte 0) (byte 0))
210
211def utf8NaturalOne =
212 (succ zero)
213
214def utf8NaturalTwo =
215 (succ utf8NaturalOne)
216
217def utf8NaturalThree =
218 (succ utf8NaturalTwo)
219
220def utf8NaturalSix =
221 (byte-to-nat (byte 6))
222
223def utf8NaturalTwelve =
224 (byte-to-nat (byte 12))
225
226def utf8NaturalEighteen =
227 (byte-to-nat (byte 18))
228
229def utf8NaturalSixtyFour =
230 (byte-to-nat (byte 64))
231
232def utf8NaturalOneHundredTwentyEight =
233 (naturalPowerOfTwo (byte-to-nat (byte 7)))
234
235def utf8NaturalTwoThousandFortyEight =
236 (naturalPowerOfTwo (byte-to-nat (byte 11)))
237
238def utf8NaturalFiftyFiveThousandTwoHundredNinetySix =
239 (naturalMultiply (byte-to-nat (byte 216)) byteNaturalTwoHundredFiftySix)
240
241def utf8NaturalFiftySevenThousandThreeHundredFortyFour =
242 (naturalMultiply (byte-to-nat (byte 224)) byteNaturalTwoHundredFiftySix)
243
244def utf8NaturalSixtyFiveThousandFiveHundredThirtySix =
245 (naturalPowerOfTwo (byte-to-nat (byte 16)))
246
247def utf8NaturalOneMillionOneHundredFourteenThousandOneHundredTwelve =
248 (naturalMultiply (byte-to-nat (byte 17)) utf8NaturalSixtyFiveThousandFiveHundredThirtySix)
249
250-- Delegates to the one owner (Std.Flag): this body is alpha-equivalent to
251-- Std.Flag.inferenceFlagNot (binder renamed value<->flag, otherwise
252-- identical) -- missed by `alpha-ast duplicates`' exact (binder-name-
253-- sensitive) shape digest, found by manual inspection after that tool
254-- grouped it with Std.Natural.naturalIsZero instead (also alpha-equivalent
255-- to inferenceFlagNot, coincidentally under the same binder name "value").
256def utf8FlagNot =
257 inferenceFlagNot
258
259-- Delegates to the one owner (Std.Flag), which this file already had a
260-- byte-for-byte copy of before `alpha-ast duplicates` found it (L24d).
261def utf8FlagAnd =
262 inferenceFlagAnd
263
264def utf8ByteAtLeast =
265 (lambda unrestricted value : Byte .
266 (lambda unrestricted minimum : Byte . (utf8FlagNot (byte-less-than value minimum))))
267
268def utf8ByteInHalfOpenRange =
269 (lambda unrestricted value : Byte .
270 (lambda unrestricted minimum : Byte .
271 (lambda unrestricted maximum : Byte .
272 (utf8FlagAnd (utf8ByteAtLeast value minimum) (byte-less-than value maximum)))))
273
274def utf8ContinuationValid =
275 (lambda unrestricted value : Byte . (utf8ByteInHalfOpenRange value (byte 128) (byte 192)))
276
277def utf8LeadTwoValid =
278 (lambda unrestricted value : Byte . (utf8ByteInHalfOpenRange value (byte 194) (byte 224)))
279
280def utf8LeadThreeValid =
281 (lambda unrestricted value : Byte . (utf8ByteInHalfOpenRange value (byte 224) (byte 240)))
282
283def utf8LeadFourValid =
284 (lambda unrestricted value : Byte . (utf8ByteInHalfOpenRange value (byte 240) (byte 245)))
285
286def utf8OffsetWord =
287 (lambda unrestricted offset : Nat . (modelWord32FromNaturalTruncated offset))
288
289-- Build a failed machine at byte offset `offset` (a `Nat` already threaded via
290-- `succ`; converted to the public ModelWord32 offset once, in `decodeUTF8`).
291def utf8MachineFailAt =
292 (lambda unrestricted code : (family UTF8ErrorCode) .
293 (lambda unrestricted offset : Nat .
294 (constructor UTF8DecodeMachine UTF8DecodeMachineFailed code offset)))
295
296-- Build a still-going machine.
297def utf8MachineGoing =
298 (lambda unrestricted remaining : Bytes .
299 (lambda unrestricted offset : Nat .
300 (lambda unrestricted pending : (family UTF8DecodePending) .
301 (lambda unrestricted reversed : (family UTF8Codepoints) .
302 (constructor UTF8DecodeMachine UTF8DecodeMachineGoing remaining offset pending reversed)))))
303
304-- Complete a codepoint: return to `Ready` with the codepoint prepended onto the
305-- reversed accumulator (O(1)).
306def utf8MachineEmit =
307 (lambda unrestricted codepoint : (family UTF8Codepoint) .
308 (lambda unrestricted remaining : Bytes .
309 (lambda unrestricted offset : Nat .
310 (lambda unrestricted reversed : (family UTF8Codepoints) .
311 (utf8MachineGoing
312 remaining
313 offset
314 (constructor UTF8DecodePending UTF8PendingReady)
315 (constructor UTF8Codepoints UTF8CodepointsNext codepoint reversed))))))
316
317-- Codepoint words are composed from the byte bits directly (D17): no natural
318-- arithmetic, so a decoded character costs a handful of byte operations
319-- instead of a fold over the codepoint's value.
320def utf8CodepointWord =
321 (lambda unrestricted b0 : Byte .
322 (lambda unrestricted b1 : Byte .
323 (lambda unrestricted b2 : Byte .
324 (constructor
325 UTF8Codepoint
326 UTF8CodepointValue
327 (constructor ModelWord32 ModelWord32Value b0 b1 b2 (byte 0))))))
328
329def utf8CodepointFromOne =
330 (lambda unrestricted lead : Byte . (utf8CodepointWord lead (byte 0) (byte 0)))
331
332-- (lead & 0x1F) << 6 | (b1 & 0x3F)
333def utf8CodepointFromTwo =
334 (lambda unrestricted lead : Byte .
335 (lambda unrestricted b1 : Byte .
336 (utf8CodepointWord
337 (byteOr
338 (byteShiftLeftTruncated (byteAnd lead (byte 3)) utf8NaturalSix)
339 (byteAnd b1 (byte 63)))
340 (byteShiftRight (byteAnd lead (byte 31)) utf8NaturalTwo)
341 (byte 0))))
342
343-- (lead & 0x0F) << 12 | (b1 & 0x3F) << 6 | (b2 & 0x3F)
344def utf8CodepointFromThree =
345 (lambda unrestricted lead : Byte .
346 (lambda unrestricted b1 : Byte .
347 (lambda unrestricted b2 : Byte .
348 (utf8CodepointWord
349 (byteOr
350 (byteShiftLeftTruncated (byteAnd b1 (byte 3)) utf8NaturalSix)
351 (byteAnd b2 (byte 63)))
352 (byteOr
353 (byteShiftLeftTruncated (byteAnd lead (byte 15)) (byte-to-nat (byte 4)))
354 (byteShiftRight (byteAnd b1 (byte 63)) utf8NaturalTwo))
355 (byte 0)))))
356
357-- (lead & 0x07) << 18 | (b1 & 0x3F) << 12 | (b2 & 0x3F) << 6 | (b3 & 0x3F)
358def utf8CodepointFromFour =
359 (lambda unrestricted lead : Byte .
360 (lambda unrestricted b1 : Byte .
361 (lambda unrestricted b2 : Byte .
362 (lambda unrestricted b3 : Byte .
363 (utf8CodepointWord
364 (byteOr
365 (byteShiftLeftTruncated (byteAnd b2 (byte 3)) utf8NaturalSix)
366 (byteAnd b3 (byte 63)))
367 (byteOr
368 (byteShiftLeftTruncated (byteAnd b1 (byte 15)) (byte-to-nat (byte 4)))
369 (byteShiftRight (byteAnd b2 (byte 63)) utf8NaturalTwo))
370 (byteOr
371 (byteShiftLeftTruncated (byteAnd lead (byte 7)) utf8NaturalTwo)
372 (byteShiftRight (byteAnd b1 (byte 63)) (byte-to-nat (byte 4)))))))))
373
374-- Ready-state byte: `b` is a codepoint start at byte offset `pos`; `rest` is the
375-- suffix after it and `nextOffset` = succ pos. Dispatch by class exactly as the
376-- original: ASCII emits; a 2/3/4-byte lead moves to the matching pending state;
377-- a bare continuation, a 0xC0/0xC1 lead, or any other byte fails AT `pos`.
378def utf8MachineReady =
379 (lambda unrestricted b : Byte .
380 (lambda unrestricted rest : Bytes .
381 (lambda unrestricted pos : Nat .
382 (lambda unrestricted nextOffset : Nat .
383 (lambda unrestricted reversed : (family UTF8Codepoints) .
384 (nat-eliminate
385 (lambda unrestricted ascii : Nat . (family UTF8DecodeMachine))
386 (nat-eliminate
387 (lambda unrestricted leadTwo : Nat . (family UTF8DecodeMachine))
388 (nat-eliminate
389 (lambda unrestricted leadThree : Nat . (family UTF8DecodeMachine))
390 (nat-eliminate
391 (lambda unrestricted leadFour : Nat . (family UTF8DecodeMachine))
392 (nat-eliminate
393 (lambda unrestricted continuationByte : Nat . (family UTF8DecodeMachine))
394 (nat-eliminate
395 (lambda unrestricted overlongTwo : Nat . (family UTF8DecodeMachine))
396 (utf8MachineFailAt (constructor UTF8ErrorCode UTF8InvalidLeadingByte) pos)
397 (lambda unrestricted overlongPredecessor : Nat .
398 (lambda unrestricted overlongInduction : (family UTF8DecodeMachine) .
399 (utf8MachineFailAt (constructor UTF8ErrorCode UTF8TwoByteOverlong) pos)))
400 (utf8FlagAnd (utf8ByteAtLeast b (byte 192)) (byte-less-than b (byte 194))))
401 (lambda unrestricted continuationPredecessor : Nat .
402 (lambda unrestricted continuationInduction : (family UTF8DecodeMachine) .
403 (utf8MachineFailAt
404 (constructor UTF8ErrorCode UTF8UnexpectedContinuation)
405 pos)))
406 (utf8ContinuationValid b))
407 (lambda unrestricted fourPredecessor : Nat .
408 (lambda unrestricted fourInduction : (family UTF8DecodeMachine) .
409 (utf8MachineGoing
410 rest
411 nextOffset
412 (constructor UTF8DecodePending UTF8PendingFourA b pos)
413 reversed)))
414 (utf8LeadFourValid b))
415 (lambda unrestricted threePredecessor : Nat .
416 (lambda unrestricted threeInduction : (family UTF8DecodeMachine) .
417 (utf8MachineGoing
418 rest
419 nextOffset
420 (constructor UTF8DecodePending UTF8PendingThreeA b pos)
421 reversed)))
422 (utf8LeadThreeValid b))
423 (lambda unrestricted twoPredecessor : Nat .
424 (lambda unrestricted twoInduction : (family UTF8DecodeMachine) .
425 (utf8MachineGoing
426 rest
427 nextOffset
428 (constructor UTF8DecodePending UTF8PendingTwo b)
429 reversed)))
430 (utf8LeadTwoValid b))
431 (lambda unrestricted asciiPredecessor : Nat .
432 (lambda unrestricted asciiInduction : (family UTF8DecodeMachine) .
433 (utf8MachineEmit (utf8CodepointFromOne b) rest nextOffset reversed)))
434 (byte-less-than b (byte 128))))))))
435
436-- Second byte of a two-byte sequence at offset `pos`.
437def utf8MachineTwo =
438 (lambda unrestricted lead : Byte .
439 (lambda unrestricted b : Byte .
440 (lambda unrestricted rest : Bytes .
441 (lambda unrestricted pos : Nat .
442 (lambda unrestricted nextOffset : Nat .
443 (lambda unrestricted reversed : (family UTF8Codepoints) .
444 (nat-eliminate
445 (lambda unrestricted valid : Nat . (family UTF8DecodeMachine))
446 (utf8MachineFailAt (constructor UTF8ErrorCode UTF8ContinuationInvalid) pos)
447 (lambda unrestricted predecessor : Nat .
448 (lambda unrestricted induction : (family UTF8DecodeMachine) .
449 (utf8MachineEmit (utf8CodepointFromTwo lead b) rest nextOffset reversed)))
450 (utf8ContinuationValid b))))))))
451
452-- First continuation of a three-byte sequence. `leadOffset` is the lead's byte
453-- offset (overlong and surrogate are reported there); `pos` is this byte's.
454def utf8MachineThreeA =
455 (lambda unrestricted lead : Byte .
456 (lambda unrestricted leadOffset : Nat .
457 (lambda unrestricted b : Byte .
458 (lambda unrestricted rest : Bytes .
459 (lambda unrestricted pos : Nat .
460 (lambda unrestricted nextOffset : Nat .
461 (lambda unrestricted reversed : (family UTF8Codepoints) .
462 (nat-eliminate
463 (lambda unrestricted valid : Nat . (family UTF8DecodeMachine))
464 (utf8MachineFailAt (constructor UTF8ErrorCode UTF8ContinuationInvalid) pos)
465 (lambda unrestricted predecessor : Nat .
466 (lambda unrestricted induction : (family UTF8DecodeMachine) .
467 (nat-eliminate
468 (lambda unrestricted overlong : Nat . (family UTF8DecodeMachine))
469 (nat-eliminate
470 (lambda unrestricted surrogate : Nat . (family UTF8DecodeMachine))
471 (utf8MachineGoing
472 rest
473 nextOffset
474 (constructor UTF8DecodePending UTF8PendingThreeB lead b)
475 reversed)
476 (lambda unrestricted surrogatePredecessor : Nat .
477 (lambda unrestricted surrogateInduction : (family UTF8DecodeMachine) .
478 (utf8MachineFailAt
479 (constructor UTF8ErrorCode UTF8SurrogateCodepoint)
480 leadOffset)))
481 (utf8FlagAnd (byte-equal lead (byte 237)) (utf8ByteAtLeast b (byte 160))))
482 (lambda unrestricted overlongPredecessor : Nat .
483 (lambda unrestricted overlongInduction : (family UTF8DecodeMachine) .
484 (utf8MachineFailAt
485 (constructor UTF8ErrorCode UTF8ThreeByteOverlong)
486 leadOffset)))
487 (utf8FlagAnd (byte-equal lead (byte 224)) (byte-less-than b (byte 160))))))
488 (utf8ContinuationValid b)))))))))
489
490-- Second continuation of a three-byte sequence, completing the codepoint.
491def utf8MachineThreeB =
492 (lambda unrestricted lead : Byte .
493 (lambda unrestricted b1 : Byte .
494 (lambda unrestricted b : Byte .
495 (lambda unrestricted rest : Bytes .
496 (lambda unrestricted pos : Nat .
497 (lambda unrestricted nextOffset : Nat .
498 (lambda unrestricted reversed : (family UTF8Codepoints) .
499 (nat-eliminate
500 (lambda unrestricted valid : Nat . (family UTF8DecodeMachine))
501 (utf8MachineFailAt (constructor UTF8ErrorCode UTF8ContinuationInvalid) pos)
502 (lambda unrestricted predecessor : Nat .
503 (lambda unrestricted induction : (family UTF8DecodeMachine) .
504 (utf8MachineEmit (utf8CodepointFromThree lead b1 b) rest nextOffset reversed)))
505 (utf8ContinuationValid b)))))))))
506
507-- First continuation of a four-byte sequence. `leadOffset` carries the lead's
508-- offset for the overlong and out-of-range reports.
509def utf8MachineFourA =
510 (lambda unrestricted lead : Byte .
511 (lambda unrestricted leadOffset : Nat .
512 (lambda unrestricted b : Byte .
513 (lambda unrestricted rest : Bytes .
514 (lambda unrestricted pos : Nat .
515 (lambda unrestricted nextOffset : Nat .
516 (lambda unrestricted reversed : (family UTF8Codepoints) .
517 (nat-eliminate
518 (lambda unrestricted valid : Nat . (family UTF8DecodeMachine))
519 (utf8MachineFailAt (constructor UTF8ErrorCode UTF8ContinuationInvalid) pos)
520 (lambda unrestricted predecessor : Nat .
521 (lambda unrestricted induction : (family UTF8DecodeMachine) .
522 (nat-eliminate
523 (lambda unrestricted overlong : Nat . (family UTF8DecodeMachine))
524 (nat-eliminate
525 (lambda unrestricted outOfRange : Nat . (family UTF8DecodeMachine))
526 (utf8MachineGoing
527 rest
528 nextOffset
529 (constructor UTF8DecodePending UTF8PendingFourB lead b)
530 reversed)
531 (lambda unrestricted rangePredecessor : Nat .
532 (lambda unrestricted rangeInduction : (family UTF8DecodeMachine) .
533 (utf8MachineFailAt
534 (constructor UTF8ErrorCode UTF8CodepointOutOfRange)
535 leadOffset)))
536 (utf8FlagAnd (byte-equal lead (byte 244)) (utf8ByteAtLeast b (byte 144))))
537 (lambda unrestricted overlongPredecessor : Nat .
538 (lambda unrestricted overlongInduction : (family UTF8DecodeMachine) .
539 (utf8MachineFailAt
540 (constructor UTF8ErrorCode UTF8FourByteOverlong)
541 leadOffset)))
542 (utf8FlagAnd (byte-equal lead (byte 240)) (byte-less-than b (byte 144))))))
543 (utf8ContinuationValid b)))))))))
544
545-- Second continuation of a four-byte sequence.
546def utf8MachineFourB =
547 (lambda unrestricted lead : Byte .
548 (lambda unrestricted b1 : Byte .
549 (lambda unrestricted b : Byte .
550 (lambda unrestricted rest : Bytes .
551 (lambda unrestricted pos : Nat .
552 (lambda unrestricted nextOffset : Nat .
553 (lambda unrestricted reversed : (family UTF8Codepoints) .
554 (nat-eliminate
555 (lambda unrestricted valid : Nat . (family UTF8DecodeMachine))
556 (utf8MachineFailAt (constructor UTF8ErrorCode UTF8ContinuationInvalid) pos)
557 (lambda unrestricted predecessor : Nat .
558 (lambda unrestricted induction : (family UTF8DecodeMachine) .
559 (utf8MachineGoing
560 rest
561 nextOffset
562 (constructor UTF8DecodePending UTF8PendingFourC lead b1 b)
563 reversed)))
564 (utf8ContinuationValid b)))))))))
565
566-- Third continuation of a four-byte sequence, completing the codepoint.
567def utf8MachineFourC =
568 (lambda unrestricted lead : Byte .
569 (lambda unrestricted b1 : Byte .
570 (lambda unrestricted b2 : Byte .
571 (lambda unrestricted b : Byte .
572 (lambda unrestricted rest : Bytes .
573 (lambda unrestricted pos : Nat .
574 (lambda unrestricted nextOffset : Nat .
575 (lambda unrestricted reversed : (family UTF8Codepoints) .
576 (nat-eliminate
577 (lambda unrestricted valid : Nat . (family UTF8DecodeMachine))
578 (utf8MachineFailAt (constructor UTF8ErrorCode UTF8ContinuationInvalid) pos)
579 (lambda unrestricted predecessor : Nat .
580 (lambda unrestricted induction : (family UTF8DecodeMachine) .
581 (utf8MachineEmit
582 (utf8CodepointFromFour lead b1 b2 b)
583 rest
584 nextOffset
585 reversed)))
586 (utf8ContinuationValid b))))))))))
587
588-- One decode step: `Failed` is a fixed point; `Going` peels one byte (O(1) via
589-- `bytes-head`/`bytes-tail`) at offset `offset` and dispatches on the pending
590-- state. The peeled byte's position is `offset`; the next offset is `succ
591-- 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))))
658
659-- One step of an in-place list reversal driven by a first-order state VALUE:
660-- move the head of `remaining` onto `accumulated`. Empty `remaining` is a fixed
661-- point, so surplus fuel is harmless. The `eliminate` ignores its induction, so
662-- the reference machine does not fold the tail: each step is O(1).
663def utf8CodepointsReverseStep =
664 (lambda unrestricted state : (family UTF8CodepointsReverseState) .
665 (eliminate
666 UTF8CodepointsReverseState
667 (lambda unrestricted current : (family UTF8CodepointsReverseState) .
668 (family UTF8CodepointsReverseState))
669 state
670 (branch
671 UTF8CodepointsReverseStateValue
672 remaining
673 accumulated
674 .
675 (eliminate
676 UTF8Codepoints
677 (lambda unrestricted current : (family UTF8Codepoints) .
678 (family UTF8CodepointsReverseState))
679 remaining
680 (branch
681 UTF8CodepointsEnd
682 .
683 (constructor
684 UTF8CodepointsReverseState
685 UTF8CodepointsReverseStateValue
686 (constructor UTF8Codepoints UTF8CodepointsEnd)
687 accumulated))
688 (branch
689 UTF8CodepointsNext
690 head
691 tail
692 nodeInduction
693 .
694 (constructor
695 UTF8CodepointsReverseState
696 UTF8CodepointsReverseStateValue
697 tail
698 (constructor UTF8Codepoints UTF8CodepointsNext head accumulated)))))))
699
700-- Reverse a codepoint list in O(length). `fuel` need only be an upper bound on
701-- the list length (the caller passes the input byte count, always >= the
702-- codepoint count); once the list is exhausted the state stops changing.
703def utf8CodepointsReverse =
704 (lambda unrestricted fuel : Nat .
705 (lambda unrestricted list : (family UTF8Codepoints) .
706 (eliminate
707 UTF8CodepointsReverseState
708 (lambda unrestricted current : (family UTF8CodepointsReverseState) .
709 (family UTF8Codepoints))
710 (nat-eliminate
711 (lambda unrestricted step : Nat . (family UTF8CodepointsReverseState))
712 (constructor
713 UTF8CodepointsReverseState
714 UTF8CodepointsReverseStateValue
715 list
716 (constructor UTF8Codepoints UTF8CodepointsEnd))
717 (lambda unrestricted predecessor : Nat .
718 (lambda unrestricted induction : (family UTF8CodepointsReverseState) .
719 (utf8CodepointsReverseStep induction)))
720 fuel)
721 (branch UTF8CodepointsReverseStateValue remaining accumulated . accumulated))))
722
723-- A truncation failure carrying its byte offset (already a threaded `Nat`).
724def utf8DecodeTruncatedAt =
725 (lambda unrestricted code : (family UTF8ErrorCode) .
726 (lambda unrestricted offset : Nat .
727 (constructor UTF8DecodeResult UTF8DecodeFailed code (utf8OffsetWord offset))))
728
729-- Decode UTF-8 to a codepoint list, FIRST-ORDER, byte-at-a-time, LINEAR.
730--
731-- The old driver `utf8DecodeWithFuel` was a `nat-eliminate` whose motive was a
732-- `pi` (Bytes -> Nat -> Result): the "fuel-as-function" pattern `f n = step
733-- (n-1) (f (n-1))`, which the reference machine runs unshared as `T(n) =
734-- 2*T(n-1)` -- exponential per byte (docs/ALPHA-ER-RUNPOD-TRAINING-TARGET.md
735-- 3.11) -- and which the direct lane refuses outright.
736--
737-- This driver's `nat-eliminate` motive is a first-order VALUE, `UTF8Decode
738-- Machine`, and it runs exactly `bytes-length input` steps, one input byte
739-- each. Every step is O(1) -- `bytes-head`/`bytes-tail` peel a byte, `succ`
740-- advances the offset, a completed codepoint is prepended -- because the loop
741-- never calls the reference machine's tail-folding eliminators (`bytes-
742-- eliminate`, `bytes-length`) or `naturalAdd`, each of which is O(remaining).
743-- So decode is O(length). Fuel equals the byte count exactly, so no step reads
744-- past the end. At the end the pending state decides the outcome: `Ready` is a
745-- clean success (reversed back to source order); a pending multi-byte state is a
746-- truncation whose offset is the final position (`ContinuationMissing` with no
747-- continuation collected, else `SequenceTruncated`). Success/error codes and
748-- 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)))))
824
825-- Scalar encoding is bounded by the four stored octets, never unary scalar
826-- magnitude. Masks/shifts form the exact Unicode UTF8 bit fields.
827def utf8ChooseEncoded =
828 (lambda unrestricted condition : Nat .
829 (lambda unrestricted yes : (pi unrestricted force : Nat . (family UTF8CodepointEncodeResult)) .
830 (lambda unrestricted no : (pi unrestricted force : Nat . (family UTF8CodepointEncodeResult)) .
831 (app
832 (nat-eliminate
833 (lambda unrestricted flag : Nat .
834 (pi unrestricted force : Nat . (family UTF8CodepointEncodeResult)))
835 no
836 (lambda unrestricted predecessor : Nat .
837 (lambda unrestricted unused : (pi unrestricted force : Nat . (family UTF8CodepointEncodeResult)) .
838 yes))
839 condition)
840 zero))))
841
842def utf8EncodeCodepoint =
843 (lambda unrestricted codepoint : (family UTF8Codepoint) .
844 (eliminate
845 UTF8Codepoint
846 (lambda unrestricted current : (family UTF8Codepoint) . (family UTF8CodepointEncodeResult))
847 codepoint
848 (branch
849 UTF8CodepointValue
850 word
851 .
852 (eliminate
853 ModelWord32
854 (lambda unrestricted current : (family ModelWord32) . (family UTF8CodepointEncodeResult))
855 word
856 (branch
857 ModelWord32Value
858 b0
859 b1
860 b2
861 b3
862 .
863 (utf8ChooseEncoded
864 (utf8FlagAnd (byte-equal b3 (byte 0)) (byte-less-than b2 (byte 17)))
865 (lambda unrestricted force : Nat .
866 (utf8ChooseEncoded
867 (byte-equal b2 (byte 0))
868 (lambda unrestricted force : Nat .
869 (utf8ChooseEncoded
870 (utf8FlagAnd (byte-less-than (byte 215) b1) (byte-less-than b1 (byte 224)))
871 (lambda unrestricted force : Nat .
872 (constructor
873 UTF8CodepointEncodeResult
874 UTF8CodepointRejected
875 (constructor UTF8ErrorCode UTF8SurrogateCodepoint)))
876 (lambda unrestricted force : Nat .
877 (utf8ChooseEncoded
878 (utf8FlagAnd (byte-equal b1 (byte 0)) (byte-less-than b0 (byte 128)))
879 (lambda unrestricted force : Nat .
880 (constructor
881 UTF8CodepointEncodeResult
882 UTF8CodepointEncoded
883 (bytes-cons b0 b"")))
884 (lambda unrestricted force : Nat .
885 (utf8ChooseEncoded
886 (byte-less-than b1 (byte 8))
887 (lambda unrestricted force : Nat .
888 (constructor
889 UTF8CodepointEncodeResult
890 UTF8CodepointEncoded
891 (bytes-cons
892 (Std.Byte/byteOr
893 (byte 192)
894 (Std.Byte/byteOr
895 (Std.Byte/byteShiftRight b0 (byte-to-nat (byte 6)))
896 (Std.Byte/byteShiftLeftTruncated b1 (byte-to-nat (byte 2)))))
897 (bytes-cons
898 (Std.Byte/byteOr (byte 128) (Std.Byte/byteAnd b0 (byte 63)))
899 b""))))
900 (lambda unrestricted force : Nat .
901 (constructor
902 UTF8CodepointEncodeResult
903 UTF8CodepointEncoded
904 (bytes-cons
905 (Std.Byte/byteOr
906 (byte 224)
907 (Std.Byte/byteShiftRight b1 (byte-to-nat (byte 4))))
908 (bytes-cons
909 (Std.Byte/byteOr
910 (byte 128)
911 (Std.Byte/byteOr
912 (Std.Byte/byteShiftRight b0 (byte-to-nat (byte 6)))
913 (Std.Byte/byteShiftLeftTruncated
914 (Std.Byte/byteAnd b1 (byte 15))
915 (byte-to-nat (byte 2)))))
916 (bytes-cons
917 (Std.Byte/byteOr (byte 128) (Std.Byte/byteAnd b0 (byte 63)))
918 b"")))))))))))
919 (lambda unrestricted force : Nat .
920 (constructor
921 UTF8CodepointEncodeResult
922 UTF8CodepointEncoded
923 (bytes-cons
924 (Std.Byte/byteOr
925 (byte 240)
926 (Std.Byte/byteShiftRight b2 (byte-to-nat (byte 2))))
927 (bytes-cons
928 (Std.Byte/byteOr
929 (byte 128)
930 (Std.Byte/byteOr
931 (Std.Byte/byteShiftRight b1 (byte-to-nat (byte 4)))
932 (Std.Byte/byteShiftLeftTruncated
933 (Std.Byte/byteAnd b2 (byte 3))
934 (byte-to-nat (byte 4)))))
935 (bytes-cons
936 (Std.Byte/byteOr
937 (byte 128)
938 (Std.Byte/byteOr
939 (Std.Byte/byteShiftRight b0 (byte-to-nat (byte 6)))
940 (Std.Byte/byteShiftLeftTruncated
941 (Std.Byte/byteAnd b1 (byte 15))
942 (byte-to-nat (byte 2)))))
943 (bytes-cons
944 (Std.Byte/byteOr (byte 128) (Std.Byte/byteAnd b0 (byte 63)))
945 b""))))))))
946 (lambda unrestricted force : Nat .
947 (constructor
948 UTF8CodepointEncodeResult
949 UTF8CodepointRejected
950 (constructor UTF8ErrorCode UTF8CodepointOutOfRange)))))))))
951
952def utf8EncodeBuilderFold =
953 (lambda unrestricted codepoints : (family UTF8Codepoints) .
954 (eliminate
955 UTF8Codepoints
956 (lambda unrestricted current : (family UTF8Codepoints) . (family UTF8EncodeBuilderResult))
957 codepoints
958 (branch
959 UTF8CodepointsEnd
960 .
961 (constructor UTF8EncodeBuilderResult UTF8EncodeBuilderSucceeded (bytes-builder-empty)))
962 (branch
963 UTF8CodepointsNext
964 head
965 tail
966 induction
967 .
968 (eliminate
969 UTF8CodepointEncodeResult
970 (lambda unrestricted current : (family UTF8CodepointEncodeResult) .
971 (family UTF8EncodeBuilderResult))
972 (utf8EncodeCodepoint head)
973 (branch
974 UTF8CodepointEncoded
975 encoded
976 .
977 (eliminate
978 UTF8EncodeBuilderResult
979 (lambda unrestricted current : (family UTF8EncodeBuilderResult) .
980 (family UTF8EncodeBuilderResult))
981 induction
982 (branch
983 UTF8EncodeBuilderSucceeded
984 suffix
985 .
986 (constructor
987 UTF8EncodeBuilderResult
988 UTF8EncodeBuilderSucceeded
989 (bytes-builder-append (bytes-builder-chunk encoded) suffix)))
990 (branch
991 UTF8EncodeBuilderFailed
992 code
993 offset
994 .
995 (constructor UTF8EncodeBuilderResult UTF8EncodeBuilderFailed code (succ offset)))))
996 (branch
997 UTF8CodepointRejected
998 code
999 .
1000 (constructor UTF8EncodeBuilderResult UTF8EncodeBuilderFailed code zero))))))
1001
1002def encodeUTF8 =
1003 (lambda unrestricted codepoints : (family UTF8Codepoints) .
1004 (eliminate
1005 UTF8EncodeBuilderResult
1006 (lambda unrestricted current : (family UTF8EncodeBuilderResult) . (family UTF8EncodeResult))
1007 (utf8EncodeBuilderFold codepoints)
1008 (branch
1009 UTF8EncodeBuilderSucceeded
1010 builder
1011 .
1012 (constructor UTF8EncodeResult UTF8EncodeSucceeded (bytes-builder-build builder)))
1013 (branch
1014 UTF8EncodeBuilderFailed
1015 code
1016 offset
1017 .
1018 (constructor UTF8EncodeResult UTF8EncodeFailed code (utf8OffsetWord offset)))))
1019
1020-- Delegates to the one owner (Std.Flag), which this file already had a
1021-- byte-for-byte copy of before `alpha-ast duplicates` found it (L24d).
1022def utf8FlagOr =
1023 inferenceFlagOr
1024
1025def utf8ErrorStableCode =
1026 (lambda unrestricted code : (family UTF8ErrorCode) .
1027 (eliminate
1028 UTF8ErrorCode
1029 (lambda unrestricted current : (family UTF8ErrorCode) . Bytes)
1030 code
1031 (branch UTF8UnexpectedContinuation . b"UTF8-E001")
1032 (branch UTF8InvalidLeadingByte . b"UTF8-E002")
1033 (branch UTF8ContinuationMissing . b"UTF8-E003")
1034 (branch UTF8ContinuationInvalid . b"UTF8-E004")
1035 (branch UTF8TwoByteOverlong . b"UTF8-E005")
1036 (branch UTF8ThreeByteOverlong . b"UTF8-E006")
1037 (branch UTF8FourByteOverlong . b"UTF8-E007")
1038 (branch UTF8SurrogateCodepoint . b"UTF8-E008")
1039 (branch UTF8CodepointOutOfRange . b"UTF8-E009")
1040 (branch UTF8SequenceTruncated . b"UTF8-E010")))
1041
1042def utf8WordScalarValid =
1043 (lambda unrestricted word : (family ModelWord32) .
1044 (app
1045 (lambda unrestricted value : Nat .
1046 (utf8FlagAnd
1047 (nat-less-than value utf8NaturalOneMillionOneHundredFourteenThousandOneHundredTwelve)
1048 (utf8FlagNot
1049 (utf8FlagAnd
1050 (utf8FlagNot (nat-less-than value utf8NaturalFiftyFiveThousandTwoHundredNinetySix))
1051 (nat-less-than value utf8NaturalFiftySevenThousandThreeHundredFortyFour)))))
1052 (modelWord32ToNatural word)))
1053
1054def utf8CodepointScalarValid =
1055 (lambda unrestricted codepoint : (family UTF8Codepoint) .
1056 (eliminate
1057 UTF8Codepoint
1058 (lambda unrestricted current : (family UTF8Codepoint) . Nat)
1059 codepoint
1060 (branch UTF8CodepointValue word . (utf8WordScalarValid word))))
1061
1062def utf8CodepointWidth =
1063 (lambda unrestricted codepoint : (family UTF8Codepoint) .
1064 (eliminate
1065 UTF8Codepoint
1066 (lambda unrestricted current : (family UTF8Codepoint) . Nat)
1067 codepoint
1068 (branch
1069 UTF8CodepointValue
1070 word
1071 .
1072 (app
1073 (lambda unrestricted value : Nat .
1074 (nat-eliminate
1075 (lambda unrestricted valid : Nat . Nat)
1076 zero
1077 (lambda unrestricted validPredecessor : Nat .
1078 (lambda unrestricted validInduction : Nat .
1079 (nat-eliminate
1080 (lambda unrestricted ascii : Nat . Nat)
1081 (nat-eliminate
1082 (lambda unrestricted twoByte : Nat . Nat)
1083 (nat-eliminate
1084 (lambda unrestricted threeByte : Nat . Nat)
1085 (byte-to-nat (byte 4))
1086 (lambda unrestricted threePredecessor : Nat .
1087 (lambda unrestricted threeInduction : Nat . utf8NaturalThree))
1088 (nat-less-than value utf8NaturalSixtyFiveThousandFiveHundredThirtySix))
1089 (lambda unrestricted twoPredecessor : Nat .
1090 (lambda unrestricted twoInduction : Nat . utf8NaturalTwo))
1091 (nat-less-than value utf8NaturalTwoThousandFortyEight))
1092 (lambda unrestricted asciiPredecessor : Nat .
1093 (lambda unrestricted asciiInduction : Nat . utf8NaturalOne))
1094 (nat-less-than value utf8NaturalOneHundredTwentyEight))))
1095 (utf8WordScalarValid word)))
1096 (modelWord32ToNatural word)))))
1097
1098def utf8CodepointsLength =
1099 (lambda unrestricted codepoints : (family UTF8Codepoints) .
1100 (eliminate
1101 UTF8Codepoints
1102 (lambda unrestricted current : (family UTF8Codepoints) . Nat)
1103 codepoints
1104 (branch UTF8CodepointsEnd . zero)
1105 (branch UTF8CodepointsNext head tail induction . (succ induction))))
1106
1107def utf8CodepointsWidthCount =
1108 (lambda unrestricted expected : Nat .
1109 (lambda unrestricted codepoints : (family UTF8Codepoints) .
1110 (eliminate
1111 UTF8Codepoints
1112 (lambda unrestricted current : (family UTF8Codepoints) . Nat)
1113 codepoints
1114 (branch UTF8CodepointsEnd . zero)
1115 (branch
1116 UTF8CodepointsNext
1117 head
1118 tail
1119 induction
1120 .
1121 (nat-eliminate
1122 (lambda unrestricted matches : Nat . Nat)
1123 induction
1124 (lambda unrestricted predecessor : Nat .
1125 (lambda unrestricted matchInduction : Nat . (succ induction)))
1126 (naturalEqual (utf8CodepointWidth head) expected))))))
1127
1128def utf8CodepointsInvalidCount =
1129 (lambda unrestricted codepoints : (family UTF8Codepoints) .
1130 (eliminate
1131 UTF8Codepoints
1132 (lambda unrestricted current : (family UTF8Codepoints) . Nat)
1133 codepoints
1134 (branch UTF8CodepointsEnd . zero)
1135 (branch
1136 UTF8CodepointsNext
1137 head
1138 tail
1139 induction
1140 .
1141 (nat-eliminate
1142 (lambda unrestricted valid : Nat . Nat)
1143 (succ induction)
1144 (lambda unrestricted predecessor : Nat .
1145 (lambda unrestricted validInduction : Nat . induction))
1146 (utf8CodepointScalarValid head)))))
1147
1148def utf8BytesCountWhere =
1149 (lambda unrestricted predicate : (pi unrestricted value : Byte . Nat) .
1150 (lambda unrestricted input : Bytes .
1151 (bytes-eliminate
1152 (lambda unrestricted current : Bytes . Nat)
1153 zero
1154 (lambda unrestricted head : Byte .
1155 (lambda unrestricted tail : Bytes .
1156 (lambda unrestricted induction : Nat .
1157 (nat-eliminate
1158 (lambda unrestricted matches : Nat . Nat)
1159 induction
1160 (lambda unrestricted predecessor : Nat .
1161 (lambda unrestricted matchInduction : Nat . (succ induction)))
1162 (predicate head)))))
1163 input)))
1164
1165def utf8ByteIllegal =
1166 (lambda unrestricted value : Byte .
1167 (utf8FlagNot
1168 (utf8FlagOr
1169 (byte-less-than value (byte 128))
1170 (utf8FlagOr
1171 (utf8ContinuationValid value)
1172 (utf8FlagOr
1173 (utf8LeadTwoValid value)
1174 (utf8FlagOr (utf8LeadThreeValid value) (utf8LeadFourValid value)))))))
1175
1176def utf8DecodeTelemetryFor =
1177 (lambda unrestricted input : Bytes .
1178 (lambda unrestricted inspected : Nat .
1179 (lambda unrestricted codepoints : (family UTF8Codepoints) .
1180 (lambda unrestricted failurePresent : Nat .
1181 (lambda unrestricted failureOffset : Nat .
1182 (constructor
1183 UTF8DecodeTelemetry
1184 UTF8DecodeTelemetryValue
1185 (bytes-length input)
1186 inspected
1187 (utf8CodepointsLength codepoints)
1188 (utf8CodepointsWidthCount utf8NaturalOne codepoints)
1189 (utf8CodepointsWidthCount utf8NaturalTwo codepoints)
1190 (utf8CodepointsWidthCount utf8NaturalThree codepoints)
1191 (utf8CodepointsWidthCount (byte-to-nat (byte 4)) codepoints)
1192 (utf8BytesCountWhere utf8ContinuationValid input)
1193 (utf8BytesCountWhere utf8ByteIllegal input)
1194 failurePresent
1195 failureOffset))))))
1196
1197def utf8EncodeTelemetryFor =
1198 (lambda unrestricted codepoints : (family UTF8Codepoints) .
1199 (lambda unrestricted processed : Nat .
1200 (lambda unrestricted outputBytes : Nat .
1201 (lambda unrestricted failurePresent : Nat .
1202 (lambda unrestricted failureOrdinal : Nat .
1203 (constructor
1204 UTF8EncodeTelemetry
1205 UTF8EncodeTelemetryValue
1206 (utf8CodepointsLength codepoints)
1207 processed
1208 outputBytes
1209 (utf8CodepointsWidthCount utf8NaturalOne codepoints)
1210 (utf8CodepointsWidthCount utf8NaturalTwo codepoints)
1211 (utf8CodepointsWidthCount utf8NaturalThree codepoints)
1212 (utf8CodepointsWidthCount (byte-to-nat (byte 4)) codepoints)
1213 (utf8CodepointsInvalidCount codepoints)
1214 failurePresent
1215 failureOrdinal))))))
1216
1217def decodeUTF8WithTelemetry =
1218 (lambda unrestricted input : Bytes .
1219 (eliminate
1220 UTF8DecodeResult
1221 (lambda unrestricted current : (family UTF8DecodeResult) . (family UTF8DecodeExecutionResult))
1222 (decodeUTF8 input)
1223 (branch
1224 UTF8DecodeSucceeded
1225 codepoints
1226 .
1227 (constructor
1228 UTF8DecodeExecutionResult
1229 UTF8DecodeExecutionSucceeded
1230 codepoints
1231 (utf8DecodeTelemetryFor input (bytes-length input) codepoints zero zero)))
1232 (branch
1233 UTF8DecodeFailed
1234 code
1235 offset
1236 .
1237 (app
1238 (lambda unrestricted exactOffset : Nat .
1239 (constructor
1240 UTF8DecodeExecutionResult
1241 UTF8DecodeExecutionFailed
1242 code
1243 offset
1244 (utf8ErrorStableCode code)
1245 (utf8DecodeTelemetryFor
1246 input
1247 exactOffset
1248 (constructor UTF8Codepoints UTF8CodepointsEnd)
1249 (succ zero)
1250 exactOffset)))
1251 (modelWord32ToNatural offset)))))
1252
1253def encodeUTF8WithTelemetry =
1254 (lambda unrestricted codepoints : (family UTF8Codepoints) .
1255 (eliminate
1256 UTF8EncodeResult
1257 (lambda unrestricted current : (family UTF8EncodeResult) . (family UTF8EncodeExecutionResult))
1258 (encodeUTF8 codepoints)
1259 (branch
1260 UTF8EncodeSucceeded
1261 encoded
1262 .
1263 (constructor
1264 UTF8EncodeExecutionResult
1265 UTF8EncodeExecutionSucceeded
1266 encoded
1267 (utf8EncodeTelemetryFor
1268 codepoints
1269 (utf8CodepointsLength codepoints)
1270 (bytes-length encoded)
1271 zero
1272 zero)))
1273 (branch
1274 UTF8EncodeFailed
1275 code
1276 offset
1277 .
1278 (app
1279 (lambda unrestricted exactOffset : Nat .
1280 (constructor
1281 UTF8EncodeExecutionResult
1282 UTF8EncodeExecutionFailed
1283 code
1284 offset
1285 (utf8ErrorStableCode code)
1286 (utf8EncodeTelemetryFor codepoints exactOffset zero (succ zero) exactOffset)))
1287 (modelWord32ToNatural offset)))))
1288
1289-- Text and the compiler share this validity decision with the existing decoder.
1290-- No replacement character, normalization or second validation machine.
1291def stdUtf8Valid : (pi unrestricted input : Bytes . (family StdBool)) =
1292 (lambda unrestricted input : Bytes .
1293 (eliminate
1294 UTF8DecodeResult
1295 (lambda unrestricted result : (family UTF8DecodeResult) . (family StdBool))
1296 (decodeUTF8 input)
1297 (branch UTF8DecodeSucceeded codepoints . (constructor StdBool StdTrue))
1298 (branch UTF8DecodeFailed error offset . (constructor StdBool StdFalse))))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.