Disambiguate a translation unit ensembles.
(dimb-transunit-ensemble tuens gcc) → (mv erp new-tuens)
We also pass a flag saying whether GCC extensions should be accepted.
We disambiguate all the translation units, independently. We leave the file path mapping unchanged.
Function:
(defun dimb-transunit-ensemble-loop (tumap gcc) (declare (xargs :guard (and (filepath-transunit-mapp tumap) (booleanp gcc)))) (let ((__function__ 'dimb-transunit-ensemble-loop)) (declare (ignorable __function__)) (b* (((reterr) nil) ((when (omap::emptyp tumap)) (retok nil)) ((mv path tunit) (omap::head tumap)) ((erp new-tunit) (dimb-transunit tunit gcc)) ((erp new-tumap) (dimb-transunit-ensemble-loop (omap::tail tumap) gcc))) (retok (omap::update path new-tunit new-tumap)))))
Theorem:
(defthm filepath-transunit-mapp-of-dimb-transunit-ensemble-loop.new-tumap (implies (filepath-transunit-mapp tumap) (b* (((mv acl2::?erp ?new-tumap) (dimb-transunit-ensemble-loop tumap gcc))) (filepath-transunit-mapp new-tumap))) :rule-classes :rewrite)
Theorem:
(defthm dimb-transunit-ensemble-loop-of-bool-fix-gcc (equal (dimb-transunit-ensemble-loop tumap (bool-fix gcc)) (dimb-transunit-ensemble-loop tumap gcc)))
Theorem:
(defthm dimb-transunit-ensemble-loop-iff-congruence-on-gcc (implies (iff gcc gcc-equiv) (equal (dimb-transunit-ensemble-loop tumap gcc) (dimb-transunit-ensemble-loop tumap gcc-equiv))) :rule-classes :congruence)
Theorem:
(defthm transunit-ensemble-unambp-loop-of-dimb-transunit-ensemble-loop (b* (((mv acl2::?erp ?new-tumap) (dimb-transunit-ensemble-loop tumap gcc))) (implies (not erp) (transunit-ensemble-unambp-loop new-tumap))))
Function:
(defun dimb-transunit-ensemble (tuens gcc) (declare (xargs :guard (and (transunit-ensemblep tuens) (booleanp gcc)))) (let ((__function__ 'dimb-transunit-ensemble)) (declare (ignorable __function__)) (b* (((reterr) (irr-transunit-ensemble)) (tumap (transunit-ensemble->unwrap tuens)) ((erp new-tumap) (dimb-transunit-ensemble-loop tumap gcc))) (retok (transunit-ensemble new-tumap)))))
Theorem:
(defthm transunit-ensemblep-of-dimb-transunit-ensemble.new-tuens (b* (((mv acl2::?erp ?new-tuens) (dimb-transunit-ensemble tuens gcc))) (transunit-ensemblep new-tuens)) :rule-classes :rewrite)
Theorem:
(defthm transunit-ensemble-unambp-of-dimb-transunit-ensemble (b* (((mv acl2::?erp ?new-tuens) (dimb-transunit-ensemble tuens gcc))) (implies (not erp) (transunit-ensemble-unambp new-tuens))))
Theorem:
(defthm dimb-transunit-ensemble-of-transunit-ensemble-fix-tuens (equal (dimb-transunit-ensemble (transunit-ensemble-fix tuens) gcc) (dimb-transunit-ensemble tuens gcc)))
Theorem:
(defthm dimb-transunit-ensemble-transunit-ensemble-equiv-congruence-on-tuens (implies (transunit-ensemble-equiv tuens tuens-equiv) (equal (dimb-transunit-ensemble tuens gcc) (dimb-transunit-ensemble tuens-equiv gcc))) :rule-classes :congruence)
Theorem:
(defthm dimb-transunit-ensemble-of-bool-fix-gcc (equal (dimb-transunit-ensemble tuens (bool-fix gcc)) (dimb-transunit-ensemble tuens gcc)))
Theorem:
(defthm dimb-transunit-ensemble-iff-congruence-on-gcc (implies (iff gcc gcc-equiv) (equal (dimb-transunit-ensemble tuens gcc) (dimb-transunit-ensemble tuens gcc-equiv))) :rule-classes :congruence)