2.9 "world"

(include-book "world" :dir :teachpacks)

This teachpack provides a datatype for images and a framework for interactive animations. It is partially reflected in the ACL2 logic, but some of the primitives cannot be fully reasoned about or executed due by ACL2 to their imperative and platform-specific nature.

2.9.1 Animations

These forms produce an interactive animation that reacts to events. The user must define a World datatype, representing the state of an animation, and functions to update the World in response to events such as keystrokes or mouse buttons. From this, the teachpack can generate an interactive animation.

Events are based on two extra datatypes. A KeyEvent represents a keystroke, and may be either a character or a symbol such as 'left, 'right, 'up, or 'down. A MouseEvent represents an action of the mouse cursor, and may be 'button-down, 'button-up, 'drag, 'move, 'enter, or 'leave.

(big-bang width height time world) → t

width : posp

height : posp

time : rationalp

world : t

Starts an animation, given a width and height for each frame, the time in seconds between clock ticks, and the initial World value.

(on-redraw draw) → t

draw : World -> image?

Registers a function to draw each frame of an animation.

(stop-when game-over) → t

game-over : World -> boolean?

Registers a function to report when the animation has ended.

(on-tick-event tick) → t

tick : World -> World

Registers a function to update the world each time the clock ticks.

(on-key-event press) → t

press : World KeyEvent -> World

Registers a function to update the world each time the user presses or releases a key.

(on-mouse-event click) → t

click   :   World integerp integerp MouseEvent -> World

Registers a function to update the world each time the user moves or clicks the mouse.

2.9.2 Scenes

These primitives operate on images intended as complete animation frames.

(empty-scene width height) → image?

width : posp

height : posp

Produces a blank scene of the given dimensions from which to construct an animation frame.

(place-image img x y scn) → image?

img : image?

x : integerp

y : integerp

scn : image?

Adds img to scn at the given coordinates.

2.9.3 Images

These primitives construct images as first-class values.

(rectangle w h m c) → image?   w : posp   h : posp   m : mode?   c : image-color?

(circle r m c) → image?   r : posp   m : mode?   c : image-color?

(triangle s m c) → image?   s : posp   m : mode?   c : image-color?

(line x y c) → image?   x : integerp   y : integerp   c : image-color?

These functions construct images of various geometric shapes.

(text str size color) → image?

str : stringp

size : posp

color : image-color?

Constructs an image of text.

(add-line i x1 y1 x2 y2 c) → image?

i : image?

x1 : integerp

y1 : integerp

x2 : integerp

y2 : integerp

c : image-color?

Adds a line from (x1,y1) to (x2,y2) of color c to i.

(overlay i ...) → image?   i : image?

(overlay/xy i x y j) → image?   i : image?   x : integerp   y : integerp   j : image?

These functions place one image over another. The first overlays a number of images as they are; the second overlays one image at an offset on another.

(image-width i) → posp   i : image?

(image-height i) → posp   i : image?

These functions compute the dimensions of an image.

(put-pinhole i x y) → image?   i : image?   x : integerp   y : integerp

(move-pinhole i x y) → image?   i : image?   x : integerp   y : integerp

(pinhole-x i) → integerp   i : image?

(pinhole-y i) → integerp   i : image?

These functions deal with an image’s pinhole, the point on which overlay places other images and from which place-image calculates offsets.

(image? v) → booleanp

v : t

Recognizes images.

2.9.4 Colors and Modes

(mode? v) → booleanp

v : t

Recognizes image drawing modes: 'solid or 'outline.

(image-color? v) → booleanp

v : t

Recognizes colors constructed with make-color, or color names as strings or symbols. Color names include:

DarkRed, Red, LightPink, Pink, Brown, DarkOrange, Orange, Yellow, LightYellow, Green, DarkGreen, LightGreen, Cyan, LightBlue, LightCyan, DarkBlue, Blue, Purple, Magenta, DarkMagenta, Violet, White, LightGray, Gray, DarkGray, and Black.

(make-color r g b) → color?   r : bytep   g : bytep   b : bytep

(color-red c) → bytep   c : color?

(color-green c) → bytep   c : color?

(color-blue c) → bytep   c : color?

(color? v) → booleanp   v : t

These functions (constructor, selectors, and predicate) define a datatype of colors based on red, green, and blue values between 0 and 255.

(bytep v) → booleanp

v : t

Recognizes integers between 0 and 255, inclusive.

2.9.5 Posns

(make-posn x y) → posn?   x : integerp   y : integerp

(posn-x p) → integerp   p : posn?

(posn-y p) → integerp   p : posn?

(posn? v) → booleanp   v : t

(weak-posn? v) → booleanp   v : t

Posns are structures representing positions in two-dimensional space. These procedures correspond to the constructor, selectors, predicate, and weak predicate for Posns.