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

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

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

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

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

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

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

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

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

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

     (redo-flat)

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

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

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

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

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

     (redo-flat :show t)

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

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

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

     Failed event:

     (DEFUN F3 (X) Y)
     ACL2 !>

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

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

REMOVE-CUSTOM-KEYWORD-HINT    remove a custom keyword hint

     Example Forms:
     (remove-custom-keyword-hint :my-hint)

     General Form:
     (remove-custom-keyword-hint keyword)

where keyword is a keywordp.

For an explanation of how custom keyword hints are processed, see
CUSTOM-KEYWORD-HINTS; also see ADD-CUSTOM-KEYWORD-HINT.

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

SET-BODY    set the definition body

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

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

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

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

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

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

SHOW-CUSTOM-KEYWORD-HINT-EXPANSION    print out custom keyword hints when they are expanded

       Examples:
       (show-custom-keyword-hint-expansion t)
       (show-custom-keyword-hint-expansion nil)

       General Form:
       (show-custom-keyword-hint-expansion flg)

If the value of flg is non-nil, then when custom keyword hints are
expanded, the system prints the results of each expansion.  This is
sometimes   useful for debugging custom keyword hints and, from time to
time, may be   useful in understanding how a custom hint affects some
proof attempt.

The default setting is nil.

For an explanation of how custom keyword hints are processed,   see
CUSTOM-KEYWORD-HINTS.

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

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

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.

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.

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

     Example:
     (remove-binop binary-append)

     General Form:
     (remove-binop binop)

See ADD-BINOP for a discussion of how to associate a macro name
with a binary function name for proof output purposes.  This form sets
binop-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-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.

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-NTH-ALIAS    remove the association of one symbol with another 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-UNTOUCHABLE    remove names from lists of untouchable symbols

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.

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

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