		Search-engine friendly clone of the ACL2 documentation.

Stobj-table

A stobj field mapping stobj names to stobjs

See stobj for basic background on stobjs, and see defstobj for detailed documentation on the syntax and semantics of stobjs, including fields specified with :type (stobj-table) or :type (stobj-table SIZE). In the latter case, SIZE must either be a natural number or a defined constant whose value is a natural number. We call such fields — that is, stobj fields specified with :type (stobj-table) or :type (stobj-table SIZE) — ``stobj-table fields''; this documentation topic explains them, and it assumes familiarity with stobj fields of stobjs as documented in nested-stobjs — especially, the use of stobj-let to read and write such fields. Note that the documentation for defstobj shows the default names for accessors and updaters; for a stobj-table field, TBL, these are TBL-GET and TBL-PUT, respectively.

For examples of stobj-let usage for stobj-tables, see community-book books/system/tests/stobj-table-tests-input.lsp.

A stobj-table field may be viewed as an association list mapping stobj names to corresponding stobjs, so that each stobj name maps to a stobj that satisfies the recognizer for that stobj name. This requirement is not enforced in the logic (i.e., in recognizer functions). But it is essentially maintained in raw Lisp as an invariant, except that for efficiency, a stobj-table field is implemented as a hash table (again, mapping stobj names to corresponding stobjs). Below we give more details and explain how stobj-let may be used to access and update stobjs that are in such a table.

The general forms for stobj-table fields of stobjs are as shown below.

(defstobj NAME
  (TBL1 :type (stobj-table))      ; stobj field of default size
  ...
  (TBL2 :type (stobj-table SIZE)) ; stobj field of desired size SIZE
  ...)

That is, a stobj-table field is a field whose type is of the form (stobj-table) or (stobj-table SIZE). The syntax is thus much like the syntax for hash-table fields of stobjs, except that there is no test specified for a stobj-table (it is actually eq in raw Lisp).

As noted above, a stobj-table is conceptually an alist that associates stobj names with corresponding stobjs. We say ``conceptually'' because in fact, the recognizer for any stobj-table field is t: there is no requirement that it is actually an alist. It is accessed logically with hons-assoc-equal, which is a variant of assoc that treats an arbitrary object as an alist: only pairs are considered when looking up a key, and the final cdr is ignored. A default value is returned when there is no pair with the given key. A stobj-table field is thus very much like a hash-table field. The key difference (pun somewhat intended) is that each key of a stobj-table is the name of a stobj (other than state, i.e., it is a user-defined stobj name), and the corresponding value is a stobj satisfying the recognizer for that name.

A common case is that a stobj-table field is the unique field of its parent stobj. In that case we may think of the entire stobj as a stobj-table, and that is actually consistent with the implementation: in raw Lisp, if a stobj-table field is the sole field of its parent stobj, then that stobj-table field is actually the entire stobj; there is not the usual indirection in raw Lisp, where a stobj is a vector of fields and the field is accessed as an entry in that vector. (Logically, however, a stobj is always a list of its fields, even if there is only one field.)

