src/jpeg.bend checks

raw source on the hub · import 0xde7817074d0d382dc55dfca454298427/src/jpeg.bend as Jpeg

src/jpeg: baseline JPEG. Sequential 8-bit Huffman (SOF0), JFIF APP0, grayscale or YCbCr.

1 import

import Base

Types

type Pic source · line 7 · raw

Data

a decoded picture: width, height, and row-major samples, each packed 0xAARRGGBB with alpha 255

Pic

@w:U32 -> @h:U32 -> @pixels:List<&2, U32> -> Pic

type Huff source · line 11 · raw

Data

one Huffman table: canonical codes, lengths, and symbols

Huff

@codes:List<&2, U32> -> @lens:List<&2, U32> -> @syms:List<&2, U32> -> Huff

type Frame source · line 15 · raw

Data

SOF0 frame geometry. Sampling factors are 1, 2, or 4.

Frame

@w:U32 -> @h:U32 -> @nf:U32 -> @ids:List<&2, U32> -> @hs:List<&2, U32> -> @vs:List<&2, U32> -> @tq:List<&2, U32> -> @hmax:U32 -> @vmax:U32 -> Frame

type Scan source · line 20 · raw

Data

one SOS header

Scan

@ns:U32 -> @sids:List<&2, U32> -> @td:List<&2, U32> -> @ta:List<&2, U32> -> @ss:U32 -> @se:U32 -> @ah:U32 -> Scan

type Tabs source · line 24 · raw

Data

four quant tables and four DC / AC Huffman tables

Tabs

@q0:List<&2, U32> -> @q1:List<&2, U32> -> @q2:List<&2, U32> -> @q3:List<&2, U32> -> @dc0:Huff -> @dc1:Huff -> @dc2:Huff -> @dc3:Huff -> @ac0:Huff -> @ac1:Huff -> @ac2:Huff -> @ac3:Huff -> Tabs

type Phase source · line 29 · raw

Data

marker walk: seeking, a marker byte, a length, a payload, or the entropy scan

Seek
```
Phase
```
Mark
```
Phase
```
LenHi
```
@mark:U32 -> Phase
```
LenLo
```
@mark:U32 -> @hi:U32 -> Phase
```

Pay

@mark:U32 -> @left:Nat -> @acc:List<&2, U32> -> Phase

Ent
```
Phase
```
EntFF
```
Phase
```
Stop
```
Phase
```

type St source · line 40 · raw

Data

parser state. kind 1 is a baseline frame. bad 1 rejects the file.

St

@phase:Phase -> @frame:Frame -> @scan:Scan -> @tabs:Tabs -> @ent:List<&2, U32> -> @ri:U32 -> @kind:U32 -> @bad:U32 -> St

type Bits source · line 44 · raw

Data

bit reader. n bits remain in buf. ok is 0 after a truncated or marked stream.

Bits

@n:U32 -> @ok:U32 -> @buf:U32 -> @xs:List<&2, U32> -> Bits

type Ask source · line 48 · raw

Data

a Huffman lookup in progress

Ask

@hit:Maybe<&2, U32> -> @code:U32 -> @len:U32 -> @bits:Bits -> Ask

type Hit source · line 52 · raw

Data

one decoded Huffman symbol

Hit

@sym:U32 -> @bits:Bits -> @ok:U32 -> Hit

type Ac source · line 56 · raw

Data

AC run state inside one block

Ac

@k:U32 -> @zz:List<&2, U32> -> @bits:Bits -> @done:U32 -> @ok:U32 -> Ac

type Blk source · line 60 · raw

Data

one decoded 8x8 block, level-shifted samples, and the DC predictor

Blk

@samples:List<&2, U32> -> @bits:Bits -> @pred:U32 -> @ok:U32 -> Blk

type Preds source · line 64 · raw

Data

DC predictors, one per scan component

Preds

@a:U32 -> @b:U32 -> @c:U32 -> @d:U32 -> Preds

type Ctrl source · line 68 · raw

Data

where the current block sits in the frame

Ctrl

@comp:U32 -> @bi:U32 -> @mx:U32 -> @my:U32 -> @mcu:U32 -> @rst:U32 -> Ctrl

type Adv source · line 72 · raw

Data

the block that follows, and whether a restart marker comes first

Adv

@ctrl:Ctrl -> @due:U32 -> @expect:U32 -> Adv

type Geom source · line 76 · raw

Data

pixel rectangle one block sample covers

Geom

@ox:U32 -> @oy:U32 -> @pw:U32 -> @ph:U32 -> @w:U32 -> @h:U32 -> Geom

type Cursor source · line 80 · raw

Data

sample cursor inside an upsampled block

Cursor
```
@k:U32 -> @px:U32 -> @py:U32 -> Cursor
```

type Comps source · line 84 · raw

Data

SOF component lists while they are being read

Comps

@ids:List<&2, U32> -> @hs:List<&2, U32> -> @vs:List<&2, U32> -> @tq:List<&2, U32> -> @bad:U32 -> Comps

type Cols source · line 88 · raw

Data

the eight cosine columns of the A.3.3 matrix, one list per frequency

Cols

