This is documentation for ACL2 Version 3.2
Copyright (C) 2007  University of Texas at Austin

This program is free software; you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation; either version 2 of the License, or
(at your option) any later version.

This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
GNU General Public License for more details.

You should have received a copy of the GNU General Public License
along with this program; if not, write to the Free Software
Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.

Written by:  Matt Kaufmann and J Strother Moore
Department of Computer Sciences
University of Texas at Austin
Austin, TX 78712-1188 U.S.A.

MAKE-EVENT    evaluate (expand) a given form and then evaluate the result

Make-event is a utility for generating events.  It provides a
capability not offered by Lisp macros (see DEFMACRO), as it
allows access to the ACL2 state and logical world.  In essence, the
expression (make-event form) replaces itself with the result of
evaluating form, say, ev, as though one had submitted ev instead of the
make-event call.  But the evaluation of form may involve state and even
modify state, for example by attempting to admit some definitions and
theorems.  Make-event protects the ACL2 logical world so that it is
restored after form is evaluated, before ev is submitted.

     Examples:

     ; Trivial example: evaluate (quote (defun foo (x) x)) to obtain
     ; (defun foo (x) x), which is then evaluated.
     (make-event (quote (defun foo (x) x)))

     ; Evaluate (generate-form state) to obtain (mv nil val state), and
     ; then evaluate val.  (Generate-form is not specified here, but
     ; imagine for example that it explores the state and then generates
     ; some desired definition or theorem.)
     (make-event (generate-form state))

     ; As above, but make sure that if this form is in a book, then when
     ; we include the book, the evaluation of (generate-form state)
     ; should return the same value as it did when the book was
     ; certified.
     (make-event (generate-form state)
                 :check-expansion t)

     ; As above (where the :check-expansion value can be included or
     ; not), where if there is an error during expansion, then the error
     ; message will explain that expansion was on behalf of the indicated
     ; object, typically specified as the first argument.
     (make-event (generate-form state)
                 :on-behalf-of (generate-form state))

     General Form:
     (make-event form :check-expansion chk :on-behalf-of obj)

where chk is nil (the default), t, or the intended "expansion result"
from the evaluation of form (as explained below); and if supplied, obj
is an arbitrary ACL2 object, used only in reporting errors in
expansion, i.e., in the evaluation of form.

We strongly recommend that you look at books/make-event/Readme.lsp,
which summarizes and suggests browsing of some .lisp files in that
directory, in order to understand make-event, perhaps before continuing
to read this documentation.  For example, eval.lisp contains
definitions of macros must-succeed and must-fail that are useful for
testing and are used in many other books in that directory, especially
eval-tests.lisp.  Other than the examples, the explanations here should
suffice for most users.  If you want explanations of subtler details,
see MAKE-EVENT-DETAILS.

Make-event is related to Lisp macroexpansion in the sense that its
argument is evaluated to obtain an expansion result, which is evaluated
again.  Let us elaborate on each of these notions in turn: "is
evaluated," "expansion result", and "evaluated again."

     "is evaluated" -- The argument can be any expression, which is
     evaluated as would be any expression submitted to ACL2's top level
     loop.  Thus, state and user-defined stobjs may appear in the form
     supplied to make-event.  Henceforth, we will refer to this
     evaluation as "expansion."  Expansion is actually done in a way
     that restores ACL2's built-in state global variables, including
     the logical world, to their pre-expansion values (with a few
     exceptions -- see MAKE-EVENT-DETAILS -- and where we note
     that changes to user-defined state global variables (see
     ASSIGN) are preserved).  So, for example, events might be
     evaluated during expansion, but they will disappear from the
     logical world after expansion returns its result.  Moreover,
     proofs are enabled by default at the start of expansion (see
     LD-SKIP-PROOFSP), because an anticipated use of make-event is to
     call the prover to decide which event to generate, and that would
     presumably be necessary even if proofs had been disabled.

     "expansion result" -- The above expansion may result in an ordinary
     (non-state, non-stobj) value, which we call the "expansion
     result."  Or, expansion may result in a multiple value of the form
     (mv erp val state stobj-1 ... stobj-k), where k may be 0; in fact
     the most common case is probably (mv erp val state).  In that
     case, if erp is not nil, then there is no expansion result, and
     the original make-event evaluates to a soft error.  If however erp
     is nil, then the resulting value is val.  Moreover, val must be an
     embedded event form (see EMBEDDED-EVENT-FORM); otherwise,
     the original make-event evaluates to a soft error.  Note that
     error messages from expansion are printed as described under
     "Error Reporting" below.

     "evaluated again" -- the expansion result is evaluated in place of
     the original make-event.

