RotoShop - FAQ

Design and implement a program that rotates and flips (horizontally and vertically) image files.

Image File Format
An image file, for the purposes of this project, is a BMP file containing an image that is not compressed. They are discussed in the steganography project. Use binary i/o to read BMP files. Here are some images to work with: tiny, small

Required Functions
get-bmp: Write a function invoked as (get-bmp filename state) that takes a filename (path) represented as an ACL2-string, along with the ACL2 state, and delivers a multivalue containing the ACL2 state and a representation, in the form of an ACL2 object of your design, from which the file could be reproduced. An object of this form will be referred to in this document as an image.

put-bmp: Write a function invoked (put-bmp filename image state) that takes a filename (path) represented as an ACL2-string and an image (of the form that get-bmp generates), along with the ACL2 state, and delivers a multivalue containing the ACL2 state and a string indicating the success or failure of the operation. In addition, put-bmp has the effect of writing a BMP file reflecting the contents of the image.

flip-horiz: Write a function invoked as (flip-horiz image) that takes an image (of the form that get-bmp generates) and delivers a new image like the input, but with the picture it represents flipped, left for right. For example, the pixels along the right edge of the input image, fall in the same order, top to bottom, along the left edge of the output image. The column of pixels bordering the right edge of the input image would border the left edge of the output image, and so on.

flip-vert: Write a function invoked as (flip-vert image) that takes an image (of the form that get-bmp generates) and delivers a new image like the input, but with the picture it represents flipped, top for bottom.

rotate: Write a function invoked as (rotate image) that takes an image and delivers a new image like the input, but with the picture it represents rotated ninety degrees clockwise.

Tests and Theorems

1. (flip-horiz (flip-horiz image)) is the same as image.
2. (flip-vert (flip-vert image)) is the same as image.
3. (flip-horiz (flip-vert image)) is the same as (flip-horiz (flip-vert image)).
4. (flip-horiz (flip-vert image)) is the same as (rotate (rotate image))

Performance
Your program needs to be able to successfully flip or rotate bmp files with resolutions in the range 300x300 to 400x400 within a few minutes. Tail recursion can help.