@c0:List<&2, U32> -> @c1:List<&2, U32> -> @c2:List<&2, U32> -> @c3:List<&2, U32> -> @c4:List<&2, U32> -> @c5:List<&2, U32> -> @c6:List<&2, U32> -> @c7:List<&2, U32> -> Cols

Definitions

def decode.sign source · line 92 · raw

@+aa:U32 -> U32

def decode.neg32 source · line 95 · raw

@+aa:U32 -> U32

def decode.abs.s source · line 98 · raw

@ss:U32 -> @+aa:U32 -> U32

def decode.abs source · line 105 · raw

@+aa:U32 -> U32

def decode.carry.b source · line 108 · raw

@cc:Bool -> U32

def decode.carry source · line 115 · raw

@+aa:U32 -> @+sum:U32 -> U32

def decode.neg64.c source · line 118 · raw

@zz:Bool -> @+nh:U32 -> @+nl:U32 -> Pair(U32, U32)

def decode.neg64 source · line 125 · raw

@+hh:U32 -> @+ll:U32 -> Pair(U32, U32)

def decode.split source · line 130 · raw

@+aa:U32 -> Pair(U32, U32)

def decode.widemul.pack source · line 133 · raw

@+neg:U32 -> @+hi:U32 -> @+lo:U32 -> Pair(U32, U32)

def decode.widemul.bb source · line 140 · raw

@+a0:U32 -> @+a1:U32 -> @bb:Pair(U32, U32) -> @+neg:U32 -> Pair(U32, U32)

def decode.widemul.aa source · line 151 · raw

@aa:Pair(U32, U32) -> @+bb:U32 -> @+neg:U32 -> Pair(U32, U32)

def decode.widemul.go source · line 155 · raw

@+aa:U32 -> @+bb:U32 -> @+neg:U32 -> Pair(U32, U32)

def decode.widemul source · line 158 · raw

@+aa:U32 -> @+bb:U32 -> Pair(U32, U32)

def decode.q17.res source · line 161 · raw

@+hh:U32 -> @+ll:U32 -> U32

def decode.q17.sign2 source · line 164 · raw

@neg:Bool -> @+res:U32 -> U32

def decode.q17.div source · line 171 · raw

@+hh:U32 -> @+ll:U32 -> @neg:Bool -> U32

def decode.q17.neg source · line 176 · raw

@pp:Pair(U32, U32) -> U32

def decode.q17.pos source · line 180 · raw

@pos:Bool -> @+hh:U32 -> @+ll:U32 -> U32

def decode.q17 source · line 187 · raw

@+hh:U32 -> @+ll:U32 -> U32

def decode.dot.end source · line 190 · raw

@+lo:U32 -> @+ah:U32 -> @+ph:U32 -> @+al:U32 -> U32

def decode.dot source · line 193 · raw

@cs:List<&2, U32> -> @ks:List<&2, U32> -> @have:Bool -> @prod:Pair(U32, U32) -> @+ah:U32 -> @+al:U32 -> U32

def decode.at.m source · line 225 · raw

@mm:Maybe<&2, U32> -> U32

def decode.at source · line 232 · raw

@xs:List<&2, U32> -> @+ii:U32 -> U32

def decode.column source · line 235 · raw

@+cs:List<&2, U32> -> @+xx:U32 -> List<&2, U32>

def decode.cols source · line 242 · raw

@+cs:List<&2, U32> -> Cols

one copy of each cosine column, reused for every row of the block

def decode.row8 source · line 246 · raw

@+row:List<&2, U32> -> @+cols:Cols -> List<&2, U32>

def decode.cos source · line 254 · raw

List<&2, U32>

def decode.pass source · line 262 · raw

@left:Nat -> @coeffs:List<&2, U32> -> @+cols:Cols -> @acc:List<&2, List<&2, U32>> -> List<&2, List<&2, U32>>

def decode.col source · line 278 · raw

@+rows:List<&2, List<&2, U32>> -> @+xx:U32 -> @acc:List<&2, U32> -> List<&2, U32>

def decode.backs source · line 285 · raw

@+rows:List<&2, List<&2, U32>> -> @+cols:Cols -> List<&2, List<&2, U32>>

def decode.rows.of source · line 291 · raw

@+backs:List<&2, List<&2, U32>> -> List<&2, List<&2, U32>>

def decode.flat.row source · line 296 · raw

@xs:List<&2, U32> -> @acc:List<&2, U32> -> List<&2, U32>

def decode.flat source · line 303 · raw

@rows:List<&2, List<&2, U32>> -> List<&2, U32>

def decode.clamp.hi source · line 310 · raw

@hi:Bool -> @+vv:U32 -> U32

def decode.clamp8.s source · line 317 · raw

@ss:U32 -> @+vv:U32 -> U32

def decode.clamp8 source · line 324 · raw

@+vv:U32 -> U32

def decode.level source · line 327 · raw

@xs:List<&2, U32> -> @acc:List<&2, U32> -> List<&2, U32>

def decode.zeros source · line 334 · raw

@nn:Nat -> @acc:List<&2, U32> -> List<&2, U32>

def decode.idct source · line 341 · raw

@nat:List<&2, U32> -> List<&2, U32>

def decode.huff0 source · line 345 · raw

Huff

def decode.frame0 source · line 348 · raw

Frame

def decode.scan0 source · line 351 · raw

Scan

def decode.tabs0 source · line 354 · raw

