B*
The b* macro is a replacement for let* that adds support
for multiple return values, mixing control flow with binding, causing side
effects, introducing type declarations, and doing other kinds of custom pattern
matching.
Introduction
To use b* you will need to load the following book:
(include-book "std/util/bstar" :dir :system)
In its most basic form, the b* macro is nearly a drop-in replacement
for let*. For instance, these are equivalent:
(let* ((x 1) (b* ((x 1)
(y 2) == (y 2)
(z (+ x y))) (z (+ x y)))
(list x y z)) (list x y z))
But beyond simple variable bindings, b* provides many useful, extended
b*-binders. A simple example is the mv
binder, which can nicely avoid switching between let* and mv-let. For instance:
(let* ((parts (get-parts args))) (b* ((parts (get-parts args))
(mv-let (good bad) == ((mv good bad) (split-parts parts))
(split-parts parts) (new-good (mark-good good))
(let* ((new-good (mark-good good)) (new-bad (mark-bad bad)))
(new-bad (mark-bad bad))) (append new-good new-bad))
(append new-good new-bad))))
Another example is the when
binder, which allows for a sort of "early exit" from the b* form
without needing to alternate between let* and if. For instance:
(let* ((sum (get-sum (car x)))) (b* ((sum (get-sum (car x)))
(if (< sum limit) == ((when (< sum limit))
ans ans)
(let* ((ans (+ ans sum)) (ans (+ ans sum))
(limit (+ limit 1))) (limit (+ limit 1)))
(fn (cdr x) ans limit)))) (fn (cdr x) ans limit))
The only part of the let* syntax that is not available in b* is
the declare syntax. However, ignore/ignorable declarations
are available using a different syntax (see below), and type-spec
declarations are available using the the
binder.
General Form
The general syntax of b* is:
(b* <list-of-bindings> . <list-of-result-forms>)
where a result form is any ACL2 term, and a binding is
(<binder-form> [<expression>])
Depending on the binder form, it may be that multiple expressions are
allowed or only a single one.
The std/util/bstar book comes with several useful b* binders already
defined, which we describe below. You can also define your own, custom binder
forms to extend the syntax of b* to provide additional kinds of pattern
matching or to implement common coding patterns. For example, the std::defaggregate macro automatically introduces new b* binders that let
you access the fields of structures using a C-like employee.name style
syntax.
Note: One difference between let* and b* is that b* allows
multiple forms to occur in the body, and returns the value of the last form.
For example:
(b* ((x 1)
(y 2)
(z (+ x y)))
(cw "Hello, ")
(cw " world!~%")
(list x y z))
Will print Hello, world! before returning (1 2 3), whereas putting
these cw statements into a let* form would be a syntax error.
Built-In B* Binders
Here is a nonsensical example that gives a flavor for the kind of b* binders
that are available "out of the box."
(b* ( ;; don't forget the first open paren! (like with let*)
;; 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"
;; Binding with type declaration:
((the (integer 0 100) n) (foo z))
;; MV which ignores a value:
((mv & a) (return-garbage-in-first-mv y z))
;; Binds value 0 to C and value 1 to D,
;; declares (ignorable C) and (ignore D)
((mv ?c ?!d) (another-mv a z))
;; Bind V to the middle value of an error triple,
;; quitting if there is an error condition (a la er-let*)
((er v) (trans-eval '(len (list 'a 1 2 3)) 'foo state))
;; The WHEN, IF, and UNLESS constructs insert an IF in the
;; binding stream. WHEN and IF are equivalent.
((when v) (finish-early-because-of v))
((if v) (finish-early-because-of v))
((unless c) (finish-early-unless c))
;; Pattern-based binding using cons, where D is ignorable
((cons (cons b c) ?d) (must-return-nested-conses a))
;; Patterns based on LIST and LIST* are also supported:
((list a b) '((1 2) (3 4)))
((list* a (the string b) c) '((1 2) "foo" 5 6 7))
;; Alternate form of pattern binding with cons nests, where G is
;; ignored and F has a type declaration:
(`(,e (,(the (signed-byte 8) 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))
) ;; also don't forget the close-paren after the binder list
;; the body (after the binder list) is an implicit PROGN$
(run-this-for-side-effects ...)
(return-this-expression .....))
Note: The built-in binders are all defined in the ACL2 package, and can be
used (without package prefix) in any other package that imports the binder
symbol, or with the acl2:: packge prefix anywhere. See also the note about
packages under user-defined binders below.
We now give some additional details about these built-in binders. Since
users can also define their own b* binders, you may wish to see b*-binders for a more comprehensive list of available binder forms.
- (mv a b ...)
- Produces an mv-let binding.
- (cons a b)
- Binds a and b to (car val) and (cdr val), respectively,
where val is the result of the corresponding expression.
- (er a)
- Produces an ER-LET* binding.
- (list a b ...)
- Binds a, b, ... to (car val), (cadr val), etc., where
val is the result of the corresponding expression.
- (nths a b ...)
- Binds a, b, ... to (nth 0 val), (nth 1 val), etc.,
where val is the result of the corresponding expression. This is very
much like list, but may be useful when nth is disabled.
- (list* a b)
`(,a . ,b)
- Alternatives to the cons binder.
- (the type-spec var)
- Binds var to the result of the corresponding expression, and adds
a declare form saying that var is of the given type-spec.
You can nest the patterns inside other patterns, but var must itself
be a symbol instead of a nested pattern, and type-spec must be a valid
type-spec.
- (if test)
(when test)
(unless test)
- These forms don't actually produce bindings at all. Instead, they insert
an if where one branch is the rest of the B* form and the other is
the "bound" expression. For example,
(b* (((if (atom a)) 0)
(rest (of-bindings)))
final-expr)
expands to something like this:
(if (atom a)
0
(b* ((rest (of-bindings)))
final-expr))
These forms can also create an "implicit progn" with multiple expressions,
like this:
(b* (((if (atom a))
(cw "a is an atom, returning 0")
0)
...)
...)
Note that the cons, list, list*, and backtick binders may be
nested arbitrarily inside other binders. User-defined binders may often be
arbitrarily nested. For example,
((mv (list `(,a . ,b)) (cons c d)) <form>)
will result in the following (logical) bindings:
Side Effects and Ignoring Variables
The following constructs may be used in place of variables
| - |
Dash (-), used as a top-level binding form, will run the corresponding
expressions (in an implicit progn) for side-effects without binding its value.
Used as a lower-level binding form, it will cause the binding to be ignored or
not created. |
| & |
Ampersand (&), used as a top-level binding form, will cause the
corresponding expression to be ignored and not run at all. Used as a
lower-level binding form, it will cause the binding to be ignored or not
created. |
| ?! |
Any symbol beginning with ?! works similarly to the & form. It
is declared ignored or not evaluated at all. |
| ? |
Any symbol beginning with ? but not ?! will make a binding of the symbol
obtained by removing the ?, and will make an ignorable declaration for this
variable. |
User-Defined Binders
B* expands to multiple nestings of another macro, PATBIND, analogously
to how LET* expands to multiple nestings of LET.
New b* binders may be created by defining a macro named PATBIND-<name>.
We discuss the detailed interface of user-defined binders below. But first,
note that def-patbind-macro provides a simple way to define certain user binders.
For example, this form is used to define the binder for CONS:
(def-patbind-macro cons (car cdr))
This defines a binder macro, patbind-cons, which enables (cons a
b) to be used as a binder form. This binder form must take two arguments
since two destructor functions, (car cdr), are given to
def-patbind-macro. The destructor functions are each applied to the form
to produce the bindings for the corresponding arguments of the binder.
There are many cases in which def-patbind-macro is not powerful enough.
For example, a binder produced by def-patbind-macro may only take a fixed
number of arguments. More flexible operations may be defined by hand-defining
the binder macro using the form def-b*-binder.
A binder macro, patbind-<name> must take three arguments: args,
forms, and rest-expr. The form
(b* (((foo arg1 arg2) binding1 binding2))
expr)
translates to a macro call
(patbind-foo (arg1 arg2) (binding1 binding2) expr)
That is:
- args is the list of arguments given to the binder form,
- bindings is the list of expressions bound to them, and
- expr is the result expression to be run once the bindings are in place.
The definition of the patbind-foo macro determines how this gets
further expanded. Some informative examples of these binder macros may be
found in std/util/bstar.lisp; simply search for uses of def-b*-binder.
Here are some further notes on defining binder macros.
Interaction with packages: The macro patbind-foo is derived from a use
of the foo binder using intern-in-package-of-symbol with foo as
the package witness. Practially speaking, this means that you can use a binder
from a different package (without any package prefix) if either the binder name
foo or the macro patbind-foo is imported into your package.
Additionally, if foo was defined as a binder in the bar package and
not imported into your current package, it can still be invoked as
bar::foo. Note also that when defining a binder using def-b*-binder,
the args, forms, and rest-expr formals are always in the ACL2
package.
Often the simplest way to accomplish the intended effect of a patbind macro
is to have it construct another b* form to be recursively expanded, or to
call other patbind macros. See, for example, the definition of
patbind-list.
Patbind macros for forms that are truly creating bindings should indeed use
b* (or patbind, which is what b* expands to) to create these
bindings, so that ignores and nestings are dealt with uniformly. See, for
example, the definition of patbind-nths.
In order to get good performance, destructuring binders such as are produced
by def-patbind-macro bind a variable to any binding that isn't already a
variable or quoted constant. This is important so that in the following form,
(foo x y) is run only once:
(b* (((cons a b) (foo x y))) ...)
In these cases, it is good discipline to check the new variables introduced
using the macro check-vars-not-free; since ACL2 does not have gensym, this
is the best option we have. See any definition produced by
def-patbind-macro for examples, and additionally patbind-nths,
patbind-er, and so forth.
Subtopics
- B*-binders
- List of the available directives usable in b*
- Def-b*-binder
- Introduce a new form usable inside b*.
