This is documentation for ACL2 Version 3.5
Copyright (C) 2009  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.

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.

     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).  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-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 or
linear rule is admitted.  It must be nil or a non-negative integer.
(See BACKCHAIN-LIMIT for details.)

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

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

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-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
     (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.
Future releases of ACL2 may install this setting as the default.
Please contact the ACL2 implementors if you have suggestions for
improving output in gag-mode.

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

Printing of events on behalf of certify-book, encapsulate, or defstobj
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-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)

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 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.  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, and 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-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.  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!.

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

_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-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 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-TAINTED-OK    See SET-TAINTED-OKP.

SET-TAINTED-OKP    control output

     Forms:
     (set-tainted-okp nil) ; do not allow incremental version mismatches (default)
     (set-tainted-okp t)   ; allow incremental version mismatches

Set-tainted-okp is of use only in the presence of incremental releases.
In short, evaluation of (set-tainted-okp t) instructs ACL2 to consider
an incremental release to have the same ACL2 version as the most
recently preceding normal release.  BUT THIS IS NOT THE CASE BY DEFAULT
BECAUSE ACL2 IS POTENTIALLY UNSOUND WHEN SET-TAINTED-OKP IS EVALUATED.

Incremental releases have an incremental (incrl) version field, for
example the number 1 in version  2.9.1.  (Also see VERSION.)
Ordinary releases have an implicit incrl version field of 0 (for
example, in version 2.9).  By default, include-book and certify-book
consider all fields of ACL2 version strings, including their incrl
fields, in order to decide if there are version mismatches.  But it may
be convenient to treat an incremental release as the same as the
corresponding (immediately preceding) normal release, in order to avoid
recertification of existing certified books.  SUCH RECERTIFICATION IS
LOGICALLY REQUIRED, but we provide (set-tainted-okp t) as a mechanism
to allow users to experiment with incremental releases.

Below we describe how books can be certified even though their
certification has depended on ignoring mismatches of incrl version
fields.  We call such certified books "tainted".

If (set-tainted-okp t) is evaluated, then any discrepancy is ignored
between the incrl version field of an included book (representing the
version of ACL2 in which that book was certified) and the current ACL2
version, namely the value of (@ acl2-version).  Thus, with
(set-tainted-okp t) we allow certification of books that depend on
included books that have such version mismatches with the current ACL2
version or are themselves tainted.  Any book thus certified will have
the string "(tainted)" included in its certificate's version string.
Indeed, when ACL2 detects that a book may depend either on a book whose
version's incrl field differs from that of the current ACL2 version, or
on a tainted book, then such a book is marked as tainted.

When (set-tainted-okp t) has been executed, then even though ACL2
"ignores" issues of tainting as discussed above, a "Tainted" warning is
printed whenever a tainted book is included or certified.

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

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.

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

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