Reads and writes of a stobj-table field are much like reads and writes when the field is an array of stobjs. In both cases, one uses stobj-let to access and possibly update the desired individual stobj or stobjs. The syntax thus looks as follows, where ST is a stobj name and PARENT is the name of a stobj that has a stobj-table accessor with name TBL-GET. Note that the first argument of the accessor must be the quotation of the name of the bound stobj (thus below, 'ST is the quotation of ST) and the third argument must be a call of that stobj's creator function.

(stobj-let (...                                 ; bindings
            (ST (TBL-GET 'ST PARENT (CREATE-ST)))
            ...
            )
           (...)                                ; producer variables
           (...)                                ; producer
           ...                                  ; consumer
           )

The TBL-GET call above always returns an object that satisfies the recognizer for the stobj, ST. However, that is a fact about evaluation; it is not provable in the logic. Fortunately, guard verification typically adds hypotheses to this effect when necessary.

Remark. This remark on the implementation may be skipped, but it may provide some intuition. When a stobj name is not bound in the underlying hash table, then the default value (in the example above, (CREATE-ST)) provides a suitable stobj nonetheless. And if that stobj name is among the producer variables of a stobj-let form, it will be bound in the underlying hash table when the stobj-let form completes. End of remark.

The remainder of this topic explains the use of stobj-tables by following the example in community-book std/stobjs/stobj-table.lisp. The first form in that book (after the initial in-package form) is as follows.

(defstobj stobj-table (tbl :type (stobj-table)))

This specifies a stobj named stobj-table with a unique field, tbl. As noted above, this stobj is the same as its field in raw Lisp, so even though it is the field that is truly a stobj-table, it is not conceptually problematic to call the entire stobj ``stobj-table''. This may be the most common case for a stobj-table (i.e., being a unique field of a stobj).

The remaining forms in the book are local to the book, intended to illustrate with simple examples how stobj-tables may be used. The first one just introduces a rather trivial stobj.

(defstobj st1 fld1)

The next form puts this stobj into the stobj-table after updating its field with a specified value.

(defun update-st1-in-tbl (val stobj-table)
  (declare (xargs :stobjs stobj-table))
  (stobj-let ((st1 (tbl-get 'st1 stobj-table (create-st1)))) ; bindings
             (st1)                                        ; producer variable
             (update-fld1 val st1)                        ; producer
             stobj-table                                  ; consumer
             ))

The form after that accesses the value of 'st1 in the stobj-table and returns its field's value.

(defun read-st1-in-tbl1 (stobj-table)
  (declare (xargs :stobjs stobj-table))
  (stobj-let ((st1 (tbl-get 'st1 stobj-table (create-st1)))) ; bindings
             (val)                                        ; producer variable
             (fld1 st1)                                   ; producer
             val                                          ; consumer
             ))

Next is a check that when a specific value is written for the key 'st1 with the update function defined above, the value subsequently read for key 'st1 is that written value. The reason for the mv call is that the updater returns an updated stobj-table, which therefore must be returned. However, assert-event is sufficiently clever to check that the first (i.e., ordinary) value returned is non-nil.

(assert-event
 (let ((stobj-table (update-st1-in-tbl 3 stobj-table)))
   (mv (equal (read-st1-in-tbl1 stobj-table)
              3)
       stobj-table))
 :stobjs-out '(nil stobj-table))

The computation above is a special case of a standard ``read-over-write'' property, that after a write, we read the value that was just written. This is proved automatically.

(defthm read-over-write-st1-in-tbl
  (implies (stobj-tablep stobj-table)
           (let ((stobj-table (update-st1-in-tbl val stobj-table)))
             (equal (read-st1-in-tbl1 stobj-table)
                    val))))

The other standard ``read-over-write'' property is that the write for a given key doesn't affect the value read for a different key. The following events, admitted automatically, illustrate that property: here, writing a value for the key 'st1 doesn't affect the value read for the key 'st2.

(defstobj st2 fld2)

(defun read-st2-in-tbl (stobj-table)
  (declare (xargs :stobjs stobj-table))
  (stobj-let ((st2 (tbl-get 'st2 stobj-table (create-st2)))) ; bindings
             (val)                                        ; producer variable
             (fld2 st2)                                   ; producer
             val                                          ; consumer
             ))

(defthm read-over-write-st2-in-tbl
  (implies (stobj-tablep stobj-table)
           (let ((stobj-table-2 (update-st1-in-tbl val stobj-table)))
             (equal (read-st2-in-tbl stobj-table-2)
                    (read-st2-in-tbl stobj-table)))))

Note that all keys in a stobj-table are names of stobjs. Consider what happens when we evaluate the events in the book above, including the local events, and then undo the defstobj event admitting st1. It is clear that undoing has removed the symbol st1 as a key in the stobj-table.

ACL2 !>(ld "std/stobjs/stobj-table.lisp" :dir :system)
[[.. output omitted ..]]
ACL2 !>(tbl-count stobj-table)
1
ACL2 !>:ubt st1
   d       1:x(DEFSTOBJ STOBJ-TABLE (TBL :TYPE #))
ACL2 !>(tbl-count stobj-table)
0
ACL2 !>

Finally, we remark that there is nothing special about stobj-table fields with respect to stobj fields of abstract stobjs.