Collect the nested arguments to an associative/commutative operator.
(vl-collect-ac-args op x) → args
If
(a | (b + c)) | (d & e)
Then we return a list with three expressions:
Function:
(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:
(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)