Tabs

def decode.st0 source · line 358 · raw

St

def decode.nlist source · line 361 · raw

@xs:List<&2, U32> -> @+nn:U32 -> U32

def decode.drop source · line 368 · raw

@xs:List<&2, U32> -> U32

def decode.rev3 source · line 375 · raw

@ac:List<&2, U32> -> @al:List<&2, U32> -> @ay:List<&2, U32> -> Huff

def decode.canon.shift source · line 378 · raw

@+len:U32 -> @+code:U32 -> U32

def decode.canon source · line 385 · raw

@left:Nat -> @tick:Nat -> @counts:List<&2, U32> -> @symbols:List<&2, U32> -> @+code:U32 -> @+len:U32 -> @ac:List<&2, U32> -> @al:List<&2, U32> -> @ay:List<&2, U32> -> Huff

def decode.index.keep source · line 424 · raw

@+hh:U32 -> @+ii:U32 -> U32

def decode.index.add source · line 427 · raw

@eq:Bool -> @+ii:U32 -> U32

def decode.index source · line 434 · raw

@xs:List<&2, U32> -> @eq:Bool -> @+hh:U32 -> @+want:U32 -> @+ii:U32 -> U32

def decode.look.pref source · line 449 · raw

@tail:Maybe<&2, U32> -> @eqc:Bool -> @eql:Bool -> @+ss:U32 -> Maybe<&2, U32>

def decode.look source · line 464 · raw

@codes:List<&2, U32> -> @lens:List<&2, U32> -> @syms:List<&2, U32> -> @+code:U32 -> @+len:U32 -> Maybe<&2, U32>

def decode.nbits source · line 491 · raw

@left:Nat -> @eq:Bool -> @xs:List<&2, U32> -> @+nn:U32 -> @+buf:U32 -> @+ok:U32 -> @+acc:U32 -> Pair(Bits, U32)

def decode.one source · line 517 · raw

@bits:Bits -> Pair(Bits, U32)

def decode.ask.bit source · line 522 · raw

@tab:Huff -> @got:Pair(Bits, U32) -> @+code:U32 -> @+len:U32 -> Ask

def decode.ask source · line 530 · raw

@bits:Bits -> @+code:U32 -> @+len:U32 -> @tab:Huff -> Ask

def decode.huff.use source · line 533 · raw

@hit:Maybe<&2, U32> -> @bits:Bits -> Hit

def decode.huff source · line 542 · raw

@left:Nat -> @ask:Ask -> @+tab:Huff -> Hit

def decode.bits.of source · line 557 · raw

@bits:Bits -> Pair(Nat, Pair(U32, Pair(List<&2, U32>, Pair(U32, U32))))

def decode.read.n source · line 562 · raw

@+cat:U32 -> @bits:Bits -> Pair(Bits, U32)

def decode.extend.s source · line 567 · raw

@small:Bool -> @+mag:U32 -> @+cat:U32 -> U32

def decode.extend source · line 574 · raw

@+cat:U32 -> @+mag:U32 -> U32

def decode.ac.stored source · line 581 · raw

@full:Bool -> @+kk:U32 -> @zz:List<&2, U32> -> @bits:Bits -> @+ok:U32 -> Ac

def decode.ac.store source · line 588 · raw

@got:Pair(Bits, U32) -> @+sz:U32 -> @+nk:U32 -> @zz:List<&2, U32> -> @+ok:U32 -> Ac

def decode.ac.bad source · line 593 · raw

@zz:List<&2, U32> -> @bits:Bits -> Ac

def decode.ac.run.b source · line 596 · raw

@zzz:Bool -> @over:Bool -> @+sz:U32 -> @+nk:U32 -> @bits:Bits -> @zz:List<&2, U32> -> @+ok:U32 -> Ac

def decode.ac.run source · line 607 · raw

@+sym:U32 -> @bits:Bits -> @+kk:U32 -> @zz:List<&2, U32> -> @+ok:U32 -> Ac

def decode.ac.zrl.eq source · line 612 · raw

@eq:Bool -> @zz:List<&2, U32> -> @bits:Bits -> @+ok:U32 -> Ac

def decode.ac.zrl.k source · line 619 · raw

@more:Bool -> @+nk:U32 -> @zz:List<&2, U32> -> @bits:Bits -> @+ok:U32 -> Ac

def decode.ac.zrl source · line 626 · raw

@+kk:U32 -> @zz:List<&2, U32> -> @bits:Bits -> @+ok:U32 -> Ac

def decode.ac.sym source · line 629 · raw

@+sym:U32 -> @bits:Bits -> @+kk:U32 -> @zz:List<&2, U32> -> @+ok:U32 -> Ac

def decode.ac.step source · line 638 · raw

@hit:Hit -> @+kk:U32 -> @zz:List<&2, U32> -> @+ok:U32 -> Ac

def decode.ac.full source · line 643 · raw

@done:Bool -> @short:Bool -> @ac:Ac -> Ac

def decode.ac source · line 656 · raw

@left:Nat -> @ac:Ac -> @+tab:Huff -> Ac

def decode.zig source · line 673 · raw

List<&2, U32>

def decode.nat source · line 678 · raw

@zz:List<&2, U32> -> @quant:List<&2, U32> -> @zig:List<&2, U32> -> @acc:List<&2, U32> -> List<&2, U32>

