`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 (aref (the (simple-array integer (1)) (svref counters 0)) 0)))Observe that 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)) (progn (setf (aref (the (simple-array integer (1)) (svref counters 0)) 0) (the integer v)) counters))Note that when this function is called, it does not create a new vector of length three, but ``smashes'' the existing one.

One way to see all the raw Lisp functions defined by a given `defstobj`

is
to evaluate the `defstobj`

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

. Those functions
that contain `(DECLARE (STOBJ-INLINE-FN T))`

will generate `defabbrev`

forms because the `:inline`

keyword of `defstobj`

was supplied the
value `t`

. The rest will generate `defun`

s.

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