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
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))|
PROGN$, which evaluates several forms and returns the value of the last one. Expands to a series of nested
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, 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.
DEFSUM(above), useful for defining product (tuple) datatypes.
PATTERN-MATCH, which provides pattern-matching functionality similar to that present in ML, Haskell, and other such languages.