		Search-engine friendly clone of the ACL2 documentation.

B*-binders

ACL2::patbind-stobj-get

Syntactic sugar for using stobj-let to get some fields from a sub-stobj.

This b* binder provides a way to code accesses to nested stobjs within a b* form, as an alternative to stobj-let. Here is an an example:

(b* (((stobj-get data-obj child-stobj1) ;; extracted data and updated child stobjs

      ;; bindings for subform :
      ((child-stobj1 (child-field parent-stobj))
       (child-stobj2 (child-arr n parent-stobj)))

      ;; subform:
      (b* ((data (child-stobj2-data child-stobj2))
           (child-stobj1 (update-child-stobj1-data newdata child-stobj1)))
         (mv data child-stobj1))))
  (mv data-obj parent-stobj))

The above extracts child-stobj1 and child-stobj2 from parent-stobj and binds them while evaluating the subform, which extracts a (non-stobj) data object from child-stobj2 and updates a field of child-stobj1 with some new data. We then return the data object and (implicitly) the parent-stobj, which must be returned since one of its child stobjs was updated. More explicitly, this macroexpands (more or less) to the following:

(b* (((mv data-obj parent-stobj) ;; returned values: data and modified parent stobj
      (stobj-let ((child-stobj1 (child-field parent-stobj))
                  (child-stobj2 (child-arr n parent-stobj))) ;; bindings
                 (data-obj child-stobj1) ;; producer variables
                 ;; subform:
                 (b* ((data (child-stobj2-data child-stobj2))
                      (child-stobj1 (update-child-stobj1-data newdata child-stobj1)))
                   (mv data child-stobj1))
                 ;; returned values:
                 (mv data-obj parent-stobj))))
  (mv data-obj parent-stobj))

The general form of a stobj-get binding is:

(b* (...
     ((stobj-get VARS)
      BINDINGS
      . SUBFORMS)
     ...)
 ...)

BINDINGS are bindings of stobj names to stobj accessors. SUBFORMS are the forms that are evaluated under the bindings, in an implicit progn (so all but the last are just for side effects). The VARS correspond to the values returned by the last subform.