This is documentation for ACL2 Version 3.4
Copyright (C) 2008  University of Texas at Austin

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

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

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

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

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 (integer 0 268435455) i))
       (the integer
            (aref (the (simple-array integer (*))
                       (svref ms 1))
                  (the (integer 0 268435455) i))))

     (defun update-memi (i v ms)
       (declare (type (integer 0 268435455) i)
                (type integer v))
       (progn
        (setf (aref (the (simple-array integer (*))
                         (svref ms 1))
                    (the (integer 0 268435455) 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-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.

     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 other than state, 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.

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 ino rder 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).

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

     o Otherwise file "acl2-customization.lisp" on your home directory
     is the customization file, if it 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.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

     Example:
     (add-binop append binary-append)

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

The function symbol need not be binary; the name "add-binop" is legacy
from when that was the intention.  However, the folding of
right-associated arguments suggested above only takes place for binary
function symbols.

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

This is a convenient way to add an entry to macro-aliases-table and at
the same time extend the :binop-table.  As suggested by the example
above, right-associated calls of a binary function in this table will
be printed as corresponding calls of macros.  Thus in the case of 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, then the effect is
simply to replace f by the corresponding macro symbol.  See
MACRO-ALIASES-TABLE, see REMOVE-MACRO-ALIAS, see
BINOP-TABLE, and see REMOVE-BINOP.

ADD-DEFAULT-HINTS    add to the default hints

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

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

     General Form:
     (add-default-hints lst)

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

This event is completely analogous to set-default-hints, the difference
being that add-default-hints appends the indicated hints to the end of
the list of default hints, 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.

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

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

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

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

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

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

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

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

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

where kwd is a keywordp and dir is the pathname of a directory.  The
effect of this event is to modify the meaning of the :dir keyword
argument of include-book as indicated by the examples above, namely by
associating the indicated directory with the indicated keyword for
purposes of the include-book :dir argument.  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").

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

_Remarks_

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

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

The form

     (match-free-override (w state))

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

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

     Example:
     (add-nth-alias st0 st)

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

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

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

BINOP-TABLE    associates binary function with the corresponding macro

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

See TABLE for a general discussion of tables.

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

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

DELETE-INCLUDE-BOOK-DIR    remove association of keyword for include-book's :dir argument

     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 as indicated by
the examples above, namely by removing association of any directory with
the indicated keyword for purposes of the include-book :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 generates a call (table acl2-defaults-table
:include-book-dir-alist ...)  and hence is local to any books and
encapsulate events in which it occurs. See ACL2-DEFAULTS-TABLE.

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 function name in the current ACL2 world.  See
TABLE for a general discussion of tables and the table event used to
manipulate tables.

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.

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