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 : Int | w > 0) (h : Int | h > 0) (color : Color) : {i : Image | width i = w && height i = h}

Functions

get_width

Reads the width at runtime. The return type is refined to equal the `width` measure, so the value is provably the same width the type system reasons about (e.g. `get_width (mk w h c)` has type `{r:Int | r == w}`).
def get_width (im : Image) : {r : Int | r = width im}

get_height

Reads the height at runtime; refined to equal the `height` measure (see `get_width`).
def get_height (im : Image) : {r : Int | r = height im}

mk

Creates a new image of given width, height, and color.
def mk (w : Int | w > 0) (h : Int | h > 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 : Int | x ≥ 0 && x ≤ width im) (y : Int | y ≥ 0 && y ≤ height im) (w : Int | w > 0 && x + w ≤ width im) (h : Int | h > 0 && y + h ≤ 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 : Int | w > 0) (h : Int | h > 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 : Int | max_w > 0) (max_h : Int | max_h > 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 : Int | x ≥ 0 && x < width im) (y : Int | y ≥ 0 && y < 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 : Int | x ≥ 0 && x < width im) (y : Int | y ≥ 0 && y < 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 : Int | x ≥ 0 && x + width src ≤ width dest) (y : Int | y ≥ 0 && y + 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 : Int | x ≥ 0 && x ≤ width im) (y : Int | y ≥ 0 && y ≤ height im) (w : Int | w > 0 && x + w ≤ width im) (h : Int | h > 0 && y + h ≤ 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
The image's height in pixels, as an uninterpreted measure. It carries the size contracts of every operation (`mk`, `crop`, `resize`, ...) through the type system but has no runtime value; use `get_height` to read it at runtime.
def height : (im : Image) → Int

width

uninterpreted
The image's width in pixels, as an uninterpreted measure (see `height`). Use `get_width` to read it at runtime.
def width : (im : Image) → Int