This is documentation for ACL2 Version 3.3
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.

INCLUDE-BOOK    load the events in a file

     Examples:
     (include-book "my-arith")
     (include-book "/home/smith/my-arith")
     (include-book "/../../my-arith")

     General Form:
     (include-book file :load-compiled-file action
                        :uncertified-okp t/nil      ; [default t]
                        :defaxioms-okp t/nil        ; [default t]
                        :skip-proofs-okp t/nil      ; [default t]
                        :ttags ttags                ; [default nil]
                        :dir directory
                        :doc doc-string)

where file is a book name.  See BOOKS for general information,
see BOOK-NAME for information about book names, and see
PATHNAME for information about file names.  Action is one of t, nil,
:warn, :try, :comp-raw, or :comp; these values are explained below, and
the default is :warn unless compilation is suppressed (see
COMPILATION).  The three -okp keyword arguments, which default to t,
determine whether errors or warnings are generated under certain
conditions explained below; when the argument is t, warnings are
generated.  The dir argument, if supplied, is a keyword that represents
an absolute pathname for a directory (see PATHNAME), to be used
instead of the current book directory (see CBD) for resolving
the given file argument to an absolute pathname.  In particular, :dir
:system resolves file using the distributed books/ directory of your
ACL2 installation, unless your ACL2 executable was built somewhere
other than where it currently resides; please see the "Distributed
Books Directory" below.  To define other keywords that can be used for
dir, see ADD-INCLUDE-BOOK-DIR.  Doc-string is an optional
documentation string; see DOC-STRING.  If the book has no
certificate, if its certificate is invalid or if the certificate was
produced by a different version of ACL2, a warning is printed and the
book is included anyway; see CERTIFICATE.  This can lead to
serious errors; see UNCERTIFIED-BOOKS.  If the portcullis of
the certificate (see PORTCULLIS) cannot be raised in the host
logical world, an error is caused and no change occurs to the logic.
Otherwise, the non-local events in file are assumed.  Then the keep of
the certificate is checked to ensure that the correct files were read;
see KEEP.  A warning is printed if uncertified books were
included.  Even if no warning is printed, include-book places a burden
on you; see CERTIFICATE.

The value, action, of :load-compiled-file is coerced to nil if explicit
compilation is suppressed (see COMPILATION), presumably because
the host Lisp implementation automatically compiles on the fly.  The
remainder of this paragraph assumes that explicit compilation is not
suppressed.  We also mention here a special value :comp! for action,
which is treated exactly as described for :comp below (and hence is not
mentioned further), except that if a compiled file already exists then
it is deleted before any action described below.  We now describe the
effect of action under the above assumptions.  If there is a compiled
file for the book that was created more recently than the book itself
and the value, action, of the :load-compiled-file argument is not nil,
or is omitted, then the compiled file is automatically loaded;
otherwise it is not loaded.  If the compiled file is not loaded, then
an error will occur if action is t; if action is :warn (the default)
then a warning will be printed; if action is :try then no warning will
be printed; and if action is :comp (or :comp!) then the file will be
immediately compiled and loaded.  In this case, :comp (likewise,
:comp!) causes a file to be compiled that includes executable
counterparts, in analogy to default value t for the compile-flg
argument of certify-book (see CERTIFY-BOOK).  The action
:comp-raw is handled just like :comp, with two exceptions: compilation
may be skipped if it is not needed, and executable counterparts are not
also compiled.  Certify-book can also be used to compile a book; thus,
:comp-raw and :comp do the same sort of compilation for include-book as
is done by certify-book when the latter is given a compile-flg of :raw
or t, respectively.  An effect of compilation is to speed up the
execution of the functions defined within the book when those functions
are applied to specific values.  Compilation can also remove tail
recursion, thus avoiding stack overflows.  The presence of compiled
code for the functions in the book should not otherwise affect the
performance of ACL2.  See GUARD for a discussion.  NOTES: (1)
The :load-compiled-file argument is not recursive; that is, calls of
include-book that are inside the book supplied to include-book will use
their own :load-compiled-file arguments (default :warn), not the
:load-compiled-file argument for the enclosing book.  (2) Only
functions defined non-redundantly in the book (and their executable
counterparts in circumstances as described above) are compiled, not
functions defined in sub-books or in the certification world (see
PORTCULLIS).

The three -okp arguments, :uncertified-okp, defaxioms-okp, and
skip-proofs-okp, determine the system's behavior when the book or any
subbook is found to be uncertified, when the book or any subbook is
found to contain defaxiom events, and when the book or any subbook is
found to contain skip-proofs events, respectively.  All three default
to t, which means it is "ok" for the condition to arise.  In this case,
a warning is printed but the processing to load the book is allowed to
proceed.  When one of these arguments is nil and the corresponding
condition arises, an error is signaled and processing is aborted.
*Exception*: :uncertified-okp is ignored if the include-book is being
performed on behalf of a certify-book.

