Major Section: STOBJ
(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)and the value is stored in the Common Lisp global variable named
(vector (make-array 1 :element-type 'integer :initial-element '0) (make-array 1 :element-type 'integer :initial-element '0) 'nil)
counters object is an array of length three. The first
two elements are arrays of size 1 and are used to hold the
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.
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
NodeCntis 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
arefto access the 0th element of that array.
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
countersit 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
defstobj event and then evaluate, in the ACL2 loop,
(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.