TRACE$

trace the indicated functions
Major Section:  TRACE

Example:
(trace$ foo bar)

General Form: (trace$ fn1 fn2 ... fnk)

where the fni are defined or even constrained functions. More generally, the fni may be any arguments allowed by the underlying Lisp trace, but if any fni is not a symbol then you will probably want to use trace! instead.

See untrace$ for how to undo the effect of trace$.

Basically, trace$ calls on the underlying Lisp to trace the specified functions as well as their executable-counterparts. However, for GCL, Allegro CL, and OpenMCL, the underlying Lisp trace routines are modified before an image is saved in order to hide the ACL2 world and other large data structures and provide slightly prettier output.

Recursive calls of functions whose guards have not been verified will not generally be traced. If you want to see traces for corresponding evaluations in raw Lisp, which will generally show recursive calls (except, in some Lisp implementations, for compiled tail recursive functions), then you can quit into raw Lisp (:q) and execute your form there. Alternatively, you can avoid executable-counterpart functions by using :set-raw-mode to enter a raw Lisp version of the ACL2 loop; see set-raw-mode and see set-raw-mode-on!.

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

Also see wet (``with-error-trace'') for a different way that ACL2 takes advantage of the underlying Lisp, namely to provide a backtrace when there is an error.

Note that from a logical perspective all trace printing is a fiction. For a related fiction, see cw. Trace$ returns nil.

The following example will give an idea of the options available other than just (trace$ fn1 fn2 ... fnk). It works about as shown in Allegro CL and GCL, but in OpenMCL the recursive calls are omitted unless you escape into raw Lisp and redefine fact with (declare (notinline fact)).

ACL2 !>(defun fact (n)
         (declare (xargs :guard (natp n) :mode :program))
         (if (zp n)
             1
           (* n (fact (1- n)))))

Summary Form: ( DEFUN FACT ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) FACT ACL2 !>(trace$ (fact :entry (car arglist) :exit values)) NIL ACL2 !>(fact 5) 1> (ACL2_*1*_ACL2::FACT . 5) 2> (FACT . 5) 3> (FACT . 4) 4> (FACT . 3) 5> (FACT . 2) 6> (FACT . 1) 7> (FACT . 0) <7 (FACT 1) <6 (FACT 1) <5 (FACT 2) <4 (FACT 6) <3 (FACT 24) <2 (FACT 120) <1 (ACL2_*1*_ACL2::FACT 120) 120 ACL2 !>

Here is another example.
ACL2 !>(defun fact2 (n acc)
         (declare (xargs :guard (and (natp n) (natp acc))))
         (if (zp n)
             (mv acc (* 2 acc))
           (fact2 (1- n) (* n acc))))

The admission of FACT2 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 FACT2 is described by the theorem (AND (CONSP (FACT2 N ACC)) (TRUE-LISTP (FACT2 N ACC))). We used primitive type reasoning.

(FACT2 * *) => (MV * *).

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

Summary Form: ( DEFUN FACT2 ...) Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER) (: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) FACT2 ACL2 !>(trace$ (fact2 :entry (list 'my-entry (car arglist)) :exit (list 'my-second-value (cadr values)))) NIL ACL2 !>(fact2 6 1)

1> (ACL2_*1*_ACL2::FACT2 MY-ENTRY 6)> 2> (FACT2 MY-ENTRY 6)> 3> (FACT2 MY-ENTRY 5)> 4> (FACT2 MY-ENTRY 4)> 5> (FACT2 MY-ENTRY 3)> 6> (FACT2 MY-ENTRY 2)> 7> (FACT2 MY-ENTRY 1)> 8> (FACT2 MY-ENTRY 0)> <8 (FACT2 MY-SECOND-VALUE 1440)> <7 (FACT2 MY-SECOND-VALUE 1440)> <6 (FACT2 MY-SECOND-VALUE 1440)> <5 (FACT2 MY-SECOND-VALUE 1440)> <4 (FACT2 MY-SECOND-VALUE 1440)> <3 (FACT2 MY-SECOND-VALUE 1440)> <2 (FACT2 MY-SECOND-VALUE 1440)> <1 (ACL2_*1*_ACL2::FACT2 MY-SECOND-VALUE 1440)> (720 1440) ACL2 !>(trace$ (fact2 :entry (list 'my-args-reversed (list (cadr arglist) (car arglist))) :exit (list 'values-reversed (cadr values) (car values)))) NIL ACL2 !>(fact2 6 1)

1> (ACL2_*1*_ACL2::FACT2 MY-ARGS-REVERSED (1 6))> 2> (FACT2 MY-ARGS-REVERSED (1 6))> 3> (FACT2 MY-ARGS-REVERSED (6 5))> 4> (FACT2 MY-ARGS-REVERSED (30 4))> 5> (FACT2 MY-ARGS-REVERSED (120 3))> 6> (FACT2 MY-ARGS-REVERSED (360 2))> 7> (FACT2 MY-ARGS-REVERSED (720 1))> 8> (FACT2 MY-ARGS-REVERSED (720 0))> <8 (FACT2 VALUES-REVERSED 1440 720)> <7 (FACT2 VALUES-REVERSED 1440 720)> <6 (FACT2 VALUES-REVERSED 1440 720)> <5 (FACT2 VALUES-REVERSED 1440 720)> <4 (FACT2 VALUES-REVERSED 1440 720)> <3 (FACT2 VALUES-REVERSED 1440 720)> <2 (FACT2 VALUES-REVERSED 1440 720)> <1 (ACL2_*1*_ACL2::FACT2 VALUES-REVERSED 1440 720)> (720 1440) ACL2 !>