Flatten out nested concatenations like
(vl-elim-nested-concats x) → new-x
We flatten out any top-level concatenations within
This may help vl-maybe-merge-selects to be more effective. For instance, with the help of flattening, it can merge selects such as:
{foo[3], {foo[2], foo[1]}, foo[0]}
Function:
(defun vl-elim-nested-concats (x) (declare (xargs :guard (vl-exprlist-p x))) (let ((__function__ 'vl-elim-nested-concats)) (declare (ignorable __function__)) (b* (((mv progressp x-prime) (vl-elim-nested-concats-pass x))) (if progressp (vl-elim-nested-concats x-prime) x-prime))))
Theorem:
(defthm vl-exprlist-p-of-vl-elim-nested-concats (b* ((new-x (vl-elim-nested-concats x))) (vl-exprlist-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm true-listp-of-vl-elim-nested-concats (true-listp (vl-elim-nested-concats x)) :rule-classes :type-prescription)
Theorem:
(defthm vl-elim-nested-concats-of-vl-exprlist-fix-x (equal (vl-elim-nested-concats (vl-exprlist-fix x)) (vl-elim-nested-concats x)))
Theorem:
(defthm vl-elim-nested-concats-vl-exprlist-equiv-congruence-on-x (implies (vl-exprlist-equiv x x-equiv) (equal (vl-elim-nested-concats x) (vl-elim-nested-concats x-equiv))) :rule-classes :congruence)