def decode.block.ac source · line 699 · raw

@ac:Ac -> @+pred:U32 -> @quant:List<&2, U32> -> @+qok:U32 -> Blk

def decode.block.diff source · line 704 · raw

@got:Pair(Bits, U32) -> @+cat:U32 -> @+pred:U32 -> @+ok:U32 -> @ac:Huff -> @quant:List<&2, U32> -> @+qok:U32 -> Blk

def decode.block.cat source · line 717 · raw

@zz:Bool -> @+sym:U32 -> @bits:Bits -> @+pred:U32 -> @+ok:U32 -> @ac:Huff -> @quant:List<&2, U32> -> @+qok:U32 -> Blk

def decode.block.dc source · line 733 · raw

@hit:Hit -> @+pred:U32 -> @ac:Huff -> @quant:List<&2, U32> -> @+qok:U32 -> Blk

def decode.qok.b source · line 738 · raw

@ok:Bool -> U32

def decode.qok source · line 745 · raw

@quant:List<&2, U32> -> U32

def decode.block.go source · line 748 · raw

@bits:Bits -> @+pred:U32 -> @dc:Huff -> @ac:Huff -> @+quant:List<&2, U32> -> Blk

def decode.dc.get source · line 751 · raw

@tabs:Tabs -> @+id:U32 -> Huff

def decode.ac.get source · line 764 · raw

@tabs:Tabs -> @+id:U32 -> Huff

def decode.q.get source · line 777 · raw

@tabs:Tabs -> @+id:U32 -> List<&2, U32>

def decode.pred.get source · line 790 · raw

@preds:Preds -> @+ii:U32 -> U32

def decode.pred.put source · line 803 · raw

@preds:Preds -> @+ii:U32 -> @+vv:U32 -> Preds

def decode.pred.zero source · line 816 · raw

Preds

def decode.preds.next source · line 819 · raw

@due:U32 -> @preds:Preds -> @+comp:U32 -> @+pred:U32 -> Preds

def decode.block.of source · line 828 · raw

@bits:Bits -> @+comp:U32 -> @preds:Preds -> @frame:Frame -> @scan:Scan -> @+tabs:Tabs -> Blk

def decode.rst.ok source · line 843 · raw

@eq:Bool -> @rest:List<&2, U32> -> Bits

def decode.rst.xs source · line 850 · raw

@xs:List<&2, U32> -> @+want:U32 -> Bits

def decode.rst source · line 857 · raw

@bits:Bits -> @+want:U32 -> Bits

def decode.restart source · line 862 · raw

@bits:Bits -> @+due:U32 -> @+expect:U32 -> Bits

def decode.ceil source · line 869 · raw

@+nn:U32 -> @+dd:U32 -> U32

def decode.ri.nz source · line 872 · raw

@+ri:U32 -> U32

def decode.adv.due.b source · line 879 · raw

@zero:Bool -> @hit:Bool -> @+mcu:U32 -> @+mx:U32 -> @+my:U32 -> @+rst:U32 -> Adv

def decode.adv.due source · line 890 · raw

@+mcu:U32 -> @+mx:U32 -> @+my:U32 -> @+rst:U32 -> @+ri:U32 -> Adv

def decode.adv.mx source · line 893 · raw

@inb:Bool -> @+mcu:U32 -> @+mx:U32 -> @+my:U32 -> @+rst:U32 -> @+ri:U32 -> Adv

def decode.adv.mcu source · line 900 · raw

@+mcu:U32 -> @+mx:U32 -> @+my:U32 -> @+rst:U32 -> @+ww:U32 -> @+hmax:U32 -> @+ri:U32 -> Adv

def decode.adv.comp source · line 903 · raw

@more:Bool -> @+comp:U32 -> @+mx:U32 -> @+my:U32 -> @+mcu:U32 -> @+rst:U32 -> @+ww:U32 -> @+hmax:U32 -> @+ri:U32 -> Adv

def decode.adv.bi source · line 920 · raw

@more:Bool -> @+comp:U32 -> @+bi:U32 -> @+mx:U32 -> @+my:U32 -> @+mcu:U32 -> @+rst:U32 -> @+ww:U32 -> @+hmax:U32 -> @+ns:U32 -> @+ri:U32 -> Adv

def decode.adv.go source · line 939 · raw

@+comp:U32 -> @+bi:U32 -> @+mx:U32 -> @+my:U32 -> @+mcu:U32 -> @+rst:U32 -> @+ww:U32 -> @+hmax:U32 -> @+ns:U32 -> @sids:List<&2, U32> -> @ids:List<&2, U32> -> @hs:List<&2, U32> -> @vs:List<&2, U32> -> @+ri:U32 -> Adv

def decode.adv source · line 960 · raw

@ctrl:Ctrl -> @frame:Frame -> @scan:Scan -> @+ri:U32 -> Adv

def decode.block.next.go source · line 969 · raw

@adv:Adv -> @bits:Bits -> @preds:Preds -> @+pred:U32 -> @+comp:U32 -> @frame:Frame -> @scan:Scan -> @tabs:Tabs -> Blk

def decode.block.next source · line 986 · raw

