		Search-engine friendly clone of the ACL2 documentation.

Leftright-check

Vl-collect-ac-args

Collect the nested arguments to an associative/commutative operator.

Signature
(vl-collect-ac-args op x) → args
Arguments: op — An associative and commutative binary operators.
Guard (vl-op-ac-p op).; x — An expression, typically it is an argument to op.
Guard (vl-expr-p x).
Returns: args — Type (vl-exprlist-p args), given the guard.

If x is itself an op expression, we recursively collect up the ac-args of its sub-expressions. Otherwise we just collect x. For instance, if op is | and x is:

(a | (b + c)) | (d & e)

Then we return a list with three expressions: a, b + c, and d & e.

Definitions and Theorems

Function: vl-collect-ac-args

(defun vl-collect-ac-args (op x)
  (declare (xargs :guard (and (vl-op-ac-p op) (vl-expr-p x))))
  (let ((__function__ 'vl-collect-ac-args))
    (declare (ignorable __function__))
    (b* (((when (vl-fast-atom-p x)) (list x))
         ((unless (eq (vl-nonatom->op x) op))
          (list x))
         ((when (mbe :logic (atom x) :exec nil))
          (impossible))
         (args (vl-nonatom->args x)))
      (append (vl-collect-ac-args op (first args))
              (vl-collect-ac-args op (second args))))))

Theorem: vl-exprlist-p-of-vl-collect-ac-args

(defthm vl-exprlist-p-of-vl-collect-ac-args
  (implies (and (vl-op-ac-p op) (vl-expr-p x))
           (b* ((args (vl-collect-ac-args op x)))
             (vl-exprlist-p args)))
  :rule-classes :rewrite)