1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
|
<html>
<head><title>TRACE$.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>TRACE$</h2>trace the indicated functions
<pre>Major Section: <a href="TRACE.html">TRACE</a>
</pre><p>
<pre>
Example:
(trace$ foo bar)
<p>
General Form:
(trace$ fn1 fn2 ... fnk)
</pre>
where the <code>fni</code> are defined or even constrained functions.<p>
see <a href="UNTRACE$.html">untrace$</a> for how to undo the effect of <code><a href="TRACE$.html">trace$</a></code>.<p>
Basically, <code>trace$</code> calls on the underlying Lisp to trace the specified
functions as well as their <code><a href="EXECUTABLE-COUNTERPART.html">executable-counterpart</a></code>s. 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.<p>
Recursive calls of functions whose <a href="GUARD.html">guard</a>s 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 (<code>:q</code>) and execute your form there.
Alternatively, you can avoid <a href="EXECUTABLE-COUNTERPART.html">executable-counterpart</a> functions by using
<code>:</code><code><a href="SET-RAW-MODE.html">set-raw-mode</a></code> to enter a raw Lisp version of the ACL2 loop;
see <a href="SET-RAW-MODE.html">set-raw-mode</a> and see <a href="SET-RAW-MODE-ON_bang_.html">set-raw-mode-on!</a>.<p>
Output from <code><a href="TRACE$.html">trace$</a></code> normally goes to the screen, i.e.,
<code><a href="STANDARD-CO.html">standard-co</a></code>. But it can be redirected to a file;
see <a href="OPEN-TRACE-FILE.html">open-trace-file</a>.<p>
Also see <a href="WET.html">wet</a> (``<code><a href="WITH-ERROR-TRACE.html">with-error-trace</a></code>'') for a different way that ACL2
takes advantage of the underlying Lisp, namely to provide a backtrace when
there is an error.<p>
Note that from a logical perspective all trace printing is a fiction. For a
related fiction, see <a href="CW.html">cw</a>. <code>Trace$</code> returns <code>nil</code>.<p>
The following example will give an idea of the options available other than
just <code>(trace$ fn1 fn2 ... fnk)</code>. 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 <code>fact</code> with <code>(declare (notinline fact))</code>.
<pre>
ACL2 !>(defun fact (n)
(declare (xargs :guard (natp n) :mode :program))
(if (zp n)
1
(* n (fact (1- n)))))<p>
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 !>
</pre>
Here is another example.
<pre>
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))))<p>
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.<p>
(FACT2 * *) => (MV * *).<p>
The guard conjecture for FACT2 is trivial to prove. FACT2 is compliant
with Common Lisp.<p>
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)<p>
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)<p>
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 !>
</pre>
<br><br><br><a href="acl2-doc.html"><img src="llogo.gif"></a> <a href="acl2-doc-index.html"><img src="index.gif"></a>
</body>
</html>
|
