Collect all expressions from index positions in a hid expression,
e.g., for
(vl-hidexpr-collect-indices x) → indices
Function:
(defun vl-hidexpr-collect-indices (x) (declare (xargs :guard (vl-expr-p x))) (declare (xargs :guard (vl-hidexpr-p x))) (let ((__function__ 'vl-hidexpr-collect-indices)) (declare (ignorable __function__)) (if (vl-hidexpr->endp x) nil (append (vl-hidindex->indices (vl-hidexpr->first x)) (vl-hidexpr-collect-indices (vl-hidexpr->rest x))))))
Theorem:
(defthm vl-exprlist-p-of-vl-hidexpr-collect-indices (b* ((indices (vl-hidexpr-collect-indices x))) (vl-exprlist-p indices)) :rule-classes :rewrite)
Theorem:
(defthm vl-hidexpr-collect-indices-when-endp (implies (vl-hidexpr->endp x) (equal (vl-hidexpr-collect-indices x) nil)))
Theorem:
(defthm vl-exprlist-count-of-vl-hidexpr-collect-indices-weak (implies (vl-hidexpr-p x) (<= (vl-exprlist-count (vl-hidexpr-collect-indices x)) (vl-expr-count x))) :rule-classes ((:rewrite) (:linear)))
Theorem:
(defthm vl-exprlist-count-of-vl-hidexpr-collect-indices-strong (implies (and (vl-hidexpr-p x) (not (vl-hidexpr->endp x))) (< (vl-exprlist-count (vl-hidexpr-collect-indices x)) (vl-expr-count x))) :rule-classes ((:rewrite) (:linear)))
Theorem:
(defthm vl-exprlist-count-of-vl-hidexpr-collect-indices-equal (implies (and (vl-hidexpr-p x) (case-split (not (vl-hidexpr->endp x)))) (equal (equal (vl-exprlist-count (vl-hidexpr-collect-indices x)) (vl-expr-count x)) nil)))
Theorem:
(defthm vl-hidexpr-collect-indices-of-vl-expr-fix-x (equal (vl-hidexpr-collect-indices (vl-expr-fix x)) (vl-hidexpr-collect-indices x)))
Theorem:
(defthm vl-hidexpr-collect-indices-vl-expr-equiv-congruence-on-x (implies (vl-expr-equiv x x-equiv) (equal (vl-hidexpr-collect-indices x) (vl-hidexpr-collect-indices x-equiv))) :rule-classes :congruence)