►Dracula:   Reference Manual
▼2 Teachpacks
►2.9 "world"
On this page:
2.9.1 Animations
big-bang
on-redraw
stop-when
on-tick-event
on-tick-event/  state
on-key-event
on-key-event/  state
on-mouse-event
on-mouse-event/  state
2.9.2 Scenes
empty-scene
place-image
2.9.3 Images
rectangle
circle
triangle
line
text
add-line
overlay
overlay/  xy
image-width
image-height
put-pinhole
move-pinhole
pinhole-x
pinhole-y
image?
2.9.4 Colors and Modes
mode?
image-color?
make-color
color-red
color-green
color-blue
color?
bytep
2.9.5 Posns
make-posn
posn-x
posn-y
posn?
weak-posn?
    ← prev  up  next → 

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.

procedure

(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.

procedure

(on-redraw draw) → t

  draw : World -> image?
Registers a function to draw each frame of an animation.

procedure

(stop-when game-over) → t

  game-over : World -> boolean?
Registers a function to report when the animation has ended.

procedure

(on-tick-event tick) → t

  tick : World -> World

procedure

(on-tick-event/state tick) → t

  tick : World state -> (mv World state)
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.

procedure

(on-key-event press) → t

  press : World KeyEvent -> World

procedure

(on-key-event/state press) → t

  press : World KeyEvent State -> (mv World State)
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.

procedure

(on-mouse-event click) → t

  click : 
World integerp integerp MouseEvent ->
World

procedure

(on-mouse-event/state click) → t

  click : World integerp integerp MouseEvent State -> (mv World State)
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.

procedure

(empty-scene width height) → image?

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

procedure

(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.

procedure

(rectangle w h m c) → image?

  w : posp
  h : posp
  m : mode?
  c : image-color?

procedure

(circle r m c) → image?

  r : posp
  m : mode?
  c : image-color?

procedure

(triangle s m c) → image?

  s : posp
  m : mode?
  c : image-color?

procedure

(line x y c) → image?

  x : integerp
  y : integerp
  c : image-color?
These functions construct images of various geometric shapes.

procedure

(text str size color) → image?

  str : stringp
  size : posp
  color : image-color?
Constructs an image of text.

procedure

(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.

procedure

(overlay i ...) → image?

  i : image?

procedure

(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.

procedure

(image-width i) → posp

  i : image?

procedure

(image-height i) → posp

  i : image?
These functions compute the dimensions of an image.

procedure

(put-pinhole i x y) → image?

  i : image?
  x : integerp
  y : integerp

procedure

(move-pinhole i x y) → image?

  i : image?
  x : integerp
  y : integerp

procedure

(pinhole-x i) → integerp

  i : image?

procedure

(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.

procedure

(image? v) → booleanp

  v : t
Recognizes images.

2.9.4 Colors and Modes

procedure

(mode? v) → booleanp

  v : t
Recognizes image drawing modes: 'solid or 'outline.

procedure

(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.

procedure

(make-color r g b) → color?

  r : bytep
  g : bytep
  b : bytep

procedure

(color-red c) → bytep

  c : color?

procedure

(color-green c) → bytep

  c : color?

procedure

(color-blue c) → bytep

  c : color?

procedure

(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.

procedure

(bytep v) → booleanp

  v : t
Recognizes integers between 0 and 255, inclusive.

2.9.5 Posns

procedure

(make-posn x y) → posn?

  x : integerp
  y : integerp

procedure

(posn-x p) → integerp

  p : posn?

procedure

(posn-y p) → integerp

  p : posn?

procedure

(posn? v) → booleanp

  v : t

procedure

(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.

    ← prev  up  next →