		Search-engine friendly clone of the ACL2 documentation.

Stobj

Stobj-example-2

An example of the use of arrays in single-threaded objects

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 (and fixnum (integer 0 *)) i))
  (the integer
       (aref (the (simple-array integer (*))
                  (svref ms 1))
             (the (and fixnum (integer 0 *)) i))))

(defun update-memi (i v ms)
  (declare (type (and fixnum (integer 0 *)) i)
           (type integer v))
  (progn
   (setf (aref (the (simple-array integer (*))
                    (svref ms 1))
               (the (and fixnum (integer 0 *)) i))
         (the integer v))
   ms))

If you want to see the raw Lisp supporting a defstobj, execute the defstobj and then evaluate the ACL2 form (nth 4 (global-val 'cltl-command (w state))).

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