Merge together concatenations like
(vl-maybe-merge-selects x ss) → new-x
Here,
Note: to make this function more effective,
We walk over
Function:
(defun vl-maybe-merge-selects (x ss) (declare (xargs :guard (and (vl-exprlist-p x) (vl-scopestack-p ss)))) (let ((__function__ 'vl-maybe-merge-selects)) (declare (ignorable __function__)) (b* (((when (atom x)) nil) (expr1 (vl-expr-fix (car x))) ((when (vl-fast-atom-p expr1)) (cons expr1 (vl-maybe-merge-selects (cdr x) ss))) (expr1-op (vl-nonatom->op expr1)) ((unless (or (eq expr1-op :vl-bitselect) (eq expr1-op :vl-partselect-colon))) (cons expr1 (vl-maybe-merge-selects (cdr x) ss))) (expr1-args (vl-nonatom->args expr1)) (expr1-from (first expr1-args)) (expr1-high (second expr1-args)) (expr1-low (if (eq (vl-nonatom->op expr1) :vl-bitselect) expr1-high (third expr1-args))) ((unless (and (vl-idexpr-p expr1-from) (vl-expr-resolved-p expr1-high) (vl-expr-resolved-p expr1-low))) (cons expr1 (vl-maybe-merge-selects (cdr x) ss))) (high-val (vl-resolved->val expr1-high)) (low-val (vl-resolved->val expr1-low)) ((unless (<= low-val high-val)) (cons expr1 (vl-maybe-merge-selects (cdr x) ss))) ((mv min rest) (vl-maybe-merge-selects-aux (cdr x) expr1-from low-val)) ((when (= min low-val)) (cons expr1 (vl-maybe-merge-selects (cdr x) ss))) ((mv okp range) (vl-ss-find-range (vl-idexpr->name expr1-from) ss)) ((unless okp) (cons expr1 (vl-maybe-merge-selects (cdr x) ss))) ((unless (and range (vl-range-resolved-p range) (>= (vl-resolved->val (vl-range->msb range)) (vl-resolved->val (vl-range->lsb range))) (>= (vl-resolved->val (vl-range->msb range)) high-val) (>= low-val (vl-resolved->val (vl-range->lsb range))))) (cons expr1 (vl-maybe-merge-selects (cdr x) ss))) (min-expr (vl-make-index min)) (new-expr1 (make-vl-nonatom :op :vl-partselect-colon :args (list expr1-from expr1-high min-expr) :finalwidth (+ 1 (- high-val low-val)) :finaltype :vl-unsigned :atts nil))) (cons new-expr1 (vl-maybe-merge-selects rest ss)))))
Theorem:
(defthm vl-exprlist-p-of-vl-maybe-merge-selects (b* ((new-x (vl-maybe-merge-selects x ss))) (vl-exprlist-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm vl-maybe-merge-selects-of-vl-exprlist-fix-x (equal (vl-maybe-merge-selects (vl-exprlist-fix x) ss) (vl-maybe-merge-selects x ss)))
Theorem:
(defthm vl-maybe-merge-selects-vl-exprlist-equiv-congruence-on-x (implies (vl-exprlist-equiv x x-equiv) (equal (vl-maybe-merge-selects x ss) (vl-maybe-merge-selects x-equiv ss))) :rule-classes :congruence)
Theorem:
(defthm vl-maybe-merge-selects-of-vl-scopestack-fix-ss (equal (vl-maybe-merge-selects x (vl-scopestack-fix ss)) (vl-maybe-merge-selects x ss)))
Theorem:
(defthm vl-maybe-merge-selects-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-maybe-merge-selects x ss) (vl-maybe-merge-selects x ss-equiv))) :rule-classes :congruence)