_Dracula Teachpacks / Books_

The Dracula ACL2-emulation language contains several teachpacks: ACL2 books
which provide content useful for classroom purposes.  Here are the supported
teachpacks:

(include-book "audio" :dir :teachpacks)
(include-book "avl-rational-keys" :dir :teachpacks)
(include-book "binary-io-utilities" :dir :teachpacks)
(include-book "doublecheck" :dir :teachpacks)
(include-book "io-utilities" :dir :teachpacks)
(include-book "list-utilities" :dir :teachpacks)
(include-book "rand" :dir :teachpacks)
(include-book "testing" :dir :teachpacks)
(include-book "world" :dir :teachpacks)

Documentation on each follows:

============================================================

> audio :: (include-book "audio" :dir :teachpacks)

This teachpack provides a single function:

> (play-wav file async) : Boolean
  file : String
  async : Boolean

Plays the named wav file either synchronously or asynchronously.

============================================================

> avl-rational-keys :: (include-book "avl-rational-keys" :dir :teachpacks)

Defines AVL trees (balanced binary search trees) with rational numbers as keys.
Documentation can be found in avl-rational-keys.lisp.

============================================================

> binary-io-utilities :: (include-book "binary-io-utilities" :dir :teachpacks)

This teachpack provides two functions.

> (binary-file->byte-list file state) : (mv Byte-List Error State)
  file : String
  state : State

This function reads the contents of a file as a list of bytes.

> (byte-list->binary-file file bytes state) : (mv Error State)
  file : String
  bytes : Byte-List
  state : State

This function writes a list of bytes to a file.

============================================================

> doublecheck :: (include-book "doublecheck" :dir :teachpacks)

This teachpack provides facilities for randomized testing of programs.  These
may be used as a prelude to theorem proving, or to diagnose a failed proof
attempt.  The primary forms in doublecheck are defproperty and check-properties:

> (defproperty name count ((var gen pred) ...) expr annotations ...)
  name :: Identifier
  gen  : Generator
  pred : Boolean
  expr : Boolean
  annotations: hints, etc.

> (check-properties)

This defines a property of the program to be tested.  The property has the given
name and random tests will run count repetitions.  The boolean expression expr
determines the property and each variable var is a random input.  The random
values chosen for each var are determined by the corresponding generator gen and
must satisfy the predicate pred.  Generators are constructed from special
functions determined below.

Dracula records each property, then tests each with random values when
check-properties is called.  It generates a report summarizing sucesses and
failures and listing detauls of each failure.

ACL2 treats defproperty as defthm, following this template:

(defthm name (implies (and pred ...) expr) annotations ...)

Note that the number count and the generators gen are ignored by ACL2.
Generators are not defined in ACL2 and cannot be executed in Dracula outside the
gen position in defproperty, as random number generation is not pure.  ACL2 also
ignores check-properties.

Example:

;; Test whether the result of nth is actually a member of the given list.
(defproperty nth-produces-a-member 100

  (;; Let lst be a list of between 1 and 10 symbols.
   (lst (random-list-of (random-symbol) (random-int-between 1 10))
        (symbol-listp lst))

   ;; Let idx be a valid index into lst.
   (idx (random-int-between 0 (1- (len lst)))
        (and (natp idx) (< idx (len lst)))))

  ;; Test whether (nth idx lst) is actually in lst.
  (member-equal (nth idx lst) lst))

#| In ACL2, this corresponds to the following theorem:
(defthm nth-produces-a-member
  (implies (and (symbol-listp lst)
                (natp idx)
                (< idx (len lst)))
           (member-equal (nth idx lst) lst)))
|#

DoubleCheck provides several generator functions, described below.  Any regular
ACL2 value may be supplied in place of a generator, representing a nonrandom
value.

> (random-int-between i j)

Generates integers between i and j, inclusive.

> (random-size)

Generates random, usually small, natural numbers, suitable for list sizes.

> (random-boolean)

Generates random booleans.

> (random-char)

Generates random characters.

> (random-string)

Generates random strings.

> (random-symbol)

Generates random symbols.

> (random-list-of elem-gen size-gen)

Generates random lists containing elements generated by elem-gen and of a length
generated by size-gen.

> (random-list gen ...)

Generates fixed length lists, each element of which is generated by the
corresponding gen.

> (random-apply f gen ...)

Generates the result of applying f to the value generated by each gen.

> (defgenerator name (arg ...) (weight gen) ...)

The defgenerator form allows definition of custom, potentially recursive
generators.  This form defines a function of the given name and arguments.  The
function produces a generator which chooses values from one of the internal
generators, chosen with the given weight.

Example:

;; Generate random sexpressions of pairs and symbols with the given max depth.
;; Chooses symbols over pairs with a weight of 4:1 (except at max depth).
(defgenerator random-tree (max-depth)
  (4 (random-symbol))
  ((if (posp max-depth) 1 0)
   (random-apply cons (random-tree (1- max-depth))
                      (random-tree (1- max-depth)))))

============================================================

> io-utilities :: (include-book "io-utilities" :dir :teachpacks)

This teachpack defines various utilities for input and output, mostly related to
text files or decimal representations of numbers.  Documentation can be found in
io-utilities.lisp.

============================================================

> list-utilities :: (include-book "list-utilities" :dir :teachpacks)

This teachpack defines various utilities for list processing.  Documentation can
be found in list-utilities.lisp.

============================================================

> rand :: (include-book "rand" :dir :teachpacks)

This teachpack defines pseudorandom number generation.

> (rand max seed)

Produces a number from 0 to (1- max) based on the seed value.

> (seedp seed)

Recognizes acceptable seed values.  Accepts all positive integers.

> (initial-seed)

Provides one possible initial seed for the pseudorandom number generator.

> (next-seed seed)

Produces a new seed from an old one; use this after each call to rand and store
the resulting seed for subsequent calls to ensure each pseudorandom number
differs from the last.  In practice, new seeds are capped at approximately
2^30, so the pseudorandom progression will not generate values higher than
that.

============================================================

> testing :: (include-book "testing" :dir :teachpacks)

This teachpack provides functions for checking concrete test cases.

> (check-expect actual expected)

This records a test that expects (equal actual expected) to be true.

> (check-within actual expected delta)

This records a test that expects actual and expected to be rational numbers
within the given delta of each other.

> (check-error expr message)

This records a test that expr evaluates to an error (in Dracula) with the given
message text.

> (generate-report)

In Dracula, this runs all tests previously recorded and opens a new window with
a report of all failures.  In ACL2, each check is interpreted as a theorem, and
generate-report is ignored.

============================================================

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

This teachpack defines functions for images and animations.  See documentation
on the world.ss and image.ss teachpacks in the student languages.  This
teachpack provides the following functions from them:

add-line
big-bang
circle
color-blue
color-green
color-red
color?
empty-scene
end-of-time
image-color?
image-height
image-width
make-color
make-posn
on-key-event
on-mouse-event
on-redraw
on-tick-event
overlay
overlay/xy
place-image
posn-x
posn-y
posn?
rectangle
text
weak-posn? ;; ACL2 only (not in student languages)