This directory holds miscellaneous books containing useful general-purpose macros.


bstar.lisp - Defines a macro B*, which operates similar to LET* but supports multiple values, sequential execution for side effects, and user-defined pattern-based binders. Here is an example that illustrates several of its features:

(b* ;; let*-like binding to a single variable:
    ((x (cons 'a 'b))
     ;; mv binding
     ((mv y z) (return-two-values x x))
     ;; No binding: expression evaluated for side effects
     (- (cw "Hello")) ;; prints "Hello"
     ;; Dont-care: expression not evaluated at all
     ;; (why do we want this? see below.)
     (& (cw "Hello")) ;; does not print "Hello"
     ;; MV which ignores a value:
     ((mv & a) (return-garbage-in-first-mv y z))
     ;; Pattern-based binding using cons:
     ((cons (cons b c) d) (must-return-nested-conses a))
     ;; Alternate form of pattern binding with cons nests:
     (`(,e (,f . ,g)) (makes-a-list-of-conses b))
     ;; Pattern with user-defined constructor:
     ((my-tuple foo bar hum) (something-of-type-my-tuple e c g))
     ;; Don't-cares with pattern bindings:
     ((my-tuple & (cons carbar &) hum) (something-else foo f hum))
     ;; Pattern inside an mv:
     ((mv a (cons & c)) (make-mv-with-cons)))
  (some-expression ....))
User-defined binders can be introduced using DEF-PATBIND-MACRO, as in the form
 (def-patbind-macro cons (car cdr))
which introduced the binder for cons, or by defining a macro named PATBIND-<NAME> following the example of the definitions of PATBIND-MV and PATBIND-LIST in bstar.lisp.
pack.lisp - Defines PACK, which takes a term-like object and makes a symbol that looks like it:
ACL2 !>(pack '(if a (foo b) (bar c d)))
|(IF A (FOO B) (BAR C D))|

progndollar.lisp - Defines PROGN$, which evaluates several forms and returns the value of the last one. Expands to a series of nested PROG2$s.
cws.lisp - Defines CWS, which prints the values of a series of forms and returns the value of the last one:
ACL2 !>(let ((x '(a b c)) (y '(d e f))) (cws x y))
X: (A B C)
Y: (D E F)
(D E F)

defsum.lisp - Defines DEFSUM, which introduces a sum-of-products datatype with recognizers, accessors, constructors, and theorems for reasoning about them without reference to the underlying cons structure. See also deftuple and pattern-match.
deftuple.lisp - Defines DEFTUPLE, similar DEFSUM (above), useful for defining product (tuple) datatypes.
pattern-match.lisp - Defines PATTERN-MATCH, which provides pattern-matching functionality similar to that present in ML, Haskell, and other such languages.