Major Section: STOBJ

Suppose we want to sweep a tree and (1) count the number of interior nodes, (2) count the number of tips and (3) keep a record of every tip we encounter that is an integer. We could use a single-threaded object as our ``accumulator''. Such an object would have three fields, one holding the number of nodes seen so far, one holding the number of tips, and one holding all the integer tips seen.

The following event declares `counters`

to be a single-threaded object.

(defstobj counters (NodeCnt :type integer :initially 0) (TipCnt :type integer :initially 0) (IntTipsSeen :type t :initially nil))It has three fields,

`NodeCnt`

, `TipCnt`

, and `IntTipsSeen`

.
(As always in ACL2, capitalization is irrelevant in simple symbol
names, so the first name could be written `nodecnt`

or
`NODECNT`

, etc.) Those are the name of the accessor functions for
the object. The corresponding update functions are named
`update-NodeCnt`

, `update-TipCnt`

and `update-IntTipsSeen`

.
If you do not like the default function names chosen above, there is
a feature in the `defstobj`

event that allows you to specify other
names.

If you want to see the ACL2 definitions of all the functions defined by this event, look at stobj-example-1-defuns.

If, after this event, we evaluate the top-level ``global variable''
`counters`

in the ACL2 read-eval-print loop we get:

ACL2 !>counters <counters>Note that the value printed is ``

`<counters>`

''. Actually, the
value of `counters`

in the logic is `(0 0 NIL)`

. But ACL2 always prints
single-threaded objects in this non-informative way because they are
usually so big that to do otherwise would be unpleasant.
Had you tried to evaluate the ``global variable'' `counters`

before
declaring it a single-threaded object, ACL2 would have complained that
it does not support global variables. So a lesson here is that
once you have declared a new single-threaded object your top-level
forms can reference it. In versions of ACL2 prior to Version 2.4
the only variable enjoying this status was `STATE`

. single-threaded
objects are a straightforward generalization of the long-implemented
von Neumann `state`

feature of ACL2.

We can access the fields of `counters`

as with:

ACL2 !>(NodeCnt counters) 0 ACL2 !>(IntTipsSeen counters) NILand we can set the fields of

`counters`

as with:
ACL2 !>(update-NodeCnt 3 counters) <counters> ACL2 !>(NodeCnt counters) 3Observe that when we evaluate an expression that returns a counter object, that object becomes the ``current value'' of

`counters`

.
Here is a function that ``converts'' the `counters`

object to its
``ordinary'' representation:

(defun show-counters (counters) (declare (xargs :stobjs (counters))) (list (NodeCnt counters) (TipCnt counters) (IntTipsSeen counters)))Observe that we

`defun`

, that
we mean to use the formal parameter `counters`

as a single-threaded
object! If we did not make this declaration, the body of
`show-counters`

would be processed as though `counters`

were an
ordinary object. An error would be caused because the accessors
used above cannot be applied to anything but the single-threaded
object `counters`

. If you want to know why we insist on this
declaration, see declare-stobjs.
When `show-counters`

is admitted, the following message is printed:

Since SHOW-COUNTERS is non-recursive, its admission is trivial. We observe that the type of SHOW-COUNTERS is described by the theorem (AND (CONSP (SHOW-COUNTERS COUNTERS)) (TRUE-LISTP (SHOW-COUNTERS COUNTERS))). We used primitive type reasoning.The line above containing the ``=>'' is called the ``signature'' of(SHOW-COUNTERS COUNTERS) => *.

The guard conjecture for SHOW-COUNTERS is trivial to prove. SHOW-COUNTERS is compliant with Common Lisp.

`show-counters`

; it conveys the information that the first argument
is the single-threaded object `counters`

and the only result is an
ordinary object. Here is an example of another signature:
(PROCESSOR * * COUNTERS) => (MV * COUNTERS)which indicates that the function

`PROCESSOR`

(which we haven't
shown you) takes three arguments, the third of which is the
`COUNTERS`

