Read-object-from-file
Read an ACL2 object from a file.
;; Returns (mv erp object state) where either ERP is non-nil (meaning an error
;; occurred) or else OBJECT is the first ACL2 object in the file.
;; TODO: Add option to set the package of the symbols read in? (See read-objects-from-file-with-pkg).
(defund read-object-from-file (filename state)
(declare (xargs :guard (stringp filename)
:stobjs state))
(mv-let (channel state)
(open-input-channel filename :object state)
(if (not channel)
;; Error:
(mv `(:could-not-open-channel ,filename) nil state)
(mv-let (eof maybe-object state)
(read-object channel state)
(let ((state (close-input-channel channel state)))
(if eof
;; Error (no objects in file):
(mv `(:end-of-file ,filename) nil state)
(mv nil ; no error
maybe-object
state)))))))
