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.