		Search-engine friendly clone of the ACL2 documentation.

Std/io

Read-file-characters-rev

Read an entire file into a character-listp, but in reverse order!

Signature
(read-file-characters-rev filename state) → (mv errmsg/contents state)
Arguments: filename — Guard (stringp filename).

This goofy function is just like read-file-characters except that the characters are returned in reverse.

This is faster than read-file-characters because we avoid the cost of reversing the accumulator, and thus require half as many conses.

Note: that we just leave this function enabled. Logically it's just the reverse of read-file-characters.

Definitions and Theorems

Function: read-file-characters-rev

(defun read-file-characters-rev (filename state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (stringp filename)))
  (let ((__function__ 'read-file-characters-rev))
    (declare (ignorable __function__))
    (mbe :logic
         (b* (((mv contents state)
               (read-file-characters filename state)))
           (if (stringp contents)
               (mv contents state)
             (mv (rev contents) state)))
         :exec
         (b* (((mv channel state)
               (open-input-channel filename
                                   :character state))
              ((unless channel)
               (mv (concatenate 'string
                                "Error opening file " filename)
                   state))
              ((mv contents state)
               (tr-read-char$-all channel state nil))
              (state (close-input-channel channel state)))
           (mv contents state)))))