Parse a file set.
(parse-fileset fileset) → (mv erp tunits)
We go through each file of the file set and parse it, obtaining a translation unit for each, which we return in an ensemble of translation units that corresponds to the file set. The file paths are the same for the file set and for the translation unit ensembles (they are the keys of the maps).
Function:
(defun parse-fileset-loop (filemap) (declare (xargs :guard (filepath-filedata-mapp filemap))) (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))) ((erp tunitmap) (parse-fileset-loop (omap::tail filemap)))) (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))) (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))) (implies (not erp) (equal (omap::keys tunitmap) (omap::keys filemap))))))
Function:
(defun parse-fileset (fileset) (declare (xargs :guard (filesetp fileset))) (let ((__function__ 'parse-fileset)) (declare (ignorable __function__)) (b* (((reterr) (irr-transunit-ensemble)) (filemap (fileset->unwrap fileset)) ((erp tunitmap) (parse-fileset-loop filemap))) (retok (transunit-ensemble tunitmap)))))
Theorem:
(defthm transunit-ensemblep-of-parse-fileset.tunits (b* (((mv acl2::?erp ?tunits) (parse-fileset fileset))) (transunit-ensemblep tunits)) :rule-classes :rewrite)
Theorem:
(defthm filepaths-of-parse-fileset (b* (((mv acl2::?erp ?tunits) (parse-fileset fileset))) (implies (not erp) (equal (omap::keys (transunit-ensemble->unwrap tunits)) (omap::keys (fileset->unwrap fileset))))))