		Search-engine friendly clone of the ACL2 documentation.

Expr-cleaning

Vl-elim-nested-concats

Flatten out nested concatenations like {a, b, {c, d}, { { e, f } }} into {a, b, c, d, e, f}.

Signature
(vl-elim-nested-concats x) → new-x
Arguments: x — The arguments to a concatenation.
Guard (vl-exprlist-p x).
Returns: new-x — Possibly somewhat flattened.
Type (vl-exprlist-p new-x).

We flatten out any top-level concatenations within x, and return the possibly simplified list of expressions.

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]}

Definitions and Theorems

Function: vl-elim-nested-concats

(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: vl-exprlist-p-of-vl-elim-nested-concats

(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: true-listp-of-vl-elim-nested-concats

(defthm true-listp-of-vl-elim-nested-concats
  (true-listp (vl-elim-nested-concats x))
  :rule-classes :type-prescription)

Theorem: vl-elim-nested-concats-of-vl-exprlist-fix-x

(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: vl-elim-nested-concats-vl-exprlist-equiv-congruence-on-x

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

Subtopics

Vl-elim-nested-concats-pass