@bits:Bits -> @preds:Preds -> @+pred:U32 -> @ctrl:Ctrl -> @+frame:Frame -> @+scan:Scan -> @tabs:Tabs -> @+ri:U32 -> Blk

def decode.geom.nz source · line 1000 · raw

@+nn:U32 -> U32

def decode.geom.go source · line 1010 · raw

@+comp:U32 -> @+bi:U32 -> @+mx:U32 -> @+my:U32 -> @+ww:U32 -> @+hh:U32 -> @+hmax:U32 -> @+vmax:U32 -> @sids:List<&2, U32> -> @ids:List<&2, U32> -> @hs:List<&2, U32> -> @vs:List<&2, U32> -> Geom

where block bi of a component sits in its MCU: a component's hi * vi blocks run left to right, hi to a row, then top to bottom (T.81 A.2.3), so its column is bi mod hi and its row bi div hi

def decode.geom source · line 1033 · raw

@ctrl:Ctrl -> @frame:Frame -> @scan:Scan -> Geom

def decode.cursor.py source · line 1042 · raw

@more:Bool -> @+kk:U32 -> @+py:U32 -> Cursor

def decode.cursor.px source · line 1049 · raw

@more:Bool -> @+kk:U32 -> @+px:U32 -> @+py:U32 -> @+ph:U32 -> Cursor

def decode.cursor source · line 1056 · raw

@+kk:U32 -> @+px:U32 -> @+py:U32 -> @+pw:U32 -> @+ph:U32 -> Cursor

def decode.splat.n source · line 1059 · raw

@+pw:U32 -> @+ph:U32 -> Nat

def decode.splat.in source · line 1062 · raw

@xin:Bool -> @yin:Bool -> @plane:Array<U32> -> @+xx:U32 -> @+yy:U32 -> @+ww:U32 -> @+sample:U32 -> Array<U32>

def decode.splat.put source · line 1073 · raw

@plane:Array<U32> -> @+kk:U32 -> @+px:U32 -> @+py:U32 -> @samples:List<&2, U32> -> @+ox:U32 -> @+oy:U32 -> @+pw:U32 -> @+ph:U32 -> @+ww:U32 -> @+hh:U32 -> Array<U32>

def decode.splat source · line 1090 · raw

@left:Nat -> @cur:Cursor -> @+samples:List<&2, U32> -> @plane:Array<U32> -> @+ox:U32 -> @+oy:U32 -> @+pw:U32 -> @+ph:U32 -> @+ww:U32 -> @+hh:U32 -> Array<U32>

def decode.paint.which source · line 1114 · raw

@which:Bool -> @samples:List<&2, U32> -> @plane:Array<U32> -> @+ox:U32 -> @+oy:U32 -> @+pw:U32 -> @+ph:U32 -> @+ww:U32 -> @+hh:U32 -> Array<U32>

def decode.paint.use source · line 1132 · raw

@gg:Geom -> @which:Bool -> @samples:List<&2, U32> -> @plane:Array<U32> -> Array<U32>

def decode.ctrl.comp source · line 1137 · raw

@ctrl:Ctrl -> U32

def decode.sink.leaf source · line 1142 · raw

@aa:Array<U32> -> U32

def decode.sink.p source · line 1149 · raw

@pp:Pair(Array<U32>, U32) -> U32

def decode.sink source · line 1153 · raw

@aa:Array<U32> -> U32

def decode.depth source · line 1156 · raw

@+nn:U32 -> Nat

def decode.plane source · line 1163 · raw

@+nn:U32 -> Array<U32>

def decode.emit source · line 1166 · raw

@left:Nat -> @got:Pair(Array<U32>, U32) -> @+ii:U32 -> @acc:List<&2, U32> -> @fresh:Bool -> List<&2, U32>

def decode.round.s source · line 1197 · raw

@ss:U32 -> @+prod:U32 -> U32

def decode.round source · line 1204 · raw

@+prod:U32 -> U32

def opaque source · line 1210 · raw

@+xx:U32 -> U32

a sample's colour bits made opaque: alpha 255 over the low 24 bits. The constant is the first operand, so a law over any sample sees its alpha without a case split on the sample's bits.

def rgb.bits source · line 1214 · raw

@+yy:U32 -> @+cb:U32 -> @+cr:U32 -> U32

YCbCr to colour bits, (R << 16) | (G << 8) | B, per JFIF T.871

def rgb source · line 1223 · raw

@+yy:U32 -> @+cb:U32 -> @+cr:U32 -> U32

YCbCr to a packed opaque sample, 0xFFRRGGBB

def gray.bits source · line 1227 · raw

@+yy:U32 -> U32

a gray level's low byte in R, G and B

def gray source · line 1232 · raw

@+yy:U32 -> U32

a gray level as a packed opaque sample, 0xFFvvvvvv

def decode.grays source · line 1236 · raw

@ys:List<&2, U32> -> List<&2, U32>

every gray level of a picture as a packed opaque sample

def decode.rgbs source · line 1244 · raw

@ys:List<&2, U32> -> @bs:List<&2, U32> -> @rs:List<&2, U32> -> List<&2, U32>

every Y, Cb, Cr triple of a picture as a packed opaque sample, as many as the shortest list holds

def decode.done.drop source · line 1265 · raw

@yy:Array<U32> -> @cb:Array<U32> -> @cr:Array<U32> -> Maybe<&2, Pic>

