2.9 "world"
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.
Starts an animation, given a width and height for each frame, the time in
seconds between clock ticks, and the initial World value.
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.
Registers a function to update the world each time the clock ticks. The second
version allows i/o actions during the event handler based on ACL2’s
state variable.
Registers a function to update the world each time the user presses or releases
a key. The second
version allows i/o actions during the event handler based on ACL2’s
state variable.
Registers a function to update the world each time the user moves or clicks the
mouse. The second
version allows i/o actions during the event handler based on ACL2’s
state variable.
2.9.2 Scenes
These primitives operate on images intended as complete animation frames.
Produces a blank scene of the given dimensions from which to construct an
animation frame.
Adds img to scn at the given coordinates.
2.9.3 Images
These primitives construct images as first-class values.
These functions construct images of various geometric shapes.
Constructs an image of text.
Adds a line from (x1,y1) to (x2,y2) of color
c to i.
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.
These functions compute the dimensions of an image.
These functions deal with an image’s pinhole, the point on which
overlay places other images and from which
place-image
calculates offsets.
Recognizes images.
2.9.4 Colors and Modes
Recognizes image drawing modes: 'solid or 'outline.
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.
These functions (constructor, selectors, and predicate) define a datatype of
colors based on red, green, and blue values between 0 and 255.
Recognizes integers between 0 and 255, inclusive.
2.9.5 Posns
Posns are structures representing positions in two-dimensional space. These
procedures correspond to the constructor, selectors, predicate, and weak
predicate for Posns.