Read-objects-from-file
Read the ACL2 objects from a file.
;; Returns (mv erp objects state) where either ERP is non-nil (meaning an error
;; occurred) or else OBJECTS are the ACL2 objects in the file.
;; The package used for symbols read from the file that don't have explicit
;; packages is the current package, but see read-objects-from-file-with-pkg.
(defund read-objects-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 (objects state)
(read-objects-from-channel channel state)
(let ((state (close-input-channel channel state)))
(mv nil ; no error
objects
state))))))
