WITH-LOCAL-STATE

locally bind state
Major Section:  STOBJ

This is an advanced topic, probably of interest only to system developers.

Consider the following example form:

(with-local-state
 (mv-let (result state)
         (compute-with-state x state)
         result))
This is equivalent to the following form.
(with-local-stobj
 state
 (mv-let (result state)
         (compute-with-state x state)
         result))
By default, this form is illegal, because ACL2 does not have a way to unwind all changes to the ACL2 state; we say more on this issue below. There may however be situations where you are willing to manage or overlook this issue. In that case you may execute the following form to enable the use of with-local-state, by enabling the use of with-local-stobj on state; but note that it requires an active trust tag (see defttag).
(remove-untouchable create-state t)

Please be aware that no local state is actually created, however! In particular, users of with-local-state need either to ensure that channels are closed and state global variables are returned to their original values, or else be willing to live with changes made to state that are not justified by the code that has been evaluated. You are welcome to look in the the ACL2 source code at the definition of macro channel-to-string, which employs with-local-state to create a local state for the purpose of creating a string.