TRACE*

trace function evaluations
Major Section:  TRACE

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 >