This is documentation for ACL2 Version 5.0
Copyright (C) 2012  University of Texas at Austin

This program is free software; you can redistribute it and/or modify
it under the terms of Version 2 of the GNU General Public License as
published by the Free Software Foundation.

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.

WELL-FOUNDED-RELATION    show that a relation is well-founded on a set

See RULE-CLASSES for a general discussion of rule classes and
how they are used to build rules from formulas.  An example :corollary
formula from which a :well-founded-relation rule might be built is as
follows.  (Of course, the functions pairp, lex2p, and ordinate would
have to be defined first.)

     Example:
     (and (implies (pairp x) (o-p (ordinate x)))
          (implies (and (pairp x)
                        (pairp y)
                        (lex2p x y))
                   (o< (ordinate x) (ordinate y))))

The above example establishes that lex2p is a well-founded relation on
pairps.  We explain and give details below.

Exactly two general forms are recognized:

     General Forms
     (AND (IMPLIES (mp x) (O-P (fn x)))              ; Property 1
          (IMPLIES (AND (mp x)                       ; Property 2
                        (mp y)
                        (rel x y))
                   (O< (fn x) (fn y)))),

or

     (AND (O-P (fn x))                               ; Property 1
          (IMPLIES (rel x y)                         ; Property 2
                   (O< (fn x) (fn y))))

where mp, fn, and rel are function symbols, x and y are distinct
variable symbols, and no other :well-founded-relation theorem about fn
has been proved.  When the second general form is used, we act as
though the first form were used with mp being the function that ignores
its argument and returns t.  The discussion below therefore considers
only the first general form.

Note: We are very rigid when checking that the submitted formula is of
one of these forms.  For example, in the first form, we insist that all
the conjuncts appear in the order shown above.  Thus, interchanging the
two properties in the top-level conjunct or rearranging the hyptheses
in the second conjunct both produce unrecognized forms.  The
requirement that each fn be proved well-founded at most once ensures
that for each well-founded relation, fn, there is a unique mp that
recognizes the domain on which rel is well-founded.  We impose this
requirement simply so that rel can be used as a short-hand when
specifying the well-founded relations to be used in definitions;
otherwise the specification would have to indicate which mp was to be
used.

We also insist that the new ordering be embedded into the ordinals as
handled by o-p and o< and not some into previously admitted user-defined
well-founded set and relation.  This restriction should pose no
hardship.  If mp and rel were previously shown to be well-founded via
the embedding fn, and you know how to embed some new set and relation
into mp and rel, then by composing fn with your new embedding and using
the previously proved well-founded relation lemma you can embed the new
set and relation into the ordinals.

Mp is a predicate that recognizes the objects that are supposedly
ordered in a well-founded way by rel.  We call such an object an
"mp-measure" or simply a "measure" when mp is understood.  Property 1
tells us that every measure can be mapped into an ACL2 ordinal.  (See
O-P.)  This mapping is performed by fn.  Property 2 tells us
that if the measure x is smaller than the measure y according to rel
then the image of x under fn is a smaller than that of y, according to
the well-founded relation o<.  (See O<.)  Thus, the general
form of a :well-founded-relation formula establishes that there exists a
rel-order preserving embedding (namely via fn) of the mp-measures into
the ordinals.  We can thus conclude that rel is well-founded on
mp-measures.

Such well-founded relations are used in the admissibility test for
recursive functions, in particular, to show that the recursion
terminates.  To illustrate how such information may be used, consider a
generic function definition

     (defun g (x) (if (test x) (g (step x)) (base x))).

If rel has been shown to be well-founded on mp-measures, then g's
termination can be ensured by finding a measure, (m x), with the
property that m produces a measure:

     (mp (m x)),                                     ; Defun-goal-1

and that the argument to g gets smaller (when measured by m and
compared by rel) in the recursion,

     (implies (test x) (rel (m (step x)) (m x))).    ; Defun-goal-2

If rel is selected as the :well-founded-relation to be used in the
definition of g, the definitional principal will generate and attempt
to prove defun-goal-1 and defun-goal-2 to justify g.  We show later why
these two goals are sufficient to establish the termination of g.
Observe that neither the ordinals nor the embedding, fn, of the
mp-measures into the ordinals is involved in the goals generated by the
definitional principal.

Suppose now that a :well-founded-relation theorem has been proved for
mp and rel.  How can rel be "selected as the :well-founded-relation" by
defun?  There are two ways.  First, an xargs keyword to the defun event
allows the specification of a :well-founded-relation.  Thus, the
definition of g above might be written

     (defun g (x)
      (declare (xargs :well-founded-relation (mp . rel)))
      (if (test x) (g (step x)) (base x)))

Alternatively, rel may be specified as the
:default-well-founded-relation in acl2-defaults-table by executing the
event

     (set-well-founded-relation rel).

When a defun event does not explicitly specify the relation in its
xargs the default relation is used.  When ACL2 is initialized, the
default relation is o<.

Finally, though it is probably obvious, we now show that defun-goal-1
and defun-goal-2 are sufficient to ensure the termination of g provided
property-1 and property-2 of mp and rel have been proved.  To this end,
assume we have proved defun-goal-1 and defun-goal-2 as well as
property-1 and property-2 and we show how to admit g under the
primitive ACL2 definitional principal (i.e., using only the ordinals).
In particular, consider the definition event

     (defun g (x)
      (declare (xargs :well-founded-relation o<
                      :measure (fn (m x))))
      (if (test x) (g (step x)) (base x)))

Proof that g is admissible:  To admit the definition of g above we must
prove

     (o-p (fn (m x)))                        ; *1

and

     (implies (test x)                               ; *2
              (o< (fn (m (step x))) (fn (m x)))).

But *1 can be proved by instantiating property-1 to get

     (implies (mp (m x)) (o-p (fn (m x)))),

and then relieving the hypothesis with defun-goal-1, (mp (m x)).

Similarly, *2 can be proved by instantiating property-2 to get

     (implies (and (mp (m (step x)))
                   (mp (m x))
                   (rel (m (step x)) (m x)))
              (o< (fn (m (step x))) (fn (m x))))

and relieving the first two hypotheses by appealing to two instances of
defun-goal-1, thus obtaining

     (implies (rel (m (step x)) (m x))
              (o< (fn (m (step x))) (fn (m x)))).

By chaining this together with defun-goal-2,

     (implies (test x)
              (rel (m (step x)) (m x)))

we obtain *2.  Q.E.D.

SERIALIZE    routines for saving ACL2 objects to files, and later restoring them

This documentation topic relates to an experimental extension of ACL2
that supports hons, memoization, and fast alists.  See
HONS-AND-MEMOIZATION.  Thanks to Jared Davis for contributing the
"serialization" routines for saving ACL2 objects in files for later
loading.

We implement some routines for writing arbitrary ACL2 objects to files,
and for loading those files later.  We usually call these ".sao" files,
which stands for (S)erialized (A)CL2 (O)bject.

Our serialization scheme uses a compact, binary format that preserves
structure sharing in the original object.  We optimize for read
performance.

SERIALIZE-ALTERNATIVES    alternatives to the serialize routines

Hons users could previously use the routines compact-print-file and
compact-read-file.  These are deprecated and are no longer built into
ACL2.  However, they are still available by loading the new system book,
serialize/compact-print.  Note that loading this book requires a ttag,
and these routines are still only available in raw lisp.

Another predecessor of the serialization routines were hons archives,
which are still available in the hons-archive library.  The
serialization routines are generally better and we recommend against
using hons archives for new projects.

SERIALIZE-IN-BOOKS    using serialization efficiently in books

Our serialize scheme was developed in order to allow very large ACL2
objects to be loaded into books.  Ordinarily this is carried out using
serialize-read within a make-event, e.g.,

       (make-event (mv-let (obj state)
                           (serialize-read "my-file")
                           (value `(defconst *my-file* ',obj))))

But this scheme is not particularly efficient.

During certify-book, the actual call of serialize-read is carried out,
and this is typically pretty fast.  But then a number of possibly
inefficient things occur.

     - The ACL2 function bad-lisp-object is run on the resulting
     object.  This is memoized for efficiency, but may still take
     considerable time when the file is very large.

     - The checksum of the resulting object is computed.  This is also
     memoized, but as before may still take some time.

     - The object that was just read is then written into book.cert,
     essentially with serialize-write.  This can take some time, and
     results in large certifiate files.

Then, during include-book, the make-event expansion of is loaded.  This
is now basically just a serialize-read.

The moral of the story is that using serialize will only help your
certify-book time, and it only impacts a portion of the overall time.

To avoid this overhead, we have developed an UNSOUND alternative to
serialize-read, which is available only by loading an additional book.
So, if the above scheme is not performing well for you, you may wish to
see the book serialize/unsound-read.

SERIALIZE-READ    read a serialized ACL2 object from a file

General form:

      (serialize-read filename
                      [:hons-mode {:always, :never, :smart}]   ; :smart by default
                      [:verbosep  {t, nil}])                   ; nil by default
       -->
      (mv obj state)

In the logic this is an oracle read.

Under the hood, we try to read and return a serialized object form a
file that was presumably created by serialize-write.  On success we
return the contents of the file.  Any failures (e.g., file not found,
bad file contents, etc.) will result in a hard Lisp error.

The filename should be a string that gives the path to the file.

The hons-mode controls how whether to use hons or cons to restore the
object.  The default mode is :smart, which means that conses that were
normed at the time of the file's creation should be restored with hons.
But you can override this and insist that hons is to :always or :never
be used, instead.

Why would you use :never?  If your object previously had a lot of
honses, but you no longer have any need for them to be normed, then
using :never may sometimes be a lot faster since it can avoid hons
calls.  On the other hand, if you are going to hons-copy some part of
the file's contents, then it is likely faster to use :smart or :always
instead of first creating normal conses and then copying them to build
honses.

The :verbosep flag just controls whether to print some low-level details
related to timing and memory usage as the file is being read.

SERIALIZE-WRITE    write an ACL2 object into a file

General form:

      (serialize-write filename obj
                       [:verbosep  {t, nil}])    ; nil by default
       -->
      state

In the logic this carries out an oracle read.

Under the hood, we try to save obj into the file indicated by filename,
which must be a string.  The object can later be recovered with
serialize-read.  We just return state, and any failures (e.g., file not
openable) will result in a hard Lisp error.

Writing objects to disk is generally slower than reading them back in
since some analysis is required to convert an object into our
serialized object format.

The verbosep flag just says whether to print some low-level details
related to timing and memory usage as the file is being read.

SET-SERIALIZE-CHARACTER    See WITH-SERIALIZE-CHARACTER.

WITH-SERIALIZE-CHARACTER    control output mode for print-object$

This documentation topic relates to an experimental extension of ACL2
that supports hons, memoization, and fast alists.  See
HONS-AND-MEMOIZATION.  See SERIALIZE for a discussion of
"serialization" routines, contributed by Jared Davis for saving ACL2
objects in files for later loading.

The expression (with-serialize-character char form) evaluates to the
value of form, but with the serialize-character of the state assigned to
char, which should be one of nil, #Y, or #Z.  We describe the effect of
that assignment below.  But note that if you are doing this because of
one or more specific calls of print-object$, such as (print-object$ x
channel state), then you may wish instead to evaluate
(print-object$-ser x serialize-character channel state), in which case
you will not need to use with-serialize-character.  (Note however that
serialize-character is treated as nil for other than a HONS version.)

     General forms:
     (with-serialize-character nil form)
     (with-serialize-character #Y form)
     (with-serialize-character #Z form)

where form should evaluate to an error triple, i.e. a result of the form
(mv erp val state) where erp and val are ordinary (non-stobj) values.

Note that if you prefer to obtain the same behavior (as described below)
globally, rather than only within the scope of with-serialize-character,
then use set-serialize-character in a corresponding manner:

     (set-serialize-character nil state)
     (set-serialize-character #Y state)
     (set-serialize-character #Z state)

In each case above, calls of print-object$ (see IO) in form will
produce an object that can be read by the HONS version of ACL2.  In the
first case, that object is printed as one might expect at the terminal,
as an ordinary Lisp s-expression.  But in the other cases, the object
is printed by first laying down either #Y or #Z (as indicated) and then
calling serialize-write (or more precisely, the underlying function
called by serialize-write that prints to a stream).

Consider what happens when the ACL2 reader encounters an object
produced as described above (in the #Y or #Z case).  When the object
was written, information was recorded on whether that object was a
hons.  In the case of #Z, the object will be read as a hons if and only
if it was originally written as a hons.  But in the case of #Y, it will
never be read as a hons.  Thus, #Y and #Z will behave the same if the
original written object was not a hons, creating an object that is not
a hons.  For an equivalent explanation and a bit more discussion, see
SERIALIZE-READ, in particular the discussion of the hons-mode.
The value :smart described there corresponds to #Z, while :never
corresponds to #Y.

STOBJ    single-threaded objects or "von Neumann bottlenecks"

In ACL2, a "single-threaded object" is a data structure whose use is so
syntactically restricted that only one instance of the object need ever
exist and its fields can be updated by destructive assignments.

Note: Novices are advised to avoid using single-threaded objects,
perhaps instead using distributed book
books/data-structures/structures.lisp.  At the least, consider using
(set-verify-guards-eagerness 0) to avoid guard verification.

The documentation in this section is laid out in the form of a tour that
visits the documented topics in a reasonable order.  We recommend that
you follow the tour the first time you read about stobjs.  The list of
all stobj topics is shown below.  The tour starts immediately
afterwards.  Also see DEFSTOBJ and, for so-called abstract
stobjs, see DEFABSSTOBJ.

Related topics other than immediate subtopics:

As noted, a "single-threaded object" is a data structure whose use is so
syntactically restricted that only one instance of the object need ever
exist.  Updates to the object must be sequentialized.  This allows us to
update its fields with destructive assignments without wrecking the
axiomatic semantics of update-by-copy.  For this reason,
single-threaded objects are sometimes called "von Neumann bottlenecks."

From the logical perspective, a single-threaded object is an ordinary
ACL2 object, e.g., composed of integers and conses.  Logically
speaking, ordinary ACL2 functions are defined to allow the user to
"access" and "update" its fields.  Logically speaking, when fields in
the object, obj, are "updated" with new values, a new object, obj', is
constructed.

But suppose that by syntactic means we could ensure that there were no
more references to the "old" object, obj.  Then we could create obj' by
destructively modifying the memory locations involved in the
representation of obj.  The syntactic means is pretty simple but
draconian: the only reference to obj is in the variable named OBJ.

The consequences of this simple rule are far-reaching and require some
getting used to.  For example, if OBJ has been declared as a
single-threaded object name, then the following consequences ensue (but
see the discussion of congruent stobjs below for a slight relaxation).

o OBJ is a top-level global variable that contains the current object,
obj.

o If a function uses the formal parameter OBJ, the only "actual
expression" that can be passed into that slot is the variable OBJ, not
merely a term that "evaluates to an obj"; thus, such functions can only
 operate on the current object.  So for example, instead of   (FOO
(UPDATE-FIELD1 3 ST)) write   (LET ((ST (UPDATE-FIELD1 3 ST))) (FOO
ST)).

o The accessors and updaters have a formal parameter named OBJ, thus,
those functions can only be applied to the current object.

o The ACL2 primitives, such as CONS, CAR and CDR, may not be   applied
to the variable OBJ.  Thus, for example, obj may not be consed   into a
list (which would create another pointer to it) or accessed or   copied
via "unapproved" means.

o The updaters return a "new OBJ object", i.e., obj'; thus, when   an
updater is called, the only variable which can hold its result is   OBJ.

o If a function calls an OBJ updater, it must return an OBJ object
(either as the sole value returned, or in (mv ... OBJ ...); see
MV).

o When a top-level expression involving OBJ returns an OBJ object,
that object becomes the new current value of OBJ.

What makes ACL2 different from other functional languages supporting
such operations (e.g., Haskell's "monads" and Clean's "uniqueness type
system") is that ACL2 also gives single-threaded objects an explicit
axiomatic semantics so that theorems can be proved about them.  In
particular, the syntactic restrictions noted above are enforced only
when single-threaded objects are used in function definitions (which
might be executed outside of the ACL2 read-eval-print loop in Common
Lisp).  The accessor and update functions for single-threaded objects
may be used without restriction in formulas to be proved.  Since
function evaluation is sometimes necessary during proofs, ACL2 must be
able to evaluate these functions on logical constants representing the
object, even when the constant is not "the current object."  Thus, ACL2
supports both the efficient von Neumann semantics and the clean
applicative semantics, and uses the first in contexts where execution
speed is paramount and the second during proofs.

Defstobj and defabsstobj events introduce stobjs.  See DEFSTOBJ
for more details about stobjs.  In particular, a relatively advanced
notion of "congruent stobjs" is discussed there.  The idea is to allow
a stobj, st2, of the same "shape" as a given stobj, st1, to be used in
place of st1.  Other defstobj keywords allow inlining and renaming of
stobj accessors and updaters.

But we are getting ahead of ourselves.  To start the stobj tour, see
STOBJ-EXAMPLE-1.

DECLARE-STOBJS    declaring a formal parameter name to be a single-threaded object

When a defun uses one of its formals as a single-threaded object
(stobj), the defun _must_ include a declaration that the formal is to
be so used.  An exception is the formal "state," which if not declared
as explained below, may still be used provided an appropriate global
"declaration" is issued: see SET-STATE-OK.

If the formal in question is counters then an appropriate declaration is

     (declare (xargs :stobjs counters))

or, more generally,

     (declare (xargs :stobjs (... counters ...)))

where all the single-threaded formals are listed.

For such a declaration to be legal it must be the case that all the
names have previously been defined as single-threaded objects with
defstobj.

When an argument is declared to be single-threaded the guard of the
function is augmented by conjoining to it the condition that the
argument satisfy the recognizer for the single-threaded object.
Furthermore, the syntactic checks done to enforce the legal use of
single-threaded objects are also sufficient to allow these guard
conjuncts to be automatically proved.

The obvious question arises:  Why does ACL2 insist that you declare
stobj names before using them in defuns if you can only declare names
that have already been defined with defstobj?  What would go wrong if a
formal were treated as a single-threaded object if and only if it had
already been so defined?

Suppose that one user, say Jones, creates a book in which counters is
defined as a single-threaded object.  Suppose another user, Smith,
creates a book in which counters is used as an ordinary formal
parameter.  Finally, suppose a third user, Brown, wishes to use both
books.  If Brown includes Jones' book first and then Smith's, then
Smith's function treats counters as single-threaded.  But if Brown
includes Smith's book first, the argument is treated as ordinary.

ACL2 insists on the declaration to ensure that the definition is
processed the same way no matter what the context.

RESIZE-LIST    list resizer in support of stobjs

(Resize-list lst n default-value) takes a list, lst, and a desired
length, n, for the result list, as well as a default-value to use for
the extra elements if n is greater than the length of lst.

Resize-list has a guard of t.  This function is called in the body of
function, resize-<a> where <a> is an array field of a stobj.  See
STOBJ and see DEFSTOBJ.

STOBJ-EXAMPLE-1    an example of the use of single-threaded objects

Suppose we want to sweep a tree and (1) count the number of interior
nodes, (2) count the number of tips and (3) keep a record of every tip
we encounter that is an integer.  We could use a single-threaded object
as our "accumulator".  Such an object would have three fields, one
holding the number of nodes seen so far, one holding the number of
tips, and one holding all the integer tips seen.

The following event declares counters to be a single-threaded object.

     (defstobj counters
       (NodeCnt     :type integer :initially 0)
       (TipCnt      :type integer :initially 0)
       (IntTipsSeen :type t       :initially nil))

It has three fields, NodeCnt, TipCnt, and IntTipsSeen.  (As always in
ACL2, capitalization is irrelevant in simple symbol names, so the first
name could be written nodecnt or NODECNT, etc.) Those are the name of
the accessor functions for the object.  The corresponding update
functions are named update-NodeCnt, update-TipCnt and
update-IntTipsSeen.

If you do not like the default function names chosen above, there is a
feature in the defstobj event that allows you to specify other names.

If you want to see the ACL2 definitions of all the functions defined by
this event, look at stobj-example-1-defuns.

If, after this event, we evaluate the top-level "global variable"
counters in the ACL2 read-eval-print loop we get:

     ACL2 !>counters
     <counters>

Note that the value printed is "<counters>".  Actually, the value of
counters in the logic is (0 0 NIL).  But ACL2 always prints
single-threaded objects in this non-informative way because they are
usually so big that to do otherwise would be unpleasant.

Had you tried to evaluate the "global variable" counters before
declaring it a single-threaded object, ACL2 would have complained that
it does not support global variables.  So a lesson here is that once
you have declared a new single-threaded object your top-level forms can
reference it.  In versions of ACL2 prior to Version  2.4 the only
variable enjoying this status was STATE.  single-threaded objects are a
straightforward generalization of the long-implemented von Neumann
state feature of ACL2.

We can access the fields of counters as with:

     ACL2 !>(NodeCnt counters)
     0
     ACL2 !>(IntTipsSeen counters)
     NIL

and we can set the fields of counters as with:

     ACL2 !>(update-NodeCnt 3 counters)
     <counters>
     ACL2 !>(NodeCnt counters)
     3

Observe that when we evaluate an expression that returns a counter
object, that object becomes the "current value" of counters.

Here is a function that "converts" the counters object to its
"ordinary" representation:

     (defun show-counters (counters)
       (declare (xargs :stobjs (counters)))
       (list (NodeCnt counters)
             (TipCnt counters)
             (IntTipsSeen counters)))

Observe that we _must_ declare, at the top of the defun, that we mean
to use the formal parameter counters as a single-threaded object!  If
we did not make this declaration, the body of show-counters would be
processed as though counters were an ordinary object.  An error would
be caused because the accessors used above cannot be applied to
anything but the single-threaded object counters.  If you want to know
why we insist on this declaration, see DECLARE-STOBJS.

When show-counters is admitted, the following message is printed:

     Since SHOW-COUNTERS is non-recursive, its admission is trivial.  We
     observe that the type of SHOW-COUNTERS is described by the theorem
     (AND (CONSP (SHOW-COUNTERS COUNTERS))
          (TRUE-LISTP (SHOW-COUNTERS COUNTERS))).
     We used primitive type reasoning.

     (SHOW-COUNTERS COUNTERS) => *.

     The guard conjecture for SHOW-COUNTERS is trivial to prove.
     SHOW-COUNTERS is compliant with Common Lisp.

The line above containing the "=>" is called the "signature" of
show-counters; it conveys the information that the first argument is
the single-threaded object counters and the only result is an ordinary
object.  Here is an example of another signature:

     (PROCESSOR * * COUNTERS) => (MV * COUNTERS)

which indicates that the function PROCESSOR (which we haven't shown
you) takes three arguments, the third of which is the COUNTERS stobj,
and returns two results, the second of which is the modified COUNTERS.

Returning to the admission of show-counters above, the last sentence
printed indicates that the guard conjectures for the function were
proved.  When some argument of a function is declared to be a
single-threaded object via the xargs :stobj, we automatically add
(conjoin) to the guard the condition that the argument satisfy the
recognizer for that single-threaded object.  In the case of
show-counters the guard is (countersp counters).

Here is an example of show-counters being called:

     ACL2 !>(show-counters counters)
     (3 0 NIL)

This is what we would see had we set the NodeCnt field of the initial
value of counters to 3, as we did earlier in this example.

We next wish to define a function to reset the counters object.  We
could define it this way:

     (defun reset-counters (counters)
       (declare (xargs :stobjs (counters)))
       (let ((counters (update-NodeCnt 0 counters)))
         (let ((counters (update-TipCnt 0 counters)))
           (update-IntTipsSeen nil counters))))

which "successively" sets the NodeCnt field to 0, then the TipCnt field
to 0, and then the IntTipsSeen field to nil and returns the resulting
object.

However, the nest of let expressions is tedious and we use this
definition instead.  This definition exploits a macro, here named "seq"
(for "sequentially") which evaluates each of the forms given, binding
their results successively to the stobj name given.

     (defun reset-counters (counters)
       (declare (xargs :stobjs (counters)))
       (seq counters
            (update-NodeCnt 0 counters)
            (update-TipCnt 0 counters)
            (update-IntTipsSeen nil counters)))

This definition is syntactically identical to the one above, after macro
expansion.  Our definition of seq is shown below and is not part of
native ACL2.

     (defmacro seq (stobj &rest rst)
       (cond ((endp rst) stobj)
             ((endp (cdr rst)) (car rst))
             (t `(let ((,stobj ,(car rst)))
                  (seq ,stobj ,@(cdr rst))))))

The signature printed for reset-counters is

     (RESET-COUNTERS COUNTERS) => COUNTERS.

Here is an example.

     ACL2 !>(show-counters counters)
     (3 0 NIL)
     ACL2 !>(reset-counters counters)
     <counters>
     ACL2 !>(show-counters counters)
     (0 0 NIL)

Here finally is a function that uses counters as a single-threaded
accumulator to collect the desired information about the tree x.

     (defun sweep-tree (x counters)
       (declare (xargs :stobjs (counters)))
       (cond ((atom x)
              (seq counters
                   (update-TipCnt (+ 1 (TipCnt counters)) counters)
                   (if (integerp x)
                       (update-IntTipsSeen (cons x (IntTipsSeen counters))
                                       counters)
                     counters)))
             (t (seq counters
                     (update-NodeCnt (+ 1 (NodeCnt counters)) counters)
                     (sweep-tree (car x) counters)
                     (sweep-tree (cdr x) counters)))))

We can paraphrase this definition as follows.  If x is an atom, then
increment the TipCnt field of counters and _then_, if x is an integer,
add x to the IntTipsSeen field, and return counters.  On the other
hand, if x is not an atom, then increment the NodeCnt field of
counters, and _then_ sweep the car of x and _then_ sweep the cdr of x
and return the result.

Here is an example of its execution.  We have displayed the input tree
in full dot notation so that the number of interior nodes is just the
number of dots.

     ACL2 !>(sweep-tree '((((a . 1) . (2 . b)) . 3)
                          . (4 . (5 . d)))
                        counters)
     <counters>
     ACL2 !>(show-counters counters)
     (7 8 (5 4 3 2 1))
     ACL2 !>(reset-counters counters)
     <counters>
     ACL2 !>(show-counters counters)
     (0 0 NIL)

The counters object has two integer fields and a field whose type is
unrestricted.  single-threaded objects support other types of fields,
such as arrays.  We deal with that in the stobj-example-2.  But we
recommend that you first consider the implementation issues for the
counters example (in stobj-example-1-implementation) and then consider
the proof issues (in stobj-example-1-proofs).

To continue the stobj tour, see STOBJ-EXAMPLE-2.

STOBJ-EXAMPLE-1-DEFUNS    the defuns created by the counters stobj

Consider the event shown in stobj-example-1:

     (defstobj counters
       (NodeCnt     :type integer :initially 0)
       (TipCnt      :type integer :initially 0)
       (IntTipsSeen :type t       :initially nil))

Here is a complete list of the defuns added by the event.