Note that the result of expansion can be an ordinary event, but it can
instead be another call of make-event, or even of a call of a macro that
expands to a call of make-event.  Or, expansion itself can cause
subsidiary calls of make-event, for example if expansion uses ld to
evaluate some make-event forms.  The state global variable
make-event-debug may be set to a non-nil value in order to see a trace
of the expansion process, where the level shown (as in "3>") indicates
the depth of expansions in progress.

Expansion of a make-event call will yield an event that replaces the
original make-event call.  In particular, if you put a make-event form
in a book, then in essence it is replaced by its expansion result,
created during the proof pass of the certify-book process.  We now
elaborate on this idea of keeping the original expansion.

By default, a make-event call in a certified book is replaced (by a
process hidden from the user, in an :expansion-alist field of the book's
certificate) by the expansion result from evaluation of its first
argument.  Thus, although the book is not textually altered during
certification, one may imagine a "book expansion" corresponding to the
original book in which all of the events for which expansion took place
(during the proof phase of certification) have been replaced by their
expansions.  A subsequent include-book will then include the book
expansion corresponding to the indicated book.  When a book is compiled
during certify-book, it is actually the corresponding book expansion,
stored as a temporary file, that is compiled instead.  That temporary
file is deleted after compilation unless one first evaluates the form
(assign keep-tmp-files t).  Note however that all of the original forms
must still be legal events (see EMBEDDED-EVENT-FORM).  So for
example, if the first event in a book is (local (defmacro my-id (x)
x)), followed by (my-id (make-event ...)), the final "include-book"
pass of certify-book will fail because my-id is not defined when the
my-id call is encountered.

The preceding paragraph begins with "by default" because if you specify
:check-expansion t, then subsequent evaluation of the same make-event
call -- during the second pass of an encapsulate or during include-book
-- will do the expansion again and check that the expansion result
equals the original expansion result.  In the unusual case that you
know the expected expansion result, res, you can specify
:check-expansion res.  This will will cause a check that every
subsequent expansion result for the make-event form is res, including
the original one.

*Error Reporting.*

Suppose that expansion produces a soft error as described above.  That
is, suppose that the argument of a make-event call evaluates to a
multiple value (mv erp val state ...) where erp is not nil.  If erp is
a string, then that string is printed in the error message.  If erp is
a cons pair whose car is a string, then the error prints "~@0" with #\0
bound to that cons pair; see FMT.  Any other non-nil value of
erp causes a generic error message to be printed.

*Restriction to the Top Level.*

