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

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

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

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

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

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
(otherwise a hard error occurs).  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 a suitable trace of error functions.
Evaluate (trace$) after (break-on-error) if you want to see the
specific trace forms (which you can modify and then submit directly to
trace$, if you wish).  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 also at those times if
option :all is supplied.

NOTE: For technical reasons, you may see some error messages more than
once.

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

Finally, we remark that the use trace! can cause errors in situations
where tracing is automatically suspended and re-introduced.  This is
likely to be a rare occurrence, but consider the following example.

     (trace! (lexorder :native t :multiplicity 1))
     (certify-book "foo" 0 t)

If the certify-book causes compilation, you may see an error such as the
following.

     ACL2 Error in (CERTIFY-BOOK "foo" ...):  The keyword :NATIVE cannot
     be used in a trace spec unless there is an active trust tag.  The trace
     spec (LEXORDER :NATIVE T :MULTIPLICITY 1) is thus illegal.  Consider
     using trace! instead.  The complete list of keywords that require a
     trust tag for use in a trace spec is: (:NATIVE :DEF :MULTIPLICITY).

This error is harmless.  The function will appear, when calling
(trace$), to remain traced, but in fact there will be no tracing
behavior, so you may want to call untrace$ on the function symbol in
question.

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))))
     (trace$ (foo :native t))

     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.ccs.neu.edu/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.

Note that when trace$ is applied to a function without option :native,
that function's declarations and documentation are discarded.

Next, we introduce tracing with some examples.  After that, we provide
reference documentation for individual trace options allowed in a trace
spec.  Note that although our example focuses on user-defined
functions, trace$ can also be applied to built-in functions, though
perhaps only system hackers should take advantage of this observation.

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.  Note that 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: all of them except :multiplicity and :native itself
will be passed directly to the trace utility of the underlying Common
Lisp.

: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 nil is (cons TRACED-FN ARGLIST), and the default for the
:exit term if omitted or explicitly 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) or '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

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 the host Lisp.  In the case of Lisps for
which ACL2 uses the built-in Lisp mechanism for returning multiple
values (see MV), which are CCL and threaded SBCL as of June,
2010, :multiplicity is not needed and is ignored with :native t.  For
GCL and Allegro CL, :multiplicity is used to generate a suitable :exit
form if the :exit keyword was not already supplied.  For the other
Lisps, the :multiplicity value is treated essentially as 1 whether it
is supplied or not, because we do not know how to pass suitable
information based on this value to the host Lisp's built-in tracing
mechanism.

Note that even supplying a :multiplicity option does not change the
meaning of the variable values.  See the discussion of :native below.

A useful option can be to supply a definition as the value of :def.
(Again, note that if :native is used, then all options other than
:multiplicity are passed directly to the underlying Lisp; in particular,
:def will have no effect with :native except in the unlikely case that
the raw Lisp provides some sort of support for :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 t 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!
Moreover, if :native t is specified, then even a :multiplicity option
does not provide the meaning of the variable values that one might
desire.  In GCL for example, in the case of an mv return of a function
defined only in raw Lisp (not in ACL2), this variable will be bound to
a list containing only the first result.

: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 only in
the following cases:

     o for functions whose definitions are built into ACL2;

     o for functions that have been added (using a trust tag, an
     advanced feature, so most users can probably ignore this case) to
     either of the state global variables program-fns-with-raw-code or
     logic-fns-with-raw-code;

     o (`HONS' extension only; see HONS-AND-MEMOIZATION) for
     memoized functions.

The legal values for :notinline are t (the default for other than the
cases displayed above), nil, and :fncall.  (Except: For the 'HONS'
extension, only :fncall is legal.)

*Remarks*.

(1) If some of the given trace specs have errors, then trace$ will
generally 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 tracing behavior may disappear
if a compiled definition is installed for the function or its
in-the-logic (so-called `*1*') counterpart.

(3) Some predefined functions are called during tracing.  In order to
avoid infinite loops, such calls of traced predefined functions will be
made using the original predefined functions, not using their code
installed by trace$.

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.