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) (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
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 (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
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)) (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
to evaluate the
defstobj event and then evaluate, in the ACL2 loop, the
(nth 4 (global-val 'cltl-command (w state))). Those functions
(DECLARE (STOBJ-INLINE-FN T)) will generate
forms because the
:inline keyword of
defstobj was supplied the
t. The rest will generate
We now recommend that you look at stobj-example-1-proofs.