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
pcnor program counter, a
memor memory, and a
mem field is occupied by an object initially of type
(array integer (100000)). Logically speaking, this is a list of
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
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
ms you could evaluate:
ACL2 !>(memi 511 ms) -1The answer is
-1initially, because that is the above-specified initial value of the elements of the
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 (aref (the (simple-array integer (*)) (svref ms 1)) (the (integer 0 268435455) i))))
(defun update-memi (i v ms) (declare (type (integer 0 268435455) i) (type integer v)) (progn (setf (aref (the (simple-array integer (*)) (svref ms 1)) (the (integer 0 268435455) 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
(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.