main.bend checks

raw source on the hub · import 0xde7817074d0d382dc55dfca454298427/main.bend as Main

ezimg: images for Bend 2, with PNG and baseline JPEG decode and encode

A Raster is a width, a height, and row-major samples. PNG decode reads 8-bit images. PNG encode writes colour type 2 or 6. JPEG decode reads a baseline sequential frame, and encode_jpeg writes one.

4 imports

import Base
import ./src/png.bend as Png
import ./src/jpeg.bend as Jpeg
import ./src/jpeg_enc.bend as Jenc

Types

type Raster source · line 12 · raw

Data

a picture: width, height, and row-major samples, each packed 0xAARRGGBB

Raster

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

Definitions

def png_sig source · line 16 · raw

List<&2, U32>

the PNG signature: 137 80 78 71 13 10 26 10

def jpeg_soi source · line 20 · raw

List<&2, U32>

the JPEG start-of-image marker: 255 216

def nbytes source · line 24 · raw

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

how many samples a byte list holds

def raster source · line 28 · raw

@ww:U32 -> @hh:U32 -> @pixels:List<&2, U32> -> Raster

a picture from its width, height, and samples

def width source · line 32 · raw

@img:Raster -> U32

the width

def height source · line 38 · raw

@img:Raster -> U32

the height

def pixels source · line 44 · raw

@img:Raster -> List<&2, U32>

the samples

def size source · line 50 · raw

@img:Raster -> Pair(U32, U32)

width and height together

def count source · line 56 · raw

@img:Raster -> U32

width times height

def fill source · line 62 · raw

@+ww:U32 -> @+hh:U32 -> @+color:U32 -> Raster

a solid picture of one sample

def u.min.pick source · line 65 · raw

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

def u.min source · line 72 · raw

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

def get.y source · line 75 · raw

@yin:Bool -> @px:List<&2, U32> -> @+ww:U32 -> @+xx:U32 -> @+yy:U32 -> Maybe<&2, U32>

def get.x source · line 82 · raw

@xin:Bool -> @px:List<&2, U32> -> @+ww:U32 -> @+hh:U32 -> @+xx:U32 -> @+yy:U32 -> Maybe<&2, U32>

def get source · line 90 · raw

@img:Raster -> @+xx:U32 -> @+yy:U32 -> Maybe<&2, U32>

the sample at (x, y), or none when that point is outside the picture

def set.y source · line 95 · raw

@yin:Bool -> @+ww:U32 -> @+hh:U32 -> @px:List<&2, U32> -> @+xx:U32 -> @+yy:U32 -> @+color:U32 -> Raster

def set.x source · line 110 · raw

@xin:Bool -> @+ww:U32 -> @+hh:U32 -> @px:List<&2, U32> -> @+xx:U32 -> @+yy:U32 -> @+color:U32 -> Raster

def set source · line 126 · raw

@img:Raster -> @+xx:U32 -> @+yy:U32 -> @+color:U32 -> Raster

the picture with (x, y) replaced by color; outside, the picture is unchanged

def crop.rows source · line 131 · raw

@+nn:Nat -> @+px:List<&2, U32> -> @+rw:Nat -> @+gap:Nat -> List<&2, U32>

def crop.use source · line 139 · raw

@zh:Bool -> @+px:List<&2, U32> -> @+ww:U32 -> @+xx:U32 -> @+yy:U32 -> @+rw:U32 -> @+rh:U32 -> Raster

def crop.open source · line 156 · raw

@zw:Bool -> @zh:Bool -> @+px:List<&2, U32> -> @+ww:U32 -> @+xx:U32 -> @+yy:U32 -> @+rw:U32 -> @+rh:U32 -> Raster

def crop.box source · line 172 · raw

@+px:List<&2, U32> -> @+ww:U32 -> @+hh:U32 -> @+xx:U32 -> @+yy:U32 -> @+cw:U32 -> @+ch:U32 -> Raster

def crop.y source · line 185 · raw

@yin:Bool -> @+px:List<&2, U32> -> @+ww:U32 -> @+hh:U32 -> @+xx:U32 -> @+yy:U32 -> @+cw:U32 -> @+ch:U32 -> Raster

def crop.x source · line 201 · raw

@xin:Bool -> @+px:List<&2, U32> -> @+ww:U32 -> @+hh:U32 -> @+xx:U32 -> @+yy:U32 -> @+cw:U32 -> @+ch:U32 -> Raster

def crop source · line 219 · raw