The keyword argument :ttags may normally be omitted.  A few constructs,
used for example if you are building your own system based on ACL2, may
require it.  See DEFTTAG for an explanation of this argument.

Include-book is similar in spirit to encapsulate in that it is a single
event that "contains" other events, in this case the events listed in
the file named.  Include-book processes the non-local event forms in
the file, assuming that each is admissible.  Local events in the file
are ignored.  You may use include-book to load several books, creating
the logical world that contains the definitions and theorems of all of
them.

If any non-local event of the book attempts to define a name that has
already been defined -- and the book's definition is not syntactically
identical to the existing definition -- the attempt to include the book
fails, an error message is printed, and no change to the logical world
occurs.  See REDUNDANT-EVENTS for the details.

When a book is included, the default defun-mode (see
DEFAULT-DEFUN-MODE) for the first event is always :logic.  That is,
the default defun-mode "outside" the book -- in the environment in
which include-book was called -- is irrelevant to the book.  Events
that change the defun-mode are permitted within a book (provided they
are not in local forms).  However, such changes within a book are not
exported, i.e., at the conclusion of an include-book, the "outside"
default defun-mode is always the same as it was before the include-book.

Unlike every other event in ACL2, include-book puts a burden on you.
Used improperly, include-book can be unsound in the sense that it can
create an inconsistent extension of a consistent logical world.  A
certification mechanism is available to help you carry this burden --
but it must be understood up front that even certification is no
guarantee against inconsistency here.  The fundamental problem is one
of file system security.  See CERTIFICATE for a discussion of
the security issues.

After execution of an include-book form, the value of
acl2-defaults-table is restored to what it was immediately before that
include-book form was executed.  See ACL2-DEFAULTS-TABLE.

Distributed Books Directory.  We refer to the "books directory" of an
executable image as the full pathname string of the books directory
associated with :dir :system for that image.  This is where the
distributed books directory should reside.  By default, it is the books/
subdirectory of the directory where the sources reside and the
executable image is thus built (except for ACL2(r) -- see REAL
--, where it is books/nonstd/).  If those books reside elsewhere, the
environment variable ACL2_SYSTEM_BOOKS can be set to the books/
directory under which they reside (a Unix-style pathname, typically
ending in books/ or books, is permissible).  In most cases, your ACL2
executable is a small script in which you can set this environment
variable just above the line on which the actual ACL2 image is invoked,
for example:

     export ACL2_SYSTEM_BOOKS
     ACL2_SYSTEM_BOOKS=/home/acl2/v3-2/acl2-sources/books

This concludes the guided tour through books.  See
SET-COMPILE-FNS for a subtle point about the interaction between
include-book and on-the-fly compilation.  See CERTIFY-BOOK for
a discussion of how to certify a book.

:cited-by Programming

LOCAL    hiding an event in an encapsulation or book

     Examples:
     (local (defthm hack1
              (implies (and (acl2-numberp x)
                            (acl2-numberp y)
                            (equal (* x y) 1))
                       (equal y (/ x)))))

     (local (defun double-naturals-induction (a b)
              (cond ((and (integerp a) (integerp b) (< 0 a) (< 0 b))
                     (double-naturals-induction (1- a) (1- b)))
                    (t (list a b)))))

     General Form:
     (local ev)

where ev is an event form.  If the current default defun-mode (see
DEFAULT-DEFUN-MODE) is :logic and ld-skip-proofsp is nil or t,
then (local ev) is equivalent to ev.  But if the current default
defun-mode is :program or if ld-skip-proofsp is 'include-book, then
(local ev) is a no-op.  Thus, if such forms are in the event list of an
encapsulate event or in a book, they are processed when the
encapsulation or book is checked for admissibility in :logic mode but
are skipped when extending the host world.  Such events are thus
considered "local" to the verification of the encapsulation or book.
The non-local events are the ones "exported" by the encapsulation or
book.  See ENCAPSULATE for a thorough discussion.  Also see
LOCAL-INCOMPATIBILITY for a discussion of a commonly
encountered problem with such event hiding:  you can't make an event
local if its presence is required to make sense of a non-local one.

Note that events that change the default defun-mode, and in fact any
events that set the acl2-defaults-table, are disallowed inside the
scope of local.  See EMBEDDED-EVENT-FORM.

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.

Finally, we note that ACL2 extends the notion of "make-event expansion"
to the case that a call of make-event is found in the course of
macroexpansion.  We illustrate with the following example.

     (encapsulate
      ()
      (defmacro my-mac ()
        '(make-event '(defun foo (x) x)))
      (my-mac))
     :pe :here

