Jpeg.jpeg.scan.decode: def of gralha-jpeg-decode@0.1.0.1
Import: import gralha-jpeg-decode@0.1.0.1/jpeg.bend as Jpeg
Lines 559-574 of gralha-jpeg-decode@0.1.0.1/jpeg.bend: https://jend.leeeet.dev/read.txt?path=gralha-jpeg-decode@0.1.0.1/jpeg.bend&start_line=559&end_line=574

import Base
import gralha-text-scan@0.1.0.1/scan.bend as U
import gralha-bytes@0.1.0.1/bytes.bend as Bin

def jpeg.scan.decode(+src: Bin.Bytes, +at: U32, +end: U32, +frame: JPEGFrame) -> JPEGDecoded:
  JPEGFrame{w, h, hm, vm, progressive, components, quants, huffs, restart, adobe, valid} = frame
  +count = Bin.bytes.get(src, at)
  +cs = jpeg.scan.select(U32.to_nat(U.choose(U32, U32.is_le(count, 4), count, 0)), src, U32.inc(at), components)
  +single = U32.is_eq(count, 1)
  +cols = U.choose(U32, single, jpeg.scan.extent(cs, w, h, hm, vm, False{}), jpeg.ceil(w, (hm * 8 : U32)))
  +rows = U.choose(U32, single, jpeg.scan.extent(cs, w, h, hm, vm, True{}), jpeg.ceil(h, (vm * 8 : U32)))
  +ss = Bin.bytes.get(src, (end - 3 : U32))
  +se = Bin.bytes.get(src, (end - 2 : U32))
  +approx = Bin.bytes.get(src, (end - 1 : U32))
  +ah = (approx / 16 : U32)
  +al = (approx % 16 : U32)
  +sequential = U32.is_eq(ss, 0) && U32.is_eq(se, 63) && U32.is_eq(approx, 0)
  +spectral = U32.is_le(ss, se) && U32.is_le(se, 63) && U.choose(Bool, U32.is_eq(ss, 0), U32.is_eq(se, 0), single) && U32.is_le(al, 13) && (U32.is_eq(ah, 0) || U32.is_eq(ah, U32.inc(al)))
  +ok = valid && U.choose(Bool, progressive, spectral, sequential) && U32.is_gt(w, 0) && U32.is_gt(count, 0) && U32.is_le(count, 4) && U32.is_eq((at + 1 + count * 2 + 3 : U32), end)
  U.branch(JPEGDecoded, ok, _ => U.branch(JPEGDecoded, jpeg.scan.ready(cs, ss, se, ah, quants), _ => jpeg.scan.finish(jpeg.mcus(U32.to_nat((cols * rows : U32)), 0, cols, single, huffs, restart, JPEGScan{jpeg.scan.histories(cs, ss, se, al), JPEGStream{src, end, 0, 0, JPEGSpectral{ss, se, ah, al, 0}, True{}}}), frame), _ => JPEGDecoded{jpeg.frame.invalid(frame), end}), _ => JPEGDecoded{jpeg.frame.invalid(frame), end})

Uses (31):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.or
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.div
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.inc
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_gt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.mod
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.mul
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.sub
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=gralha-bytes@0.1.0.1/bytes.bend&name=Bytes
  https://jend.leeeet.dev/definition.txt?path=gralha-bytes@0.1.0.1/bytes.bend&name=bytes.get
  https://jend.leeeet.dev/definition.txt?path=gralha-jpeg-decode@0.1.0.1/jpeg.bend&name=JPEGDecoded
  https://jend.leeeet.dev/definition.txt?path=gralha-jpeg-decode@0.1.0.1/jpeg.bend&name=JPEGFrame
  https://jend.leeeet.dev/definition.txt?path=gralha-jpeg-decode@0.1.0.1/jpeg.bend&name=JPEGScan
  https://jend.leeeet.dev/definition.txt?path=gralha-jpeg-decode@0.1.0.1/jpeg.bend&name=JPEGSpectral
  https://jend.leeeet.dev/definition.txt?path=gralha-jpeg-decode@0.1.0.1/jpeg.bend&name=JPEGStream
  https://jend.leeeet.dev/definition.txt?path=gralha-jpeg-decode@0.1.0.1/jpeg.bend&name=jpeg.ceil
  https://jend.leeeet.dev/definition.txt?path=gralha-jpeg-decode@0.1.0.1/jpeg.bend&name=jpeg.frame.invalid
  https://jend.leeeet.dev/definition.txt?path=gralha-jpeg-decode@0.1.0.1/jpeg.bend&name=jpeg.mcus
  https://jend.leeeet.dev/definition.txt?path=gralha-jpeg-decode@0.1.0.1/jpeg.bend&name=jpeg.scan.extent
  https://jend.leeeet.dev/definition.txt?path=gralha-jpeg-decode@0.1.0.1/jpeg.bend&name=jpeg.scan.finish
  https://jend.leeeet.dev/definition.txt?path=gralha-jpeg-decode@0.1.0.1/jpeg.bend&name=jpeg.scan.histories
  https://jend.leeeet.dev/definition.txt?path=gralha-jpeg-decode@0.1.0.1/jpeg.bend&name=jpeg.scan.ready
  https://jend.leeeet.dev/definition.txt?path=gralha-jpeg-decode@0.1.0.1/jpeg.bend&name=jpeg.scan.select
  https://jend.leeeet.dev/definition.txt?path=gralha-text-scan@0.1.0.1/scan.bend&name=branch
  https://jend.leeeet.dev/definition.txt?path=gralha-text-scan@0.1.0.1/scan.bend&name=choose