@img:Raster -> @+xx:U32 -> @+yy:U32 -> @+cw:U32 -> @+ch:U32 -> Raster

the intersection of rectangle (x, y, cw, ch) with the picture. A miss, or a zero side, is an empty picture.

def blit.row source · line 224 · raw

@+dp:List<&2, U32> -> @+sp:List<&2, U32> -> @+left:Nat -> @+cover:Nat -> @+tail:Nat -> List<&2, U32>

def blit.rows source · line 235 · raw

@+nn:Nat -> @+dp:List<&2, U32> -> @+sp:List<&2, U32> -> @+left:Nat -> @+cover:Nat -> @+tail:Nat -> @+dw:Nat -> @+sw:Nat -> List<&2, U32>

def blit.join source · line 252 · raw

@+dp:List<&2, U32> -> @+sp:List<&2, U32> -> @+dw:U32 -> @+dh:U32 -> @+sw:U32 -> @+sh:U32 -> @+ox:U32 -> @+oy:U32 -> List<&2, U32>

def blit.y source · line 274 · raw

@inside:Bool -> @+dp:List<&2, U32> -> @+sp:List<&2, U32> -> @+dw:U32 -> @+dh:U32 -> @+sw:U32 -> @+sh:U32 -> @+ox:U32 -> @+oy:U32 -> List<&2, U32>

def blit.src source · line 291 · raw

@src:Raster -> @+dw:U32 -> @+dh:U32 -> @dp:List<&2, U32> -> @+xx:U32 -> @+yy:U32 -> Raster

def blit source · line 298 · raw

@dst:Raster -> @src:Raster -> @+xx:U32 -> @+yy:U32 -> Raster

src pasted onto dst at (x, y). dst keeps its size; samples past its edge are dropped, and an overlapping sample takes the source.

def sig.match source · line 320 · raw

@want:List<&2, U32> -> @bytes:List<&2, U32> -> @ok:Bool -> Bool

do the bytes open with the bytes of want? Each byte is compared with U32.is_eq, not a literal pattern: a literal pattern matches bit by bit, so a law over a symbolic byte cannot get past it, while is_eq has a lemma (ueq). ok carries the answer so far, so the walk is a tail call.

def sig.pick source · line 330 · raw

@ok:Bool -> Maybe<&2, List<&2, U32>>

def parse_signature source · line 338 · raw

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

the PNG signature when the bytes open with it, otherwise none

def decode_png.pic source · line 341 · raw

@mm:Maybe<&2, 0xde7817074d0d382dc55dfca454298427/src/png.Pic> -> Maybe<&2, Raster>

def decode_png.of source · line 348 · raw

@mm:Maybe<&2, List<&2, U32>> -> @+bytes:List<&2, U32> -> Maybe<&2, Raster>

def decode_png source · line 358 · raw

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

PNG bytes, or none when the signature or the encoding is rejected

def encode_png source · line 364 · raw

@img:Raster -> Maybe<&2, List<&2, U32>>

ISO/IEC 15948 / W3C PNG — bytes of an 8-bit picture, interlace method 0. Colour type 2 when every sample is opaque, otherwise colour type 6. None when a side is zero or the sample count is not the area.

def decode_jpeg.out source · line 369 · raw

@got:Maybe<&2, 0xde7817074d0d382dc55dfca454298427/src/jpeg.Pic> -> Maybe<&2, Raster>

def decode_jpeg source · line 377 · raw

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

a baseline sequential JPEG, or none when the bytes are not one

def colour source · line 382 · raw

@+pp:U32 -> U32

a sample's colour, alpha cleared. The mask is the first operand, so a law over any sample sees its bits without a case split.

def colours source · line 386 · raw

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

every sample's colour, alpha cleared

def encode_jpeg.pick source · line 393 · raw

@ok:Bool -> @+ww:U32 -> @+hh:U32 -> @px:List<&2, U32> -> Maybe<&2, List<&2, U32>>

def encode_jpeg source · line 404 · raw

@img:Raster -> Maybe<&2, List<&2, U32>>

a baseline sequential 4:4:4 JPEG of the samples' colour: alpha is cleared before the encoder sees a sample. None exactly when encode_png is none: a side is zero, the area passes 2^32, or the sample count is not the area. Both ask the same guard, Png.enc.good.

Templates

template map.go source · line 303 · raw

@-ff:(@_:U32 -> U32) -> @px:List<&2, U32> -> List<&2, U32>

template map source · line 311 · raw

@-ff:(@_:U32 -> U32) -> @img:Raster -> Raster

every sample passed through f; the width and the height stay