/usr/share/acl2-7.2dfsg/books/hacking/evalable-ld-printing.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 | ; evalable-ld-printing.lisp - Print LD results in "evalable" way, as provided
; by "evalable-printing" book.
;
; To activate, include this book and assign a non-nil value to the state
; global EVALABLE-LD-PRINTINGP, as in
; (assign evalable-ld-printingp t)
;
; If ld-post-eval-print is :command-conventions, we do not make error
; triple output evalable. To make error triple output looks especially
; unique, I recommend making it look like a comment:
; (assign triple-print-prefix "; ")
;
; Requires a trust tag :evalable-ld-printing
;
; Peter C. Dillinger, Northeastern University, 2008
(in-package "ACL2")
(program)
(set-state-ok t)
(defun evalable-ld-printingp (state)
(and (f-boundp-global 'evalable-ld-printingp state)
(f-get-global 'evalable-ld-printingp state)))
(include-book "misc/evalable-printing" :dir :system)
(defttag :evalable-ld-printing)
(include-book "hacker")
(progn+all-ttags-allowed
(include-book "defcode" :ttags ((defcode)))
(include-book "subsumption")
(include-book "raw")
)
(subsume-ttags-since-defttag)
(modify-raw-defun acl2::ld-print-results original-ld-print-results (trans-ans state)
(if (or (not (acl2::live-state-p state))
(acl2::output-in-infixp 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)))
#-(or gcl cmu sbcl lispworks)
(when (acl2::raw-mode-p state)
(acl2::format (acl2::get-output-stream-from-channel output-channel) "~&"))
(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
(acl2::princ$ (if (stringp (f-get-global 'acl2::triple-print-prefix state))
(f-get-global 'acl2::triple-print-prefix state)
"")
output-channel state)
(let ((col (if (stringp (f-get-global 'acl2::triple-print-prefix state))
(length (f-get-global 'acl2::triple-print-prefix state))
0)))
(acl2::ppr (cadr valx) col output-channel state nil))
(acl2::newline output-channel state)))))
((equal (length stobjs-out) 1)
(pprogn
(acl2::ppr (car (make-evalable-with-stobjs (list valx) stobjs-out)) 0 output-channel state nil)
(acl2::newline output-channel state)))
(t
(pprogn
(acl2::ppr (cons 'mv (make-evalable-with-stobjs valx stobjs-out)) 0 output-channel state nil)
(acl2::newline output-channel state)))))))
|