STOBJ-EXAMPLE-1-DEFUNS

Major Section:  STOBJ

Consider the event shown in stobj-example-1:

(defstobj counters
  (NodeCnt     :type integer :initially 0)
  (TipCnt      :type integer :initially 0)
  (IntTipsSeen :type t       :initially nil))

Here is a complete list of the defuns added by the event.

The careful reader will note that the counters argument below is not declared with the :stobjs xarg even though we insist that the argument be a stobj in calls of these functions. This ``mystery'' is explained below.

(defun NodeCntp (x)                 ;;; Recognizer for 1st field
  (declare (xargs :guard t :verify-guards t))
  (integerp x))


(defun TipCntp (x)                  ;;; Recognizer for 2nd field
  (declare (xargs :guard t :verify-guards t))
  (integerp x))


(defun IntTipsSeenp (x)             ;;; Recognizer for 3rd field
  (declare (xargs :guard t :verify-guards t) (ignore x))
  t)


(defun countersp (counters)         ;;; Recognizer for object
  (declare (xargs :guard t :verify-guards t))
  (and (true-listp counters)
       (= (length counters) 3)
       (NodeCntp (nth 0 counters))
       (TipCntp (nth 1 counters))
       (IntTipsSeenp (nth 2 counters))
       t))


(defun create-counters ()           ;;; Creator for object
  (declare (xargs :guard t :verify-guards t))
  (list '0 '0 'nil))


(defun NodeCnt (counters)           ;;; Accessor for 1st field
  (declare (xargs :guard (countersp counters) :verify-guards t))
  (nth 0 counters))


(defun update-NodeCnt (v counters)  ;;; Updater for 1st field
  (declare (xargs :guard
                  (and (integerp v)
                       (countersp counters))
                  :verify-guards t))
  (update-nth 0 v counters))


(defun TipCnt (counters)            ;;; Accessor for 2nd field
  (declare (xargs :guard (countersp counters) :verify-guards t))
  (nth 1 counters))


(defun update-TipCnt (v counters)   ;;; Updater for 2nd field
  (declare (xargs :guard
                  (and (integerp v)
                       (countersp counters))
                  :verify-guards t))
  (update-nth 1 v counters))


(defun IntTipsSeen (counters)       ;;; Accessor for 3rd field
  (declare (xargs :guard (countersp counters) :verify-guards t))
  (nth 2 counters))


(defun update-IntTipsSeen (v counters) ;;; Updater for 3rd field
  (declare (xargs :guard (countersp counters) :verify-guards t))
  (update-nth 2 v counters))

Observe that there is a recognizer for each of the three fields and then a recognizer for the counters object itself. Then, for each field, there is an accessor and an updater.

Observe also that the functions are guarded so that they expect a countersp for their counters argument and an appropriate value for the new field values.

You can see all of the defuns added by a defstobj event by executing the event and then using the :pcb! command on the stobj name. E.g.,

ACL2 !>:pcb! counters

We now clear up the ``mystery'' mentioned above. Note, for example in TipCnt, that the formal counters is used. From the discussion in stobj-example-1 it has been made clear that TipCnt can only be called on the counters object. And yet, in that same discussion it was said that an argument is so treated only if it it declared among the :stobjs in the definition of the function. So why doesn't TipCnt include something like (declare (xargs :stobjs (counters)))?

The explanation of this mystery is as follows. At the time TipCnt was defined, during the introduction of the counters stobj, the name ``counters'' was not yet a single-threaded object. The introduction of a new single-threaded object occurs in three steps: (1) The new primitive recognizers, accessors, and updaters are introduced as ``ordinary functions,'' producing their logical axiomatizations. (2) The executable counterparts are defined in raw Lisp to support destructive updating. (3) The new name is declared a single-threaded object to ensure that all future use of these primitives respects the single-threadedness of the object. The functions defined as part of the introduction of a new single-threaded object are the only functions in the system that have undeclared stobj formals other than state.

You may return to stobj-example-1 here.