The above call of pe shows that the form (my-mac) has a make-event
expansion of (DEFUN FOO (X) X):

     (ENCAPSULATE NIL
                  (DEFMACRO MY-MAC
                            NIL
                            '(MAKE-EVENT '(DEFUN FOO (X) X)))
                  (RECORD-EXPANSION (MY-MAC)
                                    (DEFUN FOO (X) X)))

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

However, the following form may be preferable (see PROGN!):

     (progn! :state-global-bindings <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.

MEMOIZE    turn on memoization for one function

This documentation topic relates to an experimental extension of ACL2
under development by Bob Boyer and Warren Hunt.  See
HONS-AND-MEMOIZATION for a general discussion of memoization and the
related features of hash consing and applicative hash tables.

     Examples:
     (memoize 'foo)                      ; remember the values of calls
                                         ; of foo
     (memoize 'foo :condition t)         ; same as above
     (memoize 'foo :condition '(test x)) ; memoize for args satisfying
                                         ; condition
     (memoize 'foo :condition 'test-fn)  ; memoize for args satisfying
                                         ; test-fn
     (memoize 'foo :inline nil)          ; do not inline the definition
                                         ; of foo

     * Menu:

     Related topics other than immediate subtopics:
     * HONS-AND-MEMOIZATION:: hash cons, function memoization, and applicative hash tables

     General Form:
     (memoize fn                         ; memoizes fn and returns fn
              :condition    condition    ; optional (default t)
              :condition-fn condition-fn ; optional
              :hints        hints        ; optional
              :otf-flg      otf-flg      ; optional
              :inline       inline       ; optional (default t)
              )

where fn evaluates to a user-defined function symbol; condition is
either t (the default) or 't or else evaluates to an expression whose
free variables are among the formal parameters of fn; condition-fn is
either nil (the default) or else evaluates to a legal function symbol.
Further restrictions are discussed below.

Generally fn must evaluate to a defined function symbol whose guards
have been verified.  However, this value can be the name of a macro
that is associated with such a function symbol; see
MACRO-ALIASES-TABLE.  That associated function symbol is the one
called "memoized" in the discussion below, but we make no more mention
of this subtlety.

It is illegal to memoize a function that is already memoized.  To turn
off memoization, see UNMEMOIZE.

In the most common case, memoize takes a single argument, which
evaluates to a function symbol.  We call this function symbol the
"memoized function" because "memos" are saved and re-used, in the
following sense.  When a call of the memoized function is evaluated,
the result is "memoized" by associating the call's arguments with that
result, in a suitable table.  But first an attempt is made to avoid
such evaluation, by doing a lookup in that table on the given arguments
for the result, as stored for a previous call on those arguments.  If
such a result is found, then it is returned without further
computation.  This paragraph also applies if :condition is supplied but
is t or 't.

If in addition :condition-fn is supplied, but :condition is not, then
the result of evaluating :condition-fn must be a defined function
symbol whose guards have been verified and whose formal parameter list
is the same as for the function being memoized.  Such a "condition
function" will be run whenever the memoized function is called, on the
same parameters, and the lookup or table store described above are only
performed if the result from the condition function call is non-nil.

If however :condition is supplied, then an attempt will be made to
define a condition function whose guard and formal parameters list are
the same as those of the memoized function, and whose body is the
result, r, of evaluating the given condition.  The name of that
condition function is the result of evaluating :condition-fn if
supplied, else is the result of concatenating the string
"-MEMOIZE-CONDITION" to the end of the name of the memoized function.
The condition function will be defined with guard verification turned
off, but that definition will be followed immediately by a
verify-guards event; and this is where the optional :hints and :otf-flg
are attached.  At evaluation time the condition function is used as
described in the preceding paragraph; so in effect, the condition (r,
above) is evaluated, with its variables bound to the corresponding
actuals of the memoized function call, and the memoized function
attempts a lookup or table store if and only if the result of that
evaluation is non-nil.

Calls of this macro generate events of the form (table memoize-table fn
(list condition-fn inline)).  When successful, the returned value is of
the form (mv nil function-symbol state).

When :inline has value nil, then memoize does not use the definitional
body of fn in the body of the new, memoized definition of fn.  Instead,
memoize lays down a call to the symbol-function for fn that was in
effect prior to memoization.  Use value t for :inline to avoid memoizing
recursive calls to fn directly from within fn.

If :trace has value t, then memoize also traces in the traditional Lisp
style.

Memoize works for functions that have stobj arguments or return stobj
values.  However, in some cases the memoized version of the function
may execute much less inefficiently than the unmemoized version.

Memoize causes an error if fn uses state as an explicit parameter.

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

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-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)
             (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 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*))