Given a dotted expression that indexes into a datatype, find the type of the expression.
(vl-hidexpr-traverse-datatype x type) → (mv warning restype)
A helpful invariant to remember when thinking about this function: The type and unpacked dimensions of a given call of this function belong to the base (leftmost) variable in the HID.
Also note: the datatype should be fully usertype-resolved, as by vl-datatype-usertype-elim.
BOZO Rewrite this documentation under the new assumption that the datatypes are pre-resolved.
Example: Suppose we have the following type declarations
typedef struct packed { logic [3:0] foo; } [4:0] foostruct; typedef union { foostruct [5:0] bar; logic [2:0] baz; } bunion [0:6]; typedef struct { bunion fa [0:8], logic [1:0] ba; } bstruct; bstruct myvar [8:0];
For this example, we'll write a type with both packed an unpacked dimensions with an underscore between the packed and unpacked dims.
A bunion is a type consisting of an unpacked array of 7 elements each of which may either be a packed array of 6 foostructs (a packed structure containing one 4-bit logic field) or a 3-bit logic; a bstruct is a struct containing an unpacked array of 9 bunions and an additional 2-bit logic field; and myvar is an unpacked array of 9 bstructs.
Suppose our expression is
Function:
(defun vl-hidexpr-traverse-datatype (x type) (declare (xargs :guard (and (vl-expr-p x) (vl-datatype-p type)))) (declare (xargs :guard (vl-hidexpr-p x))) (let ((__function__ 'vl-hidexpr-traverse-datatype)) (declare (ignorable __function__)) (b* ((type (vl-datatype-fix type)) ((when (vl-hidexpr->endp x)) (mv nil type)) (idx1 (vl-hidexpr->first x)) ((mv warning baretype) (vl-hidindex-datatype-resolve-dims idx1 type)) ((when warning) (mv warning nil)) ((when (or (consp (vl-datatype->udims baretype)) (consp (vl-datatype->pdims baretype)))) (mv (make-vl-warning :type :vl-hid-datatype-fail :msg "Not enough indices in dotted selector ~a0: ~ extra ~s1 dimensions." :args (list (vl-expr-fix x) (if (consp (vl-datatype->udims baretype)) "unpacked" "packed")) :fn __function__) nil)) ((mv ok members) (vl-datatype->structmembers baretype)) ((unless ok) (mv (make-vl-warning :type :vl-hid-datatype-fail :msg "Dot-indexing into a datatype that isn't a ~ struct or union: ~a0" :args (list (vl-datatype-fix baretype)) :fn __function__) nil)) (next-hid (vl-hidexpr->rest x)) (nextname (vl-hidindex->name (vl-hidexpr->first next-hid))) (member (vl-find-structmember nextname members)) ((unless member) (mv (make-vl-warning :type :vl-structindex-fail :msg "Dot-indexing failed: struct/union member ~ ~s0 not found in type ~a1" :args (list nextname (vl-datatype-fix baretype)) :fn __function__) nil)) (membtype (vl-structmember->type member))) (vl-hidexpr-traverse-datatype next-hid membtype))))
Theorem:
(defthm return-type-of-vl-hidexpr-traverse-datatype.warning (b* (((mv common-lisp::?warning ?restype) (vl-hidexpr-traverse-datatype x type))) (iff (vl-warning-p warning) warning)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-hidexpr-traverse-datatype.restype (b* (((mv common-lisp::?warning ?restype) (vl-hidexpr-traverse-datatype x type))) (iff (vl-datatype-p restype) (not warning))) :rule-classes :rewrite)
Theorem:
(defthm vl-hidexpr-traverse-datatype-of-vl-expr-fix-x (equal (vl-hidexpr-traverse-datatype (vl-expr-fix x) type) (vl-hidexpr-traverse-datatype x type)))
Theorem:
(defthm vl-hidexpr-traverse-datatype-vl-expr-equiv-congruence-on-x (implies (vl-expr-equiv x x-equiv) (equal (vl-hidexpr-traverse-datatype x type) (vl-hidexpr-traverse-datatype x-equiv type))) :rule-classes :congruence)
Theorem:
(defthm vl-hidexpr-traverse-datatype-of-vl-datatype-fix-type (equal (vl-hidexpr-traverse-datatype x (vl-datatype-fix type)) (vl-hidexpr-traverse-datatype x type)))
Theorem:
(defthm vl-hidexpr-traverse-datatype-vl-datatype-equiv-congruence-on-type (implies (vl-datatype-equiv type type-equiv) (equal (vl-hidexpr-traverse-datatype x type) (vl-hidexpr-traverse-datatype x type-equiv))) :rule-classes :congruence)