Every form enclosing a make-event call must be an embedded event form
(see EMBEDDED-EVENT-FORM).  This restriction enables ACL2 to
track expansions produced by make-event.  For example:

     ; Legal:
     (progn (with-output
             :on summary
             (make-event '(defun foo (x) x))))

     ; Illegal:
     (mv-let (erp val state)
             (make-event '(defun foo (x) x))
             (mv erp val state))

Final low-level remark, for system implementors.  There is the one
exception to this restriction: a single state-global-let* form
immediately under a progn! call.  For example:

     (progn! (state-global-let* <bindings> (make-event ...)))

See REMOVE-UNTOUCHABLE for an interesting use of this exception.

MAKE-EVENT-DETAILS    details on make-event expansion

The normal user of make-event can probably ignore this section, but we
include it for completeness.  We assume that the reader has read and
understood the basic documentation for make-event (see
MAKE-EVENT), but we begin below with a summary of expansion.

*Introduction*

Here is a summary of how we handle expansion involving make-event forms.

(make-event form :check-expansion nil)

This shows the :check-expansion default of nil, and is typical user
input.  We compute the expansion exp of form, which is the expansion of
the original make-event expression and is evaluated in place of that
expression.

(make-event form :check-expansion t)

The user presumably wants it checked that the expansion doesn't change
in the future, in particular during include-book.  If the expansion of
form is exp, then we will evaluate exp to obtain the value as before,
but this time we record that the expansion of the original make-event
expression is (make-event form :check-expansion exp) rather than simply
exp.

(make-event form :check-expansion exp) ; exp a cons

This is generated for the case that :check-expansion is t, as explained
above.  Evaluation is handled as described in that above case, except
here we check that the expansion result is the given exp.  (Actually,
the user is also allowed supply such a form.)  The original make-event
expression does not undergo any expansion (intuitively, it expands to
itself).

Now let us take a look at how we expand progn forms (encapsulate is
handled similarly).

(progn ... (make-event form :check-expansion nil) ...)

The expansion is obtained by replacing the make-event form as follows.
Let exp be the expansion of form,  Then replace the above make-event
form, which we denote as F, by (record-expansion F exp).  Here,
record-expansion is a macro that returns its second argument.

(progn ... (make-event form :check-expansion t) ...)

The expansion is of the form (record-expansion F exp) as in the nil
case above, except that this time exp is (make-event form
:check-expansion exp'), where exp' is the expansion of form.

(progn ... (make-event form :check-expansion exp) ...) ; exp a cons

No expansion takes place unless expansion takes place for at least one
of the other subforms of the progn, in which case each such form F is
replaced by (record-expansion F exp) where exp is the expansion of F.

*Detailed semantics*

In our explanation of the semantics of make-event, we assume familiarity
with the notion of "embedded event form" (see
EMBEDDED-EVENT-FORM).

Let's say that the "actual embedded event form" corresponding to a given
form is the underlying call of an ACL2 event: that is, LOCALs are
dropped when ld-skip-proofsp is 'include-book, and macros are expanded
away, thus leaving us with a progn, a make-event, or an event form
(possibly encapsulate), any of which might have surrounding local,
skip-proofs, or with-output calls.

Thus, such an actual embedded event form can be viewed as having the
form (rebuild-expansion wrappers base-form) where base-form is a progn,
a make-event, or an event form (possibly encapsulate), and wrappers are
(as in ACL2 source function destructure-expansion) the result of
successively removing the event form from the result of macroexpansion,
leaving a sequence of (local), (skip-proofs), and (with-output ...)
forms.  In this case we say that the form "destructures into" the
indicated wrappers and base-form, and that it can be "rebuilt from"
those wrappers and base-form.

Elsewhere we define the notion of the "expansion result" from an
evaluation (see MAKE-EVENT), and we mention that when expansion
concludes, the ACL2 logical world and most of the state are restored to
their pre-expansion values.  Specifically, after evaluation of the
argument of make-event (even if it is aborted), the ACL2 logical world
is restored to its pre-evaluation value, as are all state global
variables in the list *protected-system-state-globals*.  Thus,
assignments to user-defined state globals (see ASSIGN) do
persist after expansion, since they are not in that list.

We recursively define the combination of evaluation and expansion of an
embedded event form, as follows.  We also simultaneously define the
notion of "expansion takes place," which is assumed to propagate upward
(in a sense that will be obvious), such that if no expansion takes
place, then the expansion of the given form is considered to be itself.
It is useful to keep in mind a goal that we will consider later: Every
make-event subterm of an expansion result has a :check-expansion field
that is a consp, where for this purpose make-event is viewed as a macro
that returns its :check-expansion field.  (Implementation note: The
latest expansion of a make-event, progn, progn!, or encapsulate is
stored in state global 'last-make-event-expansion, except that if no
expansion has taken place for that form then 'last-make-event-expansion
has value nil.)

     If the given form is not an embedded event form, then simply cause
     a soft error, (mv erp val state) where erp is not nil.  Otherwise:

     If the evaluation of the given form does not take place
     (presumably because local events are being skipped), then no
     expansion takes place.  Otherwise:

     Let x be the actual embedded event form corresponding to the given
     form, which destructures into wrappers W and base-form B.  Then the
     original form is evaluated by evaluating x, and its expansion is as
     follows.

     If B is (make-event form :check-expansion val), then expansion
     takes place if and only if val is not a consp and no error occurs,
     as now described.  Let R be the expansion result from protected
     evaluation of form, if there is no error.  R must be an embedded
     event form, or it is an error.  Then evaluate/expand R, where if
     val is not nil then state global 'ld-skip-proofsp is initialized
     to nil.  (This initialization is important so that subsequent
     expansions are checked in a corresponding environment, i.e., where
     proofs are turned on in both the original and subsquent
     environments.)  It is an error if this evaluation causes an error.
     Otherwise, the evaluation yields a value, which is the result of
     evaluation of the original make-event expression, as well as an
     expansion, E_R.  Let E be rebuilt from W and E_R.  The expansion of
     the original form is E if val is nil, and otherwise is the result
     of replacing the original form's :check-expansion field with E,
     with the added requirement that if val is not t (thus, a consp)
     then E must equal val or else we cause an error.

     If B is either (progn form1 form2 ...) or (encapsulate sigs form1
     form2 ...), then after evaluating B, the expansion of the original
     form is the result of rebuilding from B, with wrappers W, after
     replacing each formi in B for which expansion takes place by
     (record-expansion formi formi'), where formi' is the expansion of
     formi.  Note that these expansions are determined as the formi are
     evaluated in sequence (where in the case of encapsulate, this
     determination occurs only during the first pass).  Except, if no
     expansion takes place for any formi, then the expansion of the
     original form is itself.

     Otherwise, the expansion of the original form is itself.

Similarly to the progn and encapsulate cases above, book certification
causes a book to replaced by its so-called "book expansion."  There,
each event ev for which expansion took place during the proof pass of
certification -- say, producing ev' -- is replaced by (record-expansion
ev ev').

Implementation Note. The book expansion is actually implemented by way
of the :expansion-alist field of its certificate, which associates
0-based positions of top-level forms in the book (not including the
initial in-package form) with their expansions.  Thus, the book's
source file is not overwritten; rather, the certificate's
expansion-alist is applied when the book is included or compiled.  End
of Implementation Note.

It is straightforward by computational induction to see that for any
expansion of an embedded event form, every make-event sub-event has a
consp :check-expansion field.  Here, by "sub-event" we mean to expand
macros; and we also mean to traverse progn and encapsulate forms as
well as :check-expansion fields of make-event forms.  Thus, we will
only see make-event forms with consp :check-expansion fields in the
course of include-book forms, the second pass of encapsulate forms, and
raw Lisp.  This fact guarantees that an event form will always be
treated as its original expansion.

*A note on ttags*

See DEFTTAG for documentation of the notion of "trust tag"
("ttag").  Here, we simply observe that if an event (defttag tag-name)
for non-nil tag-name is admitted during the expansion phase of a
make-event form, then although a "TTAG NOTE" will be printed to
standard output, and moreover tag-name must be an allowed tag (see
DEFTTAG), nevertheless such expansion will not cause tag-name
to be recorded once the expansion is complete.  That is, there will be
no lingering effect of this defttag form after the make-event expansion
is complete; no certificate written will be affected (where we are
certifying a book), and the set of allowed ttags will not be affected.
So for example, if this make-event form is in the top-level loop and
subsequently we certify or include a book, then tag-name will not be
associated with the top-level loop by this make-event form.

MUTUAL-RECURSION    define some mutually recursive functions

     Example:
     (mutual-recursion
      (defun evenlp (x)
        (if (consp x) (oddlp (cdr x)) t))
      (defun oddlp (x)
        (if (consp x) (evenlp (cdr x)) nil)))

     General Form:
     (mutual-recursion def1 ... defn)
     where each defi is a defun form or a defund form.

When mutually recursive functions are introduced it is necessary to do
the termination analysis on the entire clique of definitions.  Each
defun form specifies its own measure, either with the :measure keyword
xarg (see XARGS) or by default to acl2-count.  When a function
in the clique calls a function in the clique, the measure of the
callee's actuals must be smaller than the measure of the caller's
formals -- just as in the case of a simply recursive function.  But
with mutual recursion, the callee's actuals are measured as specified
by the callee's defun while the caller's formals are measured as
specified by the caller's defun.  These two measures may be different
but must be comparable in the sense that o< decreases through calls.

If you want to specify :hints or :guard-hints (see XARGS), you
can put them in the xargs declaration of any of the defun forms, as the
:hints from each form will be appended together, as will the
guard-hints from each form.

You may find it helpful to use a lexicographic order, the idea being to
have a measure that returns a list of two arguments, where the first
takes priority over the second.  Here is an example.

     (include-book "ordinals/lexicographic-ordering" :dir :system)

     (encapsulate
      ()
      (set-well-founded-relation l<) ; will be treated as LOCAL

      (mutual-recursion
       (defun foo (x)
         (declare (xargs :measure (list (acl2-count x) 1)))
         (bar x))
       (defun bar (y)
         (declare (xargs :measure (list (acl2-count y) 0)))
         (if (zp y) y (foo (1- y))))))

The guard analysis must also be done for all of the functions at the
same time.  If any one of the defuns specifies the :verify-guards xarg
to be nil, then guard verification is omitted for all of the functions.

Technical Note: Each defi above must be of the form (defun ...).  In
particular, it is not permitted for a defi to be a form that will
macroexpand into a defun form.  This is because mutual-recursion is
itself a macro, and since macroexpansion occurs from the outside in, at
the time (mutual-recursion def1 ... defk) is expanded the defi have not
yet been.  But mutual-recursion must decompose the defi.  We therefore
insist that they be explicitly presented as defuns or defunds (or a
mixture of these).

Suppose you have defined your own defun-like macro and wish to use it
in a mutual-recursion expression.  Well, you can't.  (!)  But you can
define your own version of mutual-recursion that allows your defun-like
form.  Here is an example.  Suppose you define

     (defmacro my-defun (&rest args) (my-defun-fn args))

where my-defun-fn takes the arguments of the my-defun form and produces
from them a defun form.  As noted above, you are not allowed to write
(mutual-recursion (my-defun ...) ...).  But you can define the macro
my-mutual-recursion so that

     (my-mutual-recursion (my-defun ...) ... (my-defun ...))

expands into (mutual-recursion (defun ...) ... (defun ...)) by applying
my-defun-fn to each of the arguments of my-mutual-recursion.

     (defun my-mutual-recursion-fn (lst)
       (declare (xargs :guard (alistp lst)))

     ; Each element of lst must be a consp (whose car, we assume, is always
     ; MY-DEFUN).  We apply my-defun-fn to the arguments of each element and
     ; collect the resulting list of DEFUNs.

       (cond ((atom lst) nil)
             (t (cons (my-defun-fn (cdr (car lst)))
                      (my-mutual-recursion-fn (cdr lst))))))

     (defmacro my-mutual-recursion (&rest lst)

     ; Each element of lst must be a consp (whose car, we assume, is always
     ; MY-DEFUN).  We obtain the DEFUN corresponding to each and list them
     ; all inside a MUTUAL-RECURSION form.

       (declare (xargs :guard (alistp lst)))
       (cons 'mutual-recursion (my-mutual-recursion-fn lst))).

PROGN    evaluate some events

     Example Form:
     (progn (defun foo (x) x)
            (defmacro my-defun (&rest args)
              (cons 'defun args))
            (my-defun bar (x) (foo x)))

     General form:
     (progn event1 event2 ... eventk)

where k >= 0 and each eventi is a legal embedded event form (see
EMBEDDED-EVENT-FORM).  These events are evaluated in sequence.  A
utility is provided to assist in debugging failures of such execution;
see REDO-FLAT.

NOTE: If the eventi above are not all legal embedded event forms (see
EMBEDDED-EVENT-FORM), consider using er-progn or (with great
care!) progn! instead.

For a related event form that does allows introduction of constraints
and local events, see ENCAPSULATE.

ACL2 does not allow the use of progn in definitions.  Instead, the
macro er-progn can be used for sequencing state-oriented operations;
see ER-PROGN and see STATE.  If you are using
single-threaded objects (see STOBJ) you may wish to define a
version of er-progn that cascades the object through successive
changes.  ACL2's pprogn is the state analogue of such a macro.

If your goal is simply to execute a sequence of top-level forms, for
example a sequence of definitions, consider using ld instead; see
LD.

PROGN!    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).  (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))

Progn! always returns (mv nil nil state).  (Low-level remark for those
interested: This way, we can arrange that the Common Lisp multiple
value returned is the same as the ACL2 multiple value returned, and more
important perhaps, we are guaranteed that progn! returns an error
triple.)

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 compile-flg (see
CERTIFY-BOOK).

     (in-package "ACL2")
     (defstobj st fld)
     (defttag :my-ttag)
     (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 "misc/hacker" :dir :system)
     (with-raw-mode (update-fld 3 *the-live-st*))

REDO-FLAT    redo up through a failure in an encapsulate or progn

When one submits an encapsulate or progn event and one of its
sub-events fails, ACL2 restores its logical world as though the
encapsulate or progn had not been run.  But sometimes one would like to
debug the failure by re-executing all sub-events that succeeded up to
the point of failure, and then re-executing the failed sub-event.  Said
differently, imagine that the top-level encapsulate or progn form, as
well as all such sub-forms, were flattened into a list of events that
were then submitted to ACL2 up to the point of failure.  This would put
us in the state in which the original failed event had failed, so we
could now submit that failed event and try modifying it, or first
proving additional events, in order to get it admitted.

Redo-flat is provided for this purpose.  Consider the following (rather
nonsensical) example, in which the defun of f3 fails (the body is y but
the formal parameter list is (x)).

     (encapsulate
      ()
      (defun f1 (x) x)
      (encapsulate ()
                   (local (defthm hack (equal (car (cons x y)) x))))
      (encapsulate ()
                   (local (defthm hack (equal (+ x y) (+ y x)))))
      (encapsulate ()
                   (make-event '(defun f2 (x) x))
                   (progn (defthm foo (equal x x) :rule-classes nil)
                          (defun f3 (x) y)))
      (defun f4 (x) x)
      (defun f5 (x) y))

After this attempt fails, you can evaluate the following form.

     (redo-flat)

This will first lay down a deflabel event, (deflabel r), so that you
can eventually remove your debugging work with (:ubt! r).  Then the
successful sub-events that preceded the failure will be executed with
proofs skipped (so that this execution is fast).  Then, the failed
event will be executed.  Finally, a :pbt command is executed so that
you can see a summary of the events that executed successfully.

You can eliminate some of the steps above by supplying keyword values,
as follows.

     (redo-flat
      :succ  succ ; Skip the successful sub-events if val is nil.
      :fail  fail ; Skip the failed sub-event if val is nil.
      :label lab  ; Skip deflabel if lab or succ is nil, else use (deflabel lab).
      :pbt   val  ; Skip the final :pbt if val, lab, or succ is nil.
      )

Also, you can avoid skipping proofs for the successful sub-events by
supplying keyword :succ-ld-skip-proofsp with a valid value for
ld-skip-proofsp; see LD-SKIP-PROOFSP.

If you prefer only to see the successful and failed sub-events, without
any events being re-executed, you may evaluate the following form
instead.

     (redo-flat :show t)

For the example above, this command produces the following output.

     List of events (from encapsulate or progn) preceding the failure:

     ((DEFUN F1 (X) X)
      (ENCAPSULATE NIL
                   (LOCAL (DEFTHM HACK (EQUAL (CAR (CONS X Y)) X))))
      (ENCAPSULATE NIL
                   (LOCAL (DEFTHM HACK (EQUAL (+ X Y) (+ Y X)))))
      (MAKE-EVENT '(DEFUN F2 (X) X))
      (DEFTHM FOO (EQUAL X X)
              :RULE-CLASSES NIL))

     Failed event:

     (DEFUN F3 (X) Y)
     ACL2 !>

Redo-flat uses a scheme that should not cause spurious name conflicts
for local events.  Above, it is mentioned that events are "flattened";
now we clarify this notion.  Each sub-event that succeeds and is an
encapsulate or progn is left intact.  Only such events that fail are
replaced by their component events.  Thus, in the example above, there
is no conflict between the two local sub-events named "hack," because
these are contained in successful encapsulate sub-events, which are
therefore not flattened.  The progn and two encapsulate events
surrounding the definition of f3 are, however, flattened, because that
definition failed to be admitted.

Unfortunately, an event must actually fail in order for redo-flat to
work.  So if the system is "stuck" on an event, then you may find it
helpful to insert an illegal event just in front of it before
submitting the encapsulate or progn.

SET-BODY    set the definition body

     Examples:
     (set-body foo (:definition foo)) ; restore original definition of foo
     (set-body foo foo) ; same as just above
     (set-body foo my-foo-def) ; use my-foo-def for the body of foo
     (set-body foo (:definition my-foo-def)) ; same as just above

Rules of class :definition can install a new definition body, used for
example by :expand hints.  See DEFINITION and also see
HINTS for a detailed discussion of the :install-body fields of
:definition rules and their role in :expand hints.

There may be several such definitions, but by default, the latest one
is used by :expand hints.  Although the :with keyword may be used in
:expand hints to override this behavior locally (see HINTS), it
may be convenient to install a definition for expansion other than the
latest one -- for example, the original definition.  Set-body may be
used for this purpose.

     General Form:
     (set-body function-symbol rule-name)

where rule-name is either a :definition rune or is a function symbol,
sym, which represents the rune (:definition sym).

You can view all definitions available for expansion; see
SHOW-BODIES.

SWITCHES-PARAMETERS-AND-MODES-OH-MY    a variety of ways to modify the ACL2 environment

The beginning user might pay special attention to documentation for
logic and program.  Other topics in this section can be read as one
gains familiarity with ACL2.

ADD-BINOP    associate a binary function name with a macro name

     Example:
     (add-binop append binary-append)

This example associates the function symbol binary-append with the
macro name append.  As a result, theory functions will understand that
append refers to binary-append -- see ADD-MACRO-ALIAS -- and
moreover, proof output will be printed using append rather than
binary-append, e.g., (append x y z w) is printed rather than
(binary-append x (binary-append y (binary-append z w))).

     General Form:
     (add-binop macro-name function-name)

This is a convenient way to add an entry to macro-aliases-table and at
the same time extend the :binop-table.  See
MACRO-ALIASES-TABLE, see REMOVE-MACRO-ALIAS, see
BINOP-TABLE, and see REMOVE-BINOP.

ADD-DEFAULT-HINTS    add to the default hints

     Examples:
     (add-default-hints '((computed-hint-1 clause)
                          (computed-hint-2 clause
                                           stable-under-simplificationp)))

Note: This is an event!  It does not print the usual event summary but
nevertheless changes the ACL2 logical world and is so recorded.  It is
local to the book or encapsulate form in which it occurs (see
ADD-DEFAULT-HINTS! for a corresponding non-local event).

     General Form:
     (add-default-hints lst)

where lst is a list.  Generally speaking, the elements of lst should be
suitable for use as computed-hints.

This event is completely analogous to set-default-hints, the difference
being that add-default-hints appends the indicated hints to the list of
default hints, rather than *replacing* the default hints with the
indicated hints.

Finally, note that the effects of set-default-hints, add-default-hints,
and remove-default-hints are local to the book in which they appear.
Thus, users who include a book with such forms will not have their
default hints affected by such forms.  In order to export the effect of
setting the default hints, use set-default-hints!, add-default-hints!,
or remove-default-hints!.

ADD-DEFAULT-HINTS!    add to the default hints non-locally

Please see ADD-DEFAULT-HINTS, which is the same as
add-default-hints!  except that the latter is not local to the
encapsulate or the book in which it occurs.  Probably add-default-hints
is to be preferred unless you have a good reason for wanting to export
the effect of this event outside the enclosing encapsulate or book.

ADD-DIVE-INTO-MACRO    associate proof-checker diving function with macro name

     Examples:
     (add-dive-into-macro cat expand-address-cat)

This feature is used so that the proof-checker's DV command and numeric
diving commands (e.g., 3) will dive properly into subterms.  Please see
DIVE-INTO-MACROS-TABLE.

ADD-INCLUDE-BOOK-DIR    associate directory to keyword for include-book's :dir argument

     Example Form:
     (add-include-book-dir :smith "/u/smith/")
      ; For (include-book "foo" :dir :smith), prepend "/u/smith/" to "foo".

     General Form:
     (add-include-book-dir kwd dir)

where kwd is a keywordp and dir is the absolute pathname (see
PATHNAME) of a directory.  The effect of this event is to modify the
meaning of the :dir keyword argument of include-book as indicated by
the examples above, namely by associating the indicated directory with
the indicated keyword for purposes of the include-book :dir argument.
See DELETE-INCLUDE-BOOK-DIR for how to undo this effect.

Caveat: The keyword :system cannot be redefined.  It will always point
to the absolute pathname of the distributed books directory, which by
default is immediately under the directory where the ACL2 executable
was originally built (see INCLUDE-BOOK, in particular the
discussion there of "books directory").

Note: This is an event!  It does not print the usual event summary but
nevertheless changes the ACL2 logical world and is so recorded.

This macro generates a call (table acl2-defaults-table
:include-book-dir-alist ...)  and hence is local to any books and
encapsulate events in which it occurs. See ACL2-DEFAULTS-TABLE.

ADD-INVISIBLE-FNS    make some unary functions invisible to the loop-stopper algorithm

     Examples:
     (add-invisible-fns binary-+ unary-- foo)

The setting above has makes unary functions unary- and foo "invisible"
for the purposes of applying permutative :rewrite rules to binary-+
trees.  Thus, arg and (unary- arg) will be given the same weight and
will be permuted so as to be adjacent.

     General Form:
     (add-invisible-fns top-fn unary-fn1 ... unary-fnk)

where top-fn is a function symbol and the unary-fni are unary function
symbols.

For more information see INVISIBLE-FNS-TABLE.  Also see
SET-INVISIBLE-FNS-TABLE, which explains how to set the entire table
in a single event, and see REMOVE-INVISIBLE-FNS.

ADD-MACRO-ALIAS    associate a function name with a macro name

     Example:
     (add-macro-alias append binary-append)

This example associates the function symbol binary-append with the
macro name append.  As a result, the name append may be used as a runic
designator (see THEORIES) by the various theory functions.  See
MACRO-ALIASES-TABLE for more details.

     General Form:
     (add-macro-alias macro-name function-name)

This is a convenient way to add an entry to macro-aliases-table.  See
MACRO-ALIASES-TABLE and also see REMOVE-MACRO-ALIAS.

ADD-MATCH-FREE-OVERRIDE    set :match-free value to :once or :all in existing rules

     Example Forms:
     (add-match-free-override :once t)
         ; Try only the first binding of free variables when relieving hypotheses
         ; of any rule of class :rewrite, :linear, or :forward-chaining.
     (add-match-free-override :all (:rewrite foo) (:rewrite bar))
         ; For rewrite rules foo and bar, try all bindings of free variables when
         ; relieving hypotheses.
     (add-match-free-override :clear)
         ; Restore :match-free to what was originally stored for each rule (either
         ; :all or :once).

As described elsewhere (see FREE-VARIABLES), a rewrite, linear,
or forward-chaining rule may have free variables in its hypotheses, and
ACL2 can be directed either to try all bindings (":all") or just the
first (":once") when relieving a hypothesis, as a basis for relieving
subsequent hypotheses.  This direction is generally provided by
specifying either :match-free :once or :match-free :all in the
:rule-classes of the rule, or by using the most recent
set-match-free-default event.  Also see RULE-CLASSES.

However, if a proof is going slowly, you may want to modify the
behavior of some such rules so that they use only the first match for
free variables in a hypothesis when relieving subsequent hypotheses,
rather than backtracking and trying additional matches as necessary.
The event (add-match-free-override :once t) has that effect.  Or at the
other extreme, perhaps you want to specify all rules as :all rules
except for a some specific exceptions.  Then you can execute
(add-match-free-override :all t) followed by, say,
(add-match-free-override :once (:rewrite foo) (:linear bar)).

     General Forms:
     (add-match-free-override :clear)
     (add-match-free-override flg t)
     (add-match-free-override flg rune1 rune2 ... runek)

where flg is :once or :all and the runei are runes.  If :clear is
specified then all rules will have the :all/:once behavior from when
they were first stored.  The second general form causes all rewrite
linear, and forward-chaining rules to have the behavior specified by
flg (:all or :once).  Finally, the last of these, where runes are
specified, is additive in the sense that only the indicated rules are
affected; all others keep the behavior they had just before this event
was executed (possible because of earlier add-match-free-override
events).

At the conclusion of this event, ACL2 prints out the list of all
:linear, :rewrite, and :forward-chaining runes whose rules contain free
variables in hypotheses that are to be bound :once, except that if
there are no overrides (value :clear was used), then :clear is printed.

This event only affects rules that exist at the time it is executed.
Future rules are not affected by the override.

Note: This is an event!  It does not print the usual event summary but
nevertheless changes the ACL2 logical world and is so recorded.  It
uses the acl2-defaults-table, and hence its effect is local to the book
or encapsulate form in which it occurs.

_Remarks_

Lists of the :rewrite, :linear, and :forward-chaining runes whose
behavior was originally :once or :all are returned by the following
forms, respectively.

     (free-var-runes :once (w state))
     (free-var-runes :all  (w state))

The form

     (match-free-override (w state))

evaluates to a pair, whose car is a number used by ACL2 to determine
whether a rune is sufficiently old to be affected by the override, and
whose cdr is the list of runes whose behavior is specified as :once by
add-match-free-override; except, if no runes have been overridden, then
the keyword :clear is returned.

ADD-NTH-ALIAS    associate one symbol with another for printing of nth/update-nth terms

     Example:
     (add-nth-alias st0 st)

This example associates the symbol st0 with the symbol st for purposes
of printing certain terms of the form (nth n st0) and (update-nth n val
st0).

     General Form:
     (add-nth-alias alias-name name)

This is a convenient way to add an entry to nth-aliases-table.  See
NTH-ALIASES-TABLE and also see REMOVE-NTH-ALIAS.

BINOP-TABLE    associates binary function with the corresponding macro

     Examples:
     ACL2 !>(binop-table (w state))
     '((binary-+ . +)
       (binary-* . *)
       (binary-append . append)
       (binary-logand . logand)
       (binary-logior . logior)
       (binary-logxor . logxor)
       (binary-logeqv . logeqv))

See TABLE for a general discussion of tables.

See ADD-BINOP for a more general discussion of this table.