The contents of a file (or part of it) as a string
When this macro is passed a valid filename (and the ACL2 state), it generally returns the contents of the file (or a specified part of
the file) as a string. Otherwise, it returns
Example Forms: (read-file-into-string "foo.lisp") (read-file-into-string "foo.lisp" :start 0 :bytes nil) ; same as above (read-file-into-string "foo.lisp" :start 20000 :bytes 10000) General Form: (read-file-into-string filename :start s :bytes b)
where
For examples, see community-books file
The result, when not
If
WARNING: A Lisp stream is created for the specified file, and is left open
until a call of
(prog2$ (and (= (+ position bytes) file-length) ; Then close the stream: (read-file-into-string filename :start file-length :bytes 1)) <more_code>)
End of warning.
This macro provides functionality that can be obtained through the usual
io routines provided by ACL2, as shown by the sequence of definitions
below. However, under-the-hood raw Lisp code provides an implementation that
not only is efficient, but also does not return state. Note that the
expansion of a call of this macro does take
The value of the constant
There are two checks to guarantee that
************ ABORTING from raw Lisp *********** ********** (see :DOC raw-lisp-error) ********** Error: Illegal consecutive reads from file "MY-FILE". See :DOC read-file-into-string. ***********************************************
The other check ensures that the write date of the file has not changed while the second call is in progress. For simplicity, ACL2 actually makes this check even for the first call. When the check fails the corresponding raw Lisp error is of the following form.
************ ABORTING from raw Lisp *********** ********** (see :DOC raw-lisp-error) ********** Error: Illegal attempt to call READ-FILE-INTO-STRING concurrently with some write to that file! See :DOC read-file-into-string. ***********************************************
The first of these errors can actually occur when the second read is
performed by open-input-channel of type
We close by showing the relevant ACL2 definitions in the logic, that is,
not including the special raw Lisp (under the hood) code in the definition of
Function:
(defun read-file-into-string1 (channel state ans bound) (declare (xargs :stobjs state :guard (and (symbolp channel) (open-input-channel-p channel :character state) (character-listp ans) (natp bound)))) (cond ((zp bound) (mv nil state)) (t (mv-let (val state) (read-char$ channel state) (cond ((not (characterp val)) (mv (coerce (reverse ans) 'string) state)) (t (read-file-into-string1 channel state (cons val ans) (1- bound))))))))
Definition:
(defconst *read-file-into-string-bound* (1- (ash 1 60)))
Function:
(defun read-file-into-string2-logical (filename start bytes state) (declare (xargs :stobjs state :guard (and (stringp filename) (natp start) (or (null bytes) (natp bytes))))) (non-exec (mv-let (erp val state) (mv-let (chan state) (open-input-channel filename :character state) (cond ((or (null chan) (not (state-p state))) (mv nil nil state)) (t (mv-let (val state) (read-file-into-string1 chan state nil *read-file-into-string-bound*) (pprogn (ec-call (close-input-channel chan state)) (mv nil val state)))))) (declare (ignore erp state)) (and (stringp val) (<= start (length val)) (subseq val start (if bytes (min (+ start bytes) (length val)) (length val)))))))
Function:
(defun read-file-into-string2 (filename start bytes state) (declare (xargs :stobjs state :guard (and (stringp filename) (natp start) (or (null bytes) (natp bytes))))) (read-file-into-string2-logical filename start bytes state))
Macro:
(defmacro read-file-into-string (filename &key (start '0) bytes) (cons 'read-file-into-string2 (cons filename (cons start (cons bytes '(state))))))