Preliminary, minor heuristic cleanups for the arguments to a fussy size warning.
Function:
(defun vl-tweak-fussy-warning-type-preclean (x) (declare (xargs :guard (vl-expr-p x))) (let ((__function__ 'vl-tweak-fussy-warning-type-preclean)) (declare (ignorable __function__)) (let ((x (vl-expr-fix x))) (vl-expr-case x :vl-concat (if (equal (len x.parts) 1) (first x.parts) x) :vl-multiconcat (b* (((unless (and (vl-expr-resolved-p x.reps) (posp (vl-resolved->val x.reps)) (equal (len x.parts) 1))) x) (reps (vl-resolved->val x.reps)) (inner (first x.parts)) ((unless (vl-expr-case inner :vl-literal)) x) (value (vl-literal->val inner))) (vl-value-case value :vl-constint (b* ((new-value (change-vl-constint value :origwidth (* value.origwidth reps) :value (logrepeat reps value.origwidth value.value)))) (make-vl-literal :val new-value)) :otherwise x)) :otherwise x))))
Theorem:
(defthm vl-expr-p-of-vl-tweak-fussy-warning-type-preclean (b* ((new-x (vl-tweak-fussy-warning-type-preclean x))) (vl-expr-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm vl-tweak-fussy-warning-type-preclean-of-vl-expr-fix-x (equal (vl-tweak-fussy-warning-type-preclean (vl-expr-fix x)) (vl-tweak-fussy-warning-type-preclean x)))
Theorem:
(defthm vl-tweak-fussy-warning-type-preclean-vl-expr-equiv-congruence-on-x (implies (vl-expr-equiv x x-equiv) (equal (vl-tweak-fussy-warning-type-preclean x) (vl-tweak-fussy-warning-type-preclean x-equiv))) :rule-classes :congruence)