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.