An example of the use of single-threaded objects

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

(defstobj counters (NodeCnt :type integer :initially 0) (TipCnt :type integer :initially 0) (IntTipsSeen :type t :initially nil))

It has three fields,

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''

ACL2 !>counters <counters>

Note that the value printed is ``

Had you tried to evaluate the ``global variable'' `state` feature of ACL2.

We can access the fields of

ACL2 !>(NodeCnt counters) 0 ACL2 !>(IntTipsSeen counters) NIL

and we can set the fields of

ACL2 !>(update-NodeCnt 3 counters) <counters> ACL2 !>(NodeCnt counters) 3

Observe that when we evaluate an expression that returns a counter object,
that object becomes the ``current value'' of

Here is a function that ``converts'' the

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

Observe that we *must* declare, at the top of the

When

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. (SHOW-COUNTERS COUNTERS) => *. The guard conjecture for SHOW-COUNTERS is trivial to prove. SHOW-COUNTERS is compliant with Common Lisp.

The line above containing the ``=>'' is called the ``signature'' of

(PROCESSOR * * COUNTERS) => (MV * COUNTERS)

which indicates that the function

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

Here is an example of

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

This is what we would see had we set the

We next wish to define a function to reset the

(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

However, the nest of

(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

(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 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

(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 *then*, if *then* sweep the *then* sweep the

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

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