Stobj-example-1-implementation
The implementation of the counters 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.
