Major Section: STOBJ
When a defun uses one of its formals as a single-threaded object
(stobj), the defun must include a declaration that the
formal it to be so used. An exception is the formal ``state,'' which
if not declared as explained below, may still be used provided an
appropriate global ``declaration'' is issued:
see set-state-ok.
If the formal in question is counters then an appropriate declaration
is
(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 defstobj.
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 counters
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.