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-binaryop-p op) (vl-expr-p x)))) (declare (xargs :guard (vl-op-ac-p op))) (let ((__function__ 'vl-collect-ac-args)) (declare (ignorable __function__)) (b* ((x (vl-expr-fix x))) (vl-expr-case x :vl-binary (if (vl-binaryop-equiv x.op op) (append (vl-collect-ac-args op x.left) (vl-collect-ac-args op x.right)) (list x)) :otherwise (list x)))))
Theorem:
(defthm vl-exprlist-p-of-vl-collect-ac-args (b* ((args (vl-collect-ac-args op x))) (vl-exprlist-p args)) :rule-classes :rewrite)
Theorem:
(defthm vl-exprlist-count-of-collect-ac-args (and (<= (vl-exprlist-count (vl-collect-ac-args op x)) (+ 2 (vl-expr-count x))) (implies (vl-expr-case x :vl-binary (vl-binaryop-equiv x.op op) :otherwise nil) (< (vl-exprlist-count (vl-collect-ac-args op x)) (vl-expr-count x)))) :rule-classes :linear)
Theorem:
(defthm vl-collect-ac-args-of-vl-binaryop-fix-op (equal (vl-collect-ac-args (vl-binaryop-fix op) x) (vl-collect-ac-args op x)))
Theorem:
(defthm vl-collect-ac-args-vl-binaryop-equiv-congruence-on-op (implies (vl-binaryop-equiv op op-equiv) (equal (vl-collect-ac-args op x) (vl-collect-ac-args op-equiv x))) :rule-classes :congruence)
Theorem:
(defthm vl-collect-ac-args-of-vl-expr-fix-x (equal (vl-collect-ac-args op (vl-expr-fix x)) (vl-collect-ac-args op x)))
Theorem:
(defthm vl-collect-ac-args-vl-expr-equiv-congruence-on-x (implies (vl-expr-equiv x x-equiv) (equal (vl-collect-ac-args op x) (vl-collect-ac-args op x-equiv))) :rule-classes :congruence)