PROGN!

evaluate some forms, not necessarily events
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.

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). (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 book/misc/hacker.lisp 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 forms.

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

The following rather sophisticated example illustrates the power of progn!. Here, state-global-let* is an advanced programming feature that binds state global variables (see state, in particular the discussion of the global table) to values.

(progn!

(remove-untouchable 'ld-redefinition-action nil)

(state-global-let* ((ld-redefinition-action '(:doit . :overwrite)))

(defund foo (x) (cons x x))) (push-untouchable 'ld-redefinition-action nil))