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

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

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

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

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

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.

From a logical perspective all trace printing is a fiction.  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

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, but without using trace$ option :native, you will need to
supply the 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.  Note that 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 LD-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.

TRACE*    trace function evaluations

Trace* is a minor variant of trace$, the ACL2 tracing utility.  See
TRACE$ for detailed documentation.

The only difference between trace* and trace$ is that trace* provides
perhaps more pleasant output, as follows.  If a function is traced
without option :entry or :exit, then trace* avoids using the name of
the so-called "*1* function" (also known as "executable-counterpart
function" or "logic function").

The log below illustrates the difference when using :set-guard-checking
:none, which restricts execution to *1* functions.  Here we assume the
following definition.

     (defun fact (n)
       (if (zp n)
           1
         (* n (fact (1- n)))))

And here is the log promised above, first showing trace$ and then the
(prettier output from) trace*.

     ACL2 >(trace$ fact)
      ((FACT))
     ACL2 >(fact 3)
     1> (ACL2_*1*_ACL2::FACT 3)
       2> (ACL2_*1*_ACL2::FACT 2)
         3> (ACL2_*1*_ACL2::FACT 1)
           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 >(trace* fact)
      ((FACT :ENTRY (CONS 'FACT ARGLIST)
             :EXIT (CONS 'FACT VALUES)))
     ACL2 >(fact 3)
     1> (FACT 3)
       2> (FACT 2)
         3> (FACT 1)
           4> (FACT 0)
           <4 (FACT 1)
         <3 (FACT 1)
       <2 (FACT 2)
     <1 (FACT 6)
     6
     ACL2 >

UNTRACE$    untrace functions

     Examples:
     (untrace$)         ; untrace all functions previously
                        ; traced with trace$, 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 with trace$, 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.

     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 value of state
global 'user-default-evisc-tuple is used, if bound; see
LD-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.