state in raw Lisp
Major Section: ACL2-BUILT-INS
The macro with-live-state is an advanced feature that very few users will
need (basically, only system hackers). Indeed, it is untouchable;
see remove-untouchable for how to enable calling with-live-state in the
ACL2 loop.
Example Form: (with-live-state (assign y 3)) General form: (with-live-state form)where form is an arbitrary form with a free reference to the variable
state.Logically, (with-live-state FORM) macroexpands to FORM. However, in
raw Lisp it expands to:
(let ((state *the-live-state*)) FORM)
If a form that mentions the variable state might be executed in raw
Lisp -- that is, either outside the ACL2 loop or in raw
mode (see set-raw-mode) -- then the surrounding the form with
with-live-state as shown above can avoid potential warnings or (much less
likely) errors. Note however that if state is lexically bound to a state
other than the usual ``live'' state, surprising behavior may occur when
evaluating a call of with-live-state in raw Lisp or raw mode (either
directly by evaluation or at compile time), because with-live-state will
override that lexical binding of state by a lexical binding of
state to the usual ``live'' state.