The careful reader will note that the counters argument below is _not_
declared with the :stobjs xarg even though we insist that the argument
be a stobj in calls of these functions.  This "mystery" is explained
below.

     (defun NodeCntp (x)                 ;;; Recognizer for 1st field
       (declare (xargs :guard t :verify-guards t))
       (integerp x))

     (defun TipCntp (x)                  ;;; Recognizer for 2nd field
       (declare (xargs :guard t :verify-guards t))
       (integerp x))

     (defun IntTipsSeenp (x)             ;;; Recognizer for 3rd field
       (declare (xargs :guard t :verify-guards t) (ignore x))
       t)

     (defun countersp (counters)         ;;; Recognizer for object
       (declare (xargs :guard t :verify-guards t))
       (and (true-listp counters)
            (= (length counters) 3)
            (NodeCntp (nth 0 counters))
            (TipCntp (nth 1 counters))
            (IntTipsSeenp (nth 2 counters))
            t))

     (defun create-counters ()           ;;; Creator for object
       (declare (xargs :guard t :verify-guards t))
       (list '0 '0 'nil))

     (defun NodeCnt (counters)           ;;; Accessor for 1st field
       (declare (xargs :guard (countersp counters) :verify-guards t))
       (nth 0 counters))

     (defun update-NodeCnt (v counters)  ;;; Updater for 1st field
       (declare (xargs :guard
                       (and (integerp v)
                            (countersp counters))
                       :verify-guards t))
       (update-nth 0 v counters))

     (defun TipCnt (counters)            ;;; Accessor for 2nd field
       (declare (xargs :guard (countersp counters) :verify-guards t))
       (nth 1 counters))

     (defun update-TipCnt (v counters)   ;;; Updater for 2nd field
       (declare (xargs :guard
                       (and (integerp v)
                            (countersp counters))
                       :verify-guards t))
       (update-nth 1 v counters))

     (defun IntTipsSeen (counters)       ;;; Accessor for 3rd field
       (declare (xargs :guard (countersp counters) :verify-guards t))
       (nth 2 counters))

     (defun update-IntTipsSeen (v counters) ;;; Updater for 3rd field
       (declare (xargs :guard (countersp counters) :verify-guards t))
       (update-nth 2 v counters))

Observe that there is a recognizer for each of the three fields and
then a recognizer for the counters object itself.  Then, for each
field, there is an accessor and an updater.

Observe also that the functions are guarded so that they expect a
countersp for their counters argument and an appropriate value for the
new field values.

You can see all of the defuns added by a defstobj event by executing
the event and then using the :pcb! command on the stobj name.  E.g.,

     ACL2 !>:pcb! counters

will print the defuns above.

We now clear up the "mystery" mentioned above.  Note, for example in
TipCnt, that the formal counters is used.  From the discussion in
stobj-example-1 it has been made clear that TipCnt can only be called
on the counters object.  And yet, in that same discussion it was said
that an argument is so treated only if it it declared among the :stobjs
in the definition of the function.  So why doesn't TipCnt include
something like (declare (xargs :stobjs (counters)))?

The explanation of this mystery is as follows.  At the time TipCnt was
defined, during the introduction of the counters stobj, the name
"counters" was not yet a single-threaded object.  The introduction of a
new single-threaded object occurs in three steps: (1) The new primitive
recognizers, accessors, and updaters are introduced as "ordinary
functions," producing their logical axiomatizations.  (2) The
executable counterparts are defined in raw Lisp to support destructive
updating.  (3) The new name is declared a single-threaded object to
ensure that all future use of these primitives respects the
single-threadedness of the object.  The functions defined as part of
the introduction of a new single-threaded object are the only functions
in the system that have undeclared stobj formals other than state.

You may return to stobj-example-1 here.

STOBJ-EXAMPLE-1-IMPLEMENTATION    the implementation of the counters stobj

the event

     (defstobj counters
       (NodeCnt     :type integer :initially 0)
       (TipCnt      :type integer :initially 0)
       (IntTipsSeen :type t       :initially nil))

discussed in stobj-example-1, creates a Common Lisp object to represent
the current value of counters.  That object is created by evaluating
either of the following "raw" (non-ACL2) Common Lisp forms:

     (create-counters)

     (vector (make-array 1 :element-type 'integer
                           :initial-element '0)
             (make-array 1 :element-type 'integer
                           :initial-element '0)
             'nil)

and the value is stored in the Common Lisp global variable named
*the-live-counters*.

Thus, the counters object is an array of length three.  The first two
elements are arrays of size 1 and are used to hold the NodeCnt and
TipCnt fields.  The third element is the IntTipsSeen field.  The first
two fields are represented by arrays so that we can implement the
integer type specification efficiently.  Generally, integers are
"boxed" in some Common Lisp implementations, for example, GCL.
Creating a new integer requires creating a new box to put it in.  But
in some lisps, including GCL, the integers inside arrays of integers
are not boxed.

The function NodeCnt is defined in raw Lisp as:

     (defun NodeCnt (counters)
       (the integer
            (aref (the (simple-array integer (1))
                       (svref counters 0))
                  0)))

Observe that the form (svref counters 0) is evaluated to get an array
of size 1, which is followed by a call of aref to access the 0th
element of that array.

The function update-NodeCnt is defined in raw Lisp as:

     (defun update-NodeCnt (v counters)
       (declare (type integer v))
       (progn
        (setf (aref (the (simple-array integer (1))
                         (svref counters 0))
                    0)
              (the integer v))
        counters))

Note that when this function is called, it does not create a new vector
of length three, but "smashes" the existing one.

One way to see all the raw Lisp functions defined by a given defstobj is
to evaluate the defstobj event and then evaluate, in the ACL2 loop, the
expression (nth 4 (global-val 'cltl-command (w state))).  Those
functions that contain (DECLARE (STOBJ-INLINE-FN T)) will generate
defabbrev forms because the :inline keyword of defstobj was supplied the
value t.  The rest will generate defuns.

We now recommend that you look at stobj-example-1-proofs.

STOBJ-EXAMPLE-1-PROOFS    some proofs involving the counters stobj

Consider again the event

     (defstobj counters
       (NodeCnt     :type integer :initially 0)
       (TipCnt      :type integer :initially 0)
       (IntTipsSeen :type t       :initially nil))

discussed in stobj-example-1, followed by the definition

     (defun reset-counters (counters)
       (declare (xargs :stobjs (counters)))
       (seq counters
            (update-NodeCnt 0 counters)
            (update-TipCnt 0 counters)
            (update-IntTipsSeen nil counters)))

which, because of the seq macro in stobj-example-1, is just syntactic
sugar for

     (defun reset-counters (counters)
       (declare (xargs :stobjs (counters)))
       (let ((counters (update-NodeCnt 0 counters)))
         (let ((counters (update-TipCnt 0 counters)))
           (update-IntTipsSeen nil counters)))).

Here is a simple theorem about reset-counters.

     (defthm reset-counters-is-constant
       (implies (countersp x)
                (equal (reset-counters x)
                       '(0 0 nil))))

Before we talk about how to prove this theorem, note that the theorem
is unusual in two respects.

First, it calls reset-counters on an argument other than the variable
counters!  That is allowed in theorems; logically speaking, the stobj
functions are indistinguishable from ordinary functions.  Their use is
syntactically restricted only in defuns, which might be compiled and
run in raw Lisp.  Those restrictions allow us to implement stobj
modification destructively.  But logically speaking, reset-counters and
other stobj "modifying" functions just create new objects,
constructively.

Second, the theorem above explicitly provides the hypothesis that
reset-counters is being applied to an object satisfying countersp.
Such a hypothesis is not always required: reset-counters is total and
will do something no matter what x is.  But in this particular case,
the result is not '(0 0 nil) unless x is, at least, a true-list of
length three.

To make a long story short, to prove theorems about stobj functions you
behave in exactly the way you would to prove the same theorems about the
same functions defined without the stobj features.

How can we prove the above theorem?  Unfolding the definition of
reset-counters shows that (reset-counters x) is equal to

     (update-IntTipsSeen nil
       (update-TipCnt 0
         (update-NodeCnt 0 x)))

which in turn is

     (update-nth 2 nil
      (update-nth 1 0
       (update-nth 0 0 x))).

Opening up the definition of update-nth reduces this to

     (list* 0 0 nil (cdddr x)).

This is clearly equal to '(0 0 nil), provided we know that (cdddr x) is
nil.

Unfortunately, that last fact requires a lemma.  The most specific
lemma we could provide is

     (defthm special-lemma-for-counters
       (implies (countersp x)
                (equal (cdddr x) nil)))

but if you try to prove that lemma you will find that it requires some
reasoning about len and true-listp.  Furthermore, the special lemma
above is of interest only for counters.

The following lemma about len is the one we prefer.

     (defthm equal-len-n
       (implies (syntaxp (quotep n))
                (equal (equal (len x) n)
                       (if (integerp n)
                           (if (< n 0)
                               nil
                             (if (equal n 0)
                                 (atom x)
                               (and (consp x)
                                    (equal (len (cdr x)) (- n 1)))))
                         nil))))

This lemma will simplify any equality in which a len expression is
equated to any explicitly given constant _n_, e.g., 3, reducing the
equation to a conjunction of consp terms about the first _n_ cdrs.

If the above lemma is available then ACL2 immediately proves

     (defthm reset-counters-is-constant
       (implies (countersp x)
                (equal (reset-counters x)
                       '(0 0 nil))))

The point is presumably well made: proving theorems about
single-threaded object accessors and updaters is no different than
proving theorems about other recursively defined functions on lists.

As we have seen, operations on stobjs turn into definitions involving
nth and update-nth in the logic.  Here are two lemmas that are useful
for simplifying terms involving nth and update-nth, which are therefore
useful in reasoning about single-threaded objects.

     (defthm update-nth-update-nth-same
       (implies (equal (nfix i1) (nfix i2))
                (equal (update-nth i1 v1 (update-nth i2 v2 l))
                       (update-nth i1 v1 l))))

     (defthm update-nth-update-nth-diff
       (implies (not (equal (nfix i1) (nfix i2)))
                (equal (update-nth i1 v1 (update-nth i2 v2 l))
                       (update-nth i2 v2 (update-nth i1 v1 l))))
       :rule-classes ((:rewrite :loop-stopper ((i1 i2)))))

These lemmas are due to Matt Wilding.  See NU-REWRITER for a
discussion of the efficient simplification of terms of the form (nth n
(update-nth key val lst)), which can be critical in settings involving
sequential bindings that commonly arise in operations involving stobjs.

We now recommend that you see STOBJ-EXAMPLE-2.

STOBJ-EXAMPLE-2    an example of the use of arrays in single-threaded objects

The following event

     (defstobj ms
       (pcn  :type integer                  :initially 0)
       (mem  :type (array integer (100000)) :initially -1)
       (code :type t                        :initially nil))

introduces a single-threaded object named ms (which stands for "machine
state").  The object has three fields, a pcn or program counter, a mem
or memory, and a code field.

The mem field is occupied by an object initially of type (array integer
(100000)).  Logically speaking, this is a list of length 100000, each
element of which is an integer.  But in the underlying implementation
of the ms object, this field is occupied by a raw Lisp array, initially
of size 100000.

You might expect the above defstobj to define the accessor function mem
and the updater update-mem.  _That does not happen!_.

The above event defines the accessor function memi and the updater
update-memi.  These functions do not access/update the mem field of the
ms object; they access/update the individual elements of the array in
that field.

In particular, the logical definitions of the two functions are:

     (defun memi (i ms)
       (declare (xargs :guard
                       (and (msp ms)
                            (integerp i)
                            (<= 0 i)
                            (< i (mem-length ms)))))
       (nth i (nth 1 ms)))

     (defun update-memi (i v ms)
       (declare (xargs :guard
                       (and (msp ms)
                            (integerp i)
                            (<= 0 i)
                            (< i (mem-length ms))
                            (integerp v))))
       (update-nth-array 1 i v ms))

For example, to access the 511th (0-based) memory location of the
current ms you could evaluate:

     ACL2 !>(memi 511 ms)
     -1

The answer is -1 initially, because that is the above-specified initial
value of the elements of the mem array.

To set that element you could do

     ACL2 !>(update-memi 511 777 ms)
     <ms>
     ACL2 !>(memi 511 ms)
     777

The raw Lisp implementing these two functions is shown below.

     (defun memi (i ms)
       (declare (type (and fixnum (integer 0 *)) i))
       (the integer
            (aref (the (simple-array integer (*))
                       (svref ms 1))
                  (the (and fixnum (integer 0 *)) i))))

     (defun update-memi (i v ms)
       (declare (type (and fixnum (integer 0 *)) i)
                (type integer v))
       (progn
        (setf (aref (the (simple-array integer (*))
                         (svref ms 1))
                    (the (and fixnum (integer 0 *)) i))
              (the integer v))
        ms))

If you want to see the raw Lisp supporting a defstobj, execute the
defstobj and then evaluate the ACL2 form (nth 4 (global-val
'cltl-command (w state))).

To continue the stobj tour, see STOBJ-EXAMPLE-3.

STOBJ-EXAMPLE-3    another example of a single-threaded object

The event

     (defstobj $s
       (x :type integer :initially 0)
       (a :type (array (integer 0 9) (3)) :initially 9 :resizable t))

introduces a stobj named $S.  The stobj has two fields, X and A.  The A
field is an array.  The X field contains an integer and is initially 0.
The A field contains a list of integers, each between 0 and 9,
inclusively.  (Under the hood, this "list" is actually implemented as
an array.)  Initially, the A field has three elements, each of which is
9.

This event introduces the following sequence of function definitions:

     (DEFUN XP (X) ...)               ; recognizer for X field
     (DEFUN AP (X) ...)               ; recognizer of A field
     (DEFUN $SP ($S) ...)             ; top-level recognizer for stobj $S
     (DEFUN CREATE-$S NIL ...)        ; creator for stobj $S
     (DEFUN X ($S) ...)               ; accessor for X field
     (DEFUN UPDATE-X (V $S) ...)      ; updater for X field
     (DEFUN A-LENGTH ($S) ...)        ; length of A field
     (DEFUN RESIZE-A (K $S) ...)      ; resizer for A field
     (DEFUN AI (I $S) ...)            ; accessor for A field at index I
     (DEFUN UPDATE-AI (I V $S) ...)   ; updater for A field at index I

Here is the definition of $SP:

     (DEFUN $SP ($S)
       (DECLARE (XARGS :GUARD T :VERIFY-GUARDS T))
       (AND (TRUE-LISTP $S)
            (= (LENGTH $S) 2)
            (XP (NTH 0 $S))
            (AP (NTH 1 $S))
            T))

This reveals that in order to satisfy $SP an object must be a true list
of length 2 whose first element satisfies XP and whose second satisfies
AP.  By printing the definition of AP one learns that it requires its
argument to be a true list, each element of which is an integer between
0 and 9.

The initial value of stobj $S is given by zero-ary "creator" function
CREATE-$S.  Creator functions may only be used in limited contexts.
See WITH-LOCAL-STOBJ.

Here is the definition of UPDATE-AI, the updater for the A field at
index I:

     (DEFUN UPDATE-AI (I V $S)
       (DECLARE (XARGS :GUARD
                       (AND ($SP $S)
                            (INTEGERP I)
                            (<= 0 I)
                            (< I (A-LENGTH $S))
                            (AND (INTEGERP V) (<= 0 V) (<= V 9)))
                       :VERIFY-GUARDS T))
       (UPDATE-NTH-ARRAY 1 I V $S))

By definition (UPDATE-NTH-ARRAY 1 I V $S) is (UPDATE-NTH 1 (UPDATE-NTH
I V (NTH 1 $S)) $S).  This may be a little surprising but should be
perfectly clear.

First, ignore the guard, since it is irrelevant in the logic.  Reading
from the inside out, (UPDATE-AI I V $S) extracts (NTH 1 $S), which is
array a of $S.  (Recall that NTH is 0-based.)  The next higher
expression in the definition above, (UPDATE-NTH I V a), "modifies" a by
setting its Ith element to V.  Call this a'.  The next higher
expression, (UPDATE-NTH 1 a' $S), "modifies" $S by setting its 1st
component to a'.  Call this result $s'.  Then $s' is the result
returned by UPDATE-AI.

So the first useful observation is that from the perspective of the
logic, the type "restrictions" on stobjs are irrelevant.  They are
"enforced" by ACL2's guard mechanism, not by the definitions of the
updater functions.

As one might also imagine, the accessor functions do not really "care,"
logically, whether they are applied to well-formed stobjs or not.  For
example, (AI I $S) is defined to be (NTH I (NTH 1 $S)).

Thus, you will not be able to prove that (AI 2 $S) is an integer.  That
is,

     (integerp (AI 2 $S))

is not a theorem, because $S may not be well-formed.

Now (integerp (AI 2 $S)) will always evaluate to T in the top-level
ACL2 command loop, because we insist that the current value of the
stobj $S always satisfies $SP by enforcing the guards on the updaters,
independent of whether guard checking is on or off; see
SET-GUARD-CHECKING.  But in a theorem $S is just another variable,
implicitly universally quantified.

So (integerp (AI 2 $S)) is not a theorem because it is not true when
the variable $S is instantiated with, say,

     '(1 (0 1 TWO))

because, logically speaking, (AI 2 '(1 (0 1 TWO))) evaluates to the
symbol TWO.  That is,

     (equal (AI 2 '(1 (0 1 TWO))) 'TWO)

is true.

However,

     (implies (and ($SP $S) (< 2 (A-LENGTH $S))) (integerp (AI 2 $S)))

is a theorem.  To prove it, you will have to prove a lemma about AP.
The following will do:

     (defthm ap-nth
       (implies (and (AP x)
                     (integerp i)
                     (<= 0 i)
                     (< i (len x)))
                (integerp (nth i x)))).

Similarly,

     (implies (and (integerp i)
                   (<= 0 i)
                   (< i (A-LENGTH $S))
                   (integerp v)
                   (<= 0 v)
                   (<= v 9))
              ($SP (UPDATE-AI i v $S)))

is not a theorem until you add the additional hypothesis ($SP $S).  To
prove the resulting theorem, you will need a lemma such as the
following.

     (defthm ap-update-nth
       (implies (and (AP a)
                     (integerp v)
                     (<= 0 v)
                     (<= v 9)
                     (integerp i)
                     (<= 0 i)
                     (< i (len a)))
                (AP (update-nth i v a))))

The moral here is that from the logical perspective, you must provide
the hypotheses that, as a programmer, you think are implicit on the
structure of your stobjs, and you must prove their invariance.  This is
a good area for further support, perhaps in the form of a library of
macros.

_Resizing Array Fields_

Recall the specification of the array field, A for the stobj $S
introduced above:

     (a :type (array (integer 0 9) (3)) :initially 9 :resizable t)

Logically, this field is a list, initially of length 3.  Under the
hood, this field is implemented using a Common Lisp array with 3
elements.  In some applications, one may wish to lengthen an array
field, or even (to reclaim space) to shrink an array field.  The
defstobj event provides functions to access the current length of an
array field and to change the array field, with default names obtained
by suffixing the field name with "LENGTH-" or prefixing it with
"RESIZE-," respectively.  The following log shows the uses of these
fields in the above example.

     ACL2 !>(A-LENGTH $S)
     3
     ACL2 !>(RESIZE-A 10 $S) ; change length of A to 10
     <$s>
     ACL2 !>(A-LENGTH $S)
     10
     ACL2 !>(AI 7 $S)        ; new elements get value from :initially
     9
     ACL2 !>(RESIZE-A 2 $S)  ; truncate A down to first 2 elements
     <$s>
     ACL2 !>(A-LENGTH $S)
     2
     ACL2 !>(AI 7 $S)        ; error:  access past array bound

     ACL2 Error in TOP-LEVEL:  The guard for the function symbol AI, which
     is (AND ($SP $S) (INTEGERP I) (<= 0 I) (< I (A-LENGTH $S))), is violated
     by the arguments in the call (AI 7 $S).

     ACL2 !>

Here are the definitions of the relevant functions for the above
example; also see RESIZE-LIST.

     (DEFUN A-LENGTH ($S)
       (DECLARE (XARGS :GUARD ($SP $S) :VERIFY-GUARDS T))
       (LEN (NTH 1 $S)))

     (DEFUN RESIZE-A (K $S)
       (DECLARE (XARGS :GUARD ($SP $S) :VERIFY-GUARDS T))
       (UPDATE-NTH 1
                   (RESIZE-LIST (NTH 1 $S) K 9)
                   $S))

It is important to note that the implementation of array resizing in
ACL2 involves copying the entire array into a newly allocated space and
thus can be quite costly if performed often.  This approach was chosen
in order to make array access and update as efficient as possible, with
the suspicion that for most applications, array access and update are
considerably more frequent than resizing (especially if the programmer
is aware of the relative costs beforehand).

It should also be noted that computations of lengths of stobj array
fields should be fast (constant-time) in all or most Common Lisp
implementations.

Finally, if :resizable t is not supplied as shown above, then an
attempt to resize the array will result in an error.  If you do not
intend to resize the array, it is better to omit the :resizable option
(or to supply :resizable nil), since then the length function will be
defined to return a constant, namely the initial length, which can
simplify guard proofs (compare with the definition of A-LENGTH above).

This completes the tour through the documentation of stobjs.  However,
you may now wish to read the documentation for the event that
introduces a new single-threaded object; see DEFSTOBJ.

WITH-LOCAL-STATE    locally bind state

This is an advanced topic, probably of interest only to system
developers.

Consider the following example form:

     (with-local-state
      (mv-let (result state)
              (compute-with-state x state)
              result))

This is equivalent to the following form.

     (with-local-stobj
      state
      (mv-let (result state)
              (compute-with-state x state)
              result))

By default, this form is illegal, because ACL2 does not have a way to
unwind all changes to the ACL2 state; we say more on this issue below.
There may however be situations where you are willing to manage or
overlook this issue.  In that case you may execute the following form
to enable the use of with-local-state, by enabling the use of
with-local-stobj on state; but note that it requires an active trust
tag (see DEFTTAG).

     (remove-untouchable create-state t)

Please be aware that no local state is actually created, however!  In
particular, users of with-local-state need either to ensure that
channels are closed and state global variables are returned to their
original values, or else be willing to live with changes made to state
that are not justified by the code that has been evaluated.  You are
welcome to look in the the ACL2 source code at the definition of macro
channel-to-string, which employs with-local-state to create a local
state for the purpose of creating a string.

Here is an example use of with-local-state.  Notice the use of defttag
-- and indeed, please understand that we are just hacking here, and in
general it takes significant effort to be sure that one is using
with-local-state correctly!

     (defttag t)

     (remove-untouchable create-state t)

     (set-state-ok t)

     (defun foo (state)
       (declare (xargs :mode :program))
       (mv-let
        (channel state)
        (open-input-channel "my-file" :object state)
        (mv-let (eofp obj state)
                (read-object channel state)
                (declare (ignore eofp))
                (let ((state (close-input-channel channel state)))
                  (mv obj state)))))

     (defun bar ()
       (declare (xargs :mode :program))
       (with-local-state (mv-let (result state)
                                 (foo state)
                                 result)))

     ; Multiple-value return version:

     (defun foo2 (state)
       (declare (xargs :mode :program))
       (mv-let
        (channel state)
        (open-input-channel "my-file" :object state)
        (mv-let (eofp obj state)
                (read-object channel state)
                (let ((state (close-input-channel channel state)))
                  (mv eofp obj state)))))

     (defun bar2 ()
       (declare (xargs :mode :program))
       (with-local-state (mv-let (eofp result state)
                                 (foo2 state)
                                 (mv eofp result))))

WITH-LOCAL-STOBJ    locally bind a single-threaded object

See STOBJ for an introduction to single-threaded objects.

     Example Form:
     (with-local-stobj
      st
      (mv-let (result st)
              (compute-with-st x st)
              result))

With-local-stobj can be thought of as a macro, where the example form
above expands as follows.

     (mv-let (result st)
             (let ((st (create-st)))
               (compute-with-st x st))
             (declare (ignore st))
             result)

However, ACL2 expects you to use with-local-stobj, not its expansion.
More precisely, stobj creator functions are not allowed except
(implicitly) via with-local-stobj and in logic-only situations (like
theorems and hints).  Moreover, neither with-local-stobj nor its
expansions are legal when typed directly at the top-level loop.  See
TOP-LEVEL for a way to use with-local-stobj in the top-level
loop.

     General Forms:
     (with-local-stobj stobj-name mv-let-form)
     (with-local-stobj stobj-name mv-let-form creator-name)

where stobj-name is the name of a stobj, mv-let-form is a call of
mv-let, and if creator-name is supplied then it should be the name of
the creator function for stobj-name; see DEFSTOBJ.  For the
example form above, its expansion would use creator-name, if supplied,
in place of create-st.  Note that stobj-name must not be state (the
ACL2 state), except in special situations probably of interest only to
system developers; see WITH-LOCAL-STATE.

With-local-stobj can be useful when a stobj is used to memoize
intermediate results during a computation, yet it is desired not to
make the stobj a formal parameter for the function and its callers.

ACL2 can reason about these "local stobjs," and in particular about
stobj creator functions.  For technical reasons, ACL2 will not allow
you to enable the :EXECUTABLE-COUNTERPART rune of a stobj creator
function.

Finally, here is a small example concocted in order to illustrate that
with-local-stobj calls can be nested.

     (defstobj st fld1)

     (defun foo ()
       (with-local-stobj
        st ; Let us call this the ``outer binding of st''.
        (mv-let (val10 val20 st)
          (let ((st (update-fld1 10 st)))
            ;; At this point the outer binding of st has fld1 = 10.
            (let ((result (with-local-stobj
                           st ; Let us call this the ``inner binding of st''.
                           (mv-let (val st)
                             (let ((st (update-fld1 20 st)))
                               ;; Now fld1 = 20 for the inner binding of st.
                               (mv (fld1 st) st))
                             val))))
              ;; So result has been bound to 20 above, but here we are once again
              ;; looking at the outer binding of st, where fld1 is still 10.
              (mv (fld1 st) result st)))
          (mv val10 val20))))

     (thm (equal (foo) (mv 10 20))) ; succeeds

SWITCHES-PARAMETERS-AND-MODES    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.

ACL2-CUSTOMIZATION    file of initial commands for ACL2 to run at startup

ACL2 provides a mechanism to load automatically a so-called "ACL2
customization file," via ld, the first time lp is called in an ACL2
session.  ACL2 looks for this file as follows.

     o If the host Lisp reads a non-empty value for the system's
     environment variable ACL2_CUSTOMIZATION, then that string value is
     used for the customization file name.  In this case, if the file
     does not exist or if the string is "NONE" then there is no
     customization file.  Notes.  (1) If the customization file name is
     a relative pathname (see PATHNAME), then the pathname is
     considered relative to the connected book directory (see
     CBD).  (2) If this variable is not already defined, then its
     value is set to NONE when the ACL2 makefile system is invoked
     (specifically, books/Makefile-generic), e.g., for a regression.

     o Otherwise (empty environment variable value), file
     "acl2-customization.lsp" or "acl2-customization.lisp" on the
     connected book directory (see CBD), generally the current
     directory, is the customization file (in that order) if either
     exists.

     o Otherwise file "acl2-customization.lsp" or
     "acl2-customization.lisp" on your home directory is the
     customization file (in that order), if either exists (except, this
     case is skipped on Windows operating systems.

Except for the fact that this ld command is not typed explicitly by
you, it is a standard ld command, with one exception: any settings of
ld specials are remembered once this call of ld has completed.  For
example, suppose that you start your customization file with
(set-ld-skip-proofsp t state), so that proofs are skipped as it is
loaded with ld.  Then the ld special ld-skip-proofsp will remain t
after the ld has completed, causing proofs to be skipped in your ACL2
session, unless your customization file sets this variable back to nil,
say with (set-ld-skip-proofsp nil state).

If the customization file exists, it is loaded with ld using the usual
default values for the ld specials (see LD).  Thus, if an error
is encountered, no subsequent forms in the file will be evaluated.

To create a customization file it is recommended that you first give it
a name other than "acl2-customization.lsp" or "acl2-customization.lisp"
so that ACL2 does not try to include it prematurely when you next enter
lp.  Then, while in the uncustomized lp, explicitly invoke ld on your
evolving (but renamed) customization file until all forms are
successfully evaluated.  The same procedure is recommended if for some
reason ACL2 cannot successfully evaluate all forms in your
customization file: temporarily rename your customization file so that
ACL2 does not try to ld it automatically and then debug the new file by
explicit calls to ld.

WARNING!  If you certify a book after the (automatic) loading of a
customization file, the forms in that file will be part of the
portcullis of the books you certify!  That is, the forms in your
customization file at certification time will be loaded whenever
anybody uses the books you are certifying.  Since customization files
generally contain idiosyncratic commands, you may not want yours to be
part of the books you create for others.  Thus, if you have a
customization file then you may want to invoke :ubt 1 before certifying
any books; alternatively, see CERTIFY-BOOK! for automatic
invocation of ubt.

On the other hand, if you wish to prevent undoing commands from the
customization file, see RESET-PREHISTORY.

Finally, we note that except on Windows-based systems, if there is a
file acl2-init.lsp in your home directory, then it will be loaded into
raw Lisp when ACL2 is invoked.

ADD-BINOP    associate a function name with a macro name

The form (add-binop macro macro-fn) is an abbreviation for the form
(add-macro-fn macro macro-fn t).  See ADD-MACRO-FN.

ADD-DEFAULT-HINTS    add to the default hints

     Examples:
     (add-default-hints '((computed-hint-1 clause)
                          (computed-hint-2 clause
                                           stable-under-simplificationp)))
     (add-default-hints '((computed-hint-3 id clause world))
                        :at-end t)

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 Forms:
     (add-default-hints lst)
     (add-default-hints lst :at-end flg)

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 front of
the list of default hints, so that they are tried first -- or, if flg
is supplied and evaluates to other than nil, at the end of the list, so
that they are tried last -- rather than *replacing* the default hints
with the indicated hints.  Each new hint is thus considered after each
existing hints when both are applied to the same goal.  Also See
SET-DEFAULT-HINTS, see REMOVE-DEFAULT-HINTS, and see
DEFAULT-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!.

For a related feature, which however is only for advanced system
builders, see OVERRIDE-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    link keyword for :dir argument of ld and include-book

     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 pathname of a directory.  (If
the final '/' is missing, ACL2 will add it for you.)  The effect of
this event is to modify the meaning of the :dir keyword argument of
include-book as indicated by the examples above, and similarly for ld,
namely by associating the indicated directory with the indicated
keyword for purposes of the :dir argument.  By the "indicated
directory" we mean, in the case that the pathname is a relative
pathname, the directory relative to the current connected book
directory; see CBD.  See DELETE-INCLUDE-BOOK-DIR for
how to undo this effect.

A keyword that is already associated with a directory string by an
existing invocation of add-include-book-dir cannot be associated with a
different directory string.  If that is your intention, first apply
delete-include-book-dir to that keyword; see
DELETE-INCLUDE-BOOK-DIR.  If however the new directory string is
identical with the old, then the call of add-include-book-dir will be
redundant (see REDUNDANT-EVENTS).

The keyword :system can never 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").

This macro generates (in essence) 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.  Even if you invoke add-include-book-dir before
certifying a book, so that this event is among the book's portcullis
commands rather than in the book itself, nevertheless that
add-include-book-dir event will not be visible after the book is
included.  (Note: The above behavior is generally preserved in raw-mode
(see SET-RAW-MODE),though by means other than a 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-MACRO-FN    associate a function name with a macro name

     Examples:
     (add-macro-fn append binary-append)
     (add-macro-fn append binary-append t)

These examples each associate 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.  In the first case, (append x (append y z)) is printed
rather than (append x y z).  In the second case, right-associated
arguments are printed flat: (append x y z).  Such right-association is
considered only for binary function symbols; otherwise the optional
third argument is ignored.

     General Forms:
     (add-macro-fn macro-name function-name)
     (add-macro-fn macro-name function-name nil) ; same as abov
     (add-macro-fn macro-name function-name t)

This is a convenient way to add an entry to macro-aliases-table and at
the same time extend the :untrans-table.  As suggested by the example
above, calls of a function in this table will be printed as
corresponding calls of macros, with right-associated arguments printed
flat in the case of a binary function symbol if the optional third
argument is t.  In that case, for a binary function symbol fn
associated with macro name mac, then a call (fn arg1 (fn arg2 (... (fn
argk arg)))) will be displayed to the user as though the "term" were
(mac arg1 arg2 ... argk arg).  For a call (f a1 ... ak) of a function
symbol that is not binary, or the optional argument is not supplied as
t, then the effect is simply to replace f by the corresponding macro
symbol.  See MACRO-ALIASES-TABLE, see
REMOVE-MACRO-ALIAS, see UNTRANS-TABLE, and see
REMOVE-MACRO-FN.

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.
(But note: add-match-free-override is not relevant for type-prescription
rules.)  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.

ADD-OVERRIDE-HINTS    add to the override-hints

See OVERRIDE-HINTS for a discussion of override-hints.  Here we
describe how to extend the list of override-hints.  Note that the
effects of add-override-hints events are local to the books or
encapsulate events in which they reside; see
ADD-OVERRIDE-HINTS! to avoid that restriction.  Also see
SET-OVERRIDE-HINTS to set a new list of override-hints to it,
ignoring the present list rather than adding to it.

     General Forms:
     (add-override-hints form)
     (add-override-hints form :at-end t)
     (add-override-hints form :at-end nil) ; default for :at-end

where form evaluates to a list of computed hint forms.  The effect of
this event is to extend the current list of override-hints by appending
the result of that evaluation.  The default is to append the evaluation
result to the front of the current list of override-hints, but if
:at-end t is specified, then the evaluation result is appended to the
end of the current list.

ADD-OVERRIDE-HINTS!    add non-locally to the override-hints

Add-override-hints! is the same as add-override-hints, except that the
former is not local to books or encapsulate events in which it occurs.
See ADD-OVERRIDE-HINTS; also see SET-OVERRIDE-HINTS.

DEFAULT-HINTS-TABLE    a table used to provide hints for proofs

Please see SET-DEFAULT-HINTS, see ADD-DEFAULT-HINTS, and
see REMOVE-DEFAULT-HINTS for how to use this table.  For
completeness, we mention here that under the hood, these events all
update the default-hints-table by updating its key, t, for example as
follows.

     (table default-hints-table t
            '((computed-hint-1 clause)
              (computed-hint-2 clause
                               stable-under-simplificationp)))

The use of default hints is explained elsewhere; see
SET-DEFAULT-HINTS.

Advanced users only: see OVERRIDE-HINTS for an advanced variant
of default hints.

DEFAULT-VERIFY-GUARDS-EAGERNESS    See SET-VERIFY-GUARDS-EAGERNESS.

DELETE-INCLUDE-BOOK-DIR    unlink keyword for :dir argument of ld and include-book

     Example Forms:
     (delete-include-book-dir :smith)
      ; Remove association of directory with :smith for include-book.

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

where kwd is a keywordp.  The effect of this event is to modify the
meaning of the :dir keyword argument of include-book and ld as
indicated by the examples above, namely by removing association of any
directory with the indicated keyword for purposes of the include-book
(and ld) :dir argument.  Normally one would instead use
add-include-book-dir to associate a new directory with that keyword;
see ADD-INCLUDE-BOOK-DIR.

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 is local to any books and encapsulate events in which it
occurs; see ADD-INCLUDE-BOOK-DIR for a discussion of this aspect
of both macros.

DIVE-INTO-MACROS-TABLE    right-associated function information for the proof-checker

     Examples:
     ACL2 !>(dive-into-macros-table (w state))
     ((CAT . EXPAND-ADDRESS-CAT)
      (LXOR . EXPAND-ADDRESS-LXOR)

This table associates macro names with functions used by the
proof-checker's DV and numeric diving commands (e.g., 3) in order to
dive properly into subterms.  See PROOF-CHECKER, in particular
the documentation for DV.

This table can be extended easily.  See ADD-DIVE-INTO-MACRO and
also see REMOVE-DIVE-INTO-MACRO.

The symbol associated with a macro should be a function symbol taking
four arguments, in this order:

     car-addr ; the first number in the list given to the proof-checker's
                DV command
     raw-term ; the untranslated term into which we will dive
     term     ; the translated term into which we will dive
     wrld     ; the current ACL2 logical world

The function will normally return a list of positive integers,
representing the (one-based) address for diving into term that
corresponds to the single-address dive into raw-term by car-address.
However, it can return (cons str alist), where str is a string suitable
for fmt and args is the corresponding alist for fmt.

Referring to the example above, expand-address-cat would be such a
function, which will be called on raw-term values that are calls of
cat.  See the distributed book books/misc/rtl-untranslate.lisp for the
definition of such a function.

See TABLE for a general discussion of tables.

INVISIBLE-FNS-TABLE    functions that are invisible to the loop-stopper algorithm

     Examples:
     ACL2 !>(invisible-fns-table (w state))
     ((binary-+ unary--)
      (binary-* unary-/)
      (unary-- unary--)
      (unary-/ unary-/))

Among other things, the setting above has the effect of making unary-
"invisible" for the purposes of applying permutative :rewrite rules to
binary-+ trees.  Also see ADD-INVISIBLE-FNS, see
REMOVE-INVISIBLE-FNS, and see SET-INVISIBLE-FNS-TABLE.

See TABLE for a general discussion of tables.

The "invisible functions table" is an alist with elements of the
following form, where fn is a function symbol and the ufni are unary
function symbols in the current ACL2 world, and k is at least 1.

     (fn ufn1 ufn2 ... ufnk)

This table thus associates with certain function symbols, e.g., fn
above, a set of unary functions, e.g., the ufni above.  The ufni
associated with fn in the invisible functions table are said to be
"invisible with respect to fn."  If fn is not the car of any pair in
the alist, then no function is invisible for it.  Thus for example,
setting the invisible functions alist to nil completely eliminates the
consideration of invisibility.

The notion of invisibility is involved in the use of the :loop-stopper
field of :rewrite rules to prevent the indefinite application of
permutative rewrite rules.  Roughly speaking, if rewrite rules are
being used to permute arg and (ufni arg) inside of a nest of fn calls,
and ufni is invisible with respect to fn, then arg and (ufni arg) are
considered to have the same "weight" and will be permuted so as to end
up as adjacent tips in the fn nest.  See LOOP-STOPPER.

LOGIC    to set the default defun-mode to :logic

     Example:
     ACL2 p!>:logic
     ACL2 !>

Typing the keyword :logic sets the default defun-mode to :logic.

Functions defined in :logic mode are logically defined.  See
DEFUN-MODE.

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

See DEFUN-MODE for a discussion of the defun-modes available
and what their effects on the logic are.  See
DEFAULT-DEFUN-MODE for a discussion of how the default defun-mode is
used.  This event is equivalent to (table acl2-defaults-table
:defun-mode :logic), and hence is local to any books and encapsulate
events in which it occurs. See ACL2-DEFAULTS-TABLE.

Recall that the top-level form :logic is equivalent to (logic); see
KEYWORD-COMMANDS.  Thus, to change the default defun-mode to
:logic in a book, use (logic), which is an embedded event form, rather
than :logic, which is not a legal form for books.  See
EMBEDDED-EVENT-FORM.

MACRO-ALIASES-TABLE    a table used to associate function names with macro names

     Example:
     (table macro-aliases-table '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.
Thus, for example, it will be legal to write

     (in-theory (disable append))

as an abbreviation for

     (in-theory (disable binary-append))

which in turn really abbreviates

     (in-theory (set-difference-theories (current-theory :here)
                                         '(binary-append)))

     General Form:

     (table macro-aliases-table 'macro-name 'function-name)

or very generally

     (table macro-aliases-table macro-name-form function-name-form)

where macro-name-form and function-name-form evaluate, respectively, to
a macro name and a symbol in the current ACL2 world.  See TABLE
for a general discussion of tables and the table event used to
manipulate tables.

Note that function-name-form (above) does not need to evaluate to a
function symbol, but only to a symbol.  As a result, one can introduce
the alias before defining a recursive function, as follows.

     (table macro-aliases-table 'mac 'fn)
     (defun fn (x)
       (if (consp x)
           (mac (cdr x))
         x))

Although this is obviously contrived example, this flexibility can be
useful to macro writers; see for example the definition of ACL2 system
macro defun-inline.

The table macro-aliases-table is an alist that associates macro symbols
with function symbols, so that macro names may be used as runic
designators (see THEORIES).  For a convenient way to add
entries to this table, see ADD-MACRO-ALIAS.  To remove entries
from the table with ease, see REMOVE-MACRO-ALIAS.

This table is used by the theory functions.  For example, in order that
(disable append) be interpreted as (disable binary-append), it is
necessary that the example form above has been executed.  In fact, this
table does indeed associate many of the macros provided by the ACL2
system, including append, with function symbols.  Loosely speaking, it
only does so when the macro is "essentially the same thing as" a
corresponding function; for example, (append x y) and (binary-append x
y) represent the same term, for any expressions x and y.

NTH-ALIASES-TABLE    a table used to associate names for nth/update-nth printing

     Example:
     (table nth-aliases-table 'st0 'st)

This example associates the symbol st0 with the symbol st.  As a
result, when the theorem prover prints terms of the form (nth n st0) or
(update-nth n val st0), where st is a stobj whose nth accessor function
is f-n, then it will print n as *f-n*.

     General Form:
     (table nth-aliases-table 'alias-name 'name)

This event causes alias-name to be treated like name for purposes of
the printing of terms that are calls of nth and update-nth.  (Note
however that name is not recursively looked up in this table.)  Both
must be symbols other than state.  See TERM, in particular the
discussion there of untranslated terms.

For a convenient way to add entries to this table, see
ADD-NTH-ALIAS.  To remove entries from the table with ease, see
REMOVE-NTH-ALIAS.

PRINT-SUMMARY-USER    causing additional summary output

ACL2 prints summaries at the conclusions of processing events (unless
summaries are inhibited; see SET-INHIBIT-OUTPUT-LST and also
see SET-INHIBITED-SUMMARY-TYPES).  You may arrange for
information to be printed at the end of the summary, by defining a
function of state that returns an ordinary value (typically nil, but
the value is irrelevant).  This function should normally be a
guard-verified :logic mode function with no explicit guard (hence, its
guard is actually (state-p state)), but later below we discuss how to
avoid this requirement.  It is then attached (see DEFATTACH) to
the function print-summary-user.  The following example illustrates how
this all works.

     (defun print-summary-user-test (state)
       (declare (xargs :stobjs state))
       (and (f-boundp-global 'abbrev-evisc-tuple state)
            (observation-cw
             'my-test
             "~|Value of abbrev-evisc-tuple: ~x0~|"
             (f-get-global 'abbrev-evisc-tuple state))))

     (defattach print-summary-user print-summary-user-test)

After admission of the two events above, every event summary will
conclude with extra printout, for example:

     ACL2 Observation in MY-TEST:
     Value of abbrev-evisc-tuple: :DEFAULT

If the attachment function (above, print-summary-user-test) does not
meet all the requirements stated above, then you can use the
:skip-checks argument of defattach to get around the requirement, as
illustrated by the following example.

     (defun print-summary-user-test2 (state)
       (declare (xargs :stobjs state
                       :mode :program))
       (observation-cw
        'my-test
        "~|Value of term-evisc-tuple: ~x0~|"
        (f-get-global 'term-evisc-tuple state)))

     (defttag t) ; needed for :skip-checks t

     (defattach (print-summary-user print-summary-user-test2)
                :skip-checks t)

PROGRAM    to set the default defun-mode to :program

     Example:
     ACL2 !>:program
     ACL2 p!>

Typing the keyword :program sets the default defun-mode to :program.

Functions defined in :program mode are logically undefined but can be
executed on constants outside of deductive contexts.  See
DEFUN-MODE.

Calls of the following macros are ignored (skipped) when in :program
mode.

     local
     verify-guards
     verify-termination
     defaxiom
     defthm
     deftheory
     in-theory
     in-arithmetic-theory
     regenerate-tau-data-base
     theory-invariant
     defchoose

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

See DEFUN-MODE for a discussion of the defun-modes available
and what their effects on the logic are.  See
DEFAULT-DEFUN-MODE for a discussion of how the default defun-mode is
used.  This event is equivalent to (table acl2-defaults-table
:defun-mode :program), and hence is local to any books and encapsulate
events in which it occurs. See ACL2-DEFAULTS-TABLE.

Recall that the top-level form :program is equivalent to (program); see
KEYWORD-COMMANDS.  Thus, to change the default defun-mode to
:program in a book, use (program), which is an embedded event form,
rather than :program, which is not a legal form for books.  See
EMBEDDED-EVENT-FORM.

PUSH-UNTOUCHABLE    add name or list of names to the list of untouchable symbols

     Examples:
     (push-untouchable my-var nil)
     (push-untouchable set-mem t)

     General Form:
     (push-untouchable name{s}  fn-p :doc doc-string)

where name{s} is a non-nil symbol or a non-nil true list of symbols,
fn-p is any value (but generally nil or t), and doc-string is an
optional documentation string not beginning with ":Doc-Section ...".
If name{s} is a symbol it is treated as the singleton list containing
that symbol.  The effect of this event is to union the given symbols
into the list of "untouchable variables" in the current world if fn-p is
nil, else to union the symbols into the list of "untouchable
functions".  This event is redundant if every symbol listed is already
a member of the appropriate untouchables list (variables or functions).

When a symbol is on the untouchables list it is syntactically illegal
for any event to call a function or macro of that name, if fn-p is
non-nil, or to change the value of a state global variable of that
name, if fn-p is nil.  Thus, the effect of pushing a function symbol,
name, onto untouchables is to prevent any future event from using that
symbol as a function or macro, or as a state global variable (according
to fn-p).  This is generally done to "fence off" some primitive
function symbol from "users" after the developer has used the symbol
freely in the development of some higher level mechanism.

Also see REMOVE-UNTOUCHABLE.

REMOVE-BINOP    remove the association of a function name with a macro name

The form (remove-binop macro-fn) is an abbreviation for the form
(remove-macro-fn macro-fn).  See REMOVE-MACRO-FN.

REMOVE-DEFAULT-HINTS    remove from the default hints

     Examples:
     (remove-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
REMOVE-DEFAULT-HINTS! for a corresponding non-local event).

     General Form:
     (remove-default-hints lst)

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

If some elements of the given list do not belong to the existing default
hints, they will simply be ignored by this event.

Also See SET-DEFAULT-HINTS, see ADD-DEFAULT-HINTS, and
see DEFAULT-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!.

REMOVE-DEFAULT-HINTS!    remove from the default hints non-locally

Please see REMOVE-DEFAULT-HINTS, which is the same as
remove-default-hints!  except that the latter is not local to the
encapsulate or the book in which it occurs.  Probably
remove-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.

REMOVE-DIVE-INTO-MACRO    removes association of proof-checker diving function with macro name

     Example:
     (remove-dive-into-macro logand)

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

REMOVE-INVISIBLE-FNS    make some unary functions no longer invisible

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

The setting above has makes unary functions unary- and foo no longer
"invisible" for the purposes of applying permutative :rewrite rules to
binary-+ trees.

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

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

See ADD-INVISIBLE-FNS and also see INVISIBLE-FNS-TABLE
and see SET-INVISIBLE-FNS-TABLE.

REMOVE-MACRO-ALIAS    remove the association of a function name with a macro name

     Example:
     (remove-macro-alias append)

     General Form:
     (remove-macro-alias macro-name)

See MACRO-ALIASES-TABLE for a discussion of macro aliases; also
see ADD-MACRO-ALIAS.  This form sets macro-aliases-table to the
result of deleting the key macro-name from that table.  If the name
does not occur in the table, then this form still generates an event,
but the event has no real effect.

REMOVE-MACRO-FN    remove the association of a function name with a macro name

     Example:
     (remove-macro-fn binary-append)

     General Form:
     (remove-macro-fn macro-fn)

See ADD-MACRO-FN for a discussion of how to associate a macro
name with a function name.  This form sets untrans-table to the result
of deleting the association of a macro name with the given binary
function name.  If the function name has no such association, then this
form still generates an event, but the event has no real effect.

REMOVE-NTH-ALIAS    remove a symbol alias for printing of nth/update-nth terms

     Example:
     (remove-nth-alias append)

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

See NTH-ALIASES-TABLE for further discussion; also see
ADD-NTH-ALIAS.  This form sets nth-aliases-table to the result of
deleting the key alias-name from that table.  If the name does not
occur in the table, then this form still generates an event, but the
event has no real effect.

REMOVE-OVERRIDE-HINTS    delete from the list of override-hints

See OVERRIDE-HINTS for a discussion of override-hints.  Here we
describe how to delete from the list of override-hints.  Note that the
effects of remove-override-hints events are local to the books or
encapsulate events in which they reside; see
REMOVE-OVERRIDE-HINTS! to avoid that restriction.  Also see
ADD-OVERRIDE-HINTS and see SET-OVERRIDE-HINTS.

     General Form:
     (remove-override-hints form)

where form should evaluate to a list of computed hint forms.  The effect
of this event is to set the list of override-hints to the result of
deleting each element of the evaluation result from the override-hints,
if that element indeed belongs to the override-hints; no check is made
that these elements are actually elements of the existing
override-hints.

REMOVE-OVERRIDE-HINTS!    delete non-locally from the list of override-hints

Remove-override-hints! is the same as remove-override-hints, except
that the former is not local to books or encapsulate events in which it
occurs.  See REMOVE-OVERRIDE-HINTS; also see
ADD-OVERRIDE-HINTS and see SET-OVERRIDE-HINTS.

REMOVE-UNTOUCHABLE    remove names from lists of untouchable symbols

     Example Forms:
     (remove-untouchable my-var nil) ; then state global my-var is not untouchable
     (remove-untouchable set-mem t)  ; then function set-mem is not untouchable

Also see PUSH-UNTOUCHABLE.

This documentation topic is directed at those who build systems on top
of ACL2.  We first describe a means for removing restrictions related to
so-called "untouchables": functions (or macros) that cannot be called,
or state global variables that cannot be modified or unbound, without
intervention that requires an active trust tag (see DEFTTAG).
Then we describe the remove-untouchable event.

We begin by discussing untouchable state global variables
temp-touchable-vars and temp-touchable-fns, which initially have value
nil.  These can often be used in place of remove-untouchable.  When the
value is t, no variable (respectively, no function or macro) is treated
as untouchable, regardless of the set of initial untouchables or the
remove-untouchable or push-untouchable events that have been admitted.
Otherwise the value of each of these two variables is a symbol-listp,
and no member of this list is treated as an untouchable variable (in
the case of temp-touchable-vars) or as an untouchable function or macro
(in the case of temp-touchable-fns).  These two state global variables
can be set by set-temp-touchable-vars and set-temp-touchable-fns,
respectively, provided there is an active trust tag (see
DEFTTAG).  Here is an illustrative example.  This macro executes the
indicated forms in a context where there are no untouchable variables,
but requires an active trust tag when invoked.

     (defmacro with-all-touchable (&rest forms)
       `(progn!
         :state-global-bindings
         ((temp-touchable-vars t set-temp-touchable-vars))
         (progn! ,@forms)))

An equivalent version, which however is not recommended since
state-global-let* may have surprising behavior in raw Lisp, is as
follows.

     (defmacro with-all-touchable (&rest forms)
       `(progn!
         (state-global-let*
          ((temp-touchable-vars t set-temp-touchable-vars))
          (progn! ,@forms))))

Finally, the value t for temp-touchable-vars removes the requirement
that built-in state globals cannot be made unbound (with
makunbound-global).

We now turn to the remove-untouchable event, in case the approach above
is for some reason not adequate.  This event is illegal by default,
since it can be used to provide access to ACL2 internal functions and
data structures that are intentionally made untouchable for the user.
If you want to call it, you must first create an active trust tag; see
DEFTTAG.

     General Form:
     (remove-untouchable name{s}  fn-p :doc doc-string)

where name{s} is a non-nil symbol or a non-nil true list of symbols,
fn-p is any value (but generally nil or t), and doc-string is an
optional documentation string not beginning with ":Doc-Section ...".
If name{s} is a symbol it is treated as the singleton list containing
that symbol.  The effect of this event is to remove the given symbols
from the list of "untouchable variables" in the current world if fn-p
is nil, else to remove the symbols into the list of "untouchable
functions".  This event is redundant if no symbol listed is a member of
the appropriate untouchables list (variables or functions).

RESET-PREHISTORY    reset the prehistory

     Examples:
     (reset-prehistory)     ; restart command numbering at 0
     (reset-prehistory nil) ; same as above
     (reset-prehistory t)   ; as above except also disable ubt-prehistory

     General Forms:
     (reset-prehistory)
     (reset-prehistory permanent-p)
     (reset-prehistory permanent-p doc-string)

where permanent-p is t or nil, and doc-string is an optional
documentation string not beginning with ":Doc-Section ...".  After
execution of this command, ACL2 will change the numbering provided by
its history utilities so that this reset-prehistory command (or the
top-level compound command containing it, which for example might be an
include-book) is assigned the number 0.  The only way to undo this
command is with command ubt-prehistory.  However, even that is
disallowed if permanent-p is t.

Note that the second argument of certify-book, which specifies the
number of commands in the certification world (i.e., since
ground-zero), is not sensitive to reset-prehistory; rather, it expects
the number of commands since ground-zero.  To see such commands, :pbt
:start.

A reset-prehistory event with value nil for permanent-p (the default)
is always skipped during certify-book and include-book (indeed,
whenever ld-skip-proofsp is t).  Otherwise one would find the history
numbering reset to 0 just by virtue of including (or certifying) a book
-- probably not what was intended.

See UBT-PREHISTORY for how to undo a reset-prehistory command
that does not have a permanent-p of t.

RETURN-LAST-TABLE    install special raw Lisp behavior

Please first see RETURN-LAST for relevant background.

This table is for advanced users only, and requires an active trust tag
(see DEFTTAG).  We recommend that you do not modify this table
directly, but instead use the macro defmacro-last.  Here we augment
that discussion with some highly technical observations that can
probably be ignored if you use defmacro-last.

This table has a :guard requiring that each key be a symbol defined in
raw Lisp, generally as a macro, and requiring that each non-nil value
be associated either with a symbol that names a macro defined in ACL2,
or else with a list of one element containing such a symbol.  The table
can only be modified when there is an active trust tag; see
DEFTTAG.  If a key is associated with the value nil, then that key is
treated as though it were not in the table.

Note that keys of this table are not eligible to be bound by flet.  The
current value of this table may be obtained by evaluating the form
(table-alist 'return-last-table (w state)).  The built-in constant
*initial-return-last-table* holds the initial value of this table.

RULER-EXTENDERS    control for ACL2's termination and induction analyses

*Introduction*

Consider the following recursive definition, which returns a list of
threes of length one more than the length of x.

       (defun f (x)
         (cons 3
               (if (consp x)
                   (f (cdr x))
                 nil)))

One might expect ACL2's termination analysis to admit this function,
since we know that (cdr x) is "smaller" than x if (consp x) is true.
(By default, ACL2's notion of "smaller" is ordinary natural-number <,
and the argument x is measured by applying function acl2-count to x.)
However, that termination analysis does not consider IF tests, like
(consp x) above, when they occur under calls of functions other than
IF, such as CONS in the case above.

One way to overcome this problem is to "lift" the IF test to the top
level, as follows.

       (defun f (x)
         (if (consp x)
             (cons 3 (f (cdr x)))
           (cons 3 nil)))

But another way to overcome the problem is to tell ACL2 to extend its
termination (and induction) analysis through calls of cons, as follows.

       (defun f (x)
         (declare (xargs :ruler-extenders (cons)))
         (cons 3
               (if (consp x)
                   (f (cdr x))
                 nil)))

You may even wish to provide value :all instead of an explicit list of
ruler-extenders, so that no function call blocks the termination
analysis:

       (defun f (x)
         (declare (xargs :ruler-extenders :all))
         (cons 3
               (if (consp x)
                   (f (cdr x))
                 nil)))

Alternatively, you can omit the XARGS :RULER-EXTENDERS form, instead
modifying the global default set of ruler-extenders:

       (set-ruler-extenders :all)

       ; or, for example:
       (set-ruler-extenders '(cons return-last))

You can call the function default-ruler-extenders as follows to see the
current global default set of ruler-extenders:

     (default-ruler-extenders (w state))

We conclude this introduction by considering the handling of LET
expressions by termination analysis.  Consider the following example.

       (defun fact (n)
         (the (integer 1 *)
              (if (posp n)
                  (* n (fact (1- n)))
                1)))

ACL2 treats the call of THE in the body of this definition as follows.

       (let ((var (if (posp n)
                      (* n (fact (1- n)))
                    1)))
         (if (and (integerp var) (<= 1 var))
             var
           <some_error>))

A LET expression, in turn, is treated as a LAMBDA application:

       ((lambda (var)
          (if (if (integerp var)
                  (not (< var 1))
                nil)
              var
            <some_error>))
        (if (posp n)
            (* n (fact (1- n)))
          1))

Notice that the posp test, which governs the recursive call of fact, is
inside an argument of a function application, namely the application of
the LAMBDA expression.  So by default, ACL2 will not consider this posp
test in its termination analysis.  The keyword :LAMBDAS in the list of
ruler-extenders denotes all calls of lambda expressions, much as the
inclusion of CONS in the ruler-extenders denotes all calls of CONS.
The following definition is thus accepted by ACL2.

       (defun fact (n)
         (declare (xargs :ruler-extenders (:lambdas)))
         (the (integer 1 *)
              (if (posp n)
                  (* n (fact (1- n)))
                1)))

As a convenience, ACL2 allows the symbol :lambdas in place of
(:lambdas), and in fact the former will also include the default
ruler-extenders: RETURN-LAST (which comes from macroexpansion of calls
of PROG2$, EC-CALL, and others) and MV-LIST.

IMPORTANT REMARKS.  (1) Notice that the argument to set-ruler-extenders
is evaluated, but the argument to :RULER-EXTENDERS in XARGS is not
evaluated.  (2) Do not put macro names in your list of ruler-extenders.
For example, if you intend that + should not block the termination
analysis, in analogy to cons in the example above, then the list of
ruler-extenders should include binary-+, not +.  Of course, if you use
:all then this is not an issue, but see the next remark.  (3) Also
please note that by taking advantage of the ruler-extenders, you may be
complicating the induction scheme stored for the function, whose
computation takes similar advantage of the additional IF structure that
you are specifying.

Below we describe the notion of ruler-extenders in detail, as well as
how to set its default using set-ruler-extenders.

*Details*

We begin by discussing how to set the ruler-extenders by using the macro
set-ruler-extenders; below we will discuss the use of keyword
:ruler-extenders in XARGS declare forms.

     Examples:
     (set-ruler-extenders :basic) ; return to default
     (set-ruler-extenders *basic-ruler-extenders*) ; same as immediately above
     (set-ruler-extenders :all) ; every governing IF test rules a recursive call
     (set-ruler-extenders :lambdas) ; LET does not block termination analysis
     (set-ruler-extenders (cons :lambdas *basic-ruler-extenders*))
                                    ; same as immediately above
     (set-ruler-extenders '(f g)) ; termination analysis goes past calls of f, g

     General Form:
     (set-ruler-extenders val)

where val evaluates to one of :basic, :all, :lambdas, or a true list of
symbols containing no keyword other than, optionally, :lambdas.

When a recursive definition is submitted to ACL2 (in :logic mode), the
recursion must be proved to terminate; see DEFUN.  More
precisely, ACL2 explores the IF structure of the body of the definition
to accumulate the tests that "rule" any given recursive call.  The
following example reviews how this works.  Suppose that f has already
been defined.

       (defun g (x y)
         (declare (xargs :measure (+ (acl2-count x) (acl2-count y))))
         (if (consp x)
             (g (cdr x) y)
           (if (consp y)
               (f (g x (cdr y)))
             (f (list x y)))))

ACL2 makes the following response to this proposed definition.  Notice
that the :measure proposed above must be proved to be an ACL2 ordinal --
that is, to satisfy O-P -- and that the arguments to each recursive
call must be smaller (in the sense of that measure and O<, which here
reduces to the ordinary < relation) than the formals under the
assumption of the ruling IF tests.  The first IMPLIES term below thus
corresponds to the recursive call (g (cdr x) y), while the second
corresponds to the recursive call (g x (cdr y)).

       For the admission of G we will use the relation O< (which is known
       to be well-founded on the domain recognized by O-P) and the measure
       (+ (ACL2-COUNT X) (ACL2-COUNT Y)).  The non-trivial part of the measure
       conjecture is

       Goal
       (AND (O-P (+ (ACL2-COUNT X) (ACL2-COUNT Y)))
            (IMPLIES (CONSP X)
                     (O< (+ (ACL2-COUNT (CDR X)) (ACL2-COUNT Y))
                         (+ (ACL2-COUNT X) (ACL2-COUNT Y))))
            (IMPLIES (AND (NOT (CONSP X)) (CONSP Y))
                     (O< (+ (ACL2-COUNT X) (ACL2-COUNT (CDR Y)))
                         (+ (ACL2-COUNT X) (ACL2-COUNT Y))))).

Now consider the following alternate version of the above definition.

       (defun g (x y)
         (declare (xargs :measure (+ (acl2-count x) (acl2-count y))))
         (if (consp x)
             (g (cdr x) y)
           (f (if (consp y)
                  (g x (cdr y))
                (list x y)))))

The first test, (consp x), still rules the first recursive call, (g
(cdr x) y).  And the negation of that test, namely (not (consp x)),
still rules the second recursive call (g x (cdr y)).  But the call of f
blocks the top-down exploration of the IF structure of the body of g,
so (consp y) does not rule that second recursive call, which (again) is
(g x (cdr y)).  As a result, ACL2 fails to admit the above definition.

Set-ruler-extenders is provided to overcome the sort of blocking
described above.  Suppose for example that the following event is
submitted:

       (set-ruler-extenders '(f))

Then the alternate definition of g above is admissible, because the call
of f no longer blocks the top-down exploration of the IF structure of
the body of g: that is, (consp y) becomes a ruler of the recursive call
(g x (cdr y)).  In this case, we say that f is a "ruler-extender".  The
same result obtains if we first submit

       (set-ruler-extenders :all)

as this removes all function calls as blockers of the top-down
analysis.  In other words, with :all it is the case that for every
recursive call, every test argument of a superior call of IF
contributes a ruler of that recursive call.

ACL2 handles LET (and LET*) expressions by translating them to LAMBDA
expressions (see TERM).  The next examples illustrates
termination analysis involving such expressions.  First consider the
following (admittedly inefficient) definition.

       (defun fact (n)
         (let ((k (if (natp n) n 0)))
           (if (equal k 0)
               1
             (* k (fact (+ -1 k))))))

ACL2 translates the body of this definition to a LAMBDA application,
essentially:

       ((lambda (k)
          (if (equal k 0)
              1
            (* k (fact (+ -1 k)))))
        (if (natp n) n 0))

As with the application of any function other than IF, the top-down
termination analysis does not dive into arguments: the LAMBDA blocks the
continuation of the analysis into its argument.  But here, the argument
of the LAMBDA is (if (natp n) n 0), which has no recursive calls to
consider anyhow.  What is more interesting: ACL2 does continue its
termination analysis into the body of the LAMBDA, in an environment
binding the LAMBDA formals to its actuals.  In this case, the
termination analysis thus continues into the term

       (if (equal k 0)
           1
         (* k (fact (+ -1 k))))

in the environment that binds k to the term (if (natp n) n 0).  Thus,
the proof obligation is successfully discharged, as reported by ACL2:

       For the admission of FACT we will use the relation O< (which is known
       to be well-founded on the domain recognized by O-P) and the measure
       (ACL2-COUNT N).  The non-trivial part of the measure conjecture is

       Goal
       (IMPLIES (NOT (EQUAL (IF (NATP N) N 0) 0))
                (O< (ACL2-COUNT (+ -1 (IF (NATP N) N 0)))
                    (ACL2-COUNT N))).
       .....
       Q.E.D.

       That completes the proof of the measure theorem for FACT.

But now consider the following definition, in which the recursion takes
place inside the argument of the LAMBDA rather than inside the LAMBDA
body.

       (defun app (x y)
         (let ((result (if (endp x)
                           y
                         (cons (car x)
                               (app (cdr x) y)))))
           (if (our-test result)
               result
             0)))

Writing the body in LAMBDA notation:

       ((lambda (result)
          (if (our-test result)
              result
            0))
        (if (endp x)
            y
          (cons (car x)
                (app (cdr x) y))))

By default, the LAMBDA call blocks the top-down termination analysis
from proceeding into the term (if (endp x) ...).  To solve this, one can
submit the event:

       (set-ruler-extenders :lambdas)

The above definition of app is then admitted by ACL2, because the
termination analysis is no longer blocked by the LAMBDA call.

The example just above illustrates that the heuristically-chosen
measure is suitably sensitive to the ruler-extenders.  Specifically:
that measure is the application of acl2-count to the first formal
parameter of the function that is tested along every branch of the
relevant IF structure (as determined by the rulers) and occurs as a
proper subterm at the same argument position in every recursive call.
The heuristics for choosing the controller-alist for a definition rule
are similarly sensitive to the ruler-extenders (see DEFINITION).

The remarks above for defun events are equally applicable when a
definition sits inside a mutual-recursion event, except of course that
in this case, a "recursive call" is a call of any function being
defined by that mutual-recursion event.

Rules of class :definition are sensitive to set-ruler-extenders in
analogy to the case of defun events.

This macro generates a call (table acl2-defaults-table :ruler-extenders
val) and hence is local to any books and encapsulate events in which it
occurs. See ACL2-DEFAULTS-TABLE.  The current list of
ruler-extenders may be obtained as

       (cdr (assoc-eq :ruler-extenders
            (table-alist 'acl2-defaults-table (w state))))

or more conveniently, as:

       (default-ruler-extenders (w state))

Note that evaluation of (set-ruler-extenders lst), where lst evaluates
to a list, does not necessarily include the default ruler-extenders --
i.e., those included for the argument, :basic -- which are the elements
of the list constant *basic-ruler-extenders*, namely return-last and
mv-list.  You may, of course, include these explicitly in your list
argument.

We conclude our discussion by noting that the set of ruler-extenders can
affect the induction scheme that is stored with a recursive definition.
The distributed book books/misc/misc2/ruler-extenders-tests.lisp
explains how induction schemes are derived in this case.  Consider the
following example.

       (defun tree-of-nils-p (x)
         (if (consp x)
             (and (tree-of-nils-p (car x))
                  (tree-of-nils-p (cdr x)))
           (null x)))

The above definition generates the following induction scheme.  Note
that (and u v) expands to (if u v nil), which explains why the term
(tree-of-nils-p (car x)) rules the recursive call (tree-of-nils-p (cdr
x)), resulting in the hypothesis (tree-of-nils-p (car x)) in the final
conjunct below.

       (AND (IMPLIES (NOT (CONSP X)) (:P X))
            (IMPLIES (AND (CONSP X)
                          (NOT (TREE-OF-NILS-P (CAR X)))
                          (:P (CAR X)))
                     (:P X))
            (IMPLIES (AND (CONSP X)
                          (TREE-OF-NILS-P (CAR X))
                          (:P (CAR X))
                          (:P (CDR X)))
                     (:P X)))

Now consider the following variant of the above definition, in which a
call of the function identity blocks the termination analysis.

       (defun tree-of-nils-p (x)
         (if (consp x)
             (identity (and (tree-of-nils-p (car x))
                            (tree-of-nils-p (cdr x))))
           (null x)))

This time the induction scheme is as follows, since only the top-level
IF test contributes rulers to the termination analysis.

       (AND (IMPLIES (NOT (CONSP X)) (:P X))
            (IMPLIES (AND (CONSP X)
                          (:P (CAR X))
                          (:P (CDR X)))
                     (:P X)))

But now suppose we first designate identity as a ruler-extender.

     (set-ruler-extenders '(identity))

Then the induction scheme generated for the both of the above variants
of tree-of-nils-p is the one shown for the first variant, which is
reasonable because both definitions now produce essentially the same
termination analysis.

SET-BACKCHAIN-LIMIT    sets the backchain-limit used by the type-set and rewriting mechanisms

Note: This is an event!  It does not print the usual event summary but
nevertheless changes the ACL2 logical world and is so recorded.
Moreover, its effect is to set the acl2-defaults-table, and hence its
effect is local to the book or encapsulate form containing it; see
ACL2-DEFAULTS-TABLE.

This event sets the global backchain-limit used by the ACL2 type-set
and rewriting mechanisms.  Its value may be a cons whose car and cdr
are each either nil or a non-negative integer.  Its value x may also be
nil or a non-negative integer, which is treated as a cons whose car and
cdr are both x.

The car is used to limit backchaining used by the ACL2 type-set
mechanism, while the cdr is used to limit backchaining used by the
rewriting mechanism.  See BACKCHAIN-LIMIT for details about how
backchain-limits are used.  Rewrite backchain limits may also be
installed at the level of hints; see HINTS for a discussion of
:backchain-limit-rw.

     :set-backchain-limit nil  ; do not impose any additional limits
     :set-backchain-limit 0    ; allow only type-set reasoning for rewriting
                               ; hypotheses
     :set-backchain-limit 500  ; allow backchaining to a depth of no more
                               ; than 500 for rewriting hypotheses
     (set-backchain-limit 500) ; same as above
     :set-backchain-limit (500 500)
                               ; same as above
     (set-backchain-limit '(500 500))
                               ; same as above
     (set-backchain-limit '(3 500))
                               ; allow type-set backchaining to a depth of no more
                               ; than 3 and rewriter backchaining to a depth of no
                               ; more than 500

The default limit is (nil nil).

SET-BOGUS-DEFUN-HINTS-OK    allow unnecessary "mutual recursion"

     General Forms:
     (set-bogus-defun-hints-ok t)
     (set-bogus-defun-hints-ok nil)
     (set-bogus-defun-hints-ok :warn)

By default, ACL2 causes an error when the keyword :hints is supplied in
an xargs declare form for a definition (see DEFUN).  This
behavior can be defeated with (set-bogus-defun-hints-ok t), or if you
still want to see a warning in such cases, (set-bogus-defun-hints-ok
:warn).

SET-BOGUS-MUTUAL-RECURSION-OK    allow unnecessary "mutual recursion"

     Examples:
     (set-bogus-mutual-recursion-ok t)
     (set-bogus-mutual-recursion-ok nil)
     (set-bogus-mutual-recursion-ok :warn)

By default, ACL2 checks that when a "clique" of more than one function
is defined simultaneously (using mutual-recursion or defuns), then
every body calls at least one of the functions in the "clique."  Below,
we refer to definitional events that fail this check as "bogus" mutual
recursions.  The check is important because ACL2 does not store
induction schemes for functions defined with other functions in a
mutual-recursion or defuns event.  Thus, ACL2 may have difficulty
proving theorems by induction that involve such functions.  Moreover,
the check can call attention to bugs, since users generally intend that
their mutual recursions are not bogus.

Nevertheless, there are times when it is advantageous to allow bogus
mutual recursions, for example when they are generated mechanically,
even at the expense of losing stored induction schemes.  The first
example above allows bogus mutual recursion.  The second example
disallows bogus mutual recursion; this is the default.  The third
example allows bogus mutual recursion, but prints an appropriate
warning.

Note: This is an event!  It does not print the usual event summary but
nevertheless changes the ACL2 logical world and is so recorded.
Moreover, its effect is to set the acl2-defaults-table, and hence its
effect is local to the book or encapsulate form containing it; see
ACL2-DEFAULTS-TABLE.

     General Form:
     (set-bogus-mutual-recursion-ok flg)

where flg is either t, nil, or :warn.

SET-CASE-SPLIT-LIMITATIONS    set the case-split-limitations

     Examples:
     (set-case-split-limitations '(500 100))
     (set-case-split-limitations 'nil)
     (set-case-split-limitations '(500 nil))

The first of these prevents clausify from trying the
subsumption/replacement (see below) loop if more than 500 clauses are
involved.  It also discourages the clause simplifier from splitting
into more than 100 cases at once.

Note: This is an event!  It does not print the usual event summary but
nevertheless changes the ACL2 logical world and is so recorded.
Moreover, its effect is to set the acl2-defaults-table, and hence its
effect is local to the book or encapsulate form containing it; see
ACL2-DEFAULTS-TABLE.

Also see HINTS for discussion of a related hint,
:case-split-limitations.

     General Form:
     (set-case-split-limitations lst)

where lst is either nil (denoting a list of two nils), or a list of
length two, each element of which is either nil or a natural number.
When nil is used as an element, it is treated as positive infinity.  The
default setting is (500 100).

The first number specifies the maximum number of clauses that may
participate in the "subsumption/replacement" loop.  Because of the
expensive nature of that loop (which compares every clause to every
other in a way that is quadratic in the number of literals in the
clauses), when the number of clauses exceeds about 1000, the system
tends to "go into a black hole," printing nothing and not even doing
many garbage collections (because the subsumption/replacement loop does
not create new clauses so much as it just tries to delete old ones).
The initial setting is lower than the threshold at which we see
noticeably bad performance, so you probably will not see this behavior
unless you have raised or disabled the limit.

Why raise the subsumption/replacement limit?  The
subsumption/replacement loop cleans up the set of subgoals produced by
the simplifier.  For example, if one subgoal is

     (implies (and p q r) s)            [1]

and another is

     (implies (and p (not q) r) s)      [2]

then the subsumption/replacement loop would produce the single subgoal

     (implies (and p r) s)              [3]

instead.  This cleanup process is simply skipped when the number of
subgoals exceeds the subsumption/replacement limit.  But each subgoal
must nonetheless be proved.  The proofs of [1] and [2] are likely to
duplicate much work, which is only done once in proving [3].  So with a
low limit, you may find the system quickly produces a set of subgoals
but then takes a long time to prove that set.  With a higher limit, you
may find the set of subgoals to be "cleaner" and faster to prove.

Why lower the subsumption/replacement limit?  If you see the system go
into a "black hole" of the sort described above (no output, and few
garbage collections), it could due to the subsumption/replacement loop
working on a large set of large subgoals.  You might temporarily lower
the limit so that it begins to print the uncleaned set of subgoals.
Perhaps by looking at the output you will realize that some function
can be disabled so as to prevent the case explosion.  Then raise or
disable the limit again!

The second number in the case-split-limitations specifies how many case
splits the simplifier will allow before it begins to shut down case
splitting.  In normal operation, when a literal rewrites to a nest of
IFs, the system simplifies all subsequent literals in all the contexts
generated by walking through the nest in all possible ways.  This can
also cause the system to "go into a black hole" printing nothing except
garbage collection messages.  This "black hole" behavior is different
from than mentioned above because space is typically being consumed at
a prodigious rate, since the system is rewriting the literals over and
over in many different contexts.

As the simplifier sweeps across the clause, it keeps track of the
number of cases that have been generated.  When that number exceeds the
second number in case-split-limitations, the simplifier stops rewriting
literals.  The remaining, unrewritten, literals are copied over into
the output clauses.  IFs in those literals are split out, but the
literals themselves are not rewritten.  Each output clause is then
attacked again, by subsequent simplification, and eventually the
unrewritten literals in the tail of the clause will be rewritten
because the earlier literals will stabilize and stop producing case
splits.

The default setting of 100 is fairly low.  We have seen successful
proofs in which thousands of subgoals were created by a simplification.
By setting the second number to small values, you can force the system
to case split slowly.  For example, a setting of 5 will cause it to
generate "about 5" subgoals per simplification.

You can read about how the simplifier works in the book Computer-Aided
Reasoning: An Approach (Kaufmann, Manolios, Moore); also see
INTRODUCTION-TO-THE-THEOREM-PROVER for a detailed tutorial on using
the ACL2 prover.  If you think about it, you will see that with a low
case limit, the initial literals of a goal are repeatedly simplified,
because each time a subgoal is simplified we start at the left-most
subterm.  So when case splitting prevents the later subterms from being
fully split out, we revisit the earlier terms before getting to the
later ones.  This can be good.  Perhaps it takes several rounds of
rewriting before the earlier terms are in normal form and then the
later terms rewrite quickly.  But it could happen that the earlier
terms are expensive to rewrite and do not change, making the strategy
of delayed case splits less efficient.  It is up to you.

Sometimes the simplifier produces more clauses than you might expect,
even with case-split-limitations in effect.  As noted above, once the
limit has been exceeded, the simplifier does not rewrite subsequent
literals.  But IFs in those literals are split out nonetheless.
Furthermore, the enforcement of the limit is - as described above - all
or nothing: if the limit allows us to rewrite a literal then we rewrite
the literal fully, without regard for limitations, and get as many
cases as "naturally" are produced.  It quite often happens that a
single literal, when expanded, may grossly exceed the specified limits.

If the second "number" is nil and the simplifier is going to produce
more than 1000 clauses, a "helpful little message" to this effect is
printed out.  This output is printed to the system's "comment window"
not the standard proofs output.

SET-CHECKPOINT-SUMMARY-LIMIT    control printing of key checkpoints upon a proof's failure

See SET-GAG-MODE for a discussion of key checkpoints.

     Examples:

     ; (Default) When a proof fails, print all key checkpoints before
     ; induction but at most 3 key checkpoints after induction:
     (set-checkpoint-summary-limit (nil . 3))

     ; When a proof fails, print at most 3 key checkpoints before
     ; induction but all 3 key checkpoints after induction:
     (set-checkpoint-summary-limit (3 . nil))

     ; When a proof fails, print at most 3 key checkpoints before
     ; induction and at most 5 key checkpoints after induction:
     (set-checkpoint-summary-limit (3 . 5))

     ; When a proof fails, print at most 3 key checkpoints before
     ; induction and at most 3 key checkpoints after induction:
     (set-checkpoint-summary-limit (3 . 3))
     ; or equivalently,
     (set-checkpoint-summary-limit 3)

     ; When a proof fails, print all key checkpoints:
     (set-checkpoint-summary-limit (nil . nil))
     ; or equivalently,
     (set-checkpoint-summary-limit nil)

     ; When a proof fails, print no information at all about key checkpoints:
     (set-checkpoint-summary-limit t)

     General Forms:
     (set-checkpoint-summary-limit (n1 . n2))
     (set-checkpoint-summary-limit n)
     (set-checkpoint-summary-limit t)

where each of n1 and n2 is a natural number or nil.  For the second
form, n can be a natural number or nil and is treated as (n . n).  The
value t inhibits all printing of checkpoint summary information.  The
values n1 and n2 determine printing of key checkpoints generated before
the first induction and generated after the first induction,
respectively, where at most n1 or n2 (respectively) such key
checkpoints are printed unless the value is nil, in which case there is
no limitation.

The argument x for set-checkpoint-summary-limit, as described above,
may be quoted, i.e. supplied as 'x or (quote x).  Thus, you may use the
keyword form (see KEYWORD-COMMANDS) if you prefer, for example:

     :set-checkpoint-summary-limit (nil . 3)

SET-COMPILE-FNS    have each function compiled as you go along.

     Example Forms:
     (set-compile-fns t)    ; new functions compiled after DEFUN
     (set-compile-fns nil)  ; new functions not compiled after DEFUN

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

Also see COMP, because it may be more efficient in some Common
Lisps to compile many functions at once rather than to compile each one
as you go along.

     General Form:
     (set-compile-fns term)

where term is a variable-free term that evaluates to t or nil.  This
macro is equivalent to

     (table acl2-defaults-table :compile-fns term)

and hence is local to any books and encapsulate events in which it
occurs; see ACL2-DEFAULTS-TABLE.  However, unlike the above
simple call of the table event function (see TABLE), no output
results from a set-compile-fns event.

Set-compile-fns may be thought of as an event that merely sets a flag
to t or nil.  The flag's effect is felt when functions are defined, as
with defun.  If the flag is t, functions are automatically compiled
after they are defined, as are their executable counterparts (see
EXECUTABLE-COUNTERPART).  Otherwise, functions are not automatically
compiled.  Exception: The flag has no effect when explicit compilation
is suppressed; see COMPILATION.

Because set-compile-fns is an event, the old value of the flag is
restored when a set-compile-fns event is undone.

Even when :set-compile-fns t has been executed, functions are not
individually compiled when processing an include-book event.  If you
wish to include a book of compiled functions, we suggest that you first
certify it with the compilation flag set (see CERTIFY-BOOK) or
else compile the book by supplying the appropriate load-compiled-file
argument to include-book.  More generally, compilation via
set-compile-fns is suppressed when the state global variable
ld-skip-proofsp has value 'include-book.

SET-COMPILER-ENABLED    See COMPILATION.

SET-DEBUGGER-ENABLE    control whether Lisp errors and breaks invoke the Lisp debugger

     Forms (see below for explanations and GCL exceptions):

     (set-debugger-enable t)         ; enable breaks into the raw Lisp debugger
     (set-debugger-enable :break)    ; same as above
     :set-debugger-enable t          ; same as above
     (set-debugger-enable :break-bt) ; as above, but print a backtrace first
     (set-debugger-enable :bt-break) ; as above, but print a backtrace first
     (set-debugger-enable :bt)       ; print a backtrace but do not enter debugger
     (set-debugger-enable :never)    ; disable all breaks into the debugger
     (set-debugger-enable nil)       ; disable debugger except when calling break$

_Introduction._  Suppose we define foo in :program mode to take the car
of its argument.  This can cause a raw Lisp error.  ACL2 will then
return control to its top-level loop unless you enable the Lisp
debugger, as shown below (except:  the error message can be a little
different in GCL).

       ACL2 !>(defun foo (x) (declare (xargs :mode :program)) (car x))

       Summary
       Form:  ( DEFUN FOO ...)
       Rules: NIL
       Warnings:  None
       Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
        FOO
       ACL2 !>(foo 3)
       ***********************************************
       ************ ABORTING from raw Lisp ***********
       Error:  Attempt to take the car of 3 which is not listp.
       ***********************************************

       If you didn't cause an explicit interrupt (Control-C),
       then the root cause may be call of a :program mode
       function that has the wrong guard specified, or even no
       guard specified (i.e., an implicit guard of t).
       See :DOC guards.

       To enable breaks into the debugger (also see :DOC acl2-customization):
       (SET-DEBUGGER-ENABLE T)
       ACL2 !>(SET-DEBUGGER-ENABLE T)
       <state>
       ACL2 !>(foo 3)
       Error: Attempt to take the car of 3 which is not listp.
         [condition type: TYPE-ERROR]

       Restart actions (select using :continue):
        0: Abort entirely from this (lisp) process.
       [Current process: Initial Lisp Listener]
       [1] ACL2(1): [RAW LISP]

_Details._  ACL2 usage is intended to take place inside the ACL2
read-eval-print loop (see LP).  Indeed, in most Lisp
implementations ACL2 comes up inside that loop, as evidenced by the
prompt:

     ACL2 !>

However, one can occasionally hit a raw Lisp error.  Here is the above
example again, this time for a GCL implementation, which unfortunately
gives a slightly less aesthetic report.

       ACL2 !>(foo 3)

       Error: 3 is not of type LIST.
       Fast links are on: do (si::use-fast-links nil) for debugging
       Error signalled by CAR.
       Backtrace: funcall > system:top-level > lisp:lambda-closure > lp > acl2_*1*_acl2::foo > foo > car > system:universal-error-handler > system::break-level-for-acl2 > let* > UNLESS
       ACL2 !>

Here, the user has defined foo in :program mode, with an implicit guard
of t.  The ACL2 evaluator therefore called the Lisp evaluator, which
expected nil or a consp argument to car.

By default, ACL2 will return to its top-level loop (at the same level of
LD) when there is a raw Lisp error, as though a call of ER with flag
HARD has been evaluated.  If instead you want to enter the raw Lisp
debugger in such cases, evaluate the following form.

     (set-debugger-enable t)

You can subsequently return to the default behavior with:

     (set-debugger-enable nil)

Either way, you can enter the Lisp debugger from within the ACL2 loop by
evaluating (break$).  If you want break$ disabled, then evaluate the
following, which disables entry to the Lisp debugger not only for Lisp
errors but also when executing (break$).

     (set-debugger-enable :never)

The discussion above also applies to interrupts (from Control-C) in
some, but not all, host Common Lisps.

It remains to discuss options :break, :bt, :break-bt, and :bt-break.
Option :break is synonymous with option t, while option :bt prints a
backtrace (except in GCL, where a backtrace is already printed for
:break).  Options :break-bt and :bt-break are equivalent, and each has
the combined effect of :bt and :break: a backtrace is printed and then
the debugger is entered.

Note that set-debugger-enable applies not only to raw Lisp errors, but
also to ACL2 errors: those affected by break-on-error.  However, for
ACL2 errors, entering the debugger is controlled only by break-on-error,
not by set-debugger-enable; so for ACL2 errors, set-debugger-enable
values of :bt, :break-bt, and :bt-break have the same effect (namely,
of causing a backtrace to be printed, other than for GCL).

Remark for Common Lisp hackers (except for GCL).  You can customize the
form of the backtrace printed by entering raw Lisp (with :q) and then
redefining function print-call-history, whose definition immediately
precedes that of break-on-error in ACL2 source file ld.lisp.  Of
course, all bets are off when defining any function in raw Lisp, but as
a practical matter you are probably fine as long as your books are
ultimately certified with an unmodified copy of ACL2.  If you come up
with improvements to print-call-history, please pass them along to the
ACL2 implementors.

SET-DEFAULT-BACKCHAIN-LIMIT    sets the default backchain-limit used when admitting a rule

Note: This is an event!  It does not print the usual event summary but
nevertheless changes the ACL2 logical world and is so recorded.
Moreover, its effect is to set the acl2-defaults-table, and hence its
effect is local to the book or encapsulate form containing it; see
ACL2-DEFAULTS-TABLE.

This event sets the default backchain-limit used when a new rewrite,
linear, meta, or type-prescription rule is admitted.  Its value may be
a two-element list whose elements are each either nil or a non-negative
integer.  Its value x may also be nil or a non-negative integer, which
is treated as the two element list (x x).

The first element of the list is used to limit backchaining for a rule
of class type-prescription while the second element is used to limit
backchaining for the other three classes of rules mentioned above.  See
BACKCHAIN-LIMIT for details about how backchain-limits are
used.  The examples below assume that a new rule doesn't itself specify
a value for :backchain-limit-lst.

     :set-default-backchain-limit nil  ; do not impose backchain limits for the
                                       ; rule
     :set-default-backchain-limit 0    ; allow only type-set reasoning for
                                       ; relieving a new rule's hypotheses
     :set-default-backchain-limit 500  ; allow backchaining through a new rewrite,
                                       ; linear, or meta rule's hypotheses to a
                                       ; depth of no more than 500
     (set-default-backchain-limit 500) ; same as above
     :set-default-backchain-limit (nil 500)
                                       ; same as above
     (set-default-backchain-limit '(nil 500))
                                       ; same as above
     (set-default-backchain-limit '(3 500))
                                       ; for a new :type-prescription rule, allow
                                       ; type-set backchaining to a depth
                                       ; of no more than 3; for a new
                                       ; rule of class :rewrite, :linear,
                                       ; or :meta, allow backchaining to
                                       ; a depth of no more than 50
     (set-default-backchain-limit '(nil 500))
                                       ; do not limit backchaining for a
                                       ; new :type-prescription rule; for
                                       ; a new rule of class :rewrite,
                                       ; :linear, or :meta, allow
                                       ; backchaining to a depth of no
                                       ; more than 50

The initial default backchain-limit is nil.

SET-DEFAULT-HINTS    set the default hints

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

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
SET-DEFAULT-HINTS! for a corresponding non-local event).

     General Form:
     (set-default-hints lst)

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

Whenever a defthm or thm command is executed, the default hints are
appended to the right of any explicitly provided :hints in the command.
The same applies to defuns as well (:hints, :guard-hints, and (for
ACL2(r)) :std-hints).  The hints are then translated and processed just
as though they had been explicitly included.

Technically, we do not put restrictions on lst, beyond that it is a
true list.  It would be legal to execute

     (set-default-hints '(("Goal" :use lemma23)))

with the effect that the given hint is added to subsequent hints
supplied explicitly.  An explicit "Goal" hint would, however, take
priority, as suggested by the mention above of "appended to the right."

Note that set-default-hints sets the default hints as specified.  To
add to or remove from the current default, see
ADD-DEFAULT-HINTS and see REMOVE-DEFAULT-HINTS.  To see the
current default hints, see DEFAULT-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!.

For a related feature, which however is only for advanced system
builders, see OVERRIDE-HINTS.

SET-DEFAULT-HINTS!    set the default hints non-locally

Please see SET-DEFAULT-HINTS, which is the same as
set-default-hints!  except that the latter is not local to the
encapsulate or the book in which it occurs.  Probably set-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.

SET-DEFERRED-TTAG-NOTES    modify the verbosity of TTAG NOTE printing

     General Form:
     (set-deferred-ttag-notes val state)

where val is t or nil.

See DEFTTAG for a discussion of trust tags (ttags).  By
default, a "TTAG NOTE" is printed in order to indicate reliance on a
ttag.  When many such notes are printed, it may be desirable to avoid
seeing them all.  Upon evaluation of the form

     (set-deferred-ttag-notes t state)

ACL2 will enter a deferred mode for the printing of ttag notes.  In this
mode, only the first ttag note is printed for each top-level command,
and the remainder are summarized before the next top-level prompt (if
any) is printed, hence before the next command is evaluated.  That
summary is merely a list of ttags, but the summary explains that the
full ttag notes may be printed with the command (show-ttag-notes).

Note that (show-ttag-notes) spares you duplicate ttag notes.  If you
want to see every ttag note as it would normally appear, for maximum
security, do not evaluate the command (set-deferred-ttag-notes t
state).  You can undo the effect of this command, returning to an
immediate mode for printing ttag notes, by evaluating:

     (set-deferred-ttag-notes nil state)

SET-ENFORCE-REDUNDANCY    require most events to be redundant

     General Forms:
     (set-enforce-redundancy nil)   ; do not require redundancy (default)
     (set-enforce-redundancy t)     ; most events (see below) must be redundant
     (set-enforce-redundancy :warn) ; warn for most non-redundant events

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

     General Form:
     (set-enforce-redundancy flag)

where flag is nil, t, or :warn, as indicated above.  This macro is
essentially equivalent to

     (table acl2-defaults-table :enforce-redundancy flag)

and hence is local to any books and encapsulate events in which it
occurs; see ACL2-DEFAULTS-TABLE.  However, unlike the above
simple call of the table event function (see TABLE), no output
results from a set-enforce-redundancy event.

Set-enforce-redundancy may be thought of as an event that merely sets a
flag as indicated above, which determines whether most events, including
defun and defthm events, are allowed to be redundant; see
REDUNDANT-EVENTS.  The exceptions are deflabel, defpkg, encapsulate,
include-book, push-untouchable, remove-untouchable, set-body, and table
events.  Any other type of non-redundant event will cause an error if
flag is t and a warning if flag is nil, _except_ in the course of
carrying out an include-book form.

Note that because table events that set the acl2-defaults-table are
implicitly local, set-enforce-redundancy events are ignored when
including books.  However, the presence of the event
(set-enforce-redundancy t) in a book guarantees that its subsequent
definitions and theorems are redundant.  This can be a useful property
to maintain in library development, as we now describe.

An example of the use of this form can be found in the distributed books
under directory books/rtl/rel4/.  The intention in that directory has
been to put all the gory details in subdirectories support/ and
arithmetic/, so that the books in subdirectory lib/ contain only the
"exported" definitions and theorems.  This approach is useful for human
readability.  Moreover, suppose we want to prove new theorems in lib/.
Typically we wish to prove the new theorems using the existing books in
lib/; however, our methodology demands that the proofs go into books in
support/.  If every theorem in lib/ is redundant, then we can _develop_
the proofs in lib/ but then when we are done, _move_ each book with
such proofs into support/ as follows.  In any such book, we first
replace include-book forms referring to books in lib/ by include-book
forms referring to corresponding books in support/ and/or arithmetic/.
Then, we add suitable in-theory events to get us back into the original
lib/ proof environment.

The default behavior of the system is as though the :enforce-redundancy
value is nil.  The current behavior can be ascertained by evaluating the
following form.

     (cdr (assoc-eq :enforce-redundancy (table-alist 'acl2-defaults-table wrld)))

SET-GAG-MODE    modify the nature of proof output

     Examples:

     :set-gag-mode t      ; enable gag-mode, suppressing most proof commentary
     (set-gag-mode t)     ; same as above
     :set-gag-mode :goals ; same as above, but print names of goals when produced
     :set-gag-mode nil    ; disable gag-mode

     General Forms:
     (set-gag-mode val)
     :set-gag-mode val

where val is one of t, nil, or :goals.

The basic idea of gag-mode is to avoid much of the verbose output from
the theorem prover, leaving only output that is expected to be helpful.
You are strongly encouraged to put the form

     (set-gag-mode t) ; or, (set-gag-mode :goals)

in your ACL2 customization file; see ACL2-CUSTOMIZATION.  The
default value is :goals.

The basic idea of gag-mode is to focus attention on so-called "key
checkpoints".  By default, a checkpoint is a goal that cannot be
simplified.  (Below we discuss how to change this default.)  A key
checkpoint is a checkpoint that is not descended from another
checkpoint.  (Technical point: "Descended" signifies that both goals
are at the top level in the same forcing round, or are in the same
proof by induction.)  Successful ACL2 users generally focus their
attention on key checkpoints; for a discussion of how to use ACL2
prover output in an effective manner, see THE-METHOD, and see
INTRODUCTION-TO-THE-THEOREM-PROVER for a more detailed
tutorial.  In gag-mode, a key checkpoint is only displayed when ACL2 is
unable to make any further progress on that goal or some descendent of
it, other than with a proof by induction.

Evaluation of set-gag-mode t enters gag-mode, so that only key
checkpoints are printed.  Evaluation of set-gag-mode :goals also enters
gag-mode, but will additionally cause the name of a goal to be printed
as soon as it is generated (by invoking see
SET-PRINT-CLAUSE-IDS).  The :goals setting is useful for cases in
which the prover spends very little of its time generating goals to be
proved by induction, yet you want to see that it is making progress.
For finer-grained feedback about the simplifier's activity, see
DMR.

The current value of gag-mode is returned by a macro of the same name:

     (gag-mode) ; evaluates to t, nil, or :goals

(Remark for advanced users.  The notion of "checkpoint" can be modified
by the user.  The default, as discussed above, is for a checkpoint to
be a goal that cannot be simplified.  Put differently, a checkpoint is
acted on by one of the processes in the value of the form (@
checkpoint-processors); see @.  Any or all of the symbols
eliminate-destructors-clause, fertilize-clause, generalize-clause, or
eliminate-irrelevance-clause can be removed from this value in order
that invocation of the corresponding proof process does not cause its
input goal to be labeled a checkpoint.  For example, if you do not want
destructor elimination to be treated differently from simplification
for purposes of labeling checkpoints, you can evaluate the following
form (see ASSIGN):

     (assign checkpoint-processors
             (remove 'eliminate-destructors-clause
                     (@ checkpoint-processors)))

Note that the value of (@ checkpoint-processors) also affects the proof
tree display; see PROOF-TREE-DETAILS.  End of Remark.)

An alternative to gag-mode is to use proof-trees; see
PROOF-TREE.  With proof-trees it is not so important to avoid
excessive prover output, since the proof-tree display provides
structure that makes it easy to monitor proof attempts and navigate
output for a proof that has failed or seems to be failing.  Still,
output can take time to print, so you may get better performance with
gag-mode.

The intention of gag-mode is to show you only the parts of a proof
attempt that are relevant for debugging a failure; additional output is
generally more likely to be distracting than truly helpful.  But on
occasion you may want to see the full proof output after an attempt
made with gag-mode.  If so, then see PSO and see PSO!.
Since set-gag-mode takes responsibility for the saving of output,
related utility set-saved-output is disabled when gag-mode is active.
Also note that calling set-gag-mode erases the currently saved output,
if any.

You may notice that gag-mode tends to print relatively little
information about goals pushed for proof by sub-induction -- i.e., a
proof of *i.j, *i.j.k, etc.  The principle here is that sub-inductions
that do not succeed should generally be avoided, not analyzed for ways
to make them succeed.  Instead, the key checkpoint that generated the
goal pushed for this induction is more appropriate to analyze.  In
general, the "higher level" the checkpoint, the more worthy it is of
attention.  Thus, we suggest that look at the top-level checkpoints
before looking at those labeled "Key checkpoints under a top-level
induction".

SET-GUARD-CHECKING    control checking guards during execution of top-level forms

Detailed comments about the arguments of this function may be found
elsewhere: see GUARD-EVALUATION-TABLE.  Here we provide an
introduction to the use of set-guard-checking.

New users are encouraged to execute one of the following forms in order
to avoid evaluation errors due to guards:

     (set-guard-checking :none)
     (set-guard-checking nil)

The former avoids all guard-checking on user-defined functions and
should generally work fine for new users, the only drawback being
efficiency loss on compute-intensive problems.  All settings other than
:none check guards, but a value of nil allows evaluation to continue in
the logic when guards fail (avoiding the raw Lisp definition in that
case).

You may put one of the above forms in the "acl2-customization.lsp" file
in your current directory (see CBD) or your home directory; see
ACL2-CUSTOMIZATION.

Note that guards are not part of the ACL2 logic, and hence new users can
completely ignore the notion of guard (and the rest of this
documentation section after this paragraph!).  For example, (car 3) and
nil can be proved equal in the ACL2 logic, as follows, even though the
guard on car requires its first argument to be a cons pair or nil.

     (thm (equal (car 3) nil))

Moreover, unless your functions or top-level forms call built-in ACL2
functions that are defined in :program mode, the following property
will hold.

     Evaluation of (set-guard-checking :none) will allow evaluation of
     forms such as (car 3) to take place without error in the top level
     loop, not only when proving theorems.

If you feel bold, then you may wish to read the rest of this
documentation topic; also see GUARD.

See GUARD-EVALUATION-TABLE for a succinct table, with
associated discussion, that covers in detail the material presented in
the rest of the present topic.

The top-level ACL2 loop has a variable which controls which sense of
execution is provided.  To turn "guard checking on," by which we mean
that guards are checked at runtime, execute the top-level form
:set-guard-checking t.  To allow guard violations, do
:set-guard-checking nil, or do :set-guard-checking :none to turn off
all guard-checking, so that raw Lisp definitions of user-defined
functions are avoided unless their guard is t. The status of
guard-checking is reflected in the prompt.

     ACL2 !>

means guard checking is on and

     ACL2 >

means guard checking is off.  The exclamation mark can be thought of as
"barring" certain computations.  The absence of the mark suggests the
absence of error messages or unbarred access to the logical axioms.
Thus, for example

     ACL2 !>(car 'abc)

will signal an error, while

     ACL2 >(car 'abc)

will return nil.

We will return at the end of this documentation topic to discuss two
other values, :all and :nowarn, for :set-guard-checking.  We also note
that evaluation of built-in :program mode functions always takes place
in raw Lisp.

Whether guards are checked during evaluation is independent of the
default-defun-mode.  We note this simply because it is easy to confuse
":program mode" with "evaluation in Common Lisp" and thus with "guard
checking on;" and it is easy to confuse ":logic mode" with "evaluation
in the logic" and with "guard checking off."  But the
default-defun-mode determines whether newly submitted definitions
introduce programs or add logical axioms.  That mode is independent of
whether evaluation checks guards or not.  You can operate in :logic
mode with runtime guard checking on or off.  Analogously, you can
operate in :program mode with runtime guard checking on or off.

For further discussion on evaluation and guards see
GUARDS-AND-EVALUATION, in particular the exception for safe-mode in
the "Aside" there.  See GUARD for a general discussion of
guards.

Now we fulfill our promise above to discuss two other values for
:set-guard-checking:

     :set-guard-checking :nowarn
     :set-guard-checking :all

The meaning of these values is perhaps best described by the following
example provided by David Rager.

     ACL2 !>(defun my-test (expr)
              (declare (xargs :guard (true-listp expr)
                              :verify-guards nil))
              (if (atom expr)
                  expr
                (cons (my-test (car expr))
                      (my-test (cdr expr)))))

     The admission of MY-TEST is trivial, using the relation O< (which is
     known to be well-founded on the domain recognized by O-P) and the measure
     (ACL2-COUNT EXPR).  We could deduce no constraints on the type of MY-
     TEST.  However, in normalizing the definition we used primitive type
     reasoning.

     Summary
     Form:  ( DEFUN MY-TEST ...)
     Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
     Warnings:  None
     Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
      MY-TEST
     ACL2 !>(my-test '(a b c))

     ACL2 Warning [Guards] in TOP-LEVEL:  Guard-checking will be inhibited
     on recursive calls of the executable counterpart (i.e., in the ACL2
     logic) of MY-TEST.  To check guards on all recursive calls:
       (set-guard-checking :all)
     To leave behavior unchanged except for inhibiting this message:
       (set-guard-checking :nowarn)

     (A B C)
     ACL2 !>

If you think about evaluation of (my-test '(a b c)), you will see that
it leads to the recursive call (my-test 'a), which one might expect to
cause a guard violation since the symbol a is not a true-listp.
However, as the warning above explains, we do not by default check
guards on recursive calls.  The reason is efficiency -- imagine a
simple definition with a guard that is slow to evaluate.  The values
:nowarn and :all for :set-guard-checking have been introduced as ways
of dealing with the above warning.  The value :nowarn simply turns off
the warning above.  The value :all causes all guards to be checked,
even on recursive calls and even on all calls of non-built-in :program
mode functions -- unless, of course, a call is made of a function whose
guard has been verified (see VERIFY-GUARDS), where the
arguments satisfy the guard, in which case the corresponding call is
made in raw Lisp without subsidiary guard-checking.  We still say that
"guard-checking is on" after :set-guard-checking is invoked with values
t, :nowarn, and :all, otherwise (after value nil) we say
"guard-checking is off.

For technical reasons, :all does not have its advertised effect in the
case of built-in :program-mode functions.  If you are interested in
this technical detail, see the comment "In the boot-strap world..." in
source function oneify-cltl-code.

We conclude with a remark about the use of :set-guard-checking for
experimenting with ACL2 as a logic or as a programming language.  If one
views ACL2 as a logic, one may wish to use :set-guard-checking :none,
while if instead one views ACL2 as a functional programming language,
one may wish to use :set-guard-checking :all.  The following transcript
illustrates this distinction by way of example.  Specifically, (car 3)
is equal to nil in the ACL2 logic, but may be viewed as a programming
error.  The default of :set-guard-checking t is problematic for learning
ACL2 using :program mode functions, since one can get raw Lisp errors.
In the example below, the raw Lisp error occurs because foo implicitly
has a guard of t, hence (foo 3) is evaluated in raw Lisp, which leads
to a raw Lisp call of c[(car 3)].

     ACL2 !>(defun foo (x)
              (declare (xargs :mode :program))
              (car x))

     Summary
     Form:  ( DEFUN FOO ...)
     Rules: NIL
     Warnings:  None
     Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
      FOO
     ACL2 !>(foo 3)
     Error: Attempt to take the car of 3 which is not listp.
       [condition type: TYPE-ERROR]

     Restart actions (select using :continue):
      0: Abort entirely from this (lisp) process.
     [Current process: Initial Lisp Listener]
     [1] ACL2(1): [RAW LISP] :pop
     ACL2 !>:set-guard-checking :none

     Turning off guard checking entirely.  To allow execution in raw Lisp
     for functions with guards other than T, while continuing to mask guard
     violations, :SET-GUARD-CHECKING NIL.  See :DOC set-guard-checking.

     ACL2 >(foo 3)
     NIL
     ACL2 >:set-guard-checking :all

     Turning guard checking on, value :ALL.

     ACL2 !>(foo 3)

     ACL2 Error in TOP-LEVEL:  The guard for the function symbol CAR, which
     is (OR (CONSP X) (EQUAL X NIL)), is violated by the arguments in the
     call (CAR 3).  See :DOC trace for a useful debugging utility.  See :DOC
     set-guard-checking for information about suppressing this check with
     (set-guard-checking :none), as recommended for new users.

     ACL2 !>

SET-IGNORE-DOC-STRING-ERROR    allow ill-formed documentation strings

     General Forms:
     (set-ignore-doc-string-error nil)   ; :doc strings must be well-formed
     (set-ignore-doc-string-error t)     ; ill-formed :doc strings are ignored
     (set-ignore-doc-string-error :warn) ; ill-formed :doc strings are ignored
                                         ;   except for causing a warning

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

     General Form:
     (set-ignore-doc-string-error flag)

where flag is nil, t, or :warn, as indicated above.  This macro is
essentially equivalent to

     (table acl2-defaults-table :ignore-doc-string-error flag)

and hence is local to any books and encapsulate events in which it
occurs; see ACL2-DEFAULTS-TABLE.  However, unlike the above
simple call of the table event function (see TABLE), no output
results from a set-ignore-doc-string-error event.

Note that since defdoc events have the sole purpose of installing
documentation strings, these require well-formed documentation strings
even after executing a call of ignore-doc-string-error.

The default behavior of the system is as though the
:ignore-doc-string-error value is nil.  The current behavior can be
ascertained by evaluating the following form.

     (ignore-doc-string-error (w state))

SET-IGNORE-OK    allow unused formals and locals without an ignore or ignorable declaration

     Examples:
     (set-ignore-ok t)
     (set-ignore-ok nil)
     (set-ignore-ok :warn)

The first example above allows unused formals and locals, i.e.,
variables that would normally have to be declared ignored or ignorable.
The second example disallows unused formals and locals; this is the
default.  The third example allows them, but prints an appropriate
warning.

Note: This is an event!  It does not print the usual event summary but
nevertheless changes the ACL2 logical world and is so recorded.
Moreover, its effect is to set the acl2-defaults-table, and hence its
effect is local to the book or encapsulate form containing it; see
ACL2-DEFAULTS-TABLE.

     General Form:
     (set-ignore-ok flg)

where flg is either t, nil, or :warn.

One might find this event useful when one is generating function
definitions by an automated procedure, when that procedure does not
take care to make sure that all formals are actually used in the
definitions that it generates.

Note:  Defun will continue to report irrelevant formals even if
:set-ignore-ok has been set to t, unless you also use
set-irrelevant-formals-ok to instruct it otherwise.

SET-INHIBIT-OUTPUT-LST    control output

     Examples:
     (set-inhibit-output-lst '(warning))
     (set-inhibit-output-lst '(proof-tree prove proof-checker))
     (set-inhibit-output-lst *valid-output-names*) ; inhibit all prover output
     :set-inhibit-output-lst (proof-tree prove)

     General Form:
     (set-inhibit-output-lst lst)

where lst is a form (which may mention state) that evaluates to a list
of names, each of which is the name of one of the following "kinds" of
output produced by ACL2.

       error          error messages
       warning        warnings other than those related to soundness
       warning!       warnings (of all degrees of importance)
       observation    observations
       prove          commentary produced by the theorem prover
       proof-checker  commentary produced by the proof-checker
       event          non-proof commentary produced by events such as defun
                      and encapsulate
       expansion      commentary produced by make-event expansion
       summary        the summary at the successful conclusion of an event
       proof-tree     proof-tree output

It is possible to inhibit each kind of output by putting the
corresponding name into lst.  For example, if 'warning is included in
(the value of) lst, then no warnings are printed except those related
to soundness, e.g., the inclusion of an uncertified book.  Note that
proof-tree output is affected by set-inhibit-output-lst; see
PROOF-TREE.

See WITH-OUTPUT for a variant of this utility that can be used
in books.  Also see SET-INHIBIT-WARNINGS for how to inhibit
individual warning types and see SET-INHIBITED-SUMMARY-TYPES
for how to inhibit individual parts of the summary.

Printing of events on behalf of certify-book and encapsulate is
inhibited when both 'event and 'prove belong to lst.  Otherwise,
printing of events is controlled by the ld special ld-pre-eval-print.

_Note for advanced users._  By including warning! in lst, you are
automatically including warning as well: all warnings will be inhibited.
This is not the case if you modify value of state global variable
'inhibit-output-lst directly (with assign or f-put-global); then, if
you include warning! but not warning, then warnings not related to
soundness will still be printed (which is probably not what was
intended).

SET-INHIBIT-WARNINGS    control warnings

     Examples:
     (set-inhibit-warnings "theory" "use")

Note: This is an event!  It does not print the usual event summary but
nevertheless changes the ACL2 logical world and is so recorded.
Moreover, its effect is to set the acl2-defaults-table, and hence its
effect is local to the book or encapsulate form containing it; see
ACL2-DEFAULTS-TABLE.

     General Form:
     (set-inhibit-warnings string1 string2 ...)

where each string is considered without regard to case.  This macro is
equivalent to (table acl2-defaults-table :inhibit-warnings lst), where
lst is the list of strings supplied.  This macro is an event (see
TABLE), but no output results from a set-inhibit-warnings event.

The effect of this event is to suppress any warning whose label is a
member of this list (where again, case is ignored).  For example, the
warning

       ACL2 Warning [Use] in ( THM ...):  It is unusual to :USE ....

will not be printed if "use" (or "USE", etc.) is a member of the given
list of strings.

Of course, if warnings are inhibited overall -- see
SET-INHIBIT-OUTPUT-LST -- then the value of :inhibit-warnings is
entirely irrelevant.

SET-INHIBITED-SUMMARY-TYPES    control which parts of the summary are printed

     Example:
     (set-inhibited-summary-types '(rules time))

Note: This is not an event.  Rather, it changes the state, in analogy to
set-inhibit-output-lst.

     General Form:
     (set-inhibited-summary-types form)

where form evaluates to a true-list of symbols, each of which is among
the values of the constant *summary-types*, i.e.: header, form, rules,
hint-events warnings, time, steps, and value.  Each specified type
inhibits printing of the corresponding portion of the summaries printed
at the conclusions of events, where header refers to an initial newline
followed by the line containing just the word Summary.

Note the distinction between rules and hint-events.  Rules provides a
record of automatic rule usage by the prover, while hint-events shows
the names of events given to :USE or :BY hints, as well as
clause-processor functions given to :CLAUSE-PROCESSOR hints that have
an effect on the proof.

Also see SET-INHIBIT-OUTPUT-LST.  Note that
set-inhibited-summary-types has no effect when summary is one of the
types inhibited by set-inhibit-output-lst, because in that case none of
the summary will be printed.

To control summary types for a single event, see WITH-OUTPUT.

SET-INVISIBLE-FNS-TABLE    set the invisible functions table

     Examples:
     (set-invisible-fns-table ((binary-+ unary--)
                               (binary-* unary-/)
                               (unary-- unary--)
                               (unary-/ unary-/)))
     (set-invisible-fns-table t) ; restore original invisible-fns-table

Among other things, the setting above has the effect of making unary-
"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.  The form
(invisible-fns-table (w state)) returns the current value of the
invisible functions table.

Also see ADD-INVISIBLE-FNS and see REMOVE-INVISIBLE-FNS
for events that add to and remove from the invisible functions table.

     General Form:
     (set-invisible-fns-table alist)

where alist is either t or a true list of pairs, each element of which
is of the form (fn ufn1 ... ufnk), where fn is a function symbol and
each ufni is a unary function symbol.  When alist is t, the initial
value of this table is used in its place.  Modulo the replacement of
alist by the default setting when alist is t, this macro is equivalent
to

     (table invisible-fns-table nil 'alist :clear)

which is also an event (see TABLE).

Note that set-invisible-fns-table does not evaluate its argument.
However, you can call table directly for that purpose.  For example,

     (set-invisible-fns-table ((binary-+ unary--)
                               (binary-* unary-/)
                               (unary-- unary--)
                               (unary-/ unary-/)))

ie equivalent to the following; see TABLE.

     (table invisible-fns-table nil
            (quote ((binary-+ unary--)
                    (binary-* unary-/)
                    (unary-- unary--)
                    (unary-/ unary-/)))
            :clear)

See INVISIBLE-FNS-TABLE for a description of the invisible
functions table.

SET-IRRELEVANT-FORMALS-OK    allow irrelevant formals in definitions

     Examples:
     (set-irrelevant-formals-ok t)
     (set-irrelevant-formals-ok nil)
     (set-irrelevant-formals-ok :warn)

The first example above allows irrelevant formals in definitions; see
IRRELEVANT-FORMALS.  The second example disallows irrelevant
formals; this is the default.  The third example allows irrelevant
formals, but prints an appropriate warning.

Note: This is an event!  It does not print the usual event summary but
nevertheless changes the ACL2 logical world and is so recorded.
Moreover, its effect is to set the acl2-defaults-table, and hence its
effect is local to the book or encapsulate form containing it; see
ACL2-DEFAULTS-TABLE.

     General Form:
     (set-irrelevant-formals-ok flg)

where flg is either t, nil, or :warn.

SET-LD-KEYWORD-ALIASES    See LD-KEYWORD-ALIASES.

SET-LD-REDEFINITION-ACTION    See LD-REDEFINITION-ACTION.

SET-LD-SKIP-PROOFS    See SET-LD-SKIP-PROOFSP.

SET-LD-SKIP-PROOFSP    See LD-SKIP-PROOFSP.

SET-LET*-ABSTRACTION    See SET-LET*-ABSTRACTIONP.

SET-LET*-ABSTRACTIONP    to shorten many prettyprinted clauses

Note: This is an event!  It does not print the usual event summary but
nevertheless changes the ACL2 logical world and is so recorded.
Moreover, its effect is to set the acl2-defaults-table, and hence its
effect is local to the book or encapsulate form containing it; see
ACL2-DEFAULTS-TABLE.

When this flag is set to t, subterms that occur more than once in a
clause are abstracted away with let*, generally shortening the
displayed size of the clauses.  This flag only affects how clauses are
printed.  It does not change what terms the theorem prover manipulates.

     :set-let*-abstractionp t ;;; or, (set-let*-abstractionp t)

will cause the prettyprinter to do "let* abstraction" on clauses before
they are printed.  The algorithm finds the maximal multiply-occuring
subterm and extracts it, binding it to some new variable and replacing
its occurrences by that variable.  This produces a let* form.  This
process is iterated until no subterm occurs more than once.  This
process generally takes a little time, but less time than to print
large clauses.  The process can greatly reduce the amount of text
produced by the prover.

THIS ONLY AFFECTS HOW THE CLAUSES ARE PRINTED!  The unabstracted
clauses are manipulated by the theorem prover.

     :set-let*-abstractionp nil

restores normal clause printing.

The mode is stored in the defaults table, See
ACL2-DEFAULTS-TABLE.  Thus, the mode may be set locally in books.

SET-MATCH-FREE-DEFAULT    provide default for :match-free in future rules

     General Forms:
     (set-match-free-default :once)
     (set-match-free-default :all)
     (set-match-free-default nil)

Note: This utility does not apply to type-prescription rules; for a
related topic pertinent to such rules, see
FREE-VARIABLES-TYPE-PRESCRIPTION.

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 that hypothesis, as a basis for
relieving subsequent hypotheses.  This directing of :all or :once is
generally provided by specifying either :match-free :once or
:match-free :all in the :rule-classes of the rule.  If neither of these
is specified, then the most recent set-match-free-default is used by
ACL2 to fill in this missing :match-free field.  See
RULE-CLASSES.  Except: If the last set-match-free-default specifies
nil, then ACL2 reverts to the behavior it had at start-up, as described
in Remarks (2) and (3) below.

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.

(1) The use of set-match-free-default has no effect on existing rules.
In order to change the behavior of existing rules with respect to
free-variable matching, see ADD-MATCH-FREE-OVERRIDE.

(2) If you submit a rewrite, linear, or forward-chaining rule with a
free variable in a hypothesis, and no default setting was previously
specified with set-match-free-default or the default setting is nil,
and the rule is not within a book being processed with include-book,
certify-book, or rebuild, then a warning or error is caused.  In order
to make this an error instead of a warning, see
SET-MATCH-FREE-ERROR.

(3) If you submit a rewrite, linear, or forward-chaining rule with a
free variable in a hypothesis, and no default setting has been
previously specified with set-match-free-default or the default setting
is nil, and no error is caused (see (2) above), then the default :all
is used.

SET-MATCH-FREE-ERROR    control error vs. warning when :match-free is missing

     Legal Forms:
     (set-match-free-error nil)
     :set-match-free-error nil
     (set-match-free-error t)
     :set-match-free-error t

As described elsewhere (see FREE-VARIABLES), when a rewrite,
linear, or forward-chaining rule has free variables in its hypotheses,
the user can specify whether to try all bindings (":all") or just the
first (":once") when relieving its hypotheses, as a basis for relieving
subsequent hypotheses.  This direction of :all or :once is generally
provided by specifying either :match-free :once or :match-free :all in
the :rule-classes of the rule.

But suppose that neither of these is specified for such a rule.  (Note:
set-match-free-error is not relevant for type-prescription rules.)
Also suppose that set-match-free-default has not specified a default of
:once or :all (see SET-MATCH-FREE-DEFAULT).  In this case a
warning will occur except when in the context of include-book.  If you
prefer to see an error in such cases, except in the context of
certify-book, execute (set-match-free-error t).  If there is no error,
then a default of :all is used.

Note: This is NOT an event!  Instead, set-match-free-error sets the
state global 'match-free-error (see STATE and see
ASSIGN).  Thus, this form cannot be put into a book.  If you are
tempted to put it into a book, consider the fact that it really isn't
needed there, since the absence of :match-free does not cause an error
in the context of certify-book or include-book.  If you still feel the
need for such a form, consider using set-match-free-default to provide
a default, at least within the scope of the current book (if any); see
SET-MATCH-FREE-DEFAULT.

SET-MEASURE-FUNCTION    set the default measure function symbol

     Examples:
     (set-measure-function nqthm::count)

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

     General Form:
     (set-measure-function name)

where name is a function symbol of one argument.  This macro is
equivalent to (table acl2-defaults-table :measure-function 'name), and
hence is local to any books and encapsulate events in which it occurs;
see ACL2-DEFAULTS-TABLE.  Although this is thus an event (see
TABLE), nevertheless no output results from a
set-measure-function event.

This event sets the default measure function to name.  Subsequently, if
a recursively defined function is submitted to defun with no explicitly
given :measure argument, defun "guesses" the measure (name var), where
name is the then current default measure function and var is the first
formal found to be tested along every branch and changed in every
recursive call.

Note that if (table acl2-defaults-table :measure-function 'name) has its
default value of nil, then the default measure function is acl2-count.

SET-NON-LINEAR    See SET-NON-LINEARP.

SET-NON-LINEARP    to turn on or off non-linear arithmetic reasoning

     Examples:
     (set-non-linearp t)
     (set-non-linearp nil)

See NON-LINEAR-ARITHMETIC.   This event is equivalent to (table
acl2-defaults-table :non-linearp <t-or-nil>), and hence is local to any
books and encapsulate events in which it occurs; see
ACL2-DEFAULTS-TABLE.

The initial value is nil.

SET-NU-REWRITER-MODE    to turn on and off the nu-rewriter

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 event sets a flag that controls whether the ACL2 rewriter uses the
special-purpose nth/update-nth rewriter (nu-rewriter).  The flag may
have one of three values: nil, t, or :literals.

     :set-nu-rewriter-mode nil        ; do not use nu-rewriter
     :set-nu-rewriter-mode t          ; use nu-rewriter in rewriting
     :set-nu-rewriter-mode :literals  ; use nu-rewriter in rewriting after
                                      ;  a pre-pass through every literal
     (set-nu-rewriter-mode :literals) ; same as above

The value nil prevents the use of the nu-rewriter.  The other two
values allow the use of the nu-rewriter.

When the flag is non-nil and the rewriter encounters a term that
"begins with an nth", the nu-rewriter is applied.  By "begins with an
nth" here we mean either the term is an application of nth or is an
application of some nonrecursive function or lambda expression whose
body contains an expression that begins with an nth.

Note that the use of the nu-rewriter here described above is driven by
the rewriter, i.e., the nu-rewriter is applied only to terms visited by
the rewriter in its inside-out sweep.  When the flag is set to
:literals the system makes a pre-pass through every goal clause and
applies the nu-rewriter to every subterm.  The rewriter is then used on
the output of that pre-pass.

Note: This is an event!  It does not print the usual event summary but
nevertheless changes the ACL2 logical world and is so recorded.
Moreover, its effect is to set the acl2-defaults-table, and hence its
effect is local to the book or encapsulate form containing it; see
ACL2-DEFAULTS-TABLE.

We expect to write more documentation as we gain experience with the
nu-rewriter.

SET-OVERRIDE-HINTS    set the override-hints

See OVERRIDE-HINTS for a discussion of override-hints.  Here we
describe how to set them.  Note that the effects of set-override-hints
events are local to the books or encapsulate events in which they
reside; see SET-OVERRIDE-HINTS! to avoid that restriction.  Also
see ADD-OVERRIDE-HINTS to add to the list of override-hints,
rather than setting a new list and ignoring the present list.

     General Form:
     (set-override-hints form)

where form evaluates to a list of computed hint forms.  The effect of
this event is to set the list of override-hints to the result of that
evaluation.

SET-OVERRIDE-HINTS!    set the override-hints non-locally

Set-override-hints! is the same as set-override-hints, except that the
former is not local to books or encapsulate events in which it occurs.
See SET-OVERRIDE-HINTS; also see ADD-OVERRIDE-HINTS.

SET-PARALLEL-EXECUTION    for ACL2(p): enabling parallel execution for four parallelism primitives

This documentation topic relates to the experimental extension of ACL2
supporting parallel execution and proof; see PARALLELISM.  See
PARALLEL and see PARALLELISM-TUTORIAL for an
introduction to parallel execution in ACL2.

     General Forms:
     (set-parallel-execution nil) ; default for images not built for parallelism
     (set-parallel-execution t)   ; default for images built for parallelism
     (set-parallel-execution :bogus-parallelism-ok)

Set-parallel-execution takes an argument that specifies the enabling or
disabling of parallel execution for the primitives pand, por, plet, and
pargs (but not spec-mv-let, whose parallel execution remains enabled).
However, without using top-level, calls of parallelism primitives made
explicitly in the ACL2 top-level loop, as opposed to inside function
bodies, will never cause parallel execution; see
PARALLELISM-AT-THE-TOP-LEVEL.  Parallel execution is determined by
the value of the argument to set-parallel-execution, as follows.

Value t:
All parallelism primitives used in bodies of function definitions are
given the opportunity to execute in parallel.  However, the use of
parallelism primitives directly in the ACL2 top-level loop causes an
error.

Value :bogus-parallelism-ok:
Parallel execution is enabled, as for value t.  However, the use of
parallelism primitives directly in the ACL2 top-level loop does not
cause an error, but rather, simply results in serial execution for
these primitives.

Value nil:
All parallelism primitives degrade to their serial equivalents,
including their calls made directly in the ACL2 top-level loop.  Thus,
uses of parallelism primitives do not in themselves cause errors.

SET-PRINT-CLAUSE-IDS    cause subgoal numbers to be printed when 'prove output is inhibited

     General Forms:
     (set-print-clause-ids t)
     :set-print-clause-ids t
     (set-print-clause-ids nil)
     :set-print-clause-ids nil

This command affects output from the theorem prover only when 'prove
output is inhibited (see SET-INHIBIT-OUTPUT-LST) or gag-mode is
on (but in that case the :goals setting issues this command
automatically; see SET-GAG-MODE).  Calling this macro with
value t as shown above will cause subsequent proof attempts with 'prove
output inhibited to print the subgoal number, so that you can see the
progress of the proof; value nil reverts to the default behavior, where
this is not the case.  On a related note, we point out that you can
cause output to be saved for later display; see PSO and see
PSO!.

If 'prove output is inhibited or gag-mode is on, and if you issue
(set-print-clause-ids t) (either explicitly or with (set-gag-mode
:goals)), then you can restrict when subgoal numbers are printed.  In
the following example we restrict to subgoals that are no more than
four inductions deep, no more than four casesplits deep, and no more
than four single-subgoals deep.  For additional relevant explanation,
see CLAUSE-IDENTIFIER and see DEFATTACH.

     (defun print-clause-id-okp-level-4 (cl-id)
       (declare (xargs :mode :logic :guard (clause-id-p cl-id)))
       (and (<= (length (access clause-id cl-id :pool-lst))
                4)
            (<= (length (access clause-id cl-id :case-lst))
                4)
            (<= (access clause-id cl-id :primes)
                4)))

     (defattach print-clause-id-okp print-clause-id-okp-level-4)

SET-PROVER-STEP-LIMIT    sets the step-limit used by the ACL2 prover at the top level only

This event provides a way to limit the number of so-called "prover
steps" permitted for an event.  See WITH-PROVER-STEP-LIMIT for
a way to specify the limit on prover steps for a single event, rather
than globally (and without the restriction mentioned above, pertaining
to the top level).  For a related utility based on time instead of
prover steps, see WITH-PROVER-TIME-LIMIT.  For examples of how
step limits work, see the distributed book
books/misc/misc2/step-limits.lisp.

Note: This is an event!  It does not print the usual event summary but
nevertheless changes the ACL2 logical world and is so recorded.
Moreover, its effect is to set the acl2-defaults-table, and hence its
effect is local to the book or encapsulate form containing it; see
ACL2-DEFAULTS-TABLE.

     Example Forms:
     (set-prover-step-limit *default-step-limit*) ; no limit on prover steps
     (set-prover-step-limit nil)   ; abbreviation for the form just above
     (set-prover-step-limit 10000) ; allow at most 10,000 prover steps per event

     General Form:
     (set-prover-step-limit expr)

where expr evaluates either to nil or else to a natural number not
exceeding the value of *default-step-limit*.  If that value is nil or
the value of *default-step-limit*, then no default limit is placed on
the number of prover "steps" (see below) during processing of an event.
Otherwise, that value is the maximum number of prover steps permitted
before an error occurs.

This event specifies the limit on the number of "steps" counted by the
ACL2 prover during processing of an event.  Currently, a step is
counted for each call of the system functions rewrite and
expand-abbreviations.  However, the steps counted may change in future
releases of ACL2, so users would probably be well served by avoiding
the assumption that only the above two calls are counted as prover
steps.

Depending on the computer you are using, you may have only (very
roughly) a half-hour of time before the number of prover steps exceeds
the maximum step-limit, which is one less than the value of
*default-step-limit*.  Note however the exception stated above: if the
"limit" is nil or is the value of *default-step-limit*, then no limit
is imposed.

The limit is relevant for every event, to calls of thm and
certify-book, and more generally, to any form that creates a "summary
context" to print the usual event summary.  The limit is also put in
force when entering the proof-checker.  Below, at the end of this
documentation topic, we explain in detail when a call of
set-prover-step-limit is in force: in brief, it applies to all forms
that are either at the top level or are inside the same summary
contexts.

Note that the limit applies to each event, not just "atomic" events.
Consider the following example.

     (set-prover-step-limit 500)

     (encapsulate
       ()
       (defthm lemma-1 ; takes 380 steps
         (equal (append (append x y) z) (append x y z))
         :rule-classes nil)
       (defthm lemma-2 ; would take 319 steps
         (equal (len (append x y)) (+ (len x) (len y)))
         :rule-classes nil))

The first defthm event, lemma-1 takes 380 steps (as of this writing),
as shown in the summary:

     Prover steps counted:  380
     LEMMA-1

The second defthm event, lemma-2, takes 319 steps (as of this writing)
when evaluated at the top level.  However, in the context above, 380
steps of the available 500 steps (from the set-prover-step-limit event
above) have already been taken under the above encapsulate event.
Thus, when the number of steps would exceed 120, the proof of lemma-2 is
aborted:

     ACL2 Error in STEP-LIMIT:  The prover step-limit, which is 120 in the
     current context, has been exceeded.  See :DOC set-prover-step-limit.

The summary for lemma-2 reflects that situation:

     Prover steps counted:  More than 120

The  summary for the encapsulate events then indicates that the
available steps for that event have also been exceeded:

     Prover steps counted:  More than 500

The discussion above applies to any event that contains other events,
hence applies similarly to progn events.

For those who use make-event, we note that prover steps in the
expansion phase similarly contribute to the total number of steps
counted.  For example, suppose that the limit is 500 prover steps as
above, and you submit (make-event EXPR), where 300 prover steps take
place during evaluation of EXPR, producing event EV.  Then evaluation
of EV will cause an error if it takes more than 200 prover steps.  This
observation actually can be used to count prover steps for sequences of
forms that are not all legal events (see EMBEDDED-EVENT-FORM),
such as calls of thm.  For example, a small built-in ACL2 test suite
that includes thm forms can be run by evaluating the form
(mini-proveall), and the steps can be counted as shown below.  (Here we
assume a fresh ACL2 session; an error would occur if first, we evaluate
the event (set-prover-step-limit 500) displayed above.)

     ACL2 !>(make-event (er-progn (mini-proveall) (value '(value-triple nil))))
     [[... output omitted here ...]]
     Summary
     Form:  ( MAKE-EVENT (ER-PROGN ...))
     Rules: NIL
     Warnings:  Double-rewrite, Equiv, Subsume and Non-rec
     Time:  0.38 seconds (prove: 0.04, print: 0.29, other: 0.05)
     Prover steps counted:  41090
      NIL
     ACL2 !>

Technical Remark.  For a call of mfc-rw or any mfc- function (see
EXTENDED-METAFUNCTIONS), the steps taken during that call are
forgotten when returning from that call.

Finally, we discuss in some detail with a set-prover-step-limit event is
in force: it applies to a subsequent form that is either at the top
level or at the same level as the set-prover-step-limit form, in the
following sense.  Let us say that a "summary context" is any context
for which the usual ACL2 summary will ultimately be printed (if summary
printing is not inhibited).  Every event -- a call of defun or defthm,
or more generally, every embedded event form (see
EMBEDDED-EVENT-FORM) -- establishes a summary context, as do certain
other top-level forms such as calls of thm and certify-book.  (But a
call of ld does not establish a summary context.)  Here, we consider
two forms to be at the same level if they are in the same summary
contexts.  Thus, if set-prover-step-limit is called at the top level,
then this call is not in force for events under a call of certify-book,
encapsulate, progn, make-event, or (more generally) under any form that
establishes a summary context.  Also, if set-prover-step-limit is
called inside a summary context, then it does not apply above that
summary context except, if it is not local to some event, at the very
top level.

SET-RAW-MODE    enter or exit "raw mode," a raw Lisp environment

Below we discuss raw-mode.  In brief: The simplest way to turn raw-mode
on is :SET-RAW-MODE-ON!, and to turn it off, :SET-RAW-MODE NIL.  Also
see SET-RAW-MODE-ON!.

ACL2 users often find its careful syntax checking to be helpful during
code development.  Sometimes it is even useful to do code development in
:logic mode, where ACL2 can be used to check termination of (mutually)
recursive functions, verify guards, or even prove properties of the
functions.

However, loading code using include-book is much slower than using
Common Lisp load in raw Lisp, and in this sense ACL2 can get in the way
of efficient execution.  Unfortunately, it is error-prone to use ACL2
sources (or their compilations) in raw Lisp, primarily because a number
of ACL2 primitives will not let you do so.  Perhaps you have seen this
error message when trying to do so:

     HARD ACL2 ERROR in ACL2-UNWIND-PROTECT:  Apparently you have tried
     to execute a form in raw Lisp that is only intended to be executed
     inside the ACL2 loop.

Even without this problem it is important to enter the ACL2 loop (see
LP), for example in order to set the cbd and (to get more
technical) the readtable.

ACL2 provides a "raw mode" for execution of raw Lisp forms.  In this
mode, include-book reduces essentially to a Common Lisp load.  More
generally, the ACL2 logical world is not routinely extended in raw mode
(some sneaky tricks are probably required to make that happen).  To
turn raw mode off or on:

     :set-raw-mode t   ; turn raw mode on
     :set-raw-mode nil ; turn raw mode off

The way you can tell that you are in raw mode is by looking at the
prompt (see DEFAULT-PRINT-PROMPT), which uses a capital "P"
(suggesting something like program mode, but more so).

     ACL2 P>

Typical benefits of raw mode are fast loading of source and compiled
files and the capability to hack arbitrary Common Lisp code in an
environment with the ACL2 sources loaded (and hence with ACL2
primitives available).  In addition, ACL2 hard errors will put you into
the Lisp debugger, rather than returning you to the ACL2 loop, and this
may be helpful for debugging; see HARD-ERROR and see
ILLEGAL, but also see BREAK-ON-ERROR.  However, it probably
is generally best to avoid raw mode unless these advantages seem
important.  We expect the main benefit of raw mode to be in deployment
of applications, where load time is much faster than the time required
for a full-blown include-book, although in certain cases the fast
loading of books and treatment of hard errors discussed above may be
useful during development.

Raw mode is also useful for those who want to build extensions of ACL2.
For example, the following form can be put into a certifiable book to
load an arbitrary Common Lisp source or compiled file.

     (progn (defttag my-application)
            (progn! (set-raw-mode t)
                    (load "some-file")))

Also see with-raw-mode defined in books/hacking/hacker.lisp, see
DEFTTAG, and see PROGN!.

Below are several disadvantages to raw mode.  These should discourage
users from using it for general code development, as :program mode is
generally preferable.

     -- Forms are in essence executed in raw Lisp.  Hence:
        -- Syntax checking is turned off; and
        -- Guard checking is completely disabled.
     -- Table events, including logic, are ignored, as are many
        other events, including defthm and comp.
     -- Soundness claims are weakened for any ACL2 session in which raw
        mode was ever entered; see DEFTTAG.
     -- The normal undoing mechanism (see UBT) is not supported.
     -- Unexpected behavior may occur when you return from raw-mode.
        For example, if you redefine a :logic mode function whose guards
        have not been verified, you will not see the change inside the
        ACL2 loop because there, the raw Common Lisp definition is only
        executed after guards have been verified; see GUARDS-AND-EVALUATION
        and see GUARD-EVALUATION-TABLE.

We conclude with some details.

_Printing results_.  The rules for printing results are unchanged for
raw mode, with one exception.  If the value to be printed would contain
any Lisp object that is not a legal ACL2 object, then the print routine
is used from the host Lisp, rather than the usual ACL2 printing
routine.  The following example illustrates the printing used when an
illegal ACL2 object needs to be printed.  Notice how that "command
conventions" are observed (see LD-POST-EVAL-PRINT); the "[Note"
occurs one space over in the second example, and no result is printed
in the third example.

     ACL2 P>(find-package "ACL2")
     [Note:  Printing non-ACL2 result.]
     #<The ACL2 package>
     ACL2 P>(mv nil (find-package "ACL2") state)
      [Note:  Printing non-ACL2 result.]
     #<The ACL2 package>
     ACL2 P>(mv t (find-package "ACL2") state)
     ACL2 P>(mv 3 (find-package "ACL2"))
     [Note:  Printing non-ACL2 result.]
     (3 #<The ACL2 package>)
     ACL2 P>

If you have trouble with large structures being printed out, you might
want to execute appropriate Common Lisp forms in raw mode, for example,
(setq *print-length* 5) and (setq *print-level* 5).

_Include-book_.  The events add-include-book-dir and
delete-include-book-dir have been designed to work with raw mode.
However, if you enter raw mode and then evaluate such forms, then the
effects of these forms will disappear when you exit raw mode, in which
case you can expect to see a suitable warning.  Regarding
_include-book_ itself: it should work in raw mode as you might expect,
at least if a compiled file or expansion file was created when the book
was certified; see CERTIFY-BOOK.

_Packages_.  Raw mode disallows the use of defpkg.  If you want to
create a new package, first exit raw mode with :set-raw-mode nil; you
can subsequently re-enter raw mode with :set-raw-mode t if you wish.

ADD-RAW-ARITY    add arity information for raw mode

Technical note: This macro is a no-op, and is not necessary, when ACL2
is built with #-acl2-mv-as-values.

Users of raw mode (see SET-RAW-MODE) can use arbitrary raw Lisp
functions that are not known inside the usual ACL2 loop.  In such
cases, ACL2 may not know how to display a multiple value returned by
ACL2's mv macro.  The following example should make this clear.

     ACL2 P>(defun foo (x y) (mv y x))
     FOO
     ACL2 P>(foo 3 4)

     Note: Unable to compute number of values returned by this evaluation
     because function FOO is not known in the ACL2 logical world.  Presumably
     it was defined in raw Lisp or in raw mode.  Returning the first (perhaps
     only) value for calls of FOO.
     4
     ACL2 P>(add-raw-arity foo 2)
      RAW-ARITY-ALIST
     ACL2 P>(foo 3 4)
     (4 3)
     ACL2 P>

The first argument of add-raw-arity should be a symbol, representing the
name of a function, macro, or special form, and the second argument
should either be a non-negative integer (denoting the number of values
returned by ACL2) or else the symbol :LAST, meaning that the number of
values returned by the call is the number of values returned by the last
argument.

The current arity assignments can be seen by evaluating (@
raw-arity-alist).  See REMOVE-RAW-ARITY for how to undo a call
of add-raw-arity.

REMOVE-RAW-ARITY    remove arity information for raw mode

Technical note: This macro is a no-op, and is not necessary, when ACL2
is built with #-acl2-mv-as-values.

The form (remove-raw-arity fn) undoes the effect of an earlier
(remove-raw-arity fn val).  See ADD-RAW-ARITY.

SET-RAW-MODE-ON!    enter "raw mode," a raw Lisp environment

This is the same as (set-raw-mode t) except that it first introduces a
so-called "trust tag" ("ttag") so that set-raw-mode will be legal.  See
DEFTTAG for a discussion of ttags and how they affect
certify-book and include-book.

See SET-RAW-MODE for a discussion of raw-mode.

SET-RAW-PROOF-FORMAT    print runes as lists in proof output from simplification

     General Forms:
     (set-raw-proof-format t)
     :set-raw-proof-format t
     (set-raw-proof-format nil)
     :set-raw-proof-format nil

This command affects output from the theorem prover only when 'prove
output is not inhibited (see SET-INHIBIT-OUTPUT-LST) and
gag-mode is off (see SET-GAG-MODE).  Calling this macro with
value t as shown above will cause simplification steps from proof
output, including steps from preprocess (see SIMPLE), to print
the list of runes used in a list format, rather than in the English
proof commentary.  This "raw" format can be handy when you want to use
that list as a basis for hints that you construct for a subsequent
proof attempt.

SET-REWRITE-STACK-LIMIT    Sets the rewrite stack depth used by the rewriter

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

     Example Forms:
     (set-rewrite-stack-limit 30)                            ; set to small limit
     :set-rewrite-stack-limit 30                             ; same as above
     (set-rewrite-stack-limit *default-rewrite-stack-limit*) ; the default
     :set-rewrite-stack-limit (1- (expt 2 28))               ; maximum legal limit
     :set-rewrite-stack-limit nil         ; same as above -- essentially, no limit

This event sets the maximum stack depth for calls of certain functions
that implement the ACL2 rewriter; see REWRITE-STACK-LIMIT.  It
must be a non-negative integer less than 2^28.  A call
(set-rewrite-stack-limit limit) is equivalent to:

     (table acl2-defaults-table :rewrite-stack-limit limit).

The use of acl2-defaults-table ensures that this event's effect is
implicitly local to the book or encapsulate form in which it occurs.

For a different but somewhat related concept, see
BACKCHAIN-LIMIT.

SET-RULER-EXTENDERS    See RULER-EXTENDERS.

SET-RW-CACHE-STATE    set the default rw-cache-state

The ACL2 rewriter uses a data structure, called the rw-cache (rewriter
cache), to save failed attempts to apply conditional rewrite rules.  The
regression suite has taken approximately 11% less time with this
mechanism.  The rw-cache is active by default but this event allows it
to be turned off or modified.  Note that this event is local to its
context (from encapsulate or include-book).  For a non-local version,
use set-rw-cache-state!.

     Example forms:
     (set-rw-cache-state :atom)     ; default: rw-cache cleared for each literal
                                    ;   (i.e., hypothesis or conclusion of a goal)
     (set-rw-cache-state nil)       ; rw-cache is inactive
     (set-rw-cache-state t)         ; rw-cache persists beyond each literal
     (set-rw-cache-state :disabled) ; rw-cache is inactive, but the rw-cache-state
                                    ;   transitions to state t after
                                    ;   simplification takes place

     General Form:
     (set-rw-cache-state val)

where val evaluates to one of the four values shown in "Example forms"
above.  The default is :atom, which enables the rw-cache but clears it
before rewriting a hypothesis or conclusion of any goal.  The value t is
provides more aggresive use of the rw-cache, basically preserving the
rw-cache when there is a single subgoal.  The value :disabled is the
same as t, except that the rw-cache is initially inactive and only
becomes active when some simplification has taken place.  We have seen
a few cases where value t will make a proof fail but :disabled does not.

The following example illustrates the rw-cache in action.  You will see
a break during evaluation of the thm form.  Type :eval and you will see
a failed rewriting attempt.  Type :go to continue, and at the next
break type :eval again.  This time you will see the same failed
rewriting attempt, but this time labeled with a notation saying that
the failure was cached earlier, which indicates that this time the
rewriter did not even attempt to prove the hypothesis of the rewrite
rule f1->f2.

     (defstub f1 (x) t)
     (defstub f2 (x) t)
     (defaxiom f1->f2
              (implies (f1 x) (equal (f2 x) t)))
     :brr t
     :monitor (:rewrite f1->f2) t
     (thm (equal (car (f2 a)) (cdr (f2 a))))

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
SET-RW-CACHE-STATE! for a corresponding non-local event).

We also note that rw-cache-state changes may also be caused at the
subgoal level; see HINTS.

We welcome you to experiment with different rw-cache states.  If the
more aggressive values of t and :disabled cause proofs to fail, then you
can revert to the default of :atom or even turn off the rw-cache using
(set-rw-cache-state nil).  We don't expect users to need a deep
knowledge of the rw-cache in order to do such experiments, but readers
interested in details of the rw-cache implementation are invited to
read the "Essay on Rw-cache" in the ACL2 source code.

SET-RW-CACHE-STATE!    set the default rw-cache-state non-locally

Please see SET-RW-CACHE-STATE, which is the same as
set-rw-cache-state!  except that the latter is not local to the
encapsulate or the book in which it occurs.

SET-SAVED-OUTPUT    save proof output for later display with :pso or :pso!

     Examples:
     (set-saved-output t t)    ; save proof output for later, but inhibit it now
     (set-saved-output t :all) ; save proof output for later, but inhibit all
                               ;   output (except WARNING!, for critical warnings,
                               ;   and ERROR, unless these are already inhibited)
     :set-saved-output t :all  ; same as the line above
     (set-saved-output t nil)  ; save proof output for later, but print it now too
     (set-saved-output nil t)  ; do not save proof output, and inhibit it
     (set-saved-output nil nil); do not save proof output or inhibit output
     (set-saved-output nil :same), (set-saved-output t :same)
                               ; save proof output or not, as indicated, but do
                               ;   not change which output is inhibited
     (set-saved-output nil :normal)
                               ; the behavior when ACL2 first starts up: do not
                               ;   save output, and only inhibit proof-tree output
     (set-saved-output t '(warning observation proof-tree prove))
                               ; save proof output for later, and inhibit the
                               ;   indicated kinds of output

     General Form:
     (set-saved-output save-flg inhibit-flg)

Parameter save-flg is t to cause output to be saved for later display
using pso or pso!; see PSO and see PSO!, and see the
documentation for proof-checker commands of the same names.  Set
save-flg to nil to turn off this feature; except, it always stays on in
proof-checker sessions entered with verify.  The other argument,
inhibit-flg, controls whether output should be inhibited when it is
created (normally, during a proof attempt).  So a common combination is
to set both arguments to t, to indicate that output should be
suppressed for now but saved for printing with pso or pso!.  The
examples above give a good summary of the functionality for the second
argument.

Saved output is cleared at the start of every event, and also at the
start of every proof-checker commands that invoke the prover.  Note that
interactive proof-checker commands, that is, from a proof-checker
session entered with verify, are always run with output saved.

Also see SET-GAG-MODE; and see SET-PRINT-CLAUSE-IDS,
which causes subgoal numbers to be printed during proof attempts when
output is inhibited.

See SET-INHIBIT-OUTPUT-LST if you want to inhibit certain
output from the prover but not other output (e.g., not the summary),
and you don't want to save any output.

SET-STATE-OK    allow the use of STATE as a formal parameter

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

In brief:  The variable symbol STATE has an unusual status in ACL2.  In
order to use it, you either need to issue :set-state-ok t, as we
explain below, or you need to declare it to be a stobj, as explained
elsewhere (see DECLARE-STOBJS).  Now we explain in more detail.

Because the variable symbol STATE denotes the "current ACL2 state,"
ACL2 treats the symbol very restrictively when it occurs as a formal
parameter of a defined function.  The novice user, who is unlikely to
be aware of the special status of that symbol, is likely to be confused
when error messages about STATE are printed in response to the innocent
choice of that symbol as a formal variable.  Therefore the top-level
ACL2 loop can operate in a mode in which STATE is simply disallowed as
a formal parameter.

For a discussion of STATE, See STATE and see STOBJ.
Roughly speaking, at the top-level, the "current ACL2 state" is denoted
by the variable symbol STATE.  Only the current state may be passed
into a function expecting a state as an argument.  Furthermore, the
name of the formal parameter into which the current state is passed
must be STATE and nothing but the current state may be passed into a
formal of that name.  Therefore, only certain access and change
functions can use that formal -- namely those with a STATE formal --
and if any such function produces a new state it becomes the "current
state" and must be passed along in the STATE position thereafter.
Thus, ACL2 requires that the state be single-threaded.  This, in turn,
allows us to represent only one state at a time and to produce new
states from it destructively in a von Neumaneque fashion.  The
syntactic restrictions on the variable STATE are enforced by the
translate mechanism (see TRANS and see TERM) when terms
are read.

To prevent the novice user from seeing messages prohibiting certain
uses of the variable symbol STATE ACL2 has a mode in which it simply
disallows the use of that symbol as a formal parameter.  Use of the
symbol causes a simple error message.  The system is initially in that
mode.

To get out of that mode, execute:

     :set-state-ok t ;;; or, (set-state-ok t)

It is not recommended that you do this until you have read the
documentation of STATE.

To enter the mode in which use of state is prohibited as a formal
parameter, do:

     :set-state-ok nil

The mode is stored in the defaults table, See
ACL2-DEFAULTS-TABLE.  Thus, the mode may be set locally in books.

SET-TAU-AUTO-MODE    to turn on or off automatic generation of :tau-system rules

     Examples:
     (set-tau-auto-mode t)
     (set-tau-auto-mode nil)

This event is equivalent to (table acl2-defaults-table :tau-auto-modep
<t-or-nil>), and hence is local to any books and encapsulate events in
which it occurs; see ACL2-DEFAULTS-TABLE.

The initial value is nil and we say that the tau-system is in manual
mode.  In manual mode, the only events that may create :tau-system
rules are defthm events explicitly specifying the :tau-system rule
class in the :rule-classes argument.  Of course, for a :tau-system rule
to be created from a proved formula (or its specified :corollary), the
formula must be of the appropriate shape (syntactic form). See
TAU-SYSTEM.  If the :tau-system rule class is specified but the
formula is not of an appropriate shape, an error is signalled.

The tau system is initially in manual mode.

When the value of :tau-auto-modep is t we say the tau system is in
automatic mode.  In automatic mode, a :tau-system rule may be created
even by events not explicitly specifying the :tau-system rule class.

In particular, in automatic mode, a :tau-system rule may be created by
any of the events below, provided the definition or formula proved is
of an appropriate shape:

* defun events introducing "big switch" or "mv-nth synonyms,"

* defun events creating type-prescription rules that may be also
represented as "signature rules" of form 1, and

* any defthm event with a non-nil :rule-classes argument if no
:tau-system rule is among the rule classes and the formula proved is in
 the shape of any tau-system rule.

See TAU-SYSTEM for a description of the various shapes named
above.

Note that any rule (of any rule class) created when the tau system is in
manual mode is also created in automatic mode.  For example, if an event
would create a :DEFINITION, :TYPE-PRESCRIPTION, FORWARD-CHAINING, or
:REWRITE rule when the tau system is in manual mode, then the event
will create that same rule when the tau system is in automatic mode.
Automatic mode just means that some :tau-system rules may be created
also.

Of course, if a defthm event explicitly specifies a :tau-system rule
class, then even if the tau system is in automatic mode, that tau rule
is created from the proved formula (or the specified :corollary) or
else an error is caused.  But if the tau system is in automatic mode
and a defthm event doesn't explicitly specify a :tau-system rule class,
then the system quietly checks each specified :corollary -- or, in the
absence of any :corollary, it checks the proved formula -- for whether
it can be stored as a tau rule.  If so, then the system stores a tau
rule, in addition to storing the specified rule.  Of course, no error
is signalled if a proved formula of some non-:tau-system rule class
fails to be of an appropriate shape for the tau system.

Recall that the use of tau rules is controlled by the rune
(:EXECUTABLE-COUNTERPART TAU-SYSTEM).  When that rune is disabled, no
tau rules are used in proofs.  However, the tau system continues to
collect tau rules if the system is in automatic mode.  Thus, if and
when the tau system is re-enabled, rules automatically generated while
the tau system was disabled will be used as usual by the tau system.

Finally, note that defthm events with :rule-classes nil do not create
:tau-system rules even if the formula proved is of an appropriate
shape, regardless of whether the tau system is in automatic or manual
mode.

The macro tau-status provides a convenient way to enable/disable the
executable counterpart of tau-system and/or to switch between manual and
automatic modes.  It may also be used to determine the current settings
of those two flags.

SET-TOTAL-PARALLELISM-WORK-LIMIT    for ACL2(p): set thread limit for parallelism primitives

This documentation topic relates to the experimental extension of ACL2
supporting parallel execution and proof; see PARALLELISM.
While the most common use of the limit described below is in parallel
proof (see PARALLEL-PROOF), it also applies to all parallelism
primitives (see PARALLEL-PROGRAMMING) except spec-mv-let --
though we expect that rather few programming applications will encouter
this limit.

     General Forms:
     (set-total-parallelism-work-limit :none)     ; disable the limit
     (set-total-parallelism-work-limit <integer>) ; set limit to <integer>

See PARALLELISM-TUTORIAL, Section "Another Granularity Issue
Related to Thread Limitations", for an explanation of how the host Lisp
can run out of threads.  Also see
SET-TOTAL-PARALLELISM-WORK-LIMIT-ERROR.

If the underlying runtime system (the Operating System, the host Lisp,
etc.)  is unable to provide enough threads to finish executing the
parallelism work given to it, the runtime system can crash in a very
unpleasant manner (ranging from a Lisp error to completely freezing the
machine).  To avoid this unpleasantness, ACL2(p) will attempt to avoid
creating so much parallelism that the runtime system crashes.

ACL2 initially uses a conservative estimate to limit the number of
threads.  To tell ACL2(p) to use a different limit, call
set-total-parallelism-work-limit with the new limit.  For example, if
the current default limit is 10,000, then to allow 13,000 threads to
exist, issue the following form at the top level.

     (set-total-parallelism-work-limit 13000)

To disable this limit altogether, evaluate the following form:

     (set-total-parallelism-work-limit :none)

The default value of total-parallelism-work-limit can be found by
calling function default-total-parallelism-work-limit.  If the default
value is too high for your system please notify the ACL2 maintainers
with a limit that does work for your system, as they might then lower
the default limit.

SET-TOTAL-PARALLELISM-WORK-LIMIT-ERROR    for ACL2(p): control the action taken when the thread limit is exceeded

This documentation topic relates to the experimental extension of ACL2
supporting parallel execution and proof; see PARALLELISM.

     General Forms:
     (set-total-parallelism-work-limit-error t)   ; cause error (default)
     (set-total-parallelism-work-limit-error nil) ; disable error and
                                                  ; continue serially

See PARALLELISM-TUTORIAL, Section "Another Granularity Issue
Related to Thread Limitations", for an explanation of how the host Lisp
can run out of threads.  See SET-TOTAL-PARALLELISM-WORK-LIMIT
for further details, including an explanation of how to manage the
limit that triggers this error.

The value of state global total-parallelism-work-limit-error dictates
what occurs when the underlying runtime system runs reaches a limit on
the number of threads for parallel computation.  By default, when this
limit is reached, the ACL2(p) user will receive an error and
computation will halt.  At this point, the ACL2(p) user has the
following options.

(1) Remove the limit by evaluating the following form.

     (set-total-parallelism-work-limit :none)

(2) Disable the error so that execution continues serially once the
available thread resources have been exhausted.

     (set-total-parallelism-work-limit-error nil)

(3) Increase the limit on number of threads that ACL2(p) is willing to
create, in spite of potential risk (see
SET-TOTAL-PARALLELISM-WORK-LIMIT).  In this case, the following query
returns the current limit.

     (f-get-global 'total-parallelism-work-limit)

Then to increase that limit, evaluate the following form:

     (set-total-parallelism-work-limit <new-integer-value>)

For example, suppose that the value of total-parallelism-work-limit was
originally 10,000.  Then evaluation of the following form increases that
limit to 13,000.

     (set-total-parallelism-work-limit 13000)

SET-VERIFY-GUARDS-EAGERNESS    the eagerness with which guard verification is tried.

     Example Forms:                        try guard verification?
     (set-verify-guards-eagerness 0) ; no, unless :verify-guards t
     (set-verify-guards-eagerness 1) ; yes if a :guard is supplied
     (set-verify-guards-eagerness 2) ; yes, unless :verify-guards nil

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

     General Form:
     (set-verify-guards-eagerness n)

where n is a variable-free term that evaluates to 0, 1, or 2.  This
macro is essentially equivalent to

     (table acl2-defaults-table :verify-guards-eagerness n)

and hence is local to any books and encapsulate events in which it
occurs; see ACL2-DEFAULTS-TABLE.  However, unlike the above
simple call of the table event function (see TABLE), no output
results from a set-verify-guards-eagerness event.

Set-verify-guards-eagerness may be thought of as an event that merely
sets a flag to 0, 1, or 2.  The flag is used by certain defun events to
determine whether guard verification is tried.  The flag is irrelevant
to those defun events in :program mode and to those defun events in
which an explicit :verify-guards setting is provided among the xargs.
In the former case, guard verification is not done because it can only
be done when logical functions are being defined.  In the latter case,
the explicit :verify-guards setting determines whether guard
verification is tried.  So consider a :logic mode defun in which no
:verify-guards setting is provided.  Is guard verification tried?  The
answer depends on the eagerness setting as follows.  If the eagerness
is 0, guard verification is not tried.  If the eagerness is 1, it is
tried iff a :guard is explicitly provided in the defun.  If the
eagerness is 2, guard verification is tried.

The default behavior of the system is as though the
:verify-guards-eagerness is 1.  The current behavior can be ascertained
by evaluating the form (default-verify-guards-eagerness (w state)).

SET-WATERFALL-PARALLELISM    for ACL2(p): configuring the parallel execution of the waterfall

This documentation topic relates to the experimental extension of ACL2
supporting parallel execution and proof; see PARALLELISM.

     General Forms:
     (set-waterfall-parallelism nil)        ; never parallelize (serial execution)
     (set-waterfall-parallelism :full)      ; always parallelize
     (set-waterfall-parallelism :top-level) ; parallelize top-level subgoals
     (set-waterfall-parallelism             ; parallelize if sufficient resources
       :resource-based)                     ;   (recommended setting)
     (set-waterfall-parallelism t)          ; alias for :resource-based
     (set-waterfall-parallelism             ; parallelize if sufficient resources
       :resource-and-timing-based           ;   and suggested by prior attempts
     (set-waterfall-parallelism             ; never parallelize but use parallel
       :pseudo-parallel)                    ;   code base (a debug mode)

Set-waterfall-parallelism evaluates its argument, which specifies the
enabling or disabling of the parallel execution of ACL2's main proof
process, the waterfall.

It also sets state global waterfall-printing to an appropriate value.
See SET-WATERFALL-PRINTING.

Note that not all ACL2 features are supported when
waterfall-parallelism is set to non-nil (see
UNSUPPORTED-WATERFALL-PARALLELISM-FEATURES).

A value of t is treated the same as a value of :resource-based and is
provided for user convenience.

:Resource-based waterfall parallelism typically achieves the best
performance in ACL2(p), while maintaining system stability, so
:resource-based (or equivalently, t) is the recommended value.

A value of nil indicates that ACL2(p) should never prove subgoals in
parallel.

A value of :full indicates that ACL2(p) should always prove independent
subgoals in parallel.

A value of :top-level indicates that ACL2(p) should prove each of the
top-level subgoals in parallel but otherwise prove subgoals in a serial
manner.  This mode is useful when the user knows that there are enough
top-level subgoals, many of which take a non-trivial amount of time to
be proved, such that proving them in parallel will result in a useful
reduction in overall proof time.

A value of :resource-based (or equivalently, t) indicates that ACL2(p)
should use its built-in heuristics to determine whether CPU core
resources are available for parallel execution.  Note that ACL2(p) does
not hook into the operating system to determine the workload on the
machine.  ACL2(p) works off the assumption that it is the only process
using significant CPU resources, and it optimizes the amount of
parallelism based on the number of CPU cores in the system.  (Note that
ACL2(p) knows how to obtain the number of CPU cores from the operating
system in CCL, but that, in SBCL and in Lispworks, a constant is used
instead).

During the first proof attempt of a given conjecture, a value of
:resource-and-timing-based results in the same behavior as with
:resource-based.  However, on subsequent proof attempts, the time it
took to prove each subgoal will be considered when deciding whether to
parallelize execution.  If a particular theorem's proof is already
achieving satisfactory speedup via :resource-based parallelism, there
is no reason to try this setting.  However, if the user wishes to
experiment, the :resource-and-timing-based setting may improve
performance.  Note that since the initial run does not have the subgoal
proof times available, this mode will never be better than the
:resource-based setting for non-interactive theorem proving.

A value of :pseudo-parallel results in using the parallel waterfall
code, but with serial execution.  This setting is useful for debugging
the code base that supports parallel execution of the waterfall.  For
example, you may wish to use this mode if you are an "ACL2 Hacker" who
would like to see comprehensible output from tracing (see
TRACE$) the @par versions of the waterfall functions.

The following remark pertains to those using the `HONS' experimental
extension of ACL2 (see HONS-AND-MEMOIZATION; in particular, see
MEMOIZE).  Since memoization is not supported when waterfall
parallelism is enabled (see
UNSUPPORTED-WATERFALL-PARALLELISM-FEATURES), then when
set-waterfall-parallelism is called with a non-nil value, all memoized
functions are unmemoized.  When set-waterfall-parallelism is again
called with a nil value, those memoization settings are restored.

Set-waterfall-parallelism is an embedded event form.  However, a call of
this macro will not affect waterfall-parallelism when including a
certified book that contains that call.  For such an effect, you may
use the following make-event form.

     (make-event (er-progn (set-waterfall-parallelism :full)
                           (value '(value-triple nil)))
                 :check-expansion t)

SET-WATERFALL-PARALLELISM-HACKS-ENABLED    for ACL2(p): enable waterfall-parallelism hacks

This documentation topic relates to the experimental extension of ACL2
supporting parallel execution and proof; see PARALLELISM.

     General Forms:
     (set-waterfall-parallelism-hacks-enabled t)
     (set-waterfall-parallelism-hacks-enabled nil)

Some features (e.g., override-hints and clause-processors) of serial
ACL2 are by default not available in ACL2(p) with waterfall parallelism
enabled, because they offer a mechanism to modify state that is
unsound.  To allow or (once again) disallow the use the these features
in ACL2(p), call set-waterfall-parallelism-hacks-enabled with argument t
or nil, respectively.

Set-waterfall-parallelism-hacks-enabled requires the use of a trust tag
(see DEFTTAG).  One can call
set-waterfall-parallelism-hacks-enabled!  instead, which will
automatically install a trust tag named :waterfall-parallelism-hacks.

See ERROR-TRIPLES-AND-PARALLELISM for further related
discussion.

SET-WATERFALL-PARALLELISM-HACKS-ENABLED!    for ACL2(p): enabling waterfall parallelism hacks

See SET-WATERFALL-PARALLELISM-HACKS-ENABLED.

SET-WATERFALL-PRINTING    for ACL2(p): configuring the printing that occurs within the parallelized waterfall

This documentation topic relates to the experimental extension of ACL2
supporting parallel execution and proof; see PARALLELISM.

     General Forms:
     (set-waterfall-printing :full)    ; print everything
     (set-waterfall-printing :limited) ; print a subset that's thought to be useful
     (set-waterfall-printing :very-limited) ; print an even smaller subset

Set-waterfall-printing evaluates its argument, which indicates how much
printing should occur when executing ACL2 with the parallelized version
of the waterfall.  It only affects the printing that occurs when
parallelism mode is enabled for the waterfall (see
SET-WATERFALL-PARALLELISM).

A value of :full is intended to print the same output as in serial mode.
This output will be interleaved unless the waterfall-parallelism mode
is one of nil or :pseudo-parallel.

A value of :limited omits most of the output that occurs in the serial
version of the waterfall.  Instead, the proof attempt prints key
checkpoints (see ACL2P-KEY-CHECKPOINTS).  The value of :limited
also prints messages that indicate which subgoal is currently being
proved, along with the wall-clock time elapsed since the theorem began
its proof; and if state global 'waterfall-printing-when-finished has a
non-nil value, then such a message will also be printed at the
completion of each subgoal.  The function print-clause-id-okp may
receive an attachment to limit such printing; see
SET-PRINT-CLAUSE-IDS.  Naturally, these subgoal numbers can appear
out of order, because the subgoals can be proved in parallel.

A value of :very-limited is treated the same as :limited, except that
instead of printing subgoal numbers, the proof attempt prints a period
(`.') each time it starts a new subgoal.

Note that this form cannot be used at the top level of a book, or of a
progn or encapsulate event.  Here is a workaround for use in such
contexts; of course, you may replace :very-limited with any other legal
argument for set-waterfall-printing.

     (make-event (er-progn (set-waterfall-printing :very-limited)
                           (value '(value-triple nil))))

(For more about event contexts and the use of make-event, see
MAKE-EVENT, in particular the section "Restriction to Event
Contexts.")

The following form has the effect described above, except that it will
affect waterfall-printing even when including a certified book that
contains it.

     (make-event (er-progn (set-waterfall-printing :very-limited)
                           (value '(value-triple nil)))
                 :check-expansion t)

Note that set-waterfall-printing is automatically called by
set-waterfall-parallelism.

To enable the printing of information when a subgoal is finished,
assign a non-nil value to global waterfall-printing-when-finished.
This can be accomplished by entering the following at the top level:

     (f-put-global 'waterfall-printing-when-finished t state)

SET-WELL-FOUNDED-RELATION    set the default well-founded relation

     Examples:
     (set-well-founded-relation lex2)

provided lex2 has been proved to be a well-founded relation (see
WELL-FOUNDED-RELATION).  Note: This is an event!  It does not print
the usual event summary but nevertheless changes the ACL2 logical world
and is so recorded.

     General Form:
     (set-well-founded-relation rel)

where rel has been proved to be a well-founded relation on objects
satisfying some predicate, mp; see WELL-FOUNDED-RELATION.  This
macro is equivalent to (table acl2-defaults-table
:well-founded-relation 'rel), and hence is local to any books and
encapsulate events in which it occurs; see ACL2-DEFAULTS-TABLE.

This event sets the default well-founded relation to be that imposed on
mp-measures by the relation rel.  Subsequently, if a recursively
defined function is submitted to defun with no explicitly given
:well-founded-relation argument, defun uses the default relation, rel,
and the associated domain predicate mp used in its well-foundedness
theorem.  That is, the termination conditions generated will require
proving that the measure used by the defun is an mp-measure and that in
every recursive call the measure of the arguments decreases according
to rel.

SET-WRITE-ACL2X    cause certify-book to write out a .acl2x file

     Example Forms:
     (set-write-acl2x nil state)
     (set-write-acl2x t state)
     (set-write-acl2x '(nil) state) ; same as just above, but allow inclusion of
                                    ; uncertified books during certify-book
     (set-write-acl2x '(t) state)
     (set-write-acl2x '(include-book-with-locals) state)

     General Form:
     (set-write-acl2x val state)

where val evaluates to t, nil, or a one-element list whose element is a
legal value for the global 'ld-skip-proofsp; see
LD-SKIP-PROOFSP.  The value returned is an error triple, which in the
non-error case is (mv nil v state), where v is the value of val and
state is the result of updating the input state by assigning state
global 'write-acl2x the value v.

The command (set-write-acl2x val state) assigns the value of val to the
state global variable 'write-acl2x, affecting whether or not
certify-book writes out a file with extension acl2x, called a ".acl2x
file" and pronounced "dot-acl2x file".  Such a file is read or written
by certify-book when it is supplied with keyword argument :acl2x t.  By
default, such a call of certify-book reads a .acl2x file; but if the
value of state global variable 'write-acl2x is not nil, then
certify-book writes a .acl2x file (in which case it is illegal to
specify a non-nil value for certify-book keyword argument :pcert).
Consider for example (certify-book "foo" 0 nil :acl2x t).  By default,
this command reads file foo.acl2x, which supplies replacements for some
forms in foo.lisp, as described later below.  But if the value of state
global 'write-acl2x is not nil, then instead, this certify-book command
writes such a file foo.acl2x.

Before we discuss the function of .acl2x files, we first explain more
about how a non-nil value of state global 'write-acl2x affects the
behavior of a command (certify-book ... :acl2x t ...).  A significant
effect on the behavior is that after processing events in the given
book, ACL2 writes out a .acl2x file and then returns, skipping the other
subsequent actions typically performed by certify-book: a
local-incompatibility check, writing of a certificate file, and
possibly compilation.  Another effect is that proofs may be skipped when
processing events assuming that the the certify-book command does not
explicitly specify :skip-proofs-okp nil, as we now explain.  A non-nil
value of 'write-acl2x should either be t or a one-element list (x),
where x is a legal value for the state global 'ld-skip-proofsp (see
LD-SKIP-PROOFSP).  In both cases, certify-book will process
events to write out a .acl2x file as described above.  But in the
latter (list) case, event processing will take place according to the
value of x: in particular, proofs will be skipped when x is not nil,
and if moreover x is the symbol include-book-with-locals, then only one
pass will be made through each encapsulate form.  A third effect of a
non-nil value of 'write-acl2x, which is restricted to the list case, is
that include-book events encountered during event processing are
allowed to succeed on uncertified books, something that is prohibited
during most calls of certify-book.

When certify-book is used to write out a .acl2x file, there is
typically a subsequent run of certify-book that reads that file.
Consider how this can work with a book foo.lisp.  In the first call of
certify-book, a file foo.acl2x is written that contains all make-event
expansions, but foo.cert is not written.  In the second call of
certify-book, no make-event expansion typically takes place, because
foo.acl2x supplies the expansions.  The command (set-write-acl2x t
state) should be evaluated before the first certification (though
another legal non-nil value may be used in place of t), setting the
value of state global 'write-acl2x to t, to enable writing of
foo.acl2x; and the command (set-write-acl2x nil state) may be evaluated
before the second run (though this is not necessary in a fresh ACL2
session) in order to complete the certification (writing out foo.cert)
using foo.acl2x to supply the make-event expansions.

When Certify-book is supplied with keyword argument :acl2x t it will
read or write the book's .acl2x file; when supplied with :acl2x nil, it
will not read or write that .acl2x file.  The value of :acl2x is nil by
default.  The interaction of certify-book with the corresponding .acl2x
file is as follows.

     o If :acl2x is t, then:
       - If set-write-acl2x has been (most recently) called with a
         value of t for its first argument, then ACL2 writes the
         corresponding .acl2x file.
       - If set-write-acl2x has been (most recently) called with a
         value of nil for its first argument, or not called at all,
         then ACL2 insists on a corresponding .acl2x file that is at
         least as recent as the corresponding .lisp file, causing an
         error otherwise.
     o If :acl2x is nil, then:
       - If set-write-acl2x has been (most recently) called with a
         value t for its first argument, or if argument :ttagsx
         is supplied, then an error occurs.
       - If the .acl2x file exists, then regardless of whether or how
         set-write-acl2x has been called, ACL2 ignores the .acl2x
         file but issues a warning about it.

Suppose you use the two-runs approach: first write a .acl2x file, then
certify using (reading) that .acl2x file.  Then with scripts such as
makefiles, then you may wish to provide a single certify-book command
to use for both runs.  For that purpose, certify-book supports the
keyword argument :ttagsx.  If this argument is supplied and write-acl2x
is true, then this argument is treated as the :ttags argument,
overriding a :ttags argument if present.  That is, for the two runs,
:ttagsx may be used to specify the trust tags used in the first
certification while :ttags specifies the trust tags, if any (else
:ttags may be omitted), used in the second certification.  Note: If the
argument :ttagsx is not supplied, then its value defaults to the
(explicit or default) value of the :ttags argument.

The built-in ACL2 Makefile support automatically generates suitable
dependencies if you create a .acl2 file with a certify-book call
matching the following regular expression, case-independent:

       (certify-book[^;]*:acl2x t

See BOOK-MAKEFILES, and for an example .acl2 file with a
certify-book call matching the above pattern, see distributed file
books/make-event/double-cert-test-1.acl2.

Note that include-book is generally not affected by set-write-acl2x,
other than through the indirect effect on certify-book.  More
precisely: All expansions are stored in the certificate file, so when
include-book is applied to a certified book, the .acl2x file is not
consulted.

An example of how to put this all together may be found in distributed
book books/make-event/double-cert-test-1.lisp.  There, we see the
following form.

     (make-event
      (progn (defttag :my-ttag)
             (progn! (let ((val (sys-call "pwd" nil)))
                       (value (list 'defun 'foo () val))))))

Imagine that in place of the binding computed using sys-call, which by
the way requires a trust tag, is some computation of your choice (such
as reading forms from a file) that is used to construct your own event,
in place of the defun event constructed above.  The Makefile in that
directory contains the following added dependency, so that file
double-cert-test-1.acl2x will be created:

     double-cert-test-1.cert: double-cert-test-1.acl2x

There is also the file double-cert-test-1.acl2 in that directory, which
contains a single form as follows.

     (certify-book "double-cert-test-1" ? t :ttagsx :all :ttags nil)

Thus, a call of make first creates file double-cert-test-1.acl2x, which
uses the above :ttagsx argument in order to support the use of defttag
during make-event expansion.  Then, make goes on to cause a second
certification in which no trust tags are involved.  As a result, the
parent book double-cert-test.lisp is ultimately certified without
requiring any trust tags.

The discussion above is probably sufficient for most users of the
two-run approach it describes.  We conclude with further details for
those who want more information.  Those who wish to see a yet
lower-level explanation of how all this works are invited to read the
comment in the ACL2 source code entitled "Essay on .acl2x Files (Double
Certification).

Consider the .acl2x file produced by the first run as described above.
It contains a single expression, which is an association list whose
keys are all positive integers, which occur in increasing order.  When
the .acl2x file is present and at least as recent as the corresponding
.lisp file, then for a subsequent certify-book with argument :acl2x t
and the (default) value of nil for state global 'write-acl2x, that
association list will be applied to the top-level events in the book, as
follows.  Suppose the entry (n . ev) belongs to the association list in
the .acl2x file.  Then n is a positive integer, and the nth top-level
event in the book -- where the 0th event is the initial in-package form
-- will be replaced by ev.  In practice, ev is the make-event expansion
created during certification for the nth top-level event in the book;
and this will always be the case if the .acl2x file is created by
certify-book after execution of the form (set-write-acl2x t state).
However, you are welcome to associate indices manually with any events
you wish into the alist stored in the .acl2x file.

Note: Also see the distributed book make-event/acl2x-help.lisp for a
useful utility that can be used to skip proofs during the writing of
.acl2x files.

TAU-STATUS    query or set tau system status

     Examples:
     (tau-status)
     (tau-status :system t)
     (tau-status :auto-mode nil)
     (tau-status :system t :auto-mode nil)

     General Form:
     (tau-status :system a :auto-mode b)

where a and b are Booleans.  Both keyword arguments are optional and
they may be presented in either order.  Value a controls whether the
tau-system is used during subsequent proofs.  Value b controls whether
the tau rules are automatically created as rules of other rule-classes
are added.

There are two important flags associated with the tau-system: (a)
whether the tau system is used in proof attempts, and (b) whether the
tau system is automatically extending its data base when other classes
of rules are added.  These two flags are independent.  For example, the
tau system may be disabled in proof attempts even though it is actively
(and silently) extending its data base in as rules of other classes are
added.

This macro allows you to inspect or set the two flags.  Flag (a) is
actually toggled by enabling or disabling the executable-counterpart of
tau-system.  Flag (b) is toggled with the function set-tau-auto-mode,
which manipulates the acl2-defaults-table.

This macro expands into zero, one, or two events, as required by the
supplied values of flags a and b.

If no arguments are supplied the form is not an event and simply
returns (as an "error triple" (mv nil ans state)) the current settings
of the two flags.  For example:

     ACL2 !>(tau-system)
      ((:SYSTEM NIL) (:AUTO-MODE T))

intended to be self-explanatory.

TERM-TABLE    a table used to validate meta rules

     Example:
     (table term-table t '((binary-+ x y) '3 'nil (car x)))

See TABLE for a general discussion of tables and the table
event used to manipulate tables.

The "term-table" is used at the time a meta rule is checked for
syntactic correctness.  Each proposed metafunction is run on each term
in this table, and the result in each case is checked to make sure that
it is a termp in the current world.  In each case where this test
fails, a warning is printed.

Whenever a metafunction is run in support of the application of a meta
rule, the result must be a term in the current world.  When the result
is not a term, a hard error arises.  The term-table is simply a means
for providing feedback to the user at the time a meta rule is
submitted, warning of the definite possibility that such a hard error
will occur at some point in the future.

The key used in term-table is arbitrary.  The top-most value is always
the one that is used; it is the entire list of terms to be considered.
Each must be a termp in the current ACL2 world.

UNTRANS-TABLE    associates a function symbol with a macro for printing user-level terms

     Examples:
     ACL2 !>(untrans-table (w state))
     ((BINARY-+ + . T)
      (BINARY-* * . T)
      (BINARY-APPEND APPEND . T)
      (BINARY-LOGAND LOGAND . T)
      (BINARY-LOGIOR LOGIOR . T)
      (BINARY-LOGXOR LOGXOR . T)
      (BINARY-LOGEQV LOGEQV . T)
      (BINARY-POR POR . T)
      (BINARY-PAND PAND . T))

See TABLE for a general discussion of tables.

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

USER-DEFINED-FUNCTIONS-TABLE    an advanced table used to replace certain system functions

     Examples:
     (table user-defined-functions-table 'untranslate-preprocess 'my-preprocess)
     (table user-defined-functions-table 'untranslate 'my-untranslate)

This feature should perhaps only be used by advanced users who have a
thorough understanding of the system functions being replaced.  There
are currently two ways a user can affect the way ACL2 prints terms.

The first example associates the user-defined function symbol
my-preprocess with untranslate-preprocess.  As a result, when ACL2
prints a term, say during a proof, using its so-called "untranslate"
process the first thing it does is to call my-preprocess on two
arguments: that term and the current ACL2 logical world.  If the call
produces a non-nil result, then that result is passed to the untranslate
process.

The second example associates the user-defined function symbol
my-untranslate with the built-in function symbol untranslate.  As a
result, the code for my-untranslate will be run whenever the untranslate
process is run.  The formals of the two functions must agree and must
not contain any stobj names.  Note that these overrides fail to occur
upon guard violations and some other evaluation errors.

The untranslate-preprocess approach may suffice for most cases in which
a user wants to modify the way output is produced by the theorem
prover.  We present an example immediately below, but see
books/misc/untranslate-patterns.lisp for a more elaborate example.  If
the untranslate-preprocess approach does not seem sufficient for your
purposes, you are invited to look at file
books/misc/rtl-untranslate.lisp for an example of user-defined
untranslate (i.e., following the second example displayed above).

Suppose you have a large constant that you would prefer not to see in
proofs.  For example, you may have submitted the following definition
(but imagine a much larger constant, say, a list of length 1,000,000).

     (defconst *a* '(a b c d))

If you submit the following (silly) theorem

     (thm (equal (cons x *a*) (car (cons yyy zzz))))

then you will see the following output:

     (EQUAL (CONS X '(A B C D)) YYY).

If *a* had represented a much larger structure, we would wish we could
see the following instead.

     (EQUAL (CONS X *A*) YYY)

That can be accomplished as follows.  First we make the following
definition.

     (defun my-preprocess (term wrld)
       (declare (ignore wrld))
       (if (equal term (list 'quote *a*))
           '*a*
         nil))

Now we submit the following table event.

     (table user-defined-functions-table
            'untranslate-preprocess
            'my-preprocess)

This will install my-preprocess as a preprocessor before the normal
untranslation routine is applied to printing a term.  When the
untranslation routine encounters the constant (QUOTE (A B C D)), it
will replace it with *a*, and the usual untranlation routine will print
this as *A*.

VERIFY-GUARDS-EAGERNESS    See SET-VERIFY-GUARDS-EAGERNESS.

WITH-GUARD-CHECKING    suppressing or enable guard-checking for a form

     Example:

     ; Turn off all guard-checking for the indicated calls of append and car:
     (with-guard-checking :none
                          (car (append 3 4)))

     General Form:
     (with-guard-checking val form)

where val evaluates to a legal guard-checking value (see
SET-GUARD-CHECKING, or evaluate *guard-checking-values* to see the
list of such values), and form is a form to be evaluated as though we
had first executed (set-guard-checking val).  Of course, this
gaurd-checking setting is active only during evaluation of form, and is
ignored once evaluation passes into raw Lisp functions (see
GUARDS-AND-EVALUATION).

WITH-OUTPUT    suppressing or turning on specified output for an event

     Examples:

     ; Turn off all output during evaluation of the indicated thm form.
     (with-output
      :off :all
      :gag-mode nil
      (thm (equal (app (app x y) z) (app x (app y z)))))

     ; Prove the indicated theorem with the event summary turned off and
     ; using the :goals setting for gag-mode.
     (with-output
        :off summary
        :gag-mode :goals
        (defthm app-assoc (equal (app (app x y) z) (app x (app y z)))))

     ; Same effect as just above:
     (with-output
        :on summary
        :summary :all ; equivalently, the value (a list) of *summary-types*
        :gag-mode :goals
        (defthm app-assoc (equal (app (app x y) z) (app x (app y z)))))

     ; Same as just above, but turn off only the indicated parts of the summary.
     (with-output
        :on summary
        :summary (time rules)
        :gag-mode :goals  ; use gag-mode, with goal names printed
        (defthm app-assoc (equal (app (app x y) z) (app x (app y z)))))

     ; Same as specifying :off :all, but showing all output types:
     (with-output
      :off (error warning warning! observation prove proof-checker event expansion
                  summary proof-tree)
      :gag-mode nil
      (thm (equal (app (app x y) z) (app x (app y z)))))

     ; Same as above, but :stack :push says to save the current
     ; inhibit-output-lst, which can be restored in a subsidiary with-output call
     ; that specifies :stack :pop.
     (with-output
      :stack :push
      :off :all
      :gag-mode nil
      (thm (equal (app (app x y) z) (app x (app y z)))))

     General Form:
     (with-output :key1 val1 ... :keyk valk form)

where each :keyi is either :off, :on, :stack, :summary, or :gag-mode,
and vali is as follows.  If :keyi is :off or :on, then vali can be
:all, and otherwise is a symbol or non-empty list of symbols
representing output types that can be inhibited; see
SET-INHIBIT-OUTPUT-LST.  If :keyi is :gag-mode, then vali is one of
the legal values for :set-gag-mode.  If :keyi is :summary, then vali is
either :all or a true-list of symbols each of which belongs to the list
*summary-types*.  Otherwise :keyi is :stack, in which case :vali is
:push or :pop; for now assume that :stack is not specified (we'll
return to it below).  The result of evaluating the General Form above
is to evaluate form, but in an environment where output occurs as
follows.  If :on :all is specified, then every output type is turned on
except as inhibited by :off; else if :off :all is specified, then every
output type is inhibited except as specified by :on; and otherwise, the
currently-inhibited output types are reduced as specified by :on and
then extended as specified by :off.  But if :gag-mode is specified, then
before modifying how output is inhibited, gag-mode is set for the
evaluation of form as specified by the value of :gag-mode; see
SET-GAG-MODE.  If summary is among the output types that are turned
on (not inhibited), then if :summary is specified, the only parts of the
summary to be printed will be those specified by the value of :summary.
The correspondence should be clear, except perhaps that header refers to
the line containing only the word Summary, and value refers to the
value of the form printed during evaluation of sequences of events as
for progn and encapsulate.

Note that the handling of the :stack argument pays no attention to the
:summary argument.

Note: When the scope of with-output is exited, then all modifications
are undone, reverting gag-mode and the state of output inhibition to
those which were present before the with-output call was entered.

The :stack keyword's effect is illustrated by the following example,
where "(encapsulate nil)" may replaced by "(progn" without any change
to the output that is printed.

     (with-output
      :stack :push :off :all
      (encapsulate ()
        (defun f1 (x) x)
        (with-output :stack :pop (defun f2 (x) x))
        (defun f3 (x) x)
        (with-output :stack :pop :off warning (in-theory nil))
        (defun f4 (x) x)))

The outer with-output call saves the current output settings (as may
have been modified by earlier calls of set-inhibit-output-lst), by
pushing them onto a stack, and then turns off all output.  Each inner
with-output call temporarily pops that stack, restoring the starting
output settings, until it completes and undoes the effects of that pop.
Unless event output was inhibited at the top level (see
SET-INHIBIT-OUTPUT-LST), the following output is shown:

     Since F2 is non-recursive, its admission is trivial.  We observe that
     the type of F2 is described by the theorem (EQUAL (F2 X) X).

And then, if summary output was not inhibited at the top level, we get
the rest of this output:

     Summary
     Form:  ( DEFUN F2 ...)
     Rules: NIL
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)

     Summary
     Form:  ( IN-THEORY NIL)
     Rules: NIL
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)

Note that the use of :off warning supresses a "Theory" warning for the
(in-theory nil) event, and that in no case will output be printed for
definitions of f1, f3, or f4, or for the encapsulate event itself.

The following more detailed explanation of :stack is intended only for
advanced users.  After :gag-mode is handled (if present) but before :on
or :off is handled, the value of :stack is handled as follows.  If the
value is :push, then state global inhibit-output-lst-stack is modified
by pushing the value of state global inhibit-output-lst onto the value
of state global inhibit-output-lst-stack, which is nil at the top
level.  If the value is :pop, then state global
inhibit-output-lst-stack is modified only if non-nil, in which case its
top element is popped and becomes the value of of state global
inhibit-output-lst.

Warning: With-output has no effect in raw Lisp, and hence is disallowed
in function bodies.  However, you can probably get the effect you want
as illustrated below, where <form> must return an error triple (mv erp
val state); see LD.

     Examples avoiding with-output, for use in function definitions:

     ; Inhibit all output:
     (state-global-let*
      ((inhibit-output-lst *valid-output-names*))
      <form>)

     ; Inhibit all warning output:
     (state-global-let*
      ((inhibit-output-lst
        (union-eq (f-get-global 'inhibit-output-lst state)
                  '(warning warning!))))
      <form>)

Note that with-output is allowed in books.  See
EMBEDDED-EVENT-FORM.

THEORIES    sets of runes to enable/disable in concert

     Example: '((:definition app)
                (:executable-counterpart app)
                rv
                (rv)
                assoc-of-app)

See:

Related topics other than immediate subtopics:

A theory is a list of "runic designators" as described below.  Each
runic designator denotes a set of "runes" (see RUNE) and by
unioning together the runes denoted by each member of a theory we
define the set of runes corresponding to a theory.  Theories are used
to control which rules are "enabled," i.e., available for automatic
application by the theorem prover.  There is always a "current" theory.
A rule is enabled precisely if its rune is an element of the set of
runes corresponding to the current theory.  At the top-level, the
current theory is the theory selected by the most recent in-theory
event, extended with the rule names introduced since then.  Inside the
theorem prover, the :in-theory hint (see HINTS) can be used to
select a particular theory as current during the proof attempt for a
particular goal.

Theories are generally constructed by "theory expressions."  Formally,
a theory expression is any term, containing at most the single free
variable world, that when evaluated with world bound to the current
ACL2 world (see WORLD) produces a theory.  ACL2 provides
various functions for the convenient construction and manipulation of
theories.  These are called "theory functions" (see
THEORY-FUNCTIONS).  For example, the theory function union-theories
takes two theories and produces their union.  The theory function
universal-theory returns the theory containing all known rule names as
of the introduction of a given logical name.  But a theory expression
can contain constants, e.g.,

     '(assoc (assoc) (:rewrite car-cons) car-cdr-elim)

and user-defined functions.  The only important criterion is that a
theory expression mention no variable freely except world and evaluate
to a theory.

More often than not, theory expressions typed by the user do not
mention the variable world.  This is because user-typed theory
expressions are generally composed of applications of ACL2's theory
functions.  These "functions" are actually macros that expand into
terms in which world is used freely and appropriately.  Thus, the
technical definition of "theory expression" should not mislead you into
thinking that interestng theory expressions must mention world; they
probably do and you just didn't know it!

One aspect of this arrangement is that theory expressions cannot
generally be evaluated at the top-level of ACL2, because world is not
bound.  To see the value of a theory expression, expr, at the
top-level, type

     ACL2 !>(LET ((WORLD (W STATE))) expr).

However, because the built-in theories are quite long, you may be sorry
you printed the value of a theory expression!

A theory is a true list of runic designators and to each theory there
corresponds a set of runes, obtained by unioning together the sets of
runes denoted by each runic designator.  For example, the theory
constant

        '(assoc (assoc) (:rewrite car-cons) car-cdr-elim)

corresponds to the set of runes

        {(:definition assoc)
         (:induction assoc)
         (:executable-counterpart assoc)
         (:elim car-cdr-elim)
         (:rewrite car-cons)} .

Observe that the theory contains four elements but its runic
correspondent contains five.  That is because some designators denote
sets of several runes.  If the above theory were selected as current
then the five rules named in its runic counterpart would be enabled and
all other rules would be disabled.

We now precisely define the runic designators and the set of runes
denoted by each.

     o A rune is a runic designator and denotes the singleton set
     containing that rune.

     o If symb is a function symbol introduced with a defun (or defuns)
     event, then symb is a runic designator and denotes the set
     containing the runes (:definition symb) and (:induction symb),
     omitting the latter if no such induction rule exists (presumably
     because the function's definition is not singly recursive).

     o If symb is a function symbol introduced with a defun (or defuns)
     event, then (symb) is a runic designator and denotes the singleton
     set containing the rune (:executable-counterpart symb).

     o If symb is the name of a defthm (or defaxiom) event that
     introduced at least one rule, then symb is a runic designator and
     denotes the set of the names of all rules introduced by the named
     event.

     o If str is the string naming some defpkg event and symb is the
     symbol returned by (intern str "ACL2"), then symb is a runic
     designator and denotes the singleton set containing (:rewrite
     symb), which is the name of the rule stating the conditions under
     which the symbol-package-name of (intern x str) is str.

     o If symb is the name of a deftheory event, then symb is a runic
     designator and denotes the runic theory corresponding to symb.

These conventions attempt to implement the Nqthm-1992 treatment of
theories.  For example, including a function name, e.g., assoc, in the
current theory enables that function but does not enable the executable
counterpart.  Similarly, including (assoc) enables the executable
counterpart (Nqthm's *1*assoc) but not the symbolic definition.  And
including the name of a proved lemma enables all of the rules added by
the event.  These conventions are entirely consistent with Nqthm usage.
Of course, in ACL2 one can include explicitly the runes naming the
rules in question and so can avoid entirely the use of non-runic
elements in theories.

Because a rune is a runic designator denoting the set containing that
rune, a list of runes is a theory and denotes itself.  We call such
theories "runic theories."  To every theory there corresponds a runic
theory obtained by unioning together the sets denoted by each
designator in the theory.  When a theory is selected as "current" it is
actually its runic correspondent that is effectively used.  That is, a
rune is enabled iff it is a member of the runic correspondent of the
current theory.  The value of a theory defined with deftheory is the
runic correspondent of the theory computed by the defining theory
expression.  The theory manipulation functions, e.g., union-theories,
actually convert their theory arguments to their runic correspondents
before performing the required set operation.  The manipulation
functions always return runic theories.  Thus, it is sometimes
convenient to think of (non-runic) theories as merely abbreviations for
their runic correspondents, abbreviations which are "expanded" at the
first opportunity by theory manipulation functions and the "theory
consumer" functions such as in-theory and deftheory.

ACTIVE-RUNEP    check that a rune exists and is enabled

     Example:
     (active-runep '(:rewrite left-to-right))

     General Form:
     (active-runep rune)

where rune has the shape of a rune.  This macro expands to an
expression using the variables ens and state, and returns non-nil when
the given rune exists and is enabled (according to the given "enabled
structure," ens, and the current logical world of the given state).
See THEORY-INVARIANT for how this macro can be of use.

CURRENT-THEORY    currently enabled rules as of logical name

     Examples:
     (current-theory :here)
     (current-theory 'lemma3)

See LOGICAL-NAME.

     General Form:
     (current-theory logical-name)

Returns the current theory as it existed immediately after the
introduction of logical-name provided it is evaluated in an environment
in which the variable symbol WORLD is bound to the current ACL2 logical
world, (w state).  Thus,

     ACL2 !>(current-theory :here)

will cause an (unbound variable) error while

     ACL2 !>(let ((world (w state))) (current-theory :here))

will return the current theory in world.

See THEORIES and see LOGICAL-NAME for a discussion of
theories in general and why the commonly used "theory functions" such
as current-theory are really macros that expand into terms involving
the variable world.

The theory returned by current-theory is in fact the theory selected by
the in-theory event most recently preceding logical name, extended by
the rules introduced up through logical-name.

You may experience a fencepost problem in deciding which logical name
to use.  Deflabel can always be used to mark unambiguously for future
reference a particular point in the development of your theory.  The
order of events in the vicinity of an encapsulate is confusing.  See
ENCAPSULATE.

This "function" is actually a macro that expands to a term mentioning
the single free variable world.  When theory expressions are evaluated
by in-theory or the :in-theory hint, world is bound to the current ACL2
world.

DISABLE    deletes names from current theory

     Example:
     (disable fact (fact) associativity-of-app)

     General Form:
     (disable name1 name2 ... namek)

where each namei is a runic designator; see THEORIES.  The
result is the theory that contains all the names in the current theory
except those listed.  Note that this is merely a function that returns
a theory.  The result is generally a very long list of runes and you
will probably regret printing it.

The standard way to "disable" a fixed set of names, is as follows; see
HINTS and see IN-THEORY.

     :in-theory (disable name1 name2 ... namek)    ; in a hint
     (in-theory (disable name1 name2 ... namek))   ; as an event
     (local ; often desirable, to avoid exporting from the current context
      (in-theory (disable name1 name2 ... namek)))

Note that all the names are implicitly quoted.  If you wish to disable
a computed list of names, lst, use the theory expression
(set-difference-theories (current-theory :here) lst).

E/D    enable/disable rules

The macro e/d creates theory expressions for use in in-theory hints and
events.  It provides a convenient way to enable and disable
simultaneously, without having to write arcane theory expressions.

     Examples:
     (e/d (lemma1 lemma2))          ; equivalent to (enable lemma1 lemma2)
     (e/d () (lemma))               ; equivalent to (disable lemma)
     (e/d (lemma1) (lemma2 lemma3)) ; Enable lemma1 then disable lemma2, lemma3.
     (e/d () (lemma1) (lemma2))     ; Disable lemma1 then enable lemma2.

     General Form:
     (e/d enables-0 disables-0 ... enables-n disables-n)

where each enables-i and disables-i is a list of runic designators; see
THEORIES, see ENABLE, and see DISABLE.

The e/d macro takes any number of lists suitable for the enable and
disable macros, and creates a theory that is equal to (current-theory
:here) after executing the following commands.

(in-theory (enable . enables-0)) (in-theory (disable . disables-0))
[etc.]  (in-theory (enable . enables-n)) (in-theory (disable .
disables-n))

ENABLE    adds names to current theory

     Example:
     (enable fact (fact) associativity-of-app)

     General Form:
     (enable name1 name2 ... namek)

where each namei is a runic designator; see THEORIES.  The
result is the theory that contains all the names in the current theory
plus those listed.  Note that this is merely a function that returns a
theory.  The result is generally a very long list of runes and you will
probably regret printing it.

The standard way to "enable" a fixed set of names, is as follows; see
HINTS and see IN-THEORY.

     :in-theory (enable name1 name2 ... namek)  ; in a hint
     (in-theory (enable name1 name2 ... namek)) ; as an event
     (local ; often desirable, to avoid exporting from the current context
      (in-theory (enable name1 name2 ... namek)))

Note that all the names are implicitly quoted.  If you wish to enable a
computed list of names, lst, use the theory expression (union-theories
(current-theory :here) lst).