Major Section: STOBJ
The event
(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, X and
A. The A field is an array. The X field contains an
integer and is initially 0. The A field contains a list of
integers, each between 0 and 9, inclusively. (Under the hood, this
``list'' is actually implemented as an array.) Initially, the A
field 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 $SP:
(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 $SP an object must be
a true list of length 2 whose first element satisfies XP and whose
second satisfies AP. By printing the definition of AP one
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''
function 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 A field
at index I:
(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 a of $S. (Recall that NTH is
0-based.) The next higher expression in the definition above,
(UPDATE-NTH I V a), ``modifies'' a by setting its Ith
element to V. Call this a'. The next higher expression,
(UPDATE-NTH 1 a' $S), ``modifies'' $S by setting its 1st
component to a'. Call this result $s'. Then $s' is
the result returned by UPDATE-AI.
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
$S may not be well-formed.Now (integerp (AI 2 $S)) will always evaluate to T in the
top-level ACL2 command loop, because we insist that the current value of
the stobj $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.
So (integerp (AI 2 $S)) is not a theorem because it is not true when
the variable $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.
However,
(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)))).
Similarly,
(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 $S
introduced above:
(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
defstobj event 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 bound 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). ACL2 !>Here are the definitions of the relevant functions for the above example; also see resize-list.
(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.
Finally, if :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 :resizable
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
of A-LENGTH above).
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.
