Shrink a vl-reportcard-p and cleans all of its warning lists with vl-clean-warnings.
(vl-clean-reportcard x) → new-x
Cleaning can be useful before printing report cards, to minimize any useless or redundant information. We shrink the report card to eliminate any shadowed pairs, clean any redundant warnings, and eliminate entries for modules that don't have any warnings. The resulting report card doesn't have redundant/unnecessary information and is suitable for, e.g., printing.
(defun vl-clean-reportcard (x) (declare (xargs :guard (vl-reportcard-p x))) (let ((__function__ 'vl-clean-reportcard)) (declare (ignorable __function__)) (b* ((x (vl-reportcard-fix x)) (x-shrink (hons-shrink-alist x nil)) (ret (vl-clean-reportcard-aux x-shrink nil))) (fast-alist-free x-shrink) ret)))
(defthm vl-reportcard-p-of-vl-clean-reportcard (b* ((new-x (vl-clean-reportcard x))) (vl-reportcard-p new-x)) :rule-classes :rewrite)
(defthm vl-clean-reportcard-of-vl-reportcard-fix-x (equal (vl-clean-reportcard (vl-reportcard-fix x)) (vl-clean-reportcard x)))
(defthm vl-clean-reportcard-vl-reportcard-equiv-congruence-on-x (implies (vl-reportcard-equiv x x-equiv) (equal (vl-clean-reportcard x) (vl-clean-reportcard x-equiv))) :rule-classes :congruence)