STOBJ-EXAMPLE-2

an example of the use of arrays in single-threaded objects
Major Section:  STOBJ

The following event

(defstobj ms
  (pcn  :type integer                  :initially 0)
  (mem  :type (array integer (100000)) :initially -1)
  (code :type t                        :initially nil))
introduces a single-threaded object named ms (which stands for ``machine state''). The object has three fields, a pcn or program counter, a mem or memory, and a code field.

The mem field is occupied by an object initially of type (array integer (100000)). Logically speaking, this is a list of length 100000, each element of which is an integer. But in the underlying implementation of the ms object, this field is occupied by a raw Lisp array, initially of size 100000.

You might expect the above defstobj to define the accessor function mem and the updater update-mem. That does not happen!.

The above event defines the accessor function memi and the updater update-memi. These functions do not access/update the mem field of the ms object; they access/update the individual elements of the array in that field.

In particular, the logical definitions of the two functions are:

(defun memi (i ms)
  (declare (xargs :guard
                  (and (msp ms)
                       (integerp i)
                       (<= 0 i)
                       (< i (mem-length ms)))))
  (nth i (nth 1 ms)))

(defun update-memi (i v ms) (declare (xargs :guard (and (msp ms) (integerp i) (<= 0 i) (< i (mem-length ms)) (integerp v)))) (update-nth-array 1 i v ms))

For example, to access the 511th (0-based) memory location of the current ms you could evaluate:

ACL2 !>(memi 511 ms)
-1
The answer is -1 initially, because that is the above-specified initial value of the elements of the mem array.

To set that element you could do

ACL2 !>(update-memi 511 777 ms)
<ms>
ACL2 !>(memi 511 ms)
777

The raw Lisp implementing these two functions is shown below.

(defun memi (i ms)
  (declare (type (integer 0 268435455) i))
  (the integer
       (cond ((the-live-stobjp ms)
              (aref (the (simple-array integer (*))
                         (svref ms 1))
                    (the (integer 0 268435455) i)))
             (t (nth i (nth 1 ms))))))

(defun update-memi (i v ms) (declare (type (integer 0 268435455) i) (type integer v)) (cond ((the-live-stobjp ms) (cond (*wormholep* (wormhole-er 'update-memi (list i v ms))) (t (setf (aref (the (simple-array integer (*)) (svref ms 1)) (the (integer 0 268435455) i)) (the integer v)) ms))) (t (update-nth-array 1 i v ms))))

If you want to see the raw Lisp supporting a defstobj, execute the defstobj and then evaluate the ACL2 form (global-val 'cltl-command (w state)). The s-expression printed will probably be self-explanatory given the examples here.

To continue the stobj tour, see stobj-example-3.