/usr/share/acl2-8.0dfsg/books/misc/file-io.lisp is in acl2-books-source 8.0dfsg-1.
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 | ; 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")
(include-book "xdoc/top" :dir :system)
(defxdoc write-list
:parents (io)
:short "Write a list to a file"
:long "@({
Example Forms:
(write-list '(a b c) \"foo\" 'top-level state)
(write-list '(a b c) \"foo\" 'top-level state :quiet t)
General Form:
(write-list list x ctx state &key :quiet val)
})
<p>where all arguments are evaluated and @('state') must literally be the ACL2
@(see state), @('STATE'). @('List') is a true-list; @('x') is a filename or a
list of length 1 containing a filename; and @('ctx') is a context (see @(see
ctx)). By default or if :quiet is nil, a message of the form @('\"Writing
file [x]\"') is printed to @(see standard-co); otherwise, no such message is
printed.</p>")
(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 quietp)
`(let ((quietp ,quietp))
(if (not (stringp fname))
(er soft ctx
"The filename argument of write-list must evaluate to a string, ~
but it has evaluated to ~x0. See :DOC write-list."
fname)
(mv-let (channel state)
,(if bangp
'(open-output-channel! fname :character state)
'(open-output-channel fname :character state))
(if channel
(mv-let
(col state)
(cond (quietp (mv 0 state))
(t (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 quietp)
(write-list-body-fn bangp quietp))
(defun write-list-fn (list fname ctx state quiet)
(if quiet
(write-list-body nil t)
(write-list-body nil nil)))
; Pretty-print the given list of forms to file fname, except that strings are
; printed without any formatting.
(defmacro write-list (list fname ctx state &key quiet)
(declare (xargs :guard (eq state 'state)))
`(write-list-fn ,list ,fname ,ctx ,state ,quiet))
; (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:
(defmacro write-list-downcase (list fname ctx state &key quiet)
(declare (xargs :guard (eq state 'state)))
`(downcase (write-list ,list ,fname ,ctx ,state :quiet ,quiet)))
|