		Search-engine friendly clone of the ACL2 documentation.

Vl-reportcard

Vl-clean-reportcard

Shrink a vl-reportcard-p and cleans all of its warning lists with vl-clean-warnings.

Signature
(vl-clean-reportcard x) → new-x
Arguments: x — Guard (vl-reportcard-p x).
Returns: new-x — Type (vl-reportcard-p 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.

Definitions and Theorems

Function: vl-clean-reportcard

(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)))

Theorem: vl-reportcard-p-of-vl-clean-reportcard

(defthm vl-reportcard-p-of-vl-clean-reportcard
  (b* ((new-x (vl-clean-reportcard x)))
    (vl-reportcard-p new-x))
  :rule-classes :rewrite)

Theorem: vl-clean-reportcard-of-vl-reportcard-fix-x

(defthm vl-clean-reportcard-of-vl-reportcard-fix-x
  (equal (vl-clean-reportcard (vl-reportcard-fix x))
         (vl-clean-reportcard x)))

Theorem: vl-clean-reportcard-vl-reportcard-equiv-congruence-on-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)

Subtopics

Vl-clean-reportcard-aux: Assumes X has already been shrunk, so we may safely recur down it.