DEFSTOBJ

Major Section:  EVENTS

Note: Novices are advised to avoid defstobj, perhaps instead using community book books/data-structures/structures.lisp. At the least, consider using (set-verify-guards-eagerness 0) to avoid guard verification. On the other hand, after you learn to use defstobj, see defabsstobj for another way to introduce single-threaded objects.

Example:
(defconst *mem-size* 10) ; for use of *mem-size* just below
(defstobj st
          (reg :type (array (unsigned-byte 31) (8))
               :initially 0)
          (p-c :type (unsigned-byte 31)
               :initially 555)
          halt                  ; = (halt :type t :initially nil)
          (mem :type (array (unsigned-byte 31) (*mem-size*))
               :initially 0 :resizable t))

General Form:
(defstobj name
          (field1 :type type1 :initially val1 :resizable b1)
          ...
          (fieldk :type typek :initially valk :resizable bk)
          :renaming alist
          :doc doc-string
          :inline flg
          :congruent-to old-stobj-name)

The effect of this event is to introduce a new single-threaded object (i.e., a ``stobj''), named name, and the associated recognizers, creator, accessors, updaters, constants, and, for fields of ARRAY type, length and resize functions.

The Single-Threaded Object Introduced

The defstobj event effectively introduces a new global variable, named name, which has as its initial logical value a list of k elements, where k is the number of ``field descriptors'' provided. The elements are listed in the same order in which the field descriptors appear. If the :type of a field is (ARRAY type-spec (max)) then max is a non-negative integer or a constant (see defconst) whose value is a non-negative integer, and the corresponding element of the stobj is initially of length specified by max containing the value, val, specified by :initially val. Otherwise, the :type of the field is a type-spec and the corresponding element of the stobj is the specified initial value val. (The actual representation of the stobj in the underlying Lisp may be quite different; see stobj-example-2. For the moment we focus entirely on the logical aspects of the object.)

In addition, the defstobj event introduces functions for recognizing and creating the stobj and for recognizing, accessing, and updating its fields. For fields of ARRAY type, length and resize functions are also introduced. Constants are introduced that correspond to the accessor functions.

Restrictions on the Field Descriptions in Defstobj

Each field descriptor is of the form:

(fieldi :TYPE typei :INITIALLY vali)

Each typei must be either a type-spec or else a list of the form (ARRAY type-spec (max)). The latter forms are said to be ``array types.'' Examples of legal typei are:

(INTEGER 0 31)
(SIGNED-BYTE 31)
(ARRAY (SIGNED-BYTE 31) (16))
(ARRAY (SIGNED-BYTE 31) (*c*)) ; where *c* has a non-negative integer value

The typei describes the objects which are expected to occupy the given field. Those objects in fieldi should satisfy typei. We are more precise below about what we mean by ``expected.'' We first present the restrictions on typei and vali.

Non-Array Types

When typei is a type-spec it restricts the contents, x, of fieldi according to the ``meaning'' formula given in the table for type-spec. For example, the first typei above restricts the field to be an integer between 0 and 31, inclusive. The second restricts the field to be an integer between -2^30 and (2^30)-1, inclusive.

The initial value, vali, of a field description may be any ACL2 object but must satisfy typei. Note that vali is not a form to be evaluated but an object. A form that evaluates to vali could be written 'vali, but defstobj does not expect you to write the quote mark. For example, the field description

(days-off :initially (saturday sunday))

