Another example of a single-threaded object

The event

(defstobj $s (x :type integer :initially 0) (a :type (array (integer 0 9) (3)) :initially 9 :resizable t))

introduces a stobj named

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

The initial value of stobj

Here is the definition of

(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

First, ignore the guard, since it is irrelevant in the logic. Reading from
the inside out, `nth` is 0-based.) The next
higher expression in the definition above,

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,

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

Now

So

'(1 (0 1 TWO))

because, logically speaking,

(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

(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

(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 :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
``

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

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.