TRACE!

Major Section:  TRACE

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

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

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)

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