Major Section: EVENTS
WARNING! This event is intended for advanced users who, in essence, want to build extensions of ACL2. See see defttag, in particular, the ``WARNING'' there, and see the warning about stobjs at the end of this documentation topic.
Progn! can be used like
progn, even in books. But unlike
progn! does not require its constituent forms to be
events (see embedded-event-form), except that the first form cannot be
a symbol unless it is
:state-global-bindings (advanced feature, described
below). However, see make-event for a ``Restriction to the Top Level'' that
still applies under a call of
progn! allows non-events, it differs from
progn in another
progn! is illegal unless there is an active ttag;
book/misc/hacker.lisp for two macros,
with-redef-allowed, each defined in terms of
progn!, that allow
arbitrary forms in contexts that would normally require legal embedded event
Given a form
(progn! form1 form2 ... formk), ACL2 will evaluate each
formi in turn (for i from 1 to k). If a form returns more than one value
(see mv) where the first value returned is not
nil, then no later form
will be evaluated and the result returned by the
progn! call will be
(mv erp val state) for some non-
erp, signifying an
error (see ld-error-triples). Otherwise the evaluation is considered to
have succeeded, and will continue on later forms.
The normal undoing mechanism does not generally apply to forms within a
progn! that are not legal ACL2 events (see embedded-event-form).
In particular, note that a non-
local call of
progn! in an
encapsulate event will generally be evaluated twice: once on each pass.
This fact is worth keeping in mind if you are using
progn! to change the
state of the system; ask yourself if it is acceptable to apply that
state-changing operation more than once.
We now describe, for system hackers only, a sophisticated extension of
progn! not mentioned above: support for keyword argument
:state-global-bindings. If the first argument of
progn! is this
keyword, then the second argument is treated as a list of bindings as
expected by ACl2 system function
state-global-let* (not yet documented).
Thus, in the ACL2 loop,
(progn! :state-global-bindings bindings form1 form2 ... formk)is treated as follows:
(progn! (state-global-let* bindings (progn! form1 form2 ... formk)))However, in raw Lisp the former is just:
(progn form1 form2 ... formk)Thus, one should use the
:state-global-bindingsargument with care, since the behavior in the ACL2 loop can differ from that in Common Lisp. The intention is that one bind only state global variables that are relevant to evaluation of the forms within the ACL2 loop and are harmlessly ignored for evaluation of those forms in raw Lisp. Here is a typical sort of example, as state global
ld-redefinition-actionis not relevant to the evaluation of
defunin raw Lisp.
(progn! (remove-untouchable 'ld-redefinition-action nil) (progn! :state-global-bindings ((ld-redefinition-action '(:doit . :overwrite))) (defun foo (x) (cons x x))) (push-untouchable 'ld-redefinition-action nil))
Finally, we point out a pitfall of
progn! related to stobjs. The
following book can cause a hard Lisp error, depending on the host Common
Lisp, when certified with a non-
nil value for
(in-package "ACL2") (defstobj st fld) (defttag :my-ttag) (progn! (update-fld 3 st))The problem is that the stobj variable
stis not known to raw Lisp. The compilation problem disappears if the last form above is replaced with the following two forms.
(include-book "misc/hacker" :dir :system) (with-raw-mode (update-fld 3 *the-live-st*))