Defstobj
Define a new single-threaded object
Note: Novices are advised to avoid defstobj, perhaps instead
using community books std::defaggregate 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)
(ht :type (hash-table eq 70 integer) :initially 0))
General Form:
(defstobj name
(field1 :type type1
:element-type etype1
:initially val1
:resizable b1)
...
(fieldk :type typek
:element-type etypek
:initially valk
:resizable bk)
:renaming doublets
:inline flg
:congruent-to old-stobj-name
:non-memoizable nm-flg
:non-executable ne-flg)
where name is a new symbol; each fieldi is a symbol; each
typei is either a type-indicator (a type-spec or stobj
name), of the form (ARRAY type-indicator (max)), or of one of the forms
(HASH-TABLE test), (HASH-TABLE test size), (HASH-TABLE test size
type-indicator), (STOBJ-TABLE), or (STOBJ-TABLE size); each
vali is an object satisfying typei; and each bi is t or
nil. Pairs :element-type etypei, :initially vali, and
:resizable bi may be omitted; more on this below. The :renaming
doublets argument is optional and allows the user to override the default
function names introduced by this event. 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. The optional
:non-memoizable nm-flg and :non-executable ne-flg Boolean arguments
are ignored when nm-flg and ne-flg are nil, but otherwise: the
former instructs ACL2 to lay down faster code for functions that return the
new stobj but disallows memoization of any function that takes the new
stobj as an argument; and the latter avoids actually creating a global
stobj (details follow later below). We describe further restrictions on the
fieldi, typei, vali, and on doublets 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. For fields of ARRAY type, this
event also introduces length and resize functions. For fields of
HASH-TABLE type, this event also introduces boundp, get?, remove, count,
clear, and initialization functions. Fields of STOBJ-TABLE type
introduce those functions as well except for the get? function.
The Single-Threaded Object Introduced
The defstobj event effectively introduces a new ``live stobj'' object,
named name, which has as its initial logical value a list of k
elements, where k is the number of ``field descriptors'' provided. This
object has mutable updates: that is, the object is actually modified in place,
rather than copied, where for an array or hash-table field the update is made
to a corresponding raw Lisp array or hash table (respectively). This is only
possible because of syntactic restrictions enforced by ACL2 when programming
with stobjs, so that after modifying a stobj, its old versions are no longer
accessible.
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. If the
:type of a field is (HASH-TABLE test) or (HASH-TABLE test
size), or (HASH-TABLE test size type-indicator), then: test is one
of the symbols EQ, EQL, HONS-EQUAL, or EQUAL; size,
if supplied as above or in (STOBJ-TABLE size), is nil (handled the same
as when size is omitted) or a natural number; and type-indicator restrict
the values that can be stored, as discussed in the next paragraph. The
hash-table test is applied when looking up keys in the associated raw Lisp
hash table, where hons-copy is first applied to the key in the
HONS-EQUAL case; and the size is a hint to the host Lisp for the initial
size of the associated hash table in raw Lisp. (The size really is used only
as a hint. Indeed, at least one host Lisp does not support size 0, so ACL2
simply treats size 0 as size 1; and even size 1 may result in a hash table of
considerably larger size.)
If the value of :type is of the form (ARRAY type-indicator
(max)), (HASH-TABLE test size type-indicator), or 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.
A field with a STOBJ-TABLE type is logically an association list whose
keys are stobj names. ACL2 maintains the execution invariant that each
key is mapped to a stobj satisfying that key's recognizer. We say little more
here about stobj-tables; see stobj-table for relevant discussion.
Below, we refer to scalar types as stobj field types that are
neither array types, hash-table types, nor stobj-table types. Now consider
the keyword value :initially val for a stobj field. If the stobj field
is of scalar type, then val is the initial value of the field. For an
array type (ARRAY type-indicator (max)), val is the initial value of
the elements in the corresponding array. For a HASH-TABLE type, val
is the value obtained when looking up a key that is not bound in the
hash table; think of it as the default value for lookups. Finally, the
:initially keyword is illegal for fields of STOBJ-TABLE type.
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
primarily 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; see defstobj-element-type for discussion of the
:element-type keyword that may be provided for performance . For fields
of HASH-TABLE or STOBJ-TABLE type, this event also introduces
boundp, get? (HASH-TABLE types only), remove, count, clear, and
initialization functions, as discussed below. 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)), (HASH-TABLE test), (HASH-TABLE test
size), (HASH-TABLE test size type-spec), (STOBJ-TABLE), or
(STOBJ-TABLE size). (Again, we are ignoring the case of nested stobjs,
discussed elsewhere (see nested-stobjs), where a type-spec may be
replaced by a stobj name.) The latter forms are said to be ``array types'',
``hash-table types'', and stobj-table types (again, not discussed much here;
see stobj-table). 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
(HASH-TABLE HONS-EQUAL 70)
(HASH-TABLE EQL NIL (INTEGER 0 *))
(STOBJ-TABLE 70)
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.'' Below we present the
restrictions on typei and vali.
Remark on SATISFIES. As suggested above, each type indicator may be a
legal type-spec. But for a type-spec (SATISFIES pred), not only
must pred be unary — it also must be a guard-verified
:logic mode function whose guard is t. For example, since
the guard of evenp specifies an integer, the type-spec (SATISFIES
evenp) is not legal for a stobj field. However, the following is legal.
(defun my-evenp (x)
(declare (xargs :guard t))
(and (integerp x) (evenp x)))
(defstobj st (fld :type (satisfies my-evenp) :initially 4))
Scalar Types
We first discuss types that are neither array types, hash-table types, nor
stobj-table types. We call these ``scalar 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.
See defstobj-element-type for how the :element-type field may
help with performance.
Hash-table Types
When typei is of the form (HASH-TABLE test size type-spec), where
size and type-spec are optional, the field is logically an
association list, initially empty, accessed using function hons-assoc-equal (which is convenient simply because it has a guard of
t, as opposed to other flavors of assoc). Under the hood in raw
Lisp, however, there is a corresponding hash table that represents the same
association of keys with values as does the association list. Each key should
be comparable with arbitrary objects using the specified test: thus if
test is equal then there is no restriction on keys; if test
is eq or eql then the keys must be symbols or satisfy eqlablep, respectively; and if test is hons-equal then there is
no restriction on keys, but each proposed key is honsed in raw Lisp
before it is used (whether for access or update) and before it is put into the
underlying hash table. The size defaults to nil, and if supplied,
it must be either nil or a non-negative integer, or else a defined
constant evaluating to nil or a non-negative integer. When the value is
a (non-negative) integer, it may be used by the host Lisp as a hint for how to
size the associated hash table in raw Lisp.
For a hash-table field, the :initially keyword specifies a default
rather than an initial value: it provides the value (default nil)
returned by an accessor when a given key is not bound.
A hash-table field is associated not only with a recognizer, an accessor,
and an updater, but also with the following functions, whose final argument is
the stobj name but that may also take a key or, in the case of the ``init''
function, three other arguments, as follows:
- a ``boundp'' function to check whether a given key is bound;
- a ``get?'' function that, for a given key, returns two values (mv val
boundp), where: if the given key is bound then val is its value and
boundp is t, else val is as specified by the :initially
keyword (nil by default) and boundp is nil;
- a ``remove'' function for removing a given key;
- a ``count'' function that returns the number of (distinct) bound
keys;
- a ``clear'' function that creates a new empty hash table (and logically,
the empty alist);
- an ``init'' function that takes a given size, rehash-size, and
rehash-threshold (and the stobj name) and creates a new empty hash table (and
logically, the empty alist) by passing these parameters to the raw Lisp
function, (make-hash-table), that creates a hash table.
The clear and init functions both use the size argument, if supplied
and not nil, of the type of the field supplied in the defstobj
event. If a non-nil size argument was not supplied in that type,
then the size of the hash table depends on the host Lisp.
Stobj-table Types
As noted above, these are not discussed much here; see stobj-table.
The Default Function Names
To recap, in
(defstobj name
(field1 :type type1 :initially val1)
...
(fieldk :type typek :initially valk)
:renaming doublets
: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, hash-table, and stobj-table 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.
The accessor and updater functions for a hash-table field are analogous to
those for array fields. Thus, the accessor takes an additional key argument
and returns the associated value, or nil if the key is not bound. The updater
function takes a key, a new value, and the stobj, and returns a new stobj with
the indicated element replaced by the new value. See stobj-table for a
discussion of stobj-table types, which are largely ignored below.
These functions — the recognizer, accessor, and updater, and also
length and resize functions in the case of array fields, and boundp, get?,
remove, count, clear, and init functions in the case of hash-table fields
— have ``default names.'' The default names depend on the field name,
fieldi, and on whether the field is an array field, a hash-table field,
or neither (i.e., a scalar field). 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 or the size of a
resized array, k as a key (for the logical association list or raw-Lisp
hash table associated with the field), v as the ``new value'' to be
installed by an updater, and name as the single-threaded object.
scalar field array field hash-table field
and stobj-table field
recognizer (cP x) (cP x) (cP x)
accessor (c name) (cI i name)
hash-table access: (c-get k name)
stobj-table access: (c-get k name default)
updater (UPDATE-c v name) (UPDATE-cI i v name) (c-put k v name)
length (c-LENGTH name)
resize (RESIZE-c i name)
boundp (c-boundp k name)
get? [For hash-tables only, not stobj-tables] (c-get? k name)
remove (c-rem k name)
count (c-count name)
clear (c-clear name)
init (c-init ht-size
rehash-size
rehash-threshold
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)
(H :TYPE (HASH-TABLE EQ)))
introduces a stobj named $S. The stobj has three fields: X,
A, and H. The A field is an array and the A field is
a hash table. The X field contains an integer and is initially 0. The
A field contains a list of integers, each between 0 and 9, inclusive.
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 HP (X) ...) ; recognizer of H 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 (I $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
(DEFUN H-GET (K $S) ...) ; accessor for H field at key K
(DEFUN H-PUT (K V $S) ...) ; updater for H field at key K
(DEFUN H-BOUNDP (K $S) ...) ; t if key k is bound in H, else nil
(DEFUN H-GET? (K $S) ...) ; (mv val t) if key is bound in H to val;
; (mv nil nil) if key is not bound in H
(DEFUN H-REM (K $S) ...) ; remove key K from field H
(DEFUN H-COUNT ($S) ...) ; the number of (distinct) keys in field H
(DEFUN H-CLEAR ($S) ...) ; empty the hash table for field H
(DEFUN H-INIT (HT-SIZE REHASH-SIZE REHASH-THRESHOLD $S) ...)
; replace the hash table for field H with
; with a new, empty hash table with the
; given hints as described below
For the last of these, the values of HT-SIZE, REHASH-SIZE, and
REHASH-THRESHOLD are passed to the :size, :rehash-size, and
:reash-threshold arguments (respectively) of a call of
make-hash-table in raw Lisp. The :test argument of this function is
the one specified in the :type specified in the defstobj event for
the field, in this case EQ from the type (HASH-TABLE EQ); note
however that if the :type specifies the test HONS-EQUAL, then the
:test is EQL.
Avoiding the Default Function Names
If you do not like the default names listed above you may use the optional
:renaming doublets to substitute names of your own choosing. Each
element of doublets 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 I
Note that even though the renaming doublets 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 doublets may be necessary to avoid name clashes
between the default names 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 that constitute the raw
Lisp implementation of the event, evaluate the form
(nth 4 (global-val 'cltl-command (w state)))
immediately after the defstobj event has been processed. Those
functions that contain (DECLARE (STOBJ-INLINE-FN T)) will generate defabbrev forms because the :inline keyword of defstobj was
supplied the value t. The rest will generate defun forms.
A defstobj is considered redundant only if it is syntactically
identical to a previously executed defstobj. Note that a redundant
defstobj does not reset the stobj fields to their initial
values.
Performance
The :inline keyword argument controls whether or not the functions
introduced are inlined (as macros under the hood, in raw Lisp), with the
exception of the resize function. 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 perhaps 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 an 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.
It can also improve performance to specify :non-memoizable t, which
disallows memoization but therefore avoids the cost of certain ``flushing''
operations.
See defstobj-element-type for performance considerations pertaining
to the :element-type field.
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 !>
Specifying Non-executable Stobjs
As noted above, if keyword argument :non-executable t is specified
then no global stobj for the given name is created. See add-global-stobj for a discussion of global stobjs, but in a nutshell, a
global stobj is a ``live'', mutable stobj that can be referenced in the
top-level loop. So why use this keyword argument? Perhaps you would like to
do your computation on several stobjs that are all congruent to a given stobj,
st. Then by using :non-executable t to introduce st, you avoid
allocating memory for st that you never intend to use. Similarly, you
can avoid allocating such memory when your intended use of st is only as
a local stobj (see with-local-stobj) or as the type of a stobj field of
another stobj. But see add-global-stobj and remove-global-stobj
for utilities that change whether or not there is a global stobj for a given
name.
Subtopics
- Defstobj-element-type
- Specify the element type for a stobj array field
