Major Section: STOBJ
defun uses one of its formals as a single-threaded object
defun must include a declaration that the
formal is to be so used. An exception is the formal ``
if not declared as explained below, may still be used provided an
appropriate global ``declaration'' is issued:
If the formal in question is
counters then an appropriate declaration
(declare (xargs :stobjs counters))or, more generally,
(declare (xargs :stobjs (... counters ...)))where all the single-threaded formals are listed.
For such a declaration to be legal it must be the case that all the names
have previously been defined as single-threaded objects with
When an argument is declared to be single-threaded the guard of the function is augmented by conjoining to it the condition that the argument satisfy the recognizer for the single-threaded object. Furthermore, the syntactic checks done to enforce the legal use of single-threaded objects are also sufficient to allow these guard conjuncts to be automatically proved.
The obvious question arises: Why does ACL2 insist that you declare
stobj names before using them in
defuns if you can only declare names
that have already been defined with
defstobj? What would go wrong if
a formal were treated as a single-threaded object if and only if it had
already been so defined?
Suppose that one user, say Jones, creates a book in which
is defined as a single-threaded object. Suppose another user, Smith,
creates a book in which
counters is used as an ordinary formal
parameter. Finally, suppose a third user, Brown, wishes to use both
books. If Brown includes Jones' book first and then Smith's, then
Smith's function treats
counters as single-threaded. But if Brown
includes Smith's book first, the argument is treated as ordinary.
ACL2 insists on the declaration to ensure that the definition is processed the same way no matter what the context.