## STOBJ-EXAMPLE-1-IMPLEMENTATION

the implementation of the `counters`

stobj
Major Section: STOBJ

the event

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

discussed in stobj-example-1, creates a Common Lisp object to
represent the current value of `counters`

. That object is created
by evaluating either of the following ``raw'' (non-ACL2) Common Lisp
forms:
(create-counters)
(vector (make-array 1 :element-type 'integer
:initial-element '0)
(make-array 1 :element-type 'integer
:initial-element '0)
'nil)

and the value is stored in the Common Lisp global variable named
`*the-live-counters*`

.
Thus, the `counters`

object is an array of length three. The first
two elements are arrays of size 1 and are used to hold the
`NodeCnt`

and `TipCnt`

fields. The third element is the
`IntTipsSeen`

field. The first two fields are represented by
arrays so that we can implement the `integer`

type specification
efficiently. Generally, integers are ``boxed'' in some Common Lisp
implementations, for example, GCL. Creating a new integer requires
creating a new box to put it in. But in some lisps, including GCL,
the integers inside arrays of integers are not boxed.

The function `NodeCnt`

is defined in raw Lisp as:

(defun NodeCnt (counters)
(the integer
(cond ((the-live-stobjp counters)
(aref (the (simple-array integer (1))
(svref counters 0))
0))
(t (nth 0 counters)))))

Observe that if `NodeCnt`

is called on ``the live `counters`

''
then the form `(svref counters 0)`

is evaluated to get an array of
size 1, which is followed by a call of `aref`

to access the 0th
element of that array.
The function `update-NodeCnt`

is defined in raw Lisp as:

(defun update-NodeCnt (v counters)
(declare (type integer v))
(cond ((the-live-stobjp counters)
(cond (*wormholep* (wormhole-er 'update-nodecnt
(list v counters)))
(t (setf (aref (the (simple-array integer (1))
(svref counters 0))
0)
(the integer v))
counters)))
(t (update-nth 0 v counters))))

Note that when this function is called on the live `counters`

it
does not create a new vector of length three, but ``smashes'' the
existing one.
One way to see all the functions defined by a given `defstobj`

is to
evaluate the `defstobj`

event and then evaluate, in the ACL2 loop,
the expression `(global-val 'cltl-command (w state))`

. That will
print a lisp object that you can probably figure out.

We now recommend that you look at stobj-example-1-proofs.