WITH-OUTPUT    suppressing or turning on specified output for an event

     Examples:
     (with-output
        :off summary      ; turn off the event summary when evaluating the following:
        :gag-mode :goals  ; use gag-mode, with goal names printed
        (defthm app-assoc (equal (app (app x y) z) (app x (app y z)))))

     (with-output ; turn off all output
      :off :all
      :gag-mode nil
      (thm (equal (app (app x y) z) (app x (app y z)))))

     (with-output ; same as above, showing all output types
      :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)))))

     (with-output ; as above, but :stack :push says to save current
                  ; inhibit-output-lst, which can be restored in subsidiary
                  ; with-output call that specifies :stack :pop
      :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, 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.  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 all output is turned on except as
inhibited by :off; else if :off :all is specified, then all output 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.

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

EXECUTABLE-COUNTERPART-THEORY    executable counterpart rules as of logical name

     Examples:
     (executable-counterpart-theory :here)
     (executable-counterpart-theory 'lemma3)

See LOGICAL-NAME.

     General Form:
     (executable-counterpart-theory logical-name)

Returns the theory containing all the :executable-counterpart runes,
whether enabled or not, that existed immediately after logical-name was
introduced.  See the documentation for theories, logical-name,
executable-counterpart and function-theory.

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.

FUNCTION-THEORY    function symbol rules as of logical name

     Examples:
     (function-theory :here)
     (function-theory 'lemma3)

See LOGICAL-NAME.

     General Form:
     (function-theory logical-name)

Returns the theory containing all the :definition runes, whether
enabled or not, that existed immediately after logical-name was
introduced.  See the documentation for theories, logical-name and
executable-counterpart-theory.

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.

GROUND-ZERO    enabled rules in the startup theory

ACL2 concludes its initialization (boot-strapping) procedure by
defining the theory ground-zero; see THEORIES.  In fact, this
theory is just the theory defined by (current-theory :here) at the
conclusion of initialization; see CURRENT-THEORY.

Note that by evaluating the event

     (in-theory (current-theory 'ground-zero))

you can restore the current theory to its value at the time you started
up ACL2.

INCOMPATIBLE    declaring that two rules should not both be enabled

     Example:
     (theory-invariant (incompatible (:rewrite left-to-right)
                                     (:rewrite right-to-left)))

     General Form:
     (incompatible rune1 rune2)

where rune1 and rune2 are two specific runes.  The arguments are not
evaluated.  Invariant is just a macro that expands into a term that
checks that not both runes are enabled.  See THEORY-INVARIANT.

INTERSECTION-THEORIES    intersect two theories

     Example:
     (intersection-theories (current-theory :here)
                            (theory 'arith-patch))

     General Form:
     (intersection-theories th1 th2)

where th1 and th2 are theories (see THEORIES).  To each of the
arguments there corresponds a runic theory.  This function returns the
intersection of those two runic theories, represented as a list and
ordered chronologically.

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.

MINIMAL-THEORY    a minimal theory to enable

This theory (see THEORIES) enables only a few built-in
functions and executable counterparts.  It can be useful when you want
to formulate lemmas that rather immediately imply the theorem to be
proved, by way of a :use hint (see HINTS), for example as
follows.

     :use (lemma-1 lemma-2 lemma-3)
     :in-theory (union-theories '(f1 f2) (theory 'minimal-theory))

In this example, we expect the current goal to follow from lemmas
lemma-1, lemma-2, and lemma-3 together with rules f1 and f2 and some
obvious facts about built-in functions (such as the definition of
implies and the :executable-counterpart of car).  The :in-theory hint
above is intended to speed up the proof by turning off all inessential
rules.

RULE-NAMES    How rules are named.

     Examples:
     (:rewrite assoc-of-app)
     (:linear delta-aref . 2)
     (:definition length)
     (:executable-counterpart length)

See RUNE.

RUNE    a rule name

     Examples:
     (:rewrite assoc-of-app)
     (:linear delta-aref . 2)
     (:definition length)
     (:executable-counterpart length)

Background: The theorem prover is driven from a data base of rules.
The most common rules are :rewrite rules, which cause the simplifier to
replace one term with another.  Events introduce rules into the data
base.  For example, a defun event may introduce runes for symbolically
replacing a function call by its instantiated body, for evaluating the
function on constants, for determining the type of a call of the
function, and for the induction scheme introduced upon defining the
function.  Defthm may introduce several rules, one for each of the
:rule-classes specified (where one rule class is specified if
:rule-classes is omitted, namely, :rewrite).

Every rule in the system has a name.  Each name is a structured object
called a "rune," which is short for "rule name".  Runes are always of
the form (:token symbol . x), where :token is some keyword symbol
indicating what kind of rule is named, symbol is the event name that
created the rule (and is called the "base symbol" of the rune), and x
is either nil or a natural number that makes the rule name distinct
from that of rules generated by other events or by other :rule-classes
within the same event.

For example, an event of the form

     (defthm name thm
       :rule-classes ((:REWRITE :COROLLARY term1)
                      (:REWRITE :COROLLARY term2)
                      (:ELIM    :COROLLARY term3)))

typically creates three rules, each with a unique rune.  The runes are

     (:REWRITE name . 1), (:REWRITE name . 2), and (:ELIM name).

However, a given formula may create more than one rule, and all rules
generated by the same :corollary formula will share the same rune.
Consider the following example.

     (defthm my-thm
       (and (equal (foo (bar x)) x)
            (equal (bar (foo x)) x)))

This is treated identically to the following.

     (defthm my-thm
       (and (equal (foo (bar x)) x)
            (equal (bar (foo x)) x))
       :rule-classes ((:rewrite
                       :corollary
                       (and (equal (foo (bar x)) x)
                            (equal (bar (foo x)) x)))))

In either case, two rules are created: one rewriting (foo (bar x)) to
x, and one rewriting (bar (foo x)) to x.  However, only a single rune
is created, (:REWRITE MY-THM), because there is only one rule class.
But now consider the following example.

     (defthm my-thm2
       (and (equal (foo (bar x)) x)
            (equal (bar (foo x)) x))
       :rule-classes ((:rewrite
                       :corollary
                       (and (equal (foo (bar x)) x)
                            (equal (bar (foo x)) x)))
                      (:rewrite
                       :corollary
                       (and (equal (foo (bar (foo x))) (foo x))
                            (equal (bar (foo (bar x))) (bar x))))))

This time there are four rules created.  The first two rules are as
before, and are assigned the rune (:REWRITE MY-THM . 1).  The other two
rules are similarly generated for the second :corollary, and are
assigned the rune (:REWRITE MY-THM . 2).

The function corollary will return the corollary term associated with a
given rune in a given world.  Example:

     (corollary '(:TYPE-PRESCRIPTION DIGIT-TO-CHAR) (w state))

However, the preferred way to see the corollary term associated with a
rune or a name is to use :pf; see PF.

The defun event creates as many as four rules.  (:definition fn) is the
rune given to the equality axiom defining the function, fn.
(:executable-counterpart fn) is the rune given to the rule for computing
fn on known arguments.  A type prescription rule may be created under
the name (:type-prescription fn), and an induction rule may be created
under the name (:induction fn).

Runes may be individually enabled and disabled, according to whether
they are included in the current theory.  See THEORIES.  Thus,
it is permitted to disable (:elim name), say, while enabling the other
rules derived from name.  Similarly, (:definition fn) may be disabled
while (:executable-counterpart fn) and the type prescriptions for fn
are enabled.

Associated with most runes is the formula justifying the rule named.
This is called the "corollary formula" of the rune and may be obtained
via the function corollary, which takes as its argument a rune and a
property list world.  Also see PF.  The corollary formula for
(:rewrite name . 1) after the defthm event above is term1.  The
corollary formulas for (:definition fn) and (:executable-counterpart
fn) are always identical: the defining axiom.  Some runes, e.g.,
(:definition car), do not have corollary formulas.  Corollary returns
nil on such runes.  In any case, the corollary formula of a rune, when
it is non-nil, is a theorem and may be used in the :use and :by hints.

Note: The system has many built in rules that, for regularity, ought to
have names but don't because they can never be disabled.  One such rule
is that implemented by the linear arithmetic package.  Because many of
our subroutines are required by their calling conventions to return the
justifying rune, we have invented the notion of "fake runes." Fake
runes always have the base symbol nil, use a keyword token that
includes the phrase "fake-rune", and are always enabled.  For example,
(:fake-rune-for-linear nil) is a fake rune.  Occasionally the system
will print a fake rune where a rune is expected.  For example, when the
linear arithmetic fake rune is reported among the rules used in a
proof, it is an indication that the linear arithmetic package was used.
However, fake runes are not allowed in theories, they cannot be
enabled or disabled, and they do not have associated corollary
formulas.  In short, despite the fact that the user may sometimes see
fake runes printed, they should never be typed.

SET-DIFFERENCE-THEORIES    difference of two theories

     Example:
     (set-difference-theories (current-theory :here)
                              '(fact (fact)))

     General Form:
     (set-difference-theories th1 th2)

where th1 and th2 are theories (see THEORIES).  To each of the
arguments there corresponds a runic theory.  This function returns the
set-difference of those two runic theories, represented as a list and
ordered chronologically.  That is, a rune is in the result iff it is in
the first runic theory but not in the second.

The standard way to "disable" a theory, lst, is: (in-theory
(set-difference-theories (current-theory :here) lst)).

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.

THEORY    retrieve named theory

     Example:
     (theory 'ground-zero)

In the example above, the theory returned is the one in force when ACL2
is started up (see GROUND-ZERO).

     General Form:
     (theory name)

where name is the name of a previously executed deftheory event.
Returns the named theory.  See THEORIES.

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.

THEORY-FUNCTIONS    functions for obtaining or producing theories

     Example Calls of Theory Functions:
     (universal-theory :here)
     (union-theories th1 th2)
     (set-difference-theories th1 th2)

The theory functions are documented individually:

Related topics other than immediate subtopics:

The functions (actually, macros) mentioned above are convenient ways to
produce theories.  (See THEORIES.) Some, like universal-theory,
take a logical name (see LOGICAL-NAME) as an argument and
return the relevant theory as of the time that name was introduced.
Others, like union-theories, take two theories and produce a new one.
See REDUNDANT-EVENTS for a caution about the use of logical
names in theory expressions.

Theory expressions are generally composed of applications of theory
functions.  Formally, theory expressions are expressions that involve,
at most, the free variable world and that when evaluated with world
bound to the current ACL2 world (see WORLD) return theories.
The "theory functions" are actually macros that expand into forms that
involve the free variable world.  Thus, for example (universal-theory
:here) actually expands to (universal-theory-fn :here world) and when
that form is evaluated with world bound to the current ACL2 world,
universal-theory-fn scans the ACL2 property lists and computes the
current universal theory.  Because the theory functions all implicitly
use world, the variable does not generally appear in anything the user
types.

UNION-THEORIES    union two theories

     Example:
     (union-theories (current-theory 'lemma3)
                     (theory 'arith-patch))

     General Form:
     (union-theories th1 th2)

where th1 and th2 are theories (see THEORIES).  To each of the
arguments there corresponds a runic theory.  This function returns the
union of those two runic theories, represented as a list and ordered
chronologically.

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.

UNIVERSAL-THEORY    all rules as of logical name

     Examples:
     (universal-theory :here)
     (universal-theory 'lemma3)

See LOGICAL-NAME.

     General Form:
     (universal-theory logical-name)

Returns the theory consisting of all the runes that existed immediately
after logical-name was introduced.  See THEORIES and see
LOGICAL-NAME.  The theory includes logical-name itself (if there is a
rule by that name).  (Note that since some events do not introduce
rules (e.g., defmacro, defconst or defthm with :rule-classes nil), the
universal-theory does not necessarily include a rune for every event
name.)  The universal-theory is very long and you will probably regret
printing it.

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.  This
is convenient because deflabel does not introduce any rules and hence
it doesn't matter if you count it as being in the interval or not.  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.

Also see CURRENT-THEORY.  Current-theory is much more commonly
used than universal-theory.  The former includes only the enabled runes
as of the given logical-name, which is probably what you want, while
the latter includes disabled ones as well.

TRACE    tracing functions in ACL2

ACL2 provides a trace utility, trace$, with corresponding reverse
operation untrace$.  These can be used without any dependence on the
underlying Lisp utility, and are the tracing utilities of choice in
ACL2; see TRACE$ and see UNTRACE$.

However, for advanced users we note that the underlying host Lisp may
also provide a trace utility, trace, and corresponding untrace.
Moreover, these have been modified in the case that the host Lisp is
GCL, Allegro CL, or CCL (OpenMCL), to provide limited support for
:entry, :exit, and perhaps :cond keywords, to hide certain large data
structures (world, enabled structure, rewrite constant), and to trace
executable counterparts.  See source files *-trace.lisp.  For the above
Lisps, you can invoke the original trace and untrace by invoking
old-trace and old-untrace, respectively, in raw Lisp rather than in the
normal ACL2 loop.

BREAK-ON-ERROR    break when encountering a hard or soft error caused by ACL2

     General forms:
     (break-on-error t)    ; installs a trace causing a continuable error (break)
                           ;   when an error is invoked by ACL2.
     (break-on-error)      ; same as above
     (break-on-error :all) ; same as above, but even when inside the prover
     (break-on-error nil)  ; uninstall any above trace

(Break-on-error) generates approximately the following, but modified to
print appropriate extra information:

     (trace! (error1 :entry nil :exit (break))
             (throw-raw-ev-fncall :entry (break)))

This trace should cause entry to the Lisp debugger whenever ACL2 calls
its error routines, except for certain errors when inside the theorem
prover (and even then if option :all is supplied).

NOTE: For technical reasons, if you see the break message

     ACL2 Error [Breaking on error (entry to ev-fncall-msg)]:

which is followed by an explanation of the error, then if you continue
from the break, you will see that explanation again.

Finally, note that you are welcome to define your own version of
break-on-error by modifying a copy of the source definition (search for
"(defmacro break-on-error" in ACL2 source file other-events.lisp).
Please feel free to send your version of break-on-error to the ACL2
implementors, for possible inclusion into ACL2.

Break-on-error is implmented using ACL2 trace$.  See TRACE! if
you want an explanation of the "TTAG NOTE" that is printed.

The argument, if supplied, is evaluated and must evaluate to t, nil, or
:all.

Also see SET-DEBUGGER-ENABLE for how to get raw-Lisp backtrace
information when an error occurs as a result of break-on-error, or even
of a raw Lisp error, by calling set-debugger-enable with argument :bt,
:bt-break, or :break-bt.  Note that for ACL2 errors (as opposed to raw
Lisp errors), i.e. errors affected by break-on-error, all three of
those keyword values are treated equivalently (and, all are ignored for
GCL; see SET-DEBUGGER-ENABLE).

CLOSE-TRACE-FILE    stop redirecting trace output to a file

     General Form:
     (close-trace-file) ; trace output is no longer redirected to a file

Output from trace$ normally goes to the screen, or more precisely,
standard-co.  It can be redirected to a file; see
OPEN-TRACE-FILE.  Use close-trace-file to redirect trace output to
standard-co.

OPEN-TRACE-FILE    redirect trace output to a file

     Example:
     (open-trace-file "foo") ; trace output will go to file foo

     General Form:
     (open-trace-file filename) ; trace output will go to file filename

Output from trace$ normally goes to the screen, i.e., standard-co.  But
it can be redirected to a file as shown above.  See
CLOSE-TRACE-FILE for how to send trace output back to the screen.

SET-TRACE-EVISC-TUPLE    set the trace evisc tuple

A trace evisc-tuple, which is set by this utility, provides a means to
restrict printing during tracing.  See EVISC-TUPLE for an
introduction to evisc-tuples; also see SET-EVISC-TUPLE and see
SET-IPRINT.

By default the ACL2 trace mechanism, trace$, automatically deals with
stobjs, the logical world, and certain other large structures.  See
TRACE$, in particular the documentation of trace$ option :hide.
However, even with that default behavior you may want to restrict what
is printed according to the print-level and print-length of an
evisc-tuple; see EVISC-TUPLE.

     Examples:

     ; Set trace evisc tuple to a standard value, using current Lisp *print-level*
     ; and *print-length* variables:
     (set-trace-evisc-tuple t state)

     ; Set trace evisc tuple back to its default:
     (set-trace-evisc-tuple nil state)

     ; Set trace evisc tuple to restrict print-level to 3 and print-length to 4,
     ; while hiding the logical world and suitably printing stobjs even if trace$
     ; option ``:hide nil'' is used.
     (set-trace-evisc-tuple
      (evisc-tuple 3 4 (trace-evisceration-alist state) nil)
      state)

     General Forms:

     (set-trace-evisc-tuple nil state) ; trace evisc-tuple set to standard value
     (set-trace-evisc-tuple   t state) ; trace evisc-tuple set to hide the logical
                                       ;   world and deal with stobjs even when
                                       ;   trace$ option ``:hide nil'' is supplied
     (set-trace-evisc-tuple evisc-tuple state)
                                       ; tracing set to use indicated evisc-tuple

See TRACE$ for a discussion of ACL2 tracing.  The evisc-tuple
used by that trace utility is the one last installed by
set-trace-evisc-tuple (or by set-evisc-tuple for the trace-evisc-tuple)
-- initially to the default of nil -- unless overriden by trace option
:evisc-tuple.

*Remark*.  If you use value t, then ACL2 will ensure that the logical
world and stobjs are kept up-to-date in the trace evisc-tuple.

TRACE!    trace the indicated functions after creating an active trust tag

     Example:
     (trace! (fact :native t :entry *foo*))

     General Form:
     (trace! spec1 ... specn)

where the fni are suitable arguments to trace$.

Trace! is a version of trace$ that avoids the need for an
already-active trust tag (or "ttag"; see DEFTTAG), as explained
below.  See TRACE$ for when a trust tag can be necessary.

See UNTRACE$ for how to undo the effect of trace!.

The evaluation of a trace! form causes temporary creation of an active
trust tag, :trace!, followed by the corresponding trace$ form.  The
trust tag will disappear when the call to trace! completes.  Even though
trace! will remove its temporary ttag, it will still print a "TTAG
NOTE", which indicates that the session is suspect.  See DEFTTAG
and see TTAGS-SEEN for further remarks on this issue.

Because of the active trust tag, it is possible to do things with trace!
that are useful but without logical justification.  Below is an example
of how to use trace! to cause a function call to change state, even
though the function does not take state as a parameter.

     ACL2 !>(defun fact (n)
              (declare (xargs :guard (natp n) :verify-guards nil))
              (if (zp n)
                  1
                (* n (fact (1- n)))))

     The admission of FACT 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 N).  We observe that the type of FACT is described by the
     theorem (AND (INTEGERP (FACT N)) (< 0 (FACT N))).  We used the :compound-
     recognizer rule ZP-COMPOUND-RECOGNIZER and primitive type reasoning.

     Summary
     Form:  ( DEFUN FACT ...)
     Rules: ((:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER)
             (:FAKE-RUNE-FOR-TYPE-SET NIL))
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      FACT
     ACL2 !>(defun update-foo (n value state)
              (declare (xargs :stobjs state :verify-guards nil))
              (assign foo (cons (cons n value) (@ foo))))

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

     (UPDATE-FOO * * STATE) => (MV * * STATE).

     Summary
     Form:  ( DEFUN UPDATE-FOO ...)
     Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      UPDATE-FOO
     ACL2 !>(trace! (fact :exit (update-foo n value state)))

     TTAG NOTE: Adding ttag :TRACE! from the top level loop.
      ((FACT :EXIT (UPDATE-FOO N VALUE STATE)))
     ACL2 !>(assign foo nil)
      NIL
     ACL2 !>(fact 7)
     1> (ACL2_*1*_ACL2::FACT 7)
       2> (ACL2_*1*_ACL2::FACT 6)
         3> (ACL2_*1*_ACL2::FACT 5)
           4> (ACL2_*1*_ACL2::FACT 4)
             5> (ACL2_*1*_ACL2::FACT 3)
               6> (ACL2_*1*_ACL2::FACT 2)
                 7> (ACL2_*1*_ACL2::FACT 1)
                   8> (ACL2_*1*_ACL2::FACT 0)
                   <8 NIL
                 <7 NIL
               <6 NIL
             <5 NIL
           <4 NIL
         <3 NIL
       <2 NIL
     <1 NIL
     5040
     ACL2 !>(@ foo)
     ((7 . 5040)
      (6 . 720)
      (5 . 120)
      (4 . 24)
      (3 . 6)
      (2 . 2)
      (1 . 1)
      (0 . 1))
     ACL2 !>(verify-guards fact)

     Computing the guard conjecture for FACT....

     The guard conjecture for FACT is trivial to prove, given the :compound-
     recognizer rules NATP-COMPOUND-RECOGNIZER and ZP-COMPOUND-RECOGNIZER,
     primitive type reasoning and the :type-prescription rule FACT.  FACT
     is compliant with Common Lisp.

     Summary
     Form:  ( VERIFY-GUARDS FACT)
     Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER)
             (:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER)
             (:FAKE-RUNE-FOR-TYPE-SET NIL)
             (:TYPE-PRESCRIPTION FACT))
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      FACT
     ACL2 !>(assign foo nil)
      NIL
     ACL2 !>(fact 7)
     1> (ACL2_*1*_ACL2::FACT 7)
       2> (FACT 7)
         3> (FACT 6)
           4> (FACT 5)
             5> (FACT 4)
               6> (FACT 3)
                 7> (FACT 2)
                   8> (FACT 1)
                     9> (FACT 0)
                     <9 NIL
                   <8 NIL
                 <7 NIL
               <6 NIL
             <5 NIL
           <4 NIL
         <3 NIL
       <2 NIL
     <1 NIL
     5040
     ACL2 !>(@ foo)
     ((7 . 5040)
      (7 . 5040)
      (6 . 720)
      (5 . 120)
      (4 . 24)
      (3 . 6)
      (2 . 2)
      (1 . 1)
      (0 . 1))
     ACL2 !>(trace! (fact :exit (progn (update-foo n value state)
                                       (cons traced-fn values))))

     TTAG NOTE: Adding ttag :TRACE! from the top level loop.
      ((FACT :EXIT (PROGN (UPDATE-FOO N VALUE STATE)
                          (CONS TRACED-FN VALUES))))
     ACL2 !>(assign foo nil)
      NIL
     ACL2 !>(fact 7)
     1> (ACL2_*1*_ACL2::FACT 7)
       2> (FACT 7)
         3> (FACT 6)
           4> (FACT 5)
             5> (FACT 4)
               6> (FACT 3)
                 7> (FACT 2)
                   8> (FACT 1)
                     9> (FACT 0)
                     <9 (FACT 1)
                   <8 (FACT 1)
                 <7 (FACT 2)
               <6 (FACT 6)
             <5 (FACT 24)
           <4 (FACT 120)
         <3 (FACT 720)
       <2 (FACT 5040)
     <1 (ACL2_*1*_ACL2::FACT 5040)
     5040
     ACL2 !>(@ foo)
     ((7 . 5040)
      (7 . 5040)
      (6 . 720)
      (5 . 120)
      (4 . 24)
      (3 . 6)
      (2 . 2)
      (1 . 1)
      (0 . 1))
     ACL2 !>

TRACE$    trace function evaluations

     Examples:
     (trace$ foo bar)     ; trace foo and bar
     (trace$)             ; return current trace info (no new tracing specified)
     (trace$ (foo :entry  ; trace foo, printing first actual parameter upon entry
                  (car arglist)))
     (trace$ (foo :exit   ; trace foo, using fmt to print upon exit
                  (:fmt (msg "Exiting FOO with ~x0"
                             value))))

     General Forms:
     (trace$ spec1 spec2 ... specn) ; n >= 1
     (trace$)

where the speci are trace specs, as described below.

Trace$ installs alternate code for the indicated functions that prints
information upon entry to, and exit from, calls of the functions.  For
an alternate tracing utility used for educational purposes in ACL2s
(`http://acl2s.peterd.org/acl2s/doc/'), see distributed book
books/misc/trace-star.lisp.

From a logical perspective all trace printing is a fiction.  (But see
TRACE! for a way to get around this and modify state.)  For a
related fiction, see CW.  (Trace$) returns the list of
currently-active trace specs, while the application of trace$ to at
least one argument returns the list of its arguments that are
successfully acted on.

Output from trace$ normally goes to the screen, i.e., to standard-co.
But it can be redirected to a file; see OPEN-TRACE-FILE.

See UNTRACE$ for how to undo the effect of trace$.  Also see
TRACE for mention of modifications made to raw Lisp trace,
which is accessible (as described below) using the :native keyword.

Next, we introduce tracing with some examples.  After that, we provide
reference documentation for individual trace options allowed in a trace
spec.

We begin by illustrating the simplest sort of trace spec: a function
symbol.  For example, the form (trace$ foo bar) directs the tracing of
functions foo and bar by virtue of the two trace specs foo and bar.  We
can see tracing in action by first defining:

     (defun f (x)
       (cons x x))

     (defun g (x)
       (list (f x) 3))

The following log then illustrates tracing of these two functions.
Notice that before guards have been verified, the so-called "*1*"
functions (sometimes called "executable counterpart functions" or "logic
functions") are called but the corresponding raw Lisp functions are
not; but after guard verification of f, the raw Lisp counterpart of f is
indeed called.  (See GUARD and see
GUARD-EVALUATION-EXAMPLES-LOG.)

     ACL2 !>(trace$ f g)
      ((F) (G))
     ACL2 !>(g 7)
     1> (ACL2_*1*_ACL2::G 7)
       2> (ACL2_*1*_ACL2::F 7)
       <2 (ACL2_*1*_ACL2::F (7 . 7))
     <1 (ACL2_*1*_ACL2::G ((7 . 7) 3))
     ((7 . 7) 3)
     ACL2 !>(verify-guards f)

     Computing the guard conjecture for F....

     The guard conjecture for F is trivial to prove.  F is compliant with
     Common Lisp.

     Summary
     Form:  ( VERIFY-GUARDS F)
     Rules: NIL
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      F
     ACL2 !>(g 7)
     1> (ACL2_*1*_ACL2::G 7)
       2> (ACL2_*1*_ACL2::F 7)
         3> (F 7)
         <3 (F (7 . 7))
       <2 (ACL2_*1*_ACL2::F (7 . 7))
     <1 (ACL2_*1*_ACL2::G ((7 . 7) 3))
     ((7 . 7) 3)
     ACL2 !>

The following example introduces trace specs other than function
symbols.  Consider the following definition.

     (defun fact (n)
       (declare (xargs :guard (natp n)))
       (if (zp n)
           1
         (* n (fact (1- n)))))

The following log illustrates the use of trace options :cond (condition
for entering trace), :entry (what to print on entry), and :exit (what
to print on exit).  The reason for two calls on argument 4 is that we
are seeing such calls for the executable counterpart of fact and also
its raw Lisp function.

     ACL2 !>(trace$ (fact :cond (evenp (car arglist))
                          :entry (cons 'factorial-call arglist)
                          :exit (car values)))
      ((FACT :COND (EVENP (CAR ARGLIST))
             :ENTRY (CONS 'FACTORIAL-CALL ARGLIST)
             :EXIT (CAR VALUES)))
     ACL2 !>(fact 4)
     1> (FACTORIAL-CALL 4)
       2> (FACTORIAL-CALL 4)
         3> (FACTORIAL-CALL 2)
           4> (FACTORIAL-CALL 0)
           <4 1
         <3 2
       <2 24
     <1 24
     24
     ACL2 !>

Notice that VALUES above is the list of all values returned, which is a
one-element list unless mv return is used, as illustrated in the
following example, after defining: (defun two-vals (x) (mv x 7)).

     ACL2 !>(trace$ two-vals)
      ((TWO-VALS))
     ACL2 !>(two-vals 3)
     1> (ACL2_*1*_ACL2::TWO-VALS 3)
     <1 (ACL2_*1*_ACL2::TWO-VALS 3 7)
     (3 7)
     ACL2 !>(verify-guards two-vals)

     Computing the guard conjecture for TWO-VALS....

     The guard conjecture for TWO-VALS is trivial to prove, given the :executable-
     counterpart of CONS.  TWO-VALS is compliant with Common Lisp.

     Summary
     Form:  ( VERIFY-GUARDS TWO-VALS)
     Rules: ((:EXECUTABLE-COUNTERPART CONS))
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      TWO-VALS
     ACL2 !>(two-vals 3)
     1> (ACL2_*1*_ACL2::TWO-VALS 3)
       2> (TWO-VALS 3)
       <2 (TWO-VALS 3 7)
     <1 (ACL2_*1*_ACL2::TWO-VALS 3 7)
     (3 7)
     ACL2 !>

We now document all of the options that may appear in a trace spec.  A
trace spec with options is of the form

     (fn :kwd1 val1 :kwd2 val2 ... :kwdn valn)

and here we document each legal keyword :kwdi and corresponding expected
value vali.

:cond, :entry, and :exit

*Introduction*.  For each of these three options, the value is a
(user-level) term, except that for :entry and :exit the value can be of
the form (:fmt u), where u is a user-level term.  We skip this latter
case for now and return to it later.  Then the indicated term is
evaluated as indicated in the next paragraph, and if the :cond term is
omitted or evaluates to non-nil, then the value of the :entry term is
printed on entry and the value of the :exit term is printed on exit.  By
default, where :entry is omitted or is specified as nil, the value
printed for :entry is the list obtained by consing the calling function
symbol onto the list of actual parameters: in the notation described
below, this is (cons TRACED-FN ARGLIST).  Similarly, the default for
printing at the exit of the function call, i.e. where :exit is omitted
or is specified as nil, is (cons TRACED-FN VALUES) where VALUES is the
list of values returned as described below.

In the evaluations of the term described below upon a call of fn, each
formal parameter of the definition of fn will be bound to the
corresponding actual of the call, the variable ARGLIST will be bound to
the list of actuals, and the variable TRACED-FN will be bound to the
function being called (either fn or its executable counterpart function;
see above).  Additionally in the case of :exit, the variable VALUES
will be bound to the multiple values returned (thus, a one-element list
if mv is not used in the return).  Also for :exit, we bind VALUE to the
logical value returned, i.e., to the suitable list of values returned
in the mv case and otherwise to the single value returned.  So in the
mv case, VALUE is the same as VALUES, and otherwise VALUE is (car
VALUES).  Other than these variables and STATE, no other variable may
occur in the term, whose value must be a single non-stobj value, unless
there is an active trust tag (see DEFTTAG).

Now suppose fn is called.  First: If :cond is supplied and the result
of evaluating the :cond term is nil, then no tracing is done.
Otherwise tracing proceeds as follows.  First the :entry form is
evaluated, and the result is printed.  Then the call of fn is evaluated.
Finally the :exit term is evaluated and the result is printed.  As
indicated above, the default for the :entry term if omitted (or
explicitly the term nil) is (cons TRACED-FN ARGLIST), and the default
for the :exit term if omitted or explicitly the term nil is (cons
TRACED-FN VALUES).

Note that if the function has a formal named ARGLIST, then ARGLIST will
nevertheless refer to the entire list of formals, not the single formal
named ARGLIST; similarly for TRACED-FN, and additionally for VALUE and
VALUES in the case of :exit.

As mentioned above, for each of :entry and :exit, a value of nil
specifies the default behavior.  If you really want a value of nil, use
a non-nil form that evaluates to nil, for example (car nil).  However,
for :cond a value of nil means what it says: do not evaluate the :entry
or :exit forms.

Finally we discuss the case that the :entry or :exit term is of the
form (:fmt u).  In these cases, the term u is evaluated as described
above to produce a value, say msg, but instead of printing msg
directly, ACL2 calls fmt1 using the string "~@0" and the alist that
binds just character #\0 to msg.  The following example illustrates
this point, where fact is defined as above.  Also see FMT.
Note that (msg string . vals) produces a value suitable for a "~@"
directive to the fmt family of print functions.

     ACL2 !>(trace$
             (fact
              :entry (:fmt (msg "Tracing ~x0 on ~x1" traced-fn arglist))
              :exit (car values)))
      ((FACT :ENTRY (:FMT (MSG "Tracing ~x0 on ~x1" TRACED-FN ARGLIST))
             :EXIT (CAR VALUES)))
     ACL2 !>(fact 3)
     1> Tracing ACL2_*1*_ACL2::FACT on (3)
       2> Tracing FACT on (3)
         3> Tracing FACT on (2)
           4> Tracing FACT on (1)
             5> Tracing FACT on (0)
             <5 1
           <4 1
         <3 2
       <2 6
     <1 6
     6
     ACL2 !>

*ADVANCED OPTIONS* (alphabetical list)

:COMPILE

The tracing of fn installs a substitute definition of fn that prints
trace information.  If the :compile option is omitted or has value
:same, then the new definition will be compiled if and only if the
existing definition is already compiled.  Otherwise, the new definition
will be compiled exactly when the value of :compile is not nil.

:DEF, :MULTIPLICITY

Trace$ is intended primarily for functions defined in the ACL2 command
loop (see LP).  If you want to trace a function that defined in
raw Lisp, then you can use option :native (see below), but then many
other trace$ options will not be available to you, and you may need to
supply additional options, as described below.

ACL2's trace$ mechanism often needs to know the number of outputs of a
traced function, in the sense of mv.  If you trace a function that was
not defined inside the ACL2 loop (hence you are using the :native
option), or if you provide an alternative definition using option :def
(see below) and the new definition changes the number of values
returned, then a natural number value for :multiplicity informs the
trace utility of the number of expected outputs of the function being
traced.  In the case that :native is supplied, the effect of a non-nil
:multiplicity value depends on whether or not ACL2 uses the built-in
Lisp mechanism for returning multiple values (see MV).  As of
March 2009 (and through Version_3.5) such Lisps include only CCL
(OpenMCL) and threaded SBCL, and for these, :multiplicity is ignored
with :native.  For the other Lisps, the :multiplicity value is to
generate a suitable :exit form; so in this case, the underlying Lisp
needs to support the :exit keyword in its native trace.  (This is the
case for GCL and Allegro CL, as well as CCL (OpenMCL), because these
native traces have been modified for ACL2.)

A useful option for raw-Lisp functions, which can even be useful for
ACL2 functions, is to supply a definition as the value of :def.  Note
that this definition should be like a defun form, but without the
leading defun symbol; and it should define the function symbol being
traced, with the same formal parameter list.  However, tracing of the
so-called "executable counterpart" of a function (sometimes referred to
as the "*1* function", for evaluation in the ACL2 loop; see
Guards for related discussion) is not sensitive to the :def option;
rather, if a function has an executable counterpart then that
executable counterpart is traced.

:EVISC-TUPLE

The printing described above is, by default, done using the current
default trace evisc-tuple, which can be set using set-trace-evisc-tuple
(for the shape of this tuple, see EVISC-TUPLE); see
SET-TRACE-EVISC-TUPLE.  This tuple is based by default on the raw
Lisp variables *print-level* and *print-length*, and will hide the ACL2
world and handle stobjs appropriately.  You may override this default
by supplying an evisc tuple with the :evisc-tuple argument in your
trace spec.  Be careful to supply a valid evisc-tuple, or you may get a
raw Lisp error!

A special value, :print, is useful if you are doing system hacking that
can produce objects that are not valid ACL2 objects, such as raw Lisp
arrays or objects in supporting packages not visible in the ACL2
read-eval-print loop.  If you supply :evisc-tuple :print, then the
printing described above will be done with raw Lisp printing rather
than ACL2 printing: specifically, with (format *trace-output* "s%" x),
where x is the value to be printed.

A second special value for :evisc-tuple, :no-print, avoids printing the
values of the :entry and :exit forms (or their defaults, if not
specified).  This option is of use for side effects; for an example see
books/misc/wet.lisp.

Note that if :evisc-tuple X is supplied, then the form X will be
evaluated before the function body is entered.  You can thus pull some
tricks to print extra information before the :entry form is evaluated,
for example as follows for a factorial function, fact.

     ACL2 !>(trace$ (fact :evisc-tuple
                          (prog2$ (cw "~|**** HERE IS CW ****~|")
                                  nil)))
      ((FACT :EVISC-TUPLE (PROG2$ (CW "~|**** HERE IS CW ****~|")
                                  NIL)))
     ACL2 !>(fact 3)
     **** HERE IS CW ****
     1> (ACL2_*1*_ACL2::FACT 3)
     **** HERE IS CW ****
       2> (ACL2_*1*_ACL2::FACT 2)
     **** HERE IS CW ****
         3> (ACL2_*1*_ACL2::FACT 1)
     **** HERE IS CW ****
           4> (ACL2_*1*_ACL2::FACT 0)
           <4 (ACL2_*1*_ACL2::FACT 1)
         <3 (ACL2_*1*_ACL2::FACT 1)
       <2 (ACL2_*1*_ACL2::FACT 2)
     <1 (ACL2_*1*_ACL2::FACT 6)
     6
     ACL2 !>

:FORMALS

Normally ACL2 can figure out the formals for a given function.  This is
always the case for functions defined in the ACL2 command loop and when
option :def is supplied.  If neither of these cases applies then you can
still trace a function (even without using the :native option) by
supplying option :notinline :fncall, but you will still need to supply
the list of formal parameters.  The value of the :formals option should
be the list of formals in this case.

:HIDE

The default value for this advanced option is t, which causes stobjs
and the logical world to be printed as single symbols, along with
certain large structures of interest to developers (rewrite contants,
enabled structures, and event and command index structures).  If
however the value nil is supplied, then this default behavior is
defeated.  In that case, you can still arrange to print the logical
world as a symbol and to print stobjs without breaking the trace
printing: see SET-TRACE-EVISC-TUPLE for how to do this
globally, or similarly use the :evisc-tuple option to trace$ to do this
with a single trace spec.  Note however that with value nil specified
for :hide, such use of an evisc-tuple will not deal properly with local
stobjs (see WITH-LOCAL-STOBJ) or the aforementioned large
structures other than the logical world.

:NATIVE

If :native is supplied with a non-nil value, then the trace spec is
passed to the native Lisp trace (after removing the :native option).  A
trust tag (see DEFTTAG) is required in order to use this
option, because no syntactic check is made on the :cond, :entry, or
:exit forms - arbitrary raw Lisp may occur in them!

Note that by "native Lisp trace" we mean the currently installed trace.
As discussed briefly elsewhere (see TRACE), ACL2 has modified
that trace to be more useful if the underlying host Lisp is GCL,
Allegro CL, or CCL (OpenMCL).  If you need the original trace utility
supplied for those Lisps, quit the ACL2 loop with :q and call old-trace
and old-untrace in raw Lisp where you would otherwise call trace and
untrace.  Note that the original trace utility supplied with a given
Lisp will not hide the ACL2 logical world or give special treatment to
stobjs.

It is important to understand that if :native is specified, then all
other options are interpreted by the native Lisp trace.  For example,
that trace probably has no understanding of the use of :fmt described
above for :entry or :exit.  Indeed, the native trace may not even accept
any of :cond, :entry or :exit, let alone any of the advanced options!

:NOTINLINE

By default, a new definition installed by trace$ will include a
notinline declaration so that recursive calls will always be traced.  To
avoid this declaration, supply value nil.

A special value for :notinline, :fncall, will cause the traced function
to call its original definition.  Without this special value, the new
installed definition for the traced function will include the body of
the original definition.  This :fncall behavior is the default for
functions whose definitions are built into ACL2.

The legal values for :notinline are t (the default), nil, and :fncall.

*Remarks*.

(1) If some of the given trace specs have errors, then trace$ will
generally will print error messages for those but will still process
those that do not have errors.  The value returned will indicate the
trace specs that were processed successfully.

(2) If you certify or include a book that redundantly defines a
function that is currently traced, then the trace may be removed.

UNTRACE$    untrace functions

     Examples:
     (untrace$)         ; untrace all functions previously
                        ; traced (e.g. with trace$ or trace!)
     (untrace$ foo bar) ; as above, except only untrace foo and bar

     General Forms:
     (untrace$)                 ; untrace all (as noted above)
     (untrace$ fn1 fn2 ... fnk) ; untrace the indicated functions

where the fni were previously traced (e.g. with trace$ or trace!).

Untrace$ undoes the effect of trace$.  See TRACE$.  The value
returned by untrace$ gives the list of functions for which tracing is
being removed.

WET    evaluate a form and print subsequent error trace

The acronym "wet" stands for "with-error-trace".  Wet provides a
convenient way to obtain a backtrace when evaluation causes a guard
violation or other error.

The basic idea is that (wet form) evaluates form and, if there is an
error, shows a backtrace of calls that led to that error.  Note however
that by default only calls of user-defined (not built-in) functions
"supporting" form in the following sense will show up in the backtrace:
those that occur in the macroexpansion of form or (recursively) support
any of those functions.  So for example, since (make-event form)
macroexpands to (make-event-fn (quote form) ...), calls of functions
occurring in form will likely not show up in the backtrace by default.
The option :fns all overrides this default, with potential loss of
speed; more on this below.

The following example explains the use of wet.  First, submit the
following three definitions:

     (defun foo (x) (declare (xargs :guard (consp x))) (car x))
     (defun bar (x) (foo (cdr x)))
     (defun g (x) (bar (cdr x)))

Now imagine you have obtained the following guard violation:

     ACL2 !>(g '(3 4))

     ACL2 Error in TOP-LEVEL:  The guard for the function call (FOO X),
     which is (CONSP X), is violated by the arguments in the call (FOO NIL).
     To debug see :DOC print-gv, see :DOC trace, and see :DOC wet.  See
     :DOC set-guard-checking for information about suppressing this check
     with (set-guard-checking :none), as recommended for new users.

     ACL2 !>

With wet, you can get a backtrace of user-defined functions.  The
package prefixes shown below, ACL2_*1*_, indicate that the executable
(logical) counterparts of the corresponding raw Lisp functions are
being called; see GUARD.  Don't forget to start with
(include-book "misc/wet" :dir :system).

     ACL2 !>(wet (g '(3 4)))
     ; Fast loading /projects/acl2/devel/books/misc/wet.fasl

     TTAG NOTE: Adding ttag :TRACE! from the top level loop.

     ACL2 Error in WET:  The guard for the function call (FOO X), which
     is (CONSP X), is violated by the arguments in the call (FOO NIL).
     To debug see :DOC print-gv, see :DOC trace, and see :DOC wet.  See
     :DOC set-guard-checking for information about suppressing this check
     with (set-guard-checking :none), as recommended for new users.

     Backtrace stack:
     ----------------
     1. (ACL2_*1*_ACL2::FOO NIL)
     2. (ACL2_*1*_ACL2::BAR (4))
     3. (ACL2_*1*_ACL2::G (3 4))

     ACL2 !>

By default, large structures are hidden during the printing of the
backtrace stack.  But you can supply a value for keyword argument
:evisc-tuple to modify the printing: nil to avoid hiding, else a
suitable evisc-tuple, as shown below (see EVISC-TUPLE).

     ACL2 !>(wet (g '(3 4)) :evisc-tuple (evisc-tuple 1 1 nil nil))
     ; Fast loading /projects/acl2/devel/books/misc/wet.fasl

     TTAG NOTE: Adding ttag :TRACE! from the top level loop.

     ACL2 Error in WET:  The guard for the function call (FOO X), which
     is (CONSP X), is violated by the arguments in the call (FOO NIL).
     To debug see :DOC print-gv, see :DOC trace, and see :DOC wet.  See
     :DOC set-guard-checking for information about suppressing this check
     with (set-guard-checking :none), as recommended for new users.

     Backtrace stack:
     ----------------
     1. (ACL2_*1*_ACL2::FOO ...)
     2. (ACL2_*1*_ACL2::BAR ...)
     3. (ACL2_*1*_ACL2::G ...)

     ACL2 !>

For a backtrace as a data object, evaluate the form (@ wet-stack).  But
note that this object may not be a legal ACL2 value, for example
because of the "*1*" symbols shown above.

     General Form:
     (wet form           ; an arbitrary form
          :book bk-form  ; optional, not evaluated
          ;;; the rest are optional and evaluated:
          :evisc-tuple e ; an evisc-tuple
          :fns fns       ; :all, or a list of functions to show in a backtrace
          :compile c     ; :same, t, or nil; default :same (nil if :fns supplied)

Form is evaluated.  If there is an error, a backtrace stack is printed
to the standard output (*standard-co*), containing (by default) the
user-defined function calls made before the error.  Such printing is
controlled by the :evisc-tuple if supplied; otherwise, hiding of large
structures will occur.  (Technical detail: by default the global
abbrev-evisc-tuple is used, if bound; see SET-EVISC-TUPLE.

The :fns option.  As mentioned above, by default the wet backtrace
shows user-defined functions "supporting" the form being evaluated.
This default can be overridden by supplying an explicit list, fns, of
functions, using option :fns fns; these will then be the functions whose
calls are eligible for inclusion in the backtrace.  The special value
:fns :all will allow all user-defined function calls in the backtrace.

The :compile option.  Wet uses the trace$ utility to modify the
definitions of affected functions so that they can record information
for the backtrace.  As described above, these affected functions are
those "supporting" the form unless specified by the :fns option.  As is
the case for trace$ -- see TRACE$ -- the new definitions of
these affected functions may or may not be compiled.  For trace$ and for
wet, the default is to compile the new definition if and only if the
original definition was compiled, except: For wet, if option :fns :all
is provided, then the default is not to compile the affected
definitions.  And for trace$ and wet, the :compile option overrides the
default, to specify what will be compiled: value :same to compile each
affected function if and only if its original definition was compiled,
value t to compile all affected functions, and value nil to skip
compilation.

The :book option.  Wet actually works by temporarily including a
distributed book,

     (include-book "misc/wet" :dir :system)

and then passing its arguments to macro wet!, defined in that book.
The keyword argument :book allows you to specify a different book that
defines a macro wet! to which to pass its arguments.  If the value of
:book is a string, then the book named by that string is temporarily
included using include-book: (include-book "bk").  Otherwise :book
should be a list of arguments, to be provided (unevaluated) to
include-book, for example ("my-wet" :dir :my-utils).  Thus you can
experiment by copying distributed book books/misc/wet.lisp to your own
directory and making modifications to the copy.  If you make changes, we
invite you to share them with the ACL2 community (see BOOKS).
Note that you can also supply :book nil, in which case the definition
of wet! in your current session will be used without including a book.

Also see TRACE$ for a general tracing utility.  As mentioned
above, wet is implemented using trace$.  Wet actually first applies
untrace$; upon completion, wet then applies trace$ to re-trace any
functions that it had untraced, using their original trace specs.