stobj, and returns two results, the second of which
is the modified `COUNTERS`

.
Returning to the admission of `show-counters`

above, the last
sentence printed indicates that the `guard`

conjectures for the
function were proved. When some argument of a function is declared
to be a single-threaded object via the `xargs`

`:stobj`

, we
automatically add (conjoin) to the guard the condition that the
argument satisfy the recognizer for that single-threaded object. In
the case of `show-counters`

the guard is `(countersp counters)`

.

Here is an example of `show-counters`

being called:

ACL2 !>(show-counters counters) (3 0 NIL)This is what we would see had we set the

`NodeCnt`

field of the
initial value of `counters`

to `3`

, as we did earlier in this
example.
We next wish to define a function to reset the `counters`

object.
We could define it this way:

(defun reset-counters (counters) (declare (xargs :stobjs (counters))) (let ((counters (update-NodeCnt 0 counters))) (let ((counters (update-TipCnt 0 counters))) (update-IntTipsSeen nil counters))))which ``successively'' sets the

`NodeCnt`

field to `0`

, then the
`TipCnt`

field to `0`

, and then the `IntTipsSeen`

field to `nil`

and
returns the resulting object.
However, the nest of `let`

expressions is tedious and we use this
definition instead. This definition exploits a macro, here named
```seq`

'' (for ``sequentially'') which evaluates each of the forms
given, binding their results successively to the stobj name given.

(defun reset-counters (counters) (declare (xargs :stobjs (counters))) (seq counters (update-NodeCnt 0 counters) (update-TipCnt 0 counters) (update-IntTipsSeen nil counters)))This definition is syntactically identical to the one above, after macro expansion. Our definition of

`seq`

is shown below and is not part of
native ACL2.
(defmacro seq (stobj &rest rst) (cond ((endp rst) stobj) ((endp (cdr rst)) (car rst)) (t `(let ((,stobj ,(car rst))) (seq ,stobj ,@(cdr rst))))))

The signature printed for `reset-counters`

is

(RESET-COUNTERS COUNTERS) => COUNTERS.

Here is an example.

ACL2 !>(show-counters counters) (3 0 NIL) ACL2 !>(reset-counters counters) <counters> ACL2 !>(show-counters counters) (0 0 NIL)

Here finally is a function that uses `counters`

as a single-threaded
accumulator to collect the desired information about the tree `x`

.

(defun sweep-tree (x counters) (declare (xargs :stobjs (counters))) (cond ((atom x) (seq counters (update-TipCnt (+ 1 (TipCnt counters)) counters) (if (integerp x) (update-IntTipsSeen (cons x (IntTipsSeen counters)) counters) counters))) (t (seq counters (update-NodeCnt (+ 1 (NodeCnt counters)) counters) (sweep-tree (car x) counters) (sweep-tree (cdr x) counters)))))We can paraphrase this definition as follows. If

`x`

is an atom,
then increment the `TipCnt`

field of `counters`

and `x`

is an integer, add `x`

to the `IntTipsSeen`

field, and
return `counters`

. On the other hand, if `x`

is not
an atom, then increment the `NodeCnt`

field of `counters`

, and
`car`

of `x`

and `cdr`

of `x`

and return the result.Here is an example of its execution. We have displayed the input tree in full dot notation so that the number of interior nodes is just the number of dots.

ACL2 !>(sweep-tree '((((a . 1) . (2 . b)) . 3) . (4 . (5 . d))) counters) <counters> ACL2 !>(show-counters counters) (7 8 (5 4 3 2 1)) ACL2 !>(reset-counters counters) <counters> ACL2 !>(show-counters counters) (0 0 NIL)

The `counters`

object has two integer fields and a field whose
type is unrestricted. single-threaded objects support other types of
fields, such as arrays. We deal with that in the stobj-example-2.
But we recommend that you first consider the implementation issues for
the `counters`

example (in stobj-example-1-implementation) and
then consider the proof issues (in stobj-example-1-proofs).

To continue the stobj tour, see stobj-example-2.