/usr/share/acl2-7.2dfsg/books/misc/file-io.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 | ; Copyright (C) 2013, Regents of the University of Texas
; Written by Matt Kaufmann
; License: A 3-clause BSD license. See the LICENSE file distributed with ACL2.
; Utilities read-list and write-list:
; (Read-list fname ctx state) returns (mv nil lst state) where lst is the list
; of top-level forms in the file named fname. Except, if there is an error
; then (mv t nil state) is returned.
; (Write-list list fname ctx state) pretty-prints the given list of forms to
; file fname, except that strings are printed without any formatting.
; In each of the above, ctx is generally a symbol used in error messages that
; indicates the caller, e.g., 'top-level.
(in-package "ACL2")
(program)
(set-state-ok t)
(defun collect-objects (list channel state)
(mv-let (eofp obj state)
(read-object channel state)
(if eofp
(mv (reverse list) state)
(collect-objects (cons obj list) channel state))))
; Return (value result) where result is the list of top-level forms in file
; fname:
(defun read-list (fname ctx state)
(mv-let (channel state)
(open-input-channel fname :object state)
(if channel
(mv-let (result state)
(collect-objects () channel state)
(let ((state (close-input-channel channel state)))
(value result)))
(er soft ctx
"Unable to open file ~s0 for :object input."
fname))))
(defun pprint-object-or-string (obj channel state)
(if (stringp obj)
(princ$ obj channel state)
(mv-let (erp val state)
(state-global-let*
((write-for-read t))
(pprogn (ppr2 (ppr1 obj (print-base) (print-radix) 80 0 state t)
0 channel state t)
(value nil)))
(declare (ignore erp val))
state)))
(defun write-objects (list channel state)
(if (consp list)
(pprogn (pprint-object-or-string (car list) channel state)
(newline channel state)
(newline channel state)
(write-objects (cdr list) channel state))
state))
(defun write-list-body-fn (bangp)
`(mv-let (channel state)
,(if bangp
'(open-output-channel! fname :character state)
'(open-output-channel fname :character state))
(if channel
(mv-let
(col state)
(fmt1 "Writing file ~x0~%" (list (cons #\0 fname))
0 (standard-co state) state nil)
(declare (ignore col))
(let ((state (write-objects list channel state)))
(pprogn (close-output-channel channel state)
(value :invisible))))
(er soft ctx
"Unable to open file ~s0 for :character output."
fname))))
(defmacro write-list-body (bangp)
(write-list-body-fn bangp))
; Pretty-print the given list of forms to file fname, except that strings are
; printed without any formatting.
(defun write-list (list fname ctx state)
(write-list-body nil))
(defmacro write-list! (list fname ctx &optional ttag)
; A non-nil ttag must be supplied, of course, unless there is already an active
; ttag at the point where write-list! is called.
(let ((trans-eval-form `(trans-eval '(let ((list ,list)
(fname ,fname)
(ctx ,ctx))
,(write-list-body-fn t))
,ctx
state)))
`(er-progn ,(if ttag
`(progn (defttag ,ttag) (progn! ,trans-eval-form))
trans-eval-form)
(value :invisible))))
; (Downcase form) causes the execution of form but where printing is in
; :downcase mode. Form must return an error triple.
(defmacro downcase (form)
`(state-global-let*
((print-case :downcase set-print-case))
,form))
; Same as write-list above, but where printing is down in downcase mode:
(defun write-list-downcase (list fname ctx state)
(downcase (write-list list fname ctx state)))
|