With-live-state
Allow a reference to state in raw Lisp
The macro with-live-state is an advanced feature that very few
users will need (basically, only system hackers). Indeed, it is essentially
untouchable, defined with defmacro-untouchable; 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.
