Read-objects-from-book
Read the forms in a book.
;; Read forms from FILENAME but require the first form to be an IN-PACKAGE form
;; used for interpreting symbols in the rest of the forms. Returns (mv erp
;; forms state). Consider first calling something like load-port-file-if-exists
;; to ensure the packages are known.
(defund read-objects-from-book (filename state)
(declare (xargs :guard (stringp filename) ; includes the .lisp extension
:mode :program ; because of in-package-fn
:stobjs state))
;; First read just the in-package form:
(mv-let (erp first-form state)
(read-object-from-file filename state)
(if erp
(mv erp nil state)
(if (not (and (consp first-form)
(eq 'in-package (car first-form))))
(prog2$ (er hard? 'read-objects-from-book "ERROR: Expected an in-package form but got ~x0." first-form)
(mv :missing-in-package nil state))
(let ((book-package (cadr first-form)))
;; Read the book contents after temporarily setting the package to book-package:
(mv-let (erp forms state)
(read-objects-from-file-with-pkg filename book-package state)
(if erp ; error reading forms
(mv erp nil state)
;; No error:
(mv nil forms state))))))))
