Read-file-into-character-array-stobj
Read the characters from a file into a stobj array.
;; Returns (mv erp character-array-stobj state) where either ERP is non-nil (meaning an error
;; occurred) or else the characters field of CHARACTER-ARRAY-STOBJ contains the contents of FILENAME.
(defund read-file-into-character-array-stobj (filename character-array-stobj state)
(declare (xargs :guard (stringp filename)
:stobjs (character-array-stobj state)))
(mv-let (file-length state)
(file-length$ filename state)
(if (not file-length)
(mv `(:failed-to-get-file-length ,filename) character-array-stobj state)
(mv-let (channel state)
(open-input-channel filename :character state)
(if (not channel)
;; Error:
(mv `(:could-not-open-channel ,filename) character-array-stobj state)
(let ( ;; make the array the right size:
(character-array-stobj (resize-characters file-length character-array-stobj)))
(mv-let (character-array-stobj state)
(read-file-into-character-array-stobj-aux channel 0 character-array-stobj state)
(let ((state (close-input-channel channel state)))
(mv nil ; no error
character-array-stobj
state)))))))))
