AlphaGitHub
Source/Packages

Data.JSON

packages/foundation/standard/src/Data/JSON.alpha

2,617 lines251 declarations113.9 KiBSHA-256 bd63da5ed186
Download exact fileView at revision426597bda5753d86c4

def · lines 840–870

jsonParseStringBodyWithFuel

Full file
First-order string-body scan: fold the step `fuel` times over a VALUE accumulator (no function-valued fold, no tail-forcing `bytes-eliminate`), then project. `fuel = bytes-length input` bounds the scan; each step consumes at least one input byte before `Done`/`Failed`, so a well-fuelled call never ends `Going`.
840def jsonParseStringBodyWithFuel =
841  (lambda unrestricted fuel : Nat .
842    (lambda unrestricted input : Bytes .
843      (eliminate
844        JSONStringLoop
845        (lambda unrestricted current : (family JSONStringLoop) . (family JSONStringParseResult))
846        (nat-eliminate
847          (lambda unrestricted current : Nat . (family JSONStringLoop))
848          (constructor JSONStringLoop JSONStringLoopGoing (bytes-builder-empty) input)
849          (lambda unrestricted predecessor : Nat .
850            (lambda unrestricted induction : (family JSONStringLoop) .
851              (jsonParseStringBodyStep induction)))
852          fuel)
853        (branch
854          JSONStringLoopGoing
855          builder
856          remaining
857          .
858          (jsonStringFailure (constructor JSONErrorCode JSONStringUnterminated) remaining))
859        (branch
860          JSONStringLoopDone
861          builder
862          remaining
863          .
864          (constructor JSONStringParseResult JSONStringParsed builder remaining))
865        (branch
866          JSONStringLoopFailed
867          code
868          remaining
869          .
870          (constructor JSONStringParseResult JSONStringParseFailed code remaining)))))

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.