Major Section: STOBJ
See stobj for an introduction to single-threaded objects.
Example Form: (with-local-stobj st (mv-let (result st) (compute-with-st x st) result))
With-local-stobjcan be thought of as a macro, where the example form above expands as follows.
(mv-let (result st) (let ((st (create-st))) (compute-with-st x st)) (declare (ignore st)) result)However, ACL2 expects you to use
with-local-stobj, not its expansion. More precisely, stobj creator functions are not allowed except (implicitly) via
with-local-stobjand in logic-only situations (like theorems and hints). Moreover, neither
with-local-stobjnor its expansions are legal when typed directly at the top-level loop.
General Forms: (with-local-stobj stobj-name mv-let-form) (with-local-stobj stobj-name mv-let-form creator-name)where
stobj-nameis the name of a stobj other than
mv-let-formis a call of
mv-let, and if
creator-nameis supplied then it should be the name of the creator function for
stobj-name; see defstobj. For the example form above, its expansion would use
creator-name, if supplied, in place of
With-local-stobj can be useful when a stobj is used to memoize
intermediate results during a computation, yet it is desired not to
stobj a formal parameter for the function and its
ACL2 can reason about these ``local stobjs,'' and in particular
about stobj creator functions. For technical reasons, ACL2 will not
allow you to enable the
:EXECUTABLE-COUNTERPART rune of a stobj
Finally, here is a small example concocted ino rder to illustrate that
with-local-stobj calls can be nested.
(defstobj st fld1)
(defun foo () (with-local-stobj st ; Let us call this the ``outer binding of st''. (mv-let (val10 val20 st) (let ((st (update-fld1 10 st))) ;; At this point the outer binding of st has fld1 = 10. (let ((result (with-local-stobj st ; Let us call this the ``inner binding of st''. (mv-let (val st) (let ((st (update-fld1 20 st))) ;; Now fld1 = 20 for the inner binding of st. (mv (fld1 st) st)) val)))) ;; So result has been bound to 20 above, but here we are once again ;; looking at the outer binding of st, where fld1 is still 10. (mv (fld1 st) result st))) (mv val10 val20))))
(thm (equal (foo) (mv 10 20))) ; succeeds