With-local-stobj
Locally bind a single-threaded object
See stobj for an introduction to single-threaded
objects. Also see defstobj for additional background.
Example Form:
(with-local-stobj
st
(mv-let (result st)
(compute-with-st x st)
result))
With-local-stobj can 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 only allowed via
with-local-stobj or in logic-only situations (like theorems and hints).
Moreover, neither with-local-stobj nor its expansions are legal when
typed directly at the top-level loop. See top-level for a way to use
with-local-stobj in 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-name is the name of a stobj, mv-let-form is a
call of mv-let that binds stobj-name but does not return
stobj-name — in fact, if mv-let-form is (mv-let (...)
... body), then body does not even reference stobj-name —
and if creator-name is supplied then it should be the name of the creator
function for stobj-name. For the example form above, its expansion would
use creator-name, if supplied, in place of create-st. Note that
stobj-name must not be state (the ACL2 state), except in special
situations probably of interest only to system developers; see with-local-state.
Note that if a stobj ST is bound upon beginning evaluation of a form
(with-local-stobj ST ...), then the value of ST is the same
immediately before evaluating that form as it is immediately after that
evaluation. In other words, only a local version of ST is modified
inside that with-local-stobj form.
With-local-stobj can be useful when a stobj is used to memoize
intermediate results during a computation, yet it is desired not to make the
stobj a formal parameter for the function and its callers.
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 creator function.
Finally, here is a small example concocted in order 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
