Parse (the data bytes of) a file.
(parse-file path data) → (mv erp tunit)
If successful, the result is a translation unit. We initialize the parser state with the data bytes, and we attempt to parse them as a translation unit. The final parser state is discarded, since it is no longer needed.
If an error occurs, we enhance it with
information about the file path.
It is the case that
Function:
(defun parse-file (path data) (declare (xargs :guard (and (filepathp path) (byte-listp data)))) (let ((__function__ 'parse-file)) (declare (ignorable __function__)) (b* (((reterr) (irr-transunit)) (parstate (init-parstate data)) ((mv erp tunit &) (parse-translation-unit parstate)) ((when erp) (b* (((unless (msgp erp)) (raise "Internal error: ~x0 is not a message." erp) (reterr t))) (reterr (msg "Error in file ~x0: ~@1" (filepath->unwrap path) erp))))) (retok tunit))))
Theorem:
(defthm transunitp-of-parse-file.tunit (b* (((mv acl2::?erp ?tunit) (parse-file path data))) (transunitp tunit)) :rule-classes :rewrite)