STOBJ-EXAMPLE-1.html -- ACL2 Version 6.1

STOBJ-EXAMPLE-1

an example of the use of single-threaded objects

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)  
NIL

and we can set the fields of counters as with:

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 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 must declare, at the top of the 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.

(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 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 then, if 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 then sweep the car of x and then sweep the 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.