Evaluate some forms, not necessarily 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, 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!.
Because progn! allows non-events, it differs from progn in
another important respect: progn! is illegal unless there is an active
ttag; see defttag.
See community book hacker for two macros, with-raw-mode and
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-nil value erp, signifying an
error (see ld-error-triples). Otherwise the evaluation is considered
to have succeeded, and will continue with later forms. The value returned by
a call of progn! with no such error is of the form (mv nil v state),
where v depends on the last form as follows. If the last form evaluates
to a single value, then v is that value, except if the value is a stobj, say ST, then v is the symbol REPLACED-ST. Otherwise
the last form evaluates to some (mv nil x ...), and v is x
unless after the final form's evaluation we are in raw-mode (see set-raw-mode), in which case the progn! call returns nil (so that
ACL2 can at least print the result — imagine Lisp returning a pathname
object from a load call, for example).
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.
Please note that progn! may differ from progn in the following
sense: definitions within a call of progn! might not be compiled. For
example, consider the following book.
(progn (defun f1 (x) x))
(progn! (defun f2 (x) x))
If the underlying Lisp is GCL 2.6.7, then after including this certified
book (where the default certification took place, creating a compiled file),
then f1 is a compiled function but f2 is not. For other Lisps
supported by ACL2, both f1 and f2 are compiled, though we are not
sure that every function under every call of progn! would similarly be
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*. Thus, in the ACL2
(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-bindings argument 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-action is not relevant to
the evaluation of defun in raw Lisp.
(progn! (remove-untouchable 'ld-redefinition-action nil)
((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 and whether certifying or including it, when certified with a
non-nil value for compile-flg (see certify-book).
(defstobj st fld)
(progn! (update-fld 3 st))
The problem is that the stobj variable st is not known to raw
Lisp. The compilation problem disappears if the last form above is replaced
with the following two forms.
(include-book "hacking/hacker" :dir :system)
(let ((live-st (cdr (assoc-eq 'st *user-stobj-alist*))))
(update-fld 3 live-st)))
- A better way to load raw Lisp code than directly using progn!