		Search-engine friendly clone of the ACL2 documentation.

With-local-state

Locally bind state

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 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))))

Note for ACL2(p) users: When parallel-execution is enabled, invocations of with-local-state are surrounded by a lock.