ACL2::patbind-ret
b* binder for named return values from functions.
BETA. Interface may change.
ret is a very fancy b* binder that can be used to treat the return
values from a function as a single bundle which you can then access by their
names.
This feature is turned off by default. That is, by default
define does not add the necessary mechanism to allow the function it's
defining to be used by the ret patbinder; however, if it is enabled for a
given function, then the ret patbinder can be used for calls of that
function from anywhere. It can be enabled in two ways: by running
the (implicitly local) event
(make-define-config :ret-patbinder t)
which enables this feature for subsequent functions defined in the book, or
by adding the keyword argument :ret-patbinder t to a function's define
form.
Introductory Example
Here is a function, written with define, that returns two values.
(define mathstuff ((a natp)
(b natp))
:returns (mv (sum natp)
(prod natp))
:ret-patbinder t
(b* ((a (nfix a))
(b (nfix b)))
(mv (+ a b)
(* a b))))
Normally, to call this function from b*, you might use an mv
form like this:
(b* (((mv mysum myprod) (mathstuff 3 4))) ;; (:sum 7 :prod 12)
(list :sum mysum
:prod myprod))
Using the ret binder, you might instead write:
(b* (((ret mystuff) (mathstuff 3 4))) ;; (:sum 7 :prod 12)
(list :sum mystuff.sum
:prod mystuff.prod))
In other words, the ret binder lets you to treat all of the return
values for a function as if they were a single aggregate and then refer to the
individually returned values using a defaggregate- or C-like
foo.bar style syntax.
Mechanics
To a first approximation, the ret binder just expands into an
equivalent mv binder that sets up names like mystuff.sum and
mystuff.prod. However, there are (unfortunately) many subtleties that you
should be aware of.
Finding the function
To be able to know the names of the function's return values, the ret
binder obviously needs to "know" what function is being invoked.
It does this, completely barbarically, by just looking at the form on the
right hand side of the binder, even before any macro expansion. For instance,
if we write a binding form like this:
((ret myreturn) (myfn ...))
Then the ret binder will look at the right-hand side and sees that it
is a call of myfn.
Note that it is easy to write right-hand sides that ret does not
understand. For instance, if you just put a simple identity functions or
macro like time$ around your function call, e.g.,
((ret myreturn) (time$ (myfn ...)))
then the ret binder will not understand that you are calling myfn
and macroexpansion will fail. Similarly, you can't use let-bindings or
similar on the right-hand side.
Introducing the bindings
Once we know that the function being invoked is myfn, the ret
binder itself expands into a call of patbind-myfn-ret. Normally, this
should be a function that is introduced for you automatically at define
time.
Because the patbind function is constructed at define time, it
implicitly "knows" the names of the return values for your functions. It
also "knows" which of your function's return values are ACL2::stobjs
and how any such stobjs correspond to the arguments of your function.
Given all of this information, it is possible to construct a suitable mv binding that will bind:
- Each non-stobj return value to a new symbol with a dotted name like
myreturn.foo, myreturn.bar, or similar; and
- Each output stobj to the correct stobj name.
Aside from some technical details regarding congruent stobjs (see ACL2::stobj) this is almost straightforward. However, in purely logical
contexts such as theorem bodies and non-executable functions, it might be
desirable to ignore stobjs and name the stobj outputs just like all the rest.
You can use :ignore-stobjs t as an optional argument to the ret
binder, occurring after the name (if any), to get this behavior.
Ignorability
Consider our mathstuff example. We might imagine that a binding such
as:
((ret mystuff) (mathstuff 3 4))
would be expanded into:
((mv mystuff.sum mystuff.prod) (mathstuff 3 4))
This works fine if we use all of the return values, but if we (say) don't
need mystuff.prod, then we'd get errors unless we went out of our way to
use something like set-ignore-ok. To avoid this, the ret binders
will currently declare all return values as ignorable. We may eventually
revisit this decision and require some kind of more strict checking here.
Package Naming
What package does mystuff.sum belong in? The most obvious
candidate is to intern it into the package of the new variable, i.e.,
mystuff. Unfortunately this can sometimes be very confusing. For
instance, consider a code fragment like this:
(b* ((fn (get-function ...))
((ret args) (extend-args initial-args ...)))
(make-answer :fn fn
:args args.extensions
:size args.size
:warnings args.warnings))
The problem here is that args is a symbol in the *ACL2-exports*
list. So, if you submit the above code in a typical package, foo, where
you have imported the symbols from *acl2-exports*, then args is in
the acl2 package, but symbols like args.extensions, which are
presumably not imported, will instead be in the foo package.
To avoid this confusion, we scan the form for a symbol with the right name,
regardless of its package. This scan is done before macros are expanded, so it
may not work with macros that generate names like args.extensions.
