Filtering...

evalable-ld-printing

books/hacking/evalable-ld-printing

Included Books

evalable-printing hacker
other
(in-package "ACL2")
other
(program)
other
(set-state-ok t)
evalable-ld-printingpfunction
(defun evalable-ld-printingp
  (state)
  (and (f-boundp-global 'evalable-ld-printingp state)
    (f-get-global 'evalable-ld-printingp state)))
include-book
(include-book "misc/evalable-printing" :dir :system)
other
(defttag :evalable-ld-printing)
include-book
(include-book "hacker")
other
(progn+all-ttags-allowed (include-book "defcode" :ttags ((defcode)))
  (include-book "subsumption")
  (include-book "raw"))
other
(subsume-ttags-since-defttag)
other
(modify-raw-defun ld-print-results
  original-ld-print-results
  (trans-ans state)
  (if (or (not (live-state-p state))
      (not (evalable-ld-printingp state)))
    (original-ld-print-results trans-ans state)
    (let* ((output-channel (standard-co state)) (flg (ld-post-eval-print state))
        (stobjs-out (car trans-ans))
        (valx (cdr trans-ans)))
      (cond ((null flg) state)
        ((and (eq flg :command-conventions)
           (equal (length stobjs-out) 3)
           (eq (car stobjs-out) nil)
           (eq (caddr stobjs-out) 'state)) (cond ((eq (cadr valx) :invisible) state)
            (t (pprogn (princ$ (if (stringp (f-get-global 'triple-print-prefix state))
                    (f-get-global 'triple-print-prefix state)
                    "")
                  output-channel
                  state)
                (let ((col (if (stringp (f-get-global 'triple-print-prefix state))
                       (length (f-get-global 'triple-print-prefix state))
                       0)))
                  (ppr (cadr valx) col output-channel state nil))
                (newline output-channel state)))))
        ((equal (length stobjs-out) 1) (pprogn (ppr (car (make-evalable-with-stobjs (list valx) stobjs-out))
              0
              output-channel
              state
              nil)
            (newline output-channel state)))
        (t (pprogn (ppr (cons 'mv (make-evalable-with-stobjs valx stobjs-out))
              0
              output-channel
              state
              nil)
            (newline output-channel state)))))))