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.
Here is an example use of with-local-state. Notice the use of
defttag -- and indeed, please understand that we are just hacking
here, and in general it takes significant effort to be sure that one is using
with-local-state correctly!
(defttag t)
(remove-untouchable create-state t)
(set-state-ok t)
(defun foo (state)
(declare (xargs :mode :program))
(mv-let
(channel state)
(open-input-channel "my-file" :object state)
(mv-let (eofp obj state)
(read-object channel state)
(declare (ignore eofp))
(let ((state (close-input-channel channel state)))
(mv obj state)))))
(defun bar ()
(declare (xargs :mode :program))
(with-local-state (mv-let (result state)
(foo state)
result)))
; Multiple-value return version:
(defun foo2 (state)
(declare (xargs :mode :program))
(mv-let
(channel state)
(open-input-channel "my-file" :object state)
(mv-let (eofp obj state)
(read-object channel state)
(let ((state (close-input-channel channel state)))
(mv eofp obj state)))))
(defun bar2 ()
(declare (xargs :mode :program))
(with-local-state (mv-let (eofp result state)
(foo2 state)
(mv eofp result))))