def decode.done.gray source · line 1271 · raw

@+ww:U32 -> @+hh:U32 -> @yy:Array<U32> -> @cb:Array<U32> -> @cr:Array<U32> -> Maybe<&2, Pic>

def decode.done.color source · line 1277 · raw

@+ww:U32 -> @+hh:U32 -> @yy:Array<U32> -> @cb:Array<U32> -> @cr:Array<U32> -> Maybe<&2, Pic>

a colour picture: each point's Y, Cb and Cr read out in order, then packed

def decode.done.nf3 source · line 1283 · raw

@three:Bool -> @+ww:U32 -> @+hh:U32 -> @yy:Array<U32> -> @cb:Array<U32> -> @cr:Array<U32> -> Maybe<&2, Pic>

three components are colour; any other count is none

def decode.done.nf1 source · line 1291 · raw

@one:Bool -> @+nf:U32 -> @+ww:U32 -> @+hh:U32 -> @yy:Array<U32> -> @cb:Array<U32> -> @cr:Array<U32> -> Maybe<&2, Pic>

one component is gray; the rest is decided by decode.done.nf3

def decode.done.nf source · line 1307 · raw

@+nf:U32 -> @+ww:U32 -> @+hh:U32 -> @yy:Array<U32> -> @cb:Array<U32> -> @cr:Array<U32> -> Maybe<&2, Pic>

the picture by its component count. U32.is_eq, not a literal pattern, so a law reaches every count.

def decode.done.ok source · line 1311 · raw

@bad:Bool -> @frame:Frame -> @yy:Array<U32> -> @cb:Array<U32> -> @cr:Array<U32> -> Maybe<&2, Pic>

a failed scan is none; otherwise the picture by the frame's component count

def decode.done source · line 1321 · raw

@+ok:U32 -> @frame:Frame -> @yy:Array<U32> -> @cb:Array<U32> -> @cr:Array<U32> -> Maybe<&2, Pic>

the planes as a picture, or none when ok is 0

def decode.adv.ctrl source · line 1324 · raw

@adv:Adv -> Ctrl

def decode.adv.duef source · line 1329 · raw

@adv:Adv -> U32

def decode.blocks source · line 1334 · raw

@left:Nat -> @blk:Blk -> @+ctrl:Ctrl -> @+preds:Preds -> @+frame:Frame -> @+scan:Scan -> @+tabs:Tabs -> @+ri:U32 -> @yy:Array<U32> -> @cb:Array<U32> -> @cr:Array<U32> -> @+ok:U32 -> Maybe<&2, Pic>

def decode.blocks.sum source · line 1368 · raw

@hs:List<&2, U32> -> @vs:List<&2, U32> -> @+nn:U32 -> U32

def decode.start source · line 1381 · raw

@nn:Nat -> @bits:Bits -> @+frame:Frame -> @+scan:Scan -> @+tabs:Tabs -> @+ri:U32 -> @yy:Array<U32> -> @cb:Array<U32> -> @cr:Array<U32> -> Maybe<&2, Pic>

def decode.run.n source · line 1399 · raw

@empty:Bool -> @+ww:U32 -> @+hh:U32 -> @frame:Frame -> @scan:Scan -> @tabs:Tabs -> @ent:List<&2, U32> -> @+ri:U32 -> Maybe<&2, Pic>

def decode.run source · line 1420 · raw

@frame:Frame -> @scan:Scan -> @tabs:Tabs -> @ent:List<&2, U32> -> @+ri:U32 -> Maybe<&2, Pic>

def decode.finish.ok source · line 1425 · raw

@ok1:Bool -> @ok2:Bool -> @frame:Frame -> @scan:Scan -> @tabs:Tabs -> @ent:List<&2, U32> -> @+ri:U32 -> Maybe<&2, Pic>

def decode.finish.ph source · line 1444 · raw

@phase:Phase -> @frame:Frame -> @scan:Scan -> @tabs:Tabs -> @ent:List<&2, U32> -> @+ri:U32 -> @+kind:U32 -> @+bad:U32 -> Maybe<&2, Pic>

def decode.finish source · line 1460 · raw

@st:St -> Maybe<&2, Pic>

def decode.max.b source · line 1465 · raw

@gt:Bool -> @+aa:U32 -> @+bb:U32 -> U32

def decode.max source · line 1472 · raw

@+aa:U32 -> @+bb:U32 -> U32

def decode.vmax source · line 1475 · raw

@vs:List<&2, U32> -> @+mm:U32 -> U32

def decode.fac.ok source · line 1482 · raw

@+hh:U32 -> U32

def decode.fac.bad source · line 1493 · raw

@+hh:U32 -> @+vv:U32 -> @+bad:U32 -> U32

def decode.nf.ok source · line 1496 · raw

@+nf:U32 -> U32

def decode.u16 source · line 1505 · raw

@+hi:U32 -> @+lo:U32 -> U32

def decode.comps.rev source · line 1508 · raw

@cc:Comps -> Comps

def decode.read.cs source · line 1514 · raw

@left:Nat -> @xs:List<&2, U32> -> @ids:List<&2, U32> -> @hs:List<&2, U32> -> @vs:List<&2, U32> -> @tqs:List<&2, U32> -> @+bad:U32 -> Comps

