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`.
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))))))))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.