(parse-fileset-loop filemap gcc) → (mv erp tunitmap)
Function:
(defun parse-fileset-loop (filemap gcc) (declare (xargs :guard (and (filepath-filedata-mapp filemap) (booleanp gcc)))) (let ((__function__ 'parse-fileset-loop)) (declare (ignorable __function__)) (b* (((reterr) nil) ((when (omap::emptyp filemap)) (retok nil)) ((mv filepath filedata) (omap::head filemap)) ((erp tunit) (parse-file filepath (filedata->unwrap filedata) gcc)) ((erp tunitmap) (parse-fileset-loop (omap::tail filemap) gcc))) (retok (omap::update (filepath-fix filepath) tunit tunitmap)))))
Theorem:
(defthm filepath-transunit-mapp-of-parse-fileset-loop.tunitmap (b* (((mv acl2::?erp ?tunitmap) (parse-fileset-loop filemap gcc))) (filepath-transunit-mapp tunitmap)) :rule-classes :rewrite)
Theorem:
(defthm keys-of-parse-fileset-loop (implies (filepath-filedata-mapp filemap) (b* (((mv acl2::?erp ?tunitmap) (parse-fileset-loop filemap gcc))) (implies (not erp) (equal (omap::keys tunitmap) (omap::keys filemap))))))