Major Section: EVENTS

Note: Novices are advised to avoid `defstobj`

, perhaps instead using
community books `books/cutil/defaggregate.lisp`

or
`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)where

`name`

is a new symbol, each `fieldi`

is a symbol, each `typei`

is either a type-indicator (a `type-spec`

or stobj name) or of the
form `(ARRAY type-indicator max)`

, each `vali`

is an object satisfying
`typei`

, and each `bi`

is `t`

or `nil`

. Each pair
`:initially vali`

and `:resizable bi`

may be omitted; more on this below.
The `:renaming alist`

argument is optional and allows the user to override
the default function names introduced by this event. The `doc-string`

is
also optional. The `:inline flg`

Boolean argument is also optional and
declares to ACL2 that the generated access and update functions for the stobj
should be implemented as macros under the hood (which has the effect of
inlining the function calls). The optional `:congruent-to old-stobj-name`

argument specifies an existing stobj with exactly the same structure, and is
discussed below. We describe further restrictions on the `fieldi`

,
`typei`

, `vali`

, and on `alist`

below. We recommend that you read
about single-threaded objects (stobjs) in ACL2 before proceeding; see stobj.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-indicator (max))`

then `max`

is a
non-negative integer or a symbol introduced by `defconst`

) whose value is
a non-negative integer, and the corresponding element of the stobj is
initially of length specified by `max`

.

Whether the value `:type`

is of the form `(ARRAY type-indicator (max))`

or, otherwise, just `type-indicator`

, then `type-indicator`

is typically
a type-spec; see type-spec. However, `type-indicator`

can also be the
name of a stobj that was previously introduced (by `defstobj`

or
`defabsstobj`

). We ignore this ``nested stobj'' case below;
see nested-stobjs for a discussion of stobjs within stobjs.

The keyword value `:initially val`

specifies the initial value of a field,
except for the case of a `:type`

`(ARRAY type-indicator (max))`

, in which
case `val`

is the initial value of the corresponding array.

Note that 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)Note that the type and initial value are given in ``keyword argument'' format and may be given in either order. The

`typei`

and `vali`

``arguments''
are not evaluated. If omitted, the type defaults to `t`

(unrestricted) and
the initial value defaults to `nil`

.Each `typei`

must be either a `type-spec`

or else a list of the form
`(ARRAY type-spec (max))`

. (Again, we are ignoring the case of nested
stobjs, discussed elsewhere; see nested-stobjs.) 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))describes a field named

`days-off`

whose initial value is the list
consisting of the two symbols `SATURDAY`

and `SUNDAY`

. In particular,
the initial value is NOT obtained by applying the function `saturday`

to
the variable `sunday`

! Had we written
(days-off :initially '(saturday sunday))it would be equivalent to writing

(days-off :initially (quote (saturday sunday)))which would initialize the field to a list of length two, whose first element is the symbol

`quote`

and whose second element is a list containing the
symbols `saturday`

and `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)restricts the field to be a list of integers, initially of length 16, where each integer in the list is a

`(SIGNED-BYTE 31)`

. We sometimes call such a
list an ``array'' (because it is represented as an array in the underlying
Common Lisp). The elements of an array field are indexed by position,
starting at 0. Thus, the maximum legal index of an array field one less than
is specified by `max`

. Note that the value of `max`

must be less than
the Common Lisp constant `array-dimension-limit`

, and also (though this
presumably follows) less than the Common Lisp constant
`array-total-size-limit`

.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)

`name`

must be a new symbol, each `fieldi`

must be a symbol,
each `typei`

must be a `type-spec`

or `(ARRAY type-spec (max))`

,
and each `vali`

must be an object satisfying `typei`

.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))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. Initially, each of the three elements of the `A`

field is
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)))introduces the following 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 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 INote that even though the renaming alist substitutes ``

`XACCESSOR`

'' for
```X`

'' the updater for the `X`

field is still called ```UPDATE-X`

.''
That is because the renaming is applied to the default function names, not to
the field descriptors in the event.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)These constants are used for certain calls of

`nth`

and `update-nth`

that are displayed to the user in proof output. For example, for stobj
`st`

with accessor functions `a`

, `b`

, and `c`

, in that order, the
term `(nth '2 st)`

would be printed during a proof as `(nth *c* st)`

.
Also see term, in particular the discussion there of untranslated terms, and
see nth-aliases-table.*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)))

`defstobj`

event has been processed.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)))The following example shows an error that occurs when stobj arguments are repeated, i.e., at least two stobj arguments (in this case, three) get replaced by the same stobj.

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 !>