(days-off :initially '(saturday sunday))

(days-off :initially (quote (saturday sunday)))

Array Types

When typei is of the form (ARRAY type-spec (max)), the field is supposed to be a list of items, initially of length specified by max, each of which satisfies the indicated type-spec. Max must be a non-negative integer or a defined constant evaluating to a non-negative integer. Thus, each of

(ARRAY (SIGNED-BYTE 31) (16))
(ARRAY (SIGNED-BYTE 31) (*c*)) ; given previous event (defconst *c* 16)

Note also that the ARRAY type requires that the max be enclosed in parentheses. This makes ACL2's notation consistent with the Common Lisp convention of describing the (multi-)dimensionality of arrays. But ACL2 currently supports only single dimensional arrays in stobjs.

For array fields, the initial value vali must be an object satisfying the type-spec of the ARRAY description. The initial value of the field is a list of max repetitions of vali.

Array fields can be ``resized,'' that is, their lengths can be changed, if :resizable t is supplied as shown in the example and General Form above. The new length must satisfy the same restriction as does max, as described above. Each array field in a defstobj event gives rise to a length function, which gives the length of the field, and a resize function, which modifies the length of the field if :resizable t was supplied with the field when the defstobj was introduced and otherwise causes an error. If :resizable t was supplied and the resize function specifies a new length k, then: if k is less than the existing array length, the array is shortened simply by dropping elements with index at least k; otherwise, the array is extended to length k by mapping the new indices to the initial value (supplied by :initially, else default nil).

Array resizing is relatively slow, so we recommend using it somewhat sparingly.

The Default Function Names

To recap, in

(defstobj name
          (field1 :type type1 :initially val1)
          ...
          (fieldk :type typek :initially valk)
          :renaming alist
          :doc doc-string
          :inline inline-flag)

Roughly speaking, for each fieldi, a defstobj introduces a recognizer function, an accessor function, and an updater function. The accessor function, for example, takes the stobj and returns the indicated component; the updater takes a new component value and the stobj and return a new stobj with the component replaced by the new value. But that summary is inaccurate for array fields.

The accessor function for an array field does not take the stobj and return the indicated component array, which is a list of length specified by max. Instead, it takes an additional index argument and returns the indicated element of the array component. Similarly, the updater function for an array field takes an index, a new value, and the stobj, and returns a new stobj with the indicated element replaced by the new value.

These functions -- the recognizer, accessor, and updater, and also length and resize functions in the case of array fields -- have ``default names.'' The default names depend on the field name, fieldi, and on whether the field is an array field or not. For clarity, suppose fieldi is named c. The default names are shown below in calls, which also indicate the arities of the functions. In the expressions, we use x as the object to be recognized by field recognizers, i as an array index, v as the ``new value'' to be installed by an updater, and name as the single-threaded object.

                 non-array field        array field
recognizer         (cP x)                (cP x)
accessor           (c name)              (cI i name)
updater            (UPDATE-c v name)     (UPDATE-cI i v name)
length                                   (c-LENGTH name)
resize                                   (RESIZE-c k name)

Finally, a recognizer and a creator for the entire single-threaded object are introduced. The creator returns the initial stobj, but may only be used in limited contexts; see with-local-stobj. If the single-threaded object is named name, then the default names and arities are as shown below.

top recognizer     (nameP x)
creator            (CREATE-name)

For example, the event

(DEFSTOBJ $S
  (X :TYPE INTEGER :INITIALLY 0)
  (A :TYPE (ARRAY (INTEGER 0 9) (3)) :INITIALLY 9))

This event introduces the following sequence of 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 () ...)         ; 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

Avoiding the Default Function Names

If you do not like the default names listed above you may use the optional :renaming alist to substitute names of your own choosing. Each element of alist should be of the form (fn1 fn2), where fn1 is a default name and fn2 is your choice for that name.

For example

(DEFSTOBJ $S
  (X :TYPE INTEGER :INITIALLY 0)
  (A :TYPE (ARRAY (INTEGER 0 9) (3)) :INITIALLY 9)
  :renaming ((X XACCESSOR) (CREATE-$S MAKE$S)))

