Identify a sequence of decreasing bit- and part-selects.
(vl-maybe-merge-selects-aux x from n) → (mv min rest)
We look for a sequence of decreasing bit- and part- selects that
count downward from
We return the index of the final bit select that matches this criteria as
Here are some examples.
Suppose FROM is the idexpr "foo", and N is 6.
Then, given a sequence x = (foo[5] foo[4] foo[3] bar baz), we return
MIN = 3 REST = (bar baz)
But if x = (bar baz), we just immediately return
MIN = 6 REST = (bar baz)
We also handle part selects, e.g., if X is (foo[5:3], foo[2], bar, baz), we return
MIN = 2 REST = (bar baz)
Function:
(defun vl-maybe-merge-selects-aux (x from n) (declare (xargs :guard (and (vl-exprlist-p x) (vl-expr-p from) (natp n)))) (let ((__function__ 'vl-maybe-merge-selects-aux)) (declare (ignorable __function__)) (b* ((from (vl-expr-fix from)) (n (lnfix n)) ((when (atom x)) (mv n (vl-exprlist-fix x))) (expr1 (car x)) ((unless (and (not (vl-fast-atom-p expr1)) (or (eq (vl-nonatom->op expr1) :vl-bitselect) (eq (vl-nonatom->op expr1) :vl-partselect-colon)))) (mv n (vl-exprlist-fix x))) (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 (equal expr1-from from) (vl-expr-resolved-p expr1-high) (vl-expr-resolved-p expr1-low))) (mv n (vl-exprlist-fix x))) (high-val (vl-resolved->val expr1-high)) (low-val (vl-resolved->val expr1-low)) ((unless (and (natp high-val) (natp low-val) (= high-val (- n 1)) (<= low-val high-val))) (mv n (vl-exprlist-fix x)))) (vl-maybe-merge-selects-aux (cdr x) from low-val))))
Theorem:
(defthm natp-of-vl-maybe-merge-selects-aux.min (b* (((mv common-lisp::?min common-lisp::?rest) (vl-maybe-merge-selects-aux x from n))) (natp min)) :rule-classes :type-prescription)
Theorem:
(defthm vl-exprlist-p-of-vl-maybe-merge-selects-aux.rest (b* (((mv common-lisp::?min common-lisp::?rest) (vl-maybe-merge-selects-aux x from n))) (vl-exprlist-p rest)) :rule-classes :rewrite)
Theorem:
(defthm vl-exprlist-count-of-vl-maybe-merge-selects-aux-weak (<= (vl-exprlist-count (mv-nth 1 (vl-maybe-merge-selects-aux x from n))) (vl-exprlist-count x)) :rule-classes ((:rewrite) (:linear)))
Theorem:
(defthm vl-exprlist-count-of-vl-maybe-merge-selects-aux-strong (implies (not (equal (nfix n) (mv-nth 0 (vl-maybe-merge-selects-aux x from n)))) (< (vl-exprlist-count (mv-nth 1 (vl-maybe-merge-selects-aux x from n))) (vl-exprlist-count x))) :rule-classes ((:rewrite) (:linear)))
Theorem:
(defthm upper-bound-of-vl-maybe-merge-selects-aux (<= (mv-nth 0 (vl-maybe-merge-selects-aux x from n)) (nfix n)) :rule-classes :linear)
Theorem:
(defthm vl-maybe-merge-selects-aux-of-vl-exprlist-fix-x (equal (vl-maybe-merge-selects-aux (vl-exprlist-fix x) from n) (vl-maybe-merge-selects-aux x from n)))
Theorem:
(defthm vl-maybe-merge-selects-aux-vl-exprlist-equiv-congruence-on-x (implies (vl-exprlist-equiv x x-equiv) (equal (vl-maybe-merge-selects-aux x from n) (vl-maybe-merge-selects-aux x-equiv from n))) :rule-classes :congruence)
Theorem:
(defthm vl-maybe-merge-selects-aux-of-vl-expr-fix-from (equal (vl-maybe-merge-selects-aux x (vl-expr-fix from) n) (vl-maybe-merge-selects-aux x from n)))
Theorem:
(defthm vl-maybe-merge-selects-aux-vl-expr-equiv-congruence-on-from (implies (vl-expr-equiv from from-equiv) (equal (vl-maybe-merge-selects-aux x from n) (vl-maybe-merge-selects-aux x from-equiv n))) :rule-classes :congruence)
Theorem:
(defthm vl-maybe-merge-selects-aux-of-nfix-n (equal (vl-maybe-merge-selects-aux x from (nfix n)) (vl-maybe-merge-selects-aux x from n)))
Theorem:
(defthm vl-maybe-merge-selects-aux-nat-equiv-congruence-on-n (implies (acl2::nat-equiv n n-equiv) (equal (vl-maybe-merge-selects-aux x from n) (vl-maybe-merge-selects-aux x from n-equiv))) :rule-classes :congruence)