Major Section: STOBJ
(defstobj $s (x :type integer :initially 0) (a :type (array (integer 0 9) (3)) :initially 9 :resizable t))introduces a stobj named
$S. The stobj has two fields,
Afield is an array. The
Xfield contains an integer and is initially 0. The
Afield contains a list of integers, each between 0 and 9, inclusively. (Under the hood, this ``list'' is actually implemented as an array.) Initially, the
Afield has three elements, each of which is 9.
This event introduces the following sequence of function definitions:
(DEFUN XP (X) ...) ; recognizer for X field (DEFUN AP (X) ...) ; recognizer of A field (DEFUN $SP ($S) ...) ; top-level recognizer for stobj $S (DEFUN CREATE-$S NIL ...) ; creator for stobj $S (DEFUN X ($S) ...) ; accessor for X field (DEFUN UPDATE-X (V $S) ...) ; updater for X field (DEFUN A-LENGTH ($S) ...) ; length of A field (DEFUN RESIZE-A (K $S) ...) ; resizer for A field (DEFUN AI (I $S) ...) ; accessor for A field at index I (DEFUN UPDATE-AI (I V $S) ...) ; updater for A field at index I
Here is the definition of
(DEFUN $SP ($S) (DECLARE (XARGS :GUARD T :VERIFY-GUARDS T)) (AND (TRUE-LISTP $S) (= (LENGTH $S) 2) (XP (NTH 0 $S)) (AP (NTH 1 $S)) T))This reveals that in order to satisfy
$SPan object must be a true list of length 2 whose first element satisfies
XPand whose second satisfies
AP. By printing the definition of
APone learns that it requires its argument to be a true list, each element of which is an integer between 0 and 9.
The initial value of stobj
$S is given by zero-ary ``creator''
CREATE-$S. Creator functions may only be used in limited
contexts. See with-local-stobj.
Here is the definition of
UPDATE-AI, the updater for the
(DEFUN UPDATE-AI (I V $S) (DECLARE (XARGS :GUARD (AND ($SP $S) (INTEGERP I) (<= 0 I) (< I (A-LENGTH $S)) (AND (INTEGERP V) (<= 0 V) (<= V 9))) :VERIFY-GUARDS T)) (UPDATE-NTH-ARRAY 1 I V $S))By definition
(UPDATE-NTH-ARRAY 1 I V $S)is
(UPDATE-NTH 1 (UPDATE-NTH I V (NTH 1 $S)) $S). This may be a little surprising but should be perfectly clear.
First, ignore the guard, since it is irrelevant in the logic.
Reading from the inside out,
(UPDATE-AI I V $S) extracts
(NTH 1 $S),
which is array
$S. (Recall that
0-based.) The next higher expression in the definition above,
(UPDATE-NTH I V a), ``modifies''
a by setting its
V. Call this
a'. The next higher expression,
(UPDATE-NTH 1 a' $S), ``modifies''
$S by setting its 1st
a'. Call this result
the result returned by
So the first useful observation is that from the perspective of the logic, the type ``restrictions'' on stobjs are irrelevant. They are ``enforced'' by ACL2's guard mechanism, not by the definitions of the updater functions.
As one might also imagine, the accessor functions do not really
``care,'' logically, whether they are applied to well-formed stobjs
or not. For example,
(AI I $S) is defined to be
(NTH I (NTH 1 $S)).
Thus, you will not be able to prove that (AI 2 $S) is an integer. That is,
(integerp (AI 2 $S))is not a theorem, because
$Smay not be well-formed.
(integerp (AI 2 $S)) will always evaluate to
T in the
top-level ACL2 command loop, because we insist that the current value of
$S always satisfies
$SP by enforcing the guards on
the updaters, independent of whether guard checking is on or off;
see set-guard-checking. But in a theorem
$S is just
another variable, implicitly universally quantified.
(integerp (AI 2 $S)) is not a theorem because it is not true when
$S is instantiated with, say,
'(1 (0 1 TWO))because, logically speaking,
(AI 2 '(1 (0 1 TWO)))evaluates to the symbol
TWO. That is,
(equal (AI 2 '(1 (0 1 TWO))) 'TWO)is true.
(implies (and ($SP $S) (< 2 (A-LENGTH $S))) (integerp (AI 2 $S)))is a theorem. To prove it, you will have to prove a lemma about
AP. The following will do:
(defthm ap-nth (implies (and (AP x) (integerp i) (<= 0 i) (< i (len x))) (integerp (nth i x)))).
(implies (and (integerp i) (<= 0 i) (< i (A-LENGTH $S)) (integerp v) (<= 0 v) (<= v 9)) ($SP (UPDATE-AI i v $S)))is not a theorem until you add the additional hypothesis
($SP $S). To prove the resulting theorem, you will need a lemma such as the following.
(defthm ap-update-nth (implies (and (AP a) (integerp v) (<= 0 v) (<= v 9) (integerp i) (<= 0 i) (< i (len a))) (AP (update-nth i v a))))
The moral here is that from the logical perspective, you must provide the hypotheses that, as a programmer, you think are implicit on the structure of your stobjs, and you must prove their invariance. This is a good area for further support, perhaps in the form of a library of macros.
Resizing Array Fields
Recall the specification of the array field,
A for the stobj
(a :type (array (integer 0 9) (3)) :initially 9 :resizable t)Logically, this field is a list, initially of length 3. Under the hood, this field is implemented using a Common Lisp array with 3 elements. In some applications, one may wish to lengthen an array field, or even (to reclaim space) to shrink an array field. The
defstobjevent provides functions to access the current length of an array field and to change the array field, with default names obtained by suffixing the field name with ``
LENGTH-'' or prefixing it with ``
RESIZE-,'' respectively. The following log shows the uses of these fields in the above example.
ACL2 !>(A-LENGTH $S) 3 ACL2 !>(RESIZE-A 10 $S) ; change length of A to 10 <$s> ACL2 !>(A-LENGTH $S) 10 ACL2 !>(AI 7 $S) ; new elements get value from :initially 9 ACL2 !>(RESIZE-A 2 $S) ; truncate A down to first 2 elements <$s> ACL2 !>(A-LENGTH $S) 2 ACL2 !>(AI 7 $S) ; error: access past array boundHere are the definitions of the relevant functions for the above example; also see resize-list.
ACL2 Error in TOP-LEVEL: The guard for the function symbol AI, which is (AND ($SP $S) (INTEGERP I) (<= 0 I) (< I (A-LENGTH $S))), is violated by the arguments in the call (AI 7 $S).
(DEFUN A-LENGTH ($S) (DECLARE (XARGS :GUARD ($SP $S) :VERIFY-GUARDS T)) (LEN (NTH 1 $S)))
(DEFUN RESIZE-A (K $S) (DECLARE (XARGS :GUARD ($SP $S) :VERIFY-GUARDS T)) (UPDATE-NTH 1 (RESIZE-LIST (NTH 1 $S) K 9) $S))
It is important to note that the implementation of array resizing in ACL2 involves copying the entire array into a newly allocated space and thus can be quite costly if performed often. This approach was chosen in order to make array access and update as efficient as possible, with the suspicion that for most applications, array access and update are considerably more frequent than resizing (especially if the programmer is aware of the relative costs beforehand).
It should also be noted that computations of lengths of stobj array fields should be fast (constant-time) in all or most Common Lisp implementations.
:resizable t is not supplied as shown above, then
an attempt to resize the array will result in an error. If you do
not intend to resize the array, it is better to omit the
option (or to supply
:resizable nil), since then the length
function will be defined to return a constant, namely the initial
length, which can simplify guard proofs (compare with the definition
This completes the tour through the documentation of stobjs.
However, you may now wish to read the documentation for the event
that introduces a new single-threaded object; see defstobj.