STOBJ-EXAMPLE-1-IMPLEMENTATION.html -- ACL2 Version 3.1

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
       (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 defuns.

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