(DEFUN XP (X) ...)               ; recognizer for X field
(DEFUN AP (X) ...)               ; recognizer of A field
(DEFUN $SP ($S) ...)             ; top-level recognizer for stobj $S
(DEFUN MAKE$S () ...)            ; creator for stobj $S
(DEFUN XACCESSOR ($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

Use of the :renaming alist may be necessary to avoid name clashes between the default names and and pre-existing function symbols.

Constants

Defstobj events also introduce constant definitions (see defconst). One constant is introduced for each accessor function by prefixing and suffixing a `*' character on the function name. The value of that constant is the position of the field being accessed. For example, if the accessor functions are a, b, and c, in that order, then the following constant definitions are introduced.

(defconst *a* 0)
(defconst *b* 1)
(defconst *c* 2)

Inspecting the Effects of a Defstobj

Because the stobj functions are introduced as ``sub-events'' of the defstobj the history commands :pe and :pc will not print the definitions of these functions but will print the superior defstobj event. To see the definitions of these functions use the history command :pcb!.

To see an s-expression containing the definitions what constitute the raw Lisp implementation of the event, evaluate the form

(nth 4 (global-val 'cltl-command (w state)))

A defstobj is considered redundant only if the name, field descriptors, renaming alist, and inline flag are identical to a previously executed defstobj. Note that a redundant defstobj does not reset the stobj fields to their initial values.

Inlining and Performance

The :inline keyword argument controls whether or not accessor, updater, and length functions are inlined (as macros under the hood, in raw Lisp). If :inline t is provided then these are inlined; otherwise they are not. The advantage of inlining is potentially better performance; there have been contrived examples, doing essentially nothing except accessing and updating array fields, where inlining reduced the time by a factor of 10 or more; and inlining has sped up realistic examples by a factor of at least 2. Inlining may get within a factor of 2 of C execution times for such contrived examples, and within a few percent of C execution times on realistic examples.

A drawback to inlining is that redefinition may not work as expected, much as redefinition may not work as expected for macros: defined functions that call a macro, or inlined stobj function, will not see a subsequent redefinition of the macro or inlined function. Another drawback to inlining is that because inlined functions are implemented as macros in raw Lisp, tracing (see trace$) will not show their calls. These drawbacks are avoided by default, but the user who is not concerned about them is advised to specify :inline t.

Specifying Congruent Stobjs

Two stobjs are may be considered to be ``congruent'' if they have the same structure, that is, their defstobj events are identical when ignoring field names. In particular, every stobj is congruent to itself. In order to tell ACL2 that a new stobj st2 is indeed to be considered as congruent to an existing stobj st1, the defstobj event introducing st2 is given the keyword argument :congruent-to st1. Congruence is an equivalence relation: when you specify a new stobj to be congruent to an old one, you are also specifying that the new stobj is congruent to all other stobjs that are congruent to the old one. Thus, continuing the example above, if you specify that st3 is :congruent-to st2, then st1, st2, and st3 will all be congruent to each other.

When two stobjs are congruent, ACL2 allows you to substitute one for another in a function call. Any number of stobjs may be replaced with congruent stobjs in the call, provided no two get replaced with the same stobj. The return values are correspondingly modified: if stobj st1 is replaced by st2 at an argument position, and if st1 is returned in the output signature of the function, then st2 is returned in place of st1.

The following example illustrates congruent stobjs. For more examples of how to take advantage of congruent stobjs, and also of how to misuse them, see community book books/misc/congruent-stobjs-test.lisp.

(defstobj st1 fld1)
(defstobj st2 fld2 :congruent-to st1)
(defstobj st3 fld3 :congruent-to st2) ; equivalently, :congruent-to st1
(defun f (st1 st2 st3)
  (declare (xargs :stobjs (st1 st2 st3)))
  (list (fld2 st1) (fld3 st2) (fld1 st3)))
(update-fld1 1 st1)
(update-fld1 2 st2) ; notice use of update-fld1 on st2
(update-fld1 3 st3) ; notice use of update-fld1 on st3
(assert-event (equal (f st3 st2 st1) '(3 2 1)))

ACL2 !>(f st1 st1 st1)


ACL2 Error in TOP-LEVEL:  The form ST1 is being used, as an argument
to a call of F, where the single-threaded object ST2 was expected,
even though these are congruent stobjs.  See :DOC defstobj, in particular
the discussion of congruent stobjs.  Note:  this error occurred in
the context (F ST1 ST1 ST1).

ACL2 !>