First-order hex-quad reader. Each of the four byte reads was a
`bytes-eliminate` over the input, whose ignored tail-induction the runtime
forces -- a full re-walk of the whole remaining input per byte. Each is now an
O(1) `bytes-head` / `bytes-tail` peek guarded by an emptiness check, so the
four reads together are constant work. The bytes and result are unchanged.
468def jsonParseHexQuad =
469 (lambda unrestricted input : Bytes .
470 (nat-eliminate
471 (lambda unrestricted nonEmpty : Nat . (family JSONHexQuadResult))
472 (app
473 (lambda unrestricted a : Byte .
474 (app
475 (lambda unrestricted afterA : Bytes .
476 (nat-eliminate
477 (lambda unrestricted nonEmpty : Nat . (family JSONHexQuadResult))
478 (app
479 (lambda unrestricted b : Byte .
480 (app
481 (lambda unrestricted afterB : Bytes .
482 (nat-eliminate
483 (lambda unrestricted nonEmpty : Nat . (family JSONHexQuadResult))
484 (app
485 (lambda unrestricted c : Byte .
486 (app
487 (lambda unrestricted afterC : Bytes .
488 (nat-eliminate
489 (lambda unrestricted nonEmpty : Nat .
490 (family JSONHexQuadResult))
491 (jsonParseHexQuadPart1
492 input
493 a
494 b
495 c
496 (bytes-head afterC)
497 (bytes-tail afterC)
498 (constructor JSONHexQuadResult JSONHexQuadFailed afterC))
499 (lambda unrestricted emptyPredecessor : Nat .
500 (lambda unrestricted emptyInduction : (family JSONHexQuadResult) .
501 (constructor JSONHexQuadResult JSONHexQuadFailed afterC)))
502 (naturalIsZero (bytes-length afterC))))
503 (bytes-tail afterB)))
504 (bytes-head afterB))
505 (lambda unrestricted emptyPredecessor : Nat .
506 (lambda unrestricted emptyInduction : (family JSONHexQuadResult) .
507 (constructor JSONHexQuadResult JSONHexQuadFailed afterB)))
508 (naturalIsZero (bytes-length afterB))))
509 (bytes-tail afterA)))
510 (bytes-head afterA))
511 (lambda unrestricted emptyPredecessor : Nat .
512 (lambda unrestricted emptyInduction : (family JSONHexQuadResult) .
513 (constructor JSONHexQuadResult JSONHexQuadFailed afterA)))
514 (naturalIsZero (bytes-length afterA))))
515 (bytes-tail input)))
516 (bytes-head input))
517 (lambda unrestricted emptyPredecessor : Nat .
518 (lambda unrestricted emptyInduction : (family JSONHexQuadResult) .
519 (constructor JSONHexQuadResult JSONHexQuadFailed input)))
520 (naturalIsZero (bytes-length input))))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.