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,
IntTipsSeen. (As always in ACL2, capitalization is irrelevant in simple symbol names, so the first name could be written
NODECNT, etc.) Those are the name of the accessor functions for the object. The corresponding update functions are named
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
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
countersin 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''
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
objects are a straightforward generalization of the long-implemented
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
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
Here is a function that ``converts'' the
counters object to its
(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
countersas a single-threaded object! If we did not make this declaration, the body of
show-counterswould be processed as though
counterswere 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.
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
countersand 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
COUNTERSstobj, and returns two results, the second of which is the modified
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
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
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
NodeCntfield of the initial value of
3, as we did earlier in this example.
We next wish to define a function to reset the
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
0, then the
0, and then the
niland 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
seqis 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 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
(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
xis an atom, then increment the
countersand then, if
xis an integer, add
IntTipsSeenfield, and return
counters. On the other hand, if
xis not an atom, then increment the
counters, and then sweep the
xand then sweep the
xand 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)
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
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.