def decode.read.sof.ok source · line 1537 · raw

@good:Bool -> @zmax:Bool -> @+ww:U32 -> @+hh:U32 -> @+nf:U32 -> @ids:List<&2, U32> -> @+hs:List<&2, U32> -> @+vs:List<&2, U32> -> @tq:List<&2, U32> -> @scan:Scan -> @tabs:Tabs -> @ent:List<&2, U32> -> @+ri:U32 -> @+kind:U32 -> St

def decode.read.sof.f source · line 1568 · raw

@cc:Comps -> @+ww:U32 -> @+hh:U32 -> @+nf:U32 -> @scan:Scan -> @tabs:Tabs -> @ent:List<&2, U32> -> @+ri:U32 -> @+kind:U32 -> @+bad:U32 -> St

def decode.read.sof.p source · line 1586 · raw

@p8:Bool -> @xs:List<&2, U32> -> @scan:Scan -> @tabs:Tabs -> @ent:List<&2, U32> -> @+ri:U32 -> @+kind:U32 -> @+bad:U32 -> St

the SOF0 body after its precision byte: precision 8 goes on to the size and the components, any other stops

def decode.read.sof source · line 1608 · raw

@xs:List<&2, U32> -> @scan:Scan -> @tabs:Tabs -> @ent:List<&2, U32> -> @+ri:U32 -> @+kind:U32 -> @+bad:U32 -> St

an SOF0 body. The precision is compared with U32.is_eq, not a literal pattern, so a law reaches it.

def decode.take source · line 1623 · raw

@left:Nat -> @xs:List<&2, U32> -> @acc:List<&2, U32> -> Pair(List<&2, U32>, List<&2, U32>)

def decode.q.put source · line 1634 · raw

@tabs:Tabs -> @+id:U32 -> @vals:List<&2, U32> -> Tabs

def decode.read.dqt source · line 1647 · raw

@xs:List<&2, U32> -> @ok:Bool -> @phase:Nat -> @+id:U32 -> @acc:List<&2, U32> -> @frame:Frame -> @scan:Scan -> @tabs:Tabs -> @ent:List<&2, U32> -> @+ri:U32 -> @+kind:U32 -> @+bad:U32 -> St

def decode.sum.counts source · line 1696 · raw

@xs:List<&2, U32> -> @+nn:U32 -> U32

def decode.huff.put.dc source · line 1703 · raw

@+id:U32 -> @hh:Huff -> @q0:List<&2, U32> -> @q1:List<&2, U32> -> @q2:List<&2, U32> -> @q3:List<&2, U32> -> @dc0:Huff -> @dc1:Huff -> @dc2:Huff -> @dc3:Huff -> @ac0:Huff -> @ac1:Huff -> @ac2:Huff -> @ac3:Huff -> Tabs

def decode.huff.put.ac source · line 1729 · raw

@+id:U32 -> @hh:Huff -> @q0:List<&2, U32> -> @q1:List<&2, U32> -> @q2:List<&2, U32> -> @q3:List<&2, U32> -> @dc0:Huff -> @dc1:Huff -> @dc2:Huff -> @dc3:Huff -> @ac0:Huff -> @ac1:Huff -> @ac2:Huff -> @ac3:Huff -> Tabs

def decode.huff.put source · line 1755 · raw

@tabs:Tabs -> @+cls:U32 -> @+id:U32 -> @hh:Huff -> Tabs

def decode.read.dht source · line 1764 · raw

@xs:List<&2, U32> -> @ok:Bool -> @sym:Bool -> @phase:Nat -> @+cls:U32 -> @+id:U32 -> @+counts:List<&2, U32> -> @+syms:List<&2, U32> -> @frame:Frame -> @scan:Scan -> @tabs:Tabs -> @ent:List<&2, U32> -> @+ri:U32 -> @+kind:U32 -> @+bad:U32 -> St

def decode.scan.rev source · line 1855 · raw

@sids:List<&2, U32> -> @td:List<&2, U32> -> @ta:List<&2, U32> -> @+ns:U32 -> Scan

def decode.read.sos.ok source · line 1858 · raw

@ss0:Bool -> @se63:Bool -> @ah0:Bool -> @sids:List<&2, U32> -> @td:List<&2, U32> -> @ta:List<&2, U32> -> @+ns:U32 -> @frame:Frame -> @tabs:Tabs -> @ent:List<&2, U32> -> @+ri:U32 -> @+kind:U32 -> @+bad:U32 -> St

def decode.read.sos.end source · line 1887 · raw

@xs:List<&2, U32> -> @sids:List<&2, U32> -> @td:List<&2, U32> -> @ta:List<&2, U32> -> @+ns:U32 -> @frame:Frame -> @tabs:Tabs -> @ent:List<&2, U32> -> @+ri:U32 -> @+kind:U32 -> @+bad:U32 -> St

def decode.read.sos.cs source · line 1907 · raw

@left:Nat -> @xs:List<&2, U32> -> @sids:List<&2, U32> -> @td:List<&2, U32> -> @ta:List<&2, U32> -> @+ns:U32 -> @frame:Frame -> @tabs:Tabs -> @ent:List<&2, U32> -> @+ri:U32 -> @+kind:U32 -> @+bad:U32 -> St

