/usr/share/acl2-7.2dfsg/books/misc/trace-star.lisp is in acl2-books-source 7.2dfsg-3.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
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 | ; trace-star.lisp - A beginner-friendly variant of trace$.
;
; Peter C. Dillinger, Northeastern University, 2008
; Based on code from Matt Kaufmann
(in-package "ACL2")
(include-book "xdoc/top" :dir :system)
(program)
(set-state-ok t)
(include-book "evalable-printing")
(defun trace*-entry (fn)
`(:fmt
(msg "~@1~y2"
(first-trace-printing-column state)
(cond ((< 1 (@ trace-level))
"")
((not (eq ':none (@ acl2::guard-checking-on)))
"!! Warning: guard-checking is not :none, so trace !!~|~t0~
!! output could be misleading or appear incorrect. !!~|~t0~
!! (see :DOC set-guard-checking) !!~|~t0")
((getprop ',fn 'predefined nil 'current-acl2-world (w state))
"!! Warning: tracing a built-in function, so trace !!~|~t0~
!! output could be misleading or appear incorrect. !!~|~t0~
!! (Consider writing & using a wrapper function.) !!~|~t0")
(t ""))
(cons ',fn (make-evalable-with-stobjs
acl2::arglist
(getprop ',fn 'stobjs-in nil 'current-acl2-world (w state)))))))
(defun trace*-exit (fn)
`(:fmt (msg "~y2~|~t0= ~y1"
(max (- (first-trace-printing-column state) 2) 0)
(let ((stobjs-out (getprop ',fn 'stobjs-out '(nil) 'current-acl2-world (w state))))
(if (and (consp stobjs-out)
(endp (cdr stobjs-out)))
(car (make-evalable-with-stobjs values stobjs-out))
(cons 'mv
(make-evalable-with-stobjs values stobjs-out))))
(cons ',fn (make-evalable-with-stobjs
acl2::arglist
(getprop ',fn 'stobjs-in nil 'current-acl2-world (w state)))))))
(defun trace*-modify1 (ctx trace-spec)
(cond
((and (consp trace-spec)
(symbolp (car trace-spec))
(keyword-value-listp (cdr trace-spec)))
(let ((fn (car trace-spec)))
(append trace-spec
;; some defaults:
(list :entry (trace*-entry fn)
:exit (trace*-exit fn)
:hide nil
:evisc-tuple '(list (acl2::trace-evisceration-alist state)
nil nil nil)))))
((symbolp trace-spec)
(trace*-modify1 ctx (list trace-spec)))
(t (er hard ctx
"A trace spec must be a symbol or a symbol consed onto an alternating list ~
of the form (:kwd1 val1 :kwd2 val2 ...). The trace spec ~x0 is thus ~
illegal. See :DOC trace$."
trace-spec))))
(defun trace*-modify (ctx trace-specs)
(cond ((endp trace-specs)
nil)
(t (cons (trace*-modify1 ctx (car trace-specs))
(trace*-modify ctx (cdr trace-specs))))))
(defxdoc trace*
:parents (trace$)
:short "@('Trace*') is a beginner-friendly variant of @(see trace$), the ACL2
tracing utility."
:long "<p>See @(see trace$) for more documentation and advanced
functionality.</p>
<p>@('Trace*') should be used with @(':set-guard-checking :none') and should
not be used to trace built-in functions.</p>
<p>The log below illustrates the differences between @('trace*') and
@('trace$'):</p>
@({
ACL2 p>
(defun app (x y)
(if (endp x)
y
(cons (car x) (app (cdr x) y))))
...
APP
ACL2 p>(trace$ app)
((APP))
ACL2 p>(app (list 1 2) (list 3))
1> (ACL2_*1*_ACL2::APP (1 2) (3))
2> (ACL2_*1*_ACL2::APP (2) (3))
3> (ACL2_*1*_ACL2::APP NIL (3))
<3 (ACL2_*1*_ACL2::APP (3))
<2 (ACL2_*1*_ACL2::APP (2 3))
<1 (ACL2_*1*_ACL2::APP (1 2 3))
(1 2 3)
ACL2 p>(trace* app)
(APP)
ACL2 p>(app (list 1 2) (list 3))
1> (APP (LIST 1 2) (LIST 3))
2> (APP (LIST 2) (LIST 3))
3> (APP NIL (LIST 3))
<3 (APP NIL (LIST 3))
= (LIST 3)
<2 (APP (LIST 2) (LIST 3))
= (LIST 2 3)
<1 (APP (LIST 1 2) (LIST 3))
= (LIST 1 2 3)
(1 2 3)
ACL2 p>
})")
(defmacro trace* (&rest trace-specs)
`(er-progn (trace$ ,@(trace*-modify 'trace* trace-specs))
(value ',trace-specs)))
#| test
(logic)
(set-guard-checking :none)
(defun app (x y)
(if (endp x)
y
(cons (car x) (app (cdr x) y))))
(trace$ app)
(app (list 1 2) (list 3))
(trace* app)
(app (list 1 2) (list 3))
(defun fact (n)
(if (zp n)
1
(* n (fact (1- n)))))
(trace$ fact)
(fact 3)
(trace* fact)
(fact 3)
;;; Modification by Matt K. for after ACL2 3.6.1 for early loading of compiled
;;; files (see books/misc/evalable-printing.lisp):
(trace* get-evalable-printing-abstractions)
(get-evalable-printing-abstractions state)
;|#
|