Image

Imports
open Color;
Table of Contents

Types

Image

(type)
type Image

Constructors

For each type in this module: inductive types list their declared constructors; opaque types list any local function whose name starts with mk and which returns a value of that type.

Image (opaque · mk*)

mk

Creates a new image of given width, height, and color.
def mk (w: {p : Int | p > 0}) (h: {p : Int | p > 0}) (color: Color) : {i : Image | width i == w && height i == h}

Functions

mk

Creates a new image of given width, height, and color.
def mk (w: {p : Int | p > 0}) (h: {p : Int | p > 0}) (color: Color) : {i : Image | width i == w && height i == h}

copy

Returns an independent copy (PIL Image.copy).
def copy (im: Image) : {c : Image | width c == width im && height c == height im}

crop

Crops a rectangular region [x, x+w) × [y, y+h) into a new image of size w×h.
def crop (im: Image) (x: {p : Int | p >= 0 && p <= width im}) (y: {p : Int | p >= 0 && p <= height im}) (w: {p : Int | p > 0 && x + p <= width im}) (h: {p : Int | p > 0 && y + p <= height im}) : {r : Image | width r == w && height r == h}

resize

Resamples to an exact width and height (PIL Image.resize with high-quality filter).
def resize (im: Image) (w: {p : Int | p > 0}) (h: {p : Int | p > 0}) : {r : Image | width r == w && height r == h}

fit_inside

Shrinks the image in-place on a copy so it fits inside max_w×max_h while preserving aspect ratio (PIL thumbnail).
def fit_inside (im: Image) (max_w: {p : Int | p > 0}) (max_h: {p : Int | p > 0}) : Image

rotate

Rotates counter-clockwise by angle degrees; output size matches input (expand=False, PIL default behavior).
def rotate (im: Image) (angle: Float) : {r : Image | width r == width im && height r == height im}

flip_horizontal

Horizontal mirror (PIL FLIP_LEFT_RIGHT).
def flip_horizontal (im: Image) : {r : Image | width r == width im && height r == height im}

flip_vertical

Vertical mirror (PIL FLIP_TOP_BOTTOM).
def flip_vertical (im: Image) : {r : Image | width r == width im && height r == height im}

get_pixel

Samples the RGB pixel at (x, y) as a Color (always RGB mode after open/mk).
def get_pixel (im: Image) (x: {p : Int | p >= 0 && p < width im}) (y: {p : Int | p >= 0 && p < height im}) : Color

put_pixel

Functional single-pixel draw: returns a new image with one pixel replaced (PIL putpixel on a copy).
def put_pixel (im: Image) (x: {p : Int | p >= 0 && p < width im}) (y: {p : Int | p >= 0 && p < height im}) (color: Color) : {r : Image | width r == width im && height r == height im}

paste

Pastes `src` onto `dest` with top-left at (x, y); both images stay RGB-aligned in the binding layer.
def paste (dest: Image) (src: Image) (x: {p : Int | p >= 0 && p + width src <= width dest}) (y: {p : Int | p >= 0 && p + height src <= height dest}) : {r : Image | width r == width dest && height r == height dest}

grayscale

Converts to grayscale luminance then back to RGB so Color-based pipelines keep one channel width.
def grayscale (im: Image) : {g : Image | width g == width im && height g == height im}

invert

Per-channel photographic invert (ImageOps.invert).
def invert (im: Image) : {r : Image | width r == width im && height r == height im}

blur

Gaussian blur; radius is the PIL GaussianBlur radius (in pixels, ≥ 0).
def blur (im: Image) (radius: Float) : {r : Image | width r == width im && height r == height im}

show

Displays the image.
def show (image: Image) : Unit

save

Saves the image to a file.
def save (image: Image) (path: String) : Unit

open

Opens an image from a file (normalized to RGB for predictable Color / pixel operations).
def open (path: String) : Image

diff

Computes the mean squared error (MSE) difference between two images.
def diff (img: Image) (img2: Image) : Float

fitness_bw_mse

def fitness_bw_mse (candidate: Image) (reference: Image) : Float

fitness_half_size_mse

def fitness_half_size_mse (candidate: Image) (reference: Image) : Float

fitness_row_mismatch

def fitness_row_mismatch (candidate: Image) (reference: Image) : Float

fitness_col_mismatch

def fitness_col_mismatch (candidate: Image) (reference: Image) : Float

fitness_pixel_mismatch

def fitness_pixel_mismatch (candidate: Image) (reference: Image) : Float

draw_rectangle

Draws a rectangle on the image.
def draw_rectangle (im: Image) (x: {p : Int | p >= 0 && p <= width im}) (y: {p : Int | p >= 0 && p <= height im}) (w: {p : Int | p > 0 && x + p <= width im}) (h: {p : Int | p > 0 && y + p <= height im}) (color: Color) : {rim : Image | width rim == width im && height rim == height im}

Uninterpreted

Functions declared as def f ... = uninterpreted: only their signature is known to the verifier; they have no body.

height

uninterpreted
Returns the height of the image in pixels.
def height : (im : Image) -> Int

width

uninterpreted
Returns the width of the image in pixels.
def width : (im : Image) -> Int