def decode.read.sos source · line 1932 · raw

@xs:List<&2, U32> -> @frame:Frame -> @tabs:Tabs -> @ent:List<&2, U32> -> @+ri:U32 -> @+kind:U32 -> @+bad:U32 -> St

def decode.read.dri source · line 1947 · raw

@xs:List<&2, U32> -> @frame:Frame -> @scan:Scan -> @tabs:Tabs -> @ent:List<&2, U32> -> @+kind:U32 -> @+bad:U32 -> St

def decode.read.app0.den source · line 1962 · raw

@xz:Bool -> @yz:Bool -> @frame:Frame -> @scan:Scan -> @tabs:Tabs -> @ent:List<&2, U32> -> @+ri:U32 -> @+kind:U32 -> @+bad:U32 -> St

def decode.read.app0.id source · line 1984 · raw

@jfif:Bool -> @+xh:U32 -> @+xl:U32 -> @+yh:U32 -> @+yl:U32 -> @frame:Frame -> @scan:Scan -> @tabs:Tabs -> @ent:List<&2, U32> -> @+ri:U32 -> @+kind:U32 -> @+bad:U32 -> St

an APP0 body that opens with the JFIF identifier has its density checked; any other is skipped

def decode.read.app0 source · line 2006 · raw

@xs:List<&2, U32> -> @frame:Frame -> @scan:Scan -> @tabs:Tabs -> @ent:List<&2, U32> -> @+ri:U32 -> @+kind:U32 -> @+bad:U32 -> St

an APP0 body. The identifier is compared with U32.is_eq, not literal patterns, so a law reaches it.

def decode.dispatch source · line 2023 · raw

@+mark:U32 -> @xs:List<&2, U32> -> @frame:Frame -> @scan:Scan -> @tabs:Tabs -> @ent:List<&2, U32> -> @+ri:U32 -> @+kind:U32 -> @+bad:U32 -> St

def decode.between source · line 2050 · raw

@+bb:U32 -> @+lo:U32 -> @+hi:U32 -> Bool

def decode.mark.range.b source · line 2053 · raw

@sof:Bool -> @app:Bool -> @rst:Bool -> @+bb:U32 -> @frame:Frame -> @scan:Scan -> @tabs:Tabs -> @ent:List<&2, U32> -> @+ri:U32 -> @+kind:U32 -> @+bad:U32 -> St

def decode.mark.range source · line 2080 · raw

@+bb:U32 -> @frame:Frame -> @scan:Scan -> @tabs:Tabs -> @ent:List<&2, U32> -> @+ri:U32 -> @+kind:U32 -> @+bad:U32 -> St

def decode.mark source · line 2093 · raw

@+bb:U32 -> @frame:Frame -> @scan:Scan -> @tabs:Tabs -> @ent:List<&2, U32> -> @+ri:U32 -> @+kind:U32 -> @+bad:U32 -> St

def decode.step.pay0 source · line 2127 · raw

@left:Nat -> @+mark:U32 -> @frame:Frame -> @scan:Scan -> @tabs:Tabs -> @ent:List<&2, U32> -> @+ri:U32 -> @+kind:U32 -> @+bad:U32 -> St

def decode.step.len.b source · line 2144 · raw

@small:Bool -> @+mark:U32 -> @+len:U32 -> @frame:Frame -> @scan:Scan -> @tabs:Tabs -> @ent:List<&2, U32> -> @+ri:U32 -> @+kind:U32 -> @+bad:U32 -> St

def decode.step.last source · line 2162 · raw

@left:Nat -> @+bb:U32 -> @+mark:U32 -> @acc:List<&2, U32> -> @frame:Frame -> @scan:Scan -> @tabs:Tabs -> @ent:List<&2, U32> -> @+ri:U32 -> @+kind:U32 -> @+bad:U32 -> St

def decode.step.pay source · line 2181 · raw

@left:Nat -> @+bb:U32 -> @+mark:U32 -> @acc:List<&2, U32> -> @frame:Frame -> @scan:Scan -> @tabs:Tabs -> @ent:List<&2, U32> -> @+ri:U32 -> @+kind:U32 -> @+bad:U32 -> St

def decode.ent.rst.b source · line 2200 · raw

@rst:Bool -> @+bb:U32 -> @frame:Frame -> @scan:Scan -> @tabs:Tabs -> @ent:List<&2, U32> -> @+ri:U32 -> @+kind:U32 -> @+bad:U32 -> St

def decode.step.ph source · line 2217 · raw

@phase:Phase -> @+bb:U32 -> @frame:Frame -> @scan:Scan -> @tabs:Tabs -> @ent:List<&2, U32> -> @+ri:U32 -> @+kind:U32 -> @+bad:U32 -> St

def decode.step source · line 2263 · raw

@+bb:U32 -> @st:St -> St

def decode.walk source · line 2268 · raw

@xs:List<&2, U32> -> @st:St -> St

def soi source · line 2276 · raw

List<&2, U32>

the JPEG start-of-image marker, FF D8

def eoi source · line 2280 · raw

List<&2, U32>

the JPEG end-of-image marker, FF D9

def decode source · line 2284 · raw

@bytes:List<&2, U32> -> Maybe<&2, Pic>

baseline JPEG bytes, or none when the frame is not sequential Huffman