Move modules and other design elements that have fatal warnings
from the
(vl-design-filter-zombies good bad suppress-fatals) → (mv good-- bad++)
Function:
(defun vl-design-filter-zombies (good bad suppress-fatals) (declare (xargs :guard (and (vl-design-p good) (vl-design-p bad) (symbol-listp suppress-fatals)))) (let ((__function__ 'vl-design-filter-zombies)) (declare (ignorable __function__)) (b* (((vl-design good)) ((vl-design bad)) ((mv bad-mods good-mods) (vl-filter-modules (vl-modulelist-zombies good.mods suppress-fatals) good.mods)) ((mv bad-interfaces good-interfaces) (vl-filter-interfaces (vl-interfacelist-zombies good.interfaces suppress-fatals) good.interfaces)) ((mv bad-udps good-udps) (vl-filter-udps (vl-udplist-zombies good.udps suppress-fatals) good.udps)) ((mv bad-programs good-programs) (vl-filter-programs (vl-programlist-zombies good.programs suppress-fatals) good.programs)) ((mv bad-classes good-classes) (vl-filter-classes (vl-classlist-zombies good.classes suppress-fatals) good.classes)) ((mv bad-packages good-packages) (vl-filter-packages (vl-packagelist-zombies good.packages suppress-fatals) good.packages)) ((mv bad-configs good-configs) (vl-filter-configs (vl-configlist-zombies good.configs suppress-fatals) good.configs)) ((mv bad-typedefs good-typedefs) (vl-filter-typedefs (vl-typedeflist-zombies good.typedefs suppress-fatals) good.typedefs)) (good (change-vl-design good :mods good-mods :interfaces good-interfaces :udps good-udps :programs good-programs :classes good-classes :packages good-packages :configs good-configs :typedefs good-typedefs)) (bad (change-vl-design bad :mods (append bad-mods bad.mods) :interfaces (append bad-interfaces bad.interfaces) :udps (append bad-udps bad.udps) :programs (append bad-programs bad.programs) :classes (append bad-classes bad.classes) :packages (append bad-packages bad.packages) :configs (append bad-configs bad.configs) :typedefs (append bad-typedefs bad.typedefs)))) (mv good bad))))
Theorem:
(defthm vl-design-p-of-vl-design-filter-zombies.good-- (b* (((mv ?good-- ?bad++) (vl-design-filter-zombies good bad suppress-fatals))) (vl-design-p good--)) :rule-classes :rewrite)
Theorem:
(defthm vl-design-p-of-vl-design-filter-zombies.bad++ (b* (((mv ?good-- ?bad++) (vl-design-filter-zombies good bad suppress-fatals))) (vl-design-p bad++)) :rule-classes :rewrite)
Theorem:
(defthm vl-design-filter-zombies-of-vl-design-fix-good (equal (vl-design-filter-zombies (vl-design-fix good) bad suppress-fatals) (vl-design-filter-zombies good bad suppress-fatals)))
Theorem:
(defthm vl-design-filter-zombies-vl-design-equiv-congruence-on-good (implies (vl-design-equiv good good-equiv) (equal (vl-design-filter-zombies good bad suppress-fatals) (vl-design-filter-zombies good-equiv bad suppress-fatals))) :rule-classes :congruence)
Theorem:
(defthm vl-design-filter-zombies-of-vl-design-fix-bad (equal (vl-design-filter-zombies good (vl-design-fix bad) suppress-fatals) (vl-design-filter-zombies good bad suppress-fatals)))
Theorem:
(defthm vl-design-filter-zombies-vl-design-equiv-congruence-on-bad (implies (vl-design-equiv bad bad-equiv) (equal (vl-design-filter-zombies good bad suppress-fatals) (vl-design-filter-zombies good bad-equiv suppress-fatals))) :rule-classes :congruence)
Theorem:
(defthm vl-design-filter-zombies-of-symbol-list-fix-suppress-fatals (equal (vl-design-filter-zombies good bad (acl2::symbol-list-fix suppress-fatals)) (vl-design-filter-zombies good bad suppress-fatals)))
Theorem:
(defthm vl-design-filter-zombies-symbol-list-equiv-congruence-on-suppress-fatals (implies (acl2::symbol-list-equiv suppress-fatals suppress-fatals-equiv) (equal (vl-design-filter-zombies good bad suppress-fatals) (vl-design-filter-zombies good bad suppress-fatals-equiv))) :rule-classes :congruence)