Recognize a datatype for which an indexing operator is a bitselect/partselect.
(vl-datatype-bitselect-p x) → *
This is more complicated than one might think. For example, a packed struct can be bitselected/partselected from and acts just like a vector in that case. However, a packed array is always indexed as an array.
The datatype should have usertypes resolved away before calling.
Function:
(defun vl-datatype-bitselect-p (x) (declare (xargs :guard (vl-datatype-p x))) (let ((__function__ 'vl-datatype-bitselect-p)) (declare (ignorable __function__)) (b* ((udims (vl-datatype->udims x)) (pdims (vl-datatype->pdims x)) ((when (consp udims)) nil) ((when (consp pdims)) (and (eq (vl-datatype-kind x) :vl-coretype) (member (vl-coretype->name x) '(:vl-reg :vl-logic :vl-bit)) (atom (cdr pdims))))) (vl-datatype-case x (:vl-coretype (or (member x.name '(:vl-reg :vl-logic :vl-bit)) (member x.name '(:vl-byte :vl-shortint :vl-int :vl-longint :vl-integer)))) (:vl-struct x.packedp) (:vl-union x.packedp) (:otherwise nil)))))
Theorem:
(defthm vl-datatype-bitselect-p-of-vl-datatype-fix-x (equal (vl-datatype-bitselect-p (vl-datatype-fix x)) (vl-datatype-bitselect-p x)))
Theorem:
(defthm vl-datatype-bitselect-p-vl-datatype-equiv-congruence-on-x (implies (vl-datatype-equiv x x-equiv) (equal (vl-datatype-bitselect-p x) (vl-datatype-bitselect-p x-equiv))) :rule-classes :congruence)