akcl-acl2-trace - ACL2 Book

other

(cond ((null (macro-function 'old-trace)) (setf (macro-function 'old-trace) (macro-function 'trace))))

other

(cond ((null (macro-function 'old-untrace)) (setf (macro-function 'old-untrace)
      (macro-function 'untrace))))

tracemacro

(defmacro trace
  (&rest fns)
  (let (acl2-fns non-acl2-fns all-fns)
    (loop for
      fn
      in
      fns
      do
      (if (function-symbolp (cond ((symbolp fn) fn)
            ((and (consp fn) (symbolp (car fn))) (car fn))
            (t (error "Not a symbol or a cons of a symbol: ~s" fn)))
          (w *the-live-state*))
        (push fn acl2-fns)
        (push fn non-acl2-fns)))
    (cons 'old-trace
      (progn (setq acl2-fns
          (loop for
            x
            in
            acl2-fns
            collect
            (cond ((symbolp x) (list x x))
              (t (list* (car x) (car x) (cdr x))))))
        (dolist (x acl2-fns)
          (push (cons (*1*-symbol (car x)) (cdr x)) acl2-fns))
        (dolist (fn acl2-fns)
          (push (progn (cond ((member :break (cdr fn)) (interface-er "Use of :break is not permitted in ~
                                            TRACE.  Consider :entry (progn ~
                                            (break$) arglist) instead.")))
              (cons (car fn)
                (trace-fix-cond (trace-fix-entry (car fn)
                    (trace-fix-exit (car fn) (cadr fn) (cddr fn))))))
            all-fns))
        (dolist (fn non-acl2-fns)
          (let* ((spec (if (symbolp fn)
                 (list fn)
                 fn)) (fn (car spec)))
            (push (cons fn
                (trace-fix-entry-raw fn (trace-fix-exit-raw fn (cdr spec))))
              all-fns)))
        all-fns))))

untracemacro

(defmacro untrace
  (&rest fns)
  (cons 'old-untrace
    (let ((ans fns))
      (dolist (fn fns) (push (*1*-symbol fn) ans))
      ans)))

trace-ppr-gclfunction

(defun trace-ppr-gcl
  (direction x &aux (state *the-live-state*))
  (let ((*inside-trace$* t))
    (declare (special *inside-trace$* *trace-level*))
    (cond ((eq direction :in) (incf *trace-level*)))
    (let ((trace-evisc-tuple (trace-evisc-tuple)) (x (trace-hide-world-and-state x)))
      (ppr (eviscerate-top x
          (cadr trace-evisc-tuple)
          (caddr trace-evisc-tuple)
          (car trace-evisc-tuple)
          (table-alist 'evisc-table (w state))
          (car (cddddr trace-evisc-tuple))
          state)
        (+ 2 (first-trace-printing-column))
        (f-get-global 'trace-co state)
        state
        t))
    (cond ((eq direction :out) (decf *trace-level*)))
    '>))

trace-fix-entry-rawfunction

(defun trace-fix-entry-raw
  (name l)
  (cond ((null l) (list :entry `(cons ',NAME (trace-hide-world-and-state arglist))))
    ((or (atom l) (and (cdr l) (atom (cdr l)))) (error "A trace spec must be a true-list, but yours ends in ~s."
        l))
    ((eq (car l) :entry) (list* :entry `(cons ',NAME
          (trace-hide-world-and-state (let ((arglist arglist))
              ,(CADR L))))
        (cddr l)))
    (t (list* (car l) (cadr l) (trace-fix-entry-raw name (cddr l))))))

trace-fix-entryfunction

(defun trace-fix-entry
  (name l)
  (cond ((endp l) (list :entry `(trace-ppr-gcl :in (cons ',NAME arglist))))
    ((eq (car l) :entry) (list* :entry `(trace-ppr-gcl :in (cons ',NAME
            (let ((arglist arglist))
              ,(CADR L))))
        (cddr l)))
    (t (list* (car l) (cadr l) (trace-fix-entry name (cddr l))))))

trace-valuesfunction

(defun trace-values (name) (declare (ignore name)) 'values)

trace-fix-exit-rawfunction

(defun trace-fix-exit-raw
  (name l)
  (cond ((endp l) (list :exit `(cons ',NAME
          (trace-hide-world-and-state ,(TRACE-VALUES NAME)))))
    ((eq (car l) :exit) (list* :exit `(cons ',NAME
          (trace-hide-world-and-state (let ((arglist arglist))
              (declare (ignorable arglist))
              ,(CADR L))))
        (cddr l)))
    (t (list* (car l) (cadr l) (trace-fix-exit-raw name (cddr l))))))

trace-fix-exitfunction

(defun trace-fix-exit
  (name original-name l &aux (state *the-live-state*))
  (cond ((endp l) (list :exit (protect-mv `(trace-ppr-gcl :out (cons ',NAME ,(TRACE-VALUES ORIGINAL-NAME)))
          (trace-multiplicity original-name state))))
    ((eq (car l) :exit) (list* :exit (protect-mv `(trace-ppr-gcl :out (cons ',NAME
              (let* ((values ,(TRACE-VALUES ORIGINAL-NAME)) (arglist arglist))
                (declare (ignorable values arglist))
                ,(CADR L))))
          (trace-multiplicity original-name state))
        (cddr l)))
    (t (list* (car l)
        (cadr l)
        (trace-fix-exit name original-name (cddr l))))))

trace-fix-condfunction

(defun trace-fix-cond
  (trace-spec)
  (if (member-eq :cond trace-spec)
    (loop for
      tail
      on
      trace-spec
      append
      (if (eq (car tail) :cond)
        (prog1 (list :cond `(let ((arglist arglist))
              ,(CADR TAIL)))
          (setq tail (cdr tail)))
        (list (car tail))))
    trace-spec))