Given a hidindex expression, e.g. foo[5][3], and the datatype and unpacked dimensions corresponding to foo, return the datatype and unpacked dimensions corresponding to the whole expression.
(vl-hidindex-datatype-resolve-dims x type) → (mv warning type1)
Note: we don't check whether indices are in bounds or anything, just whether the number of indices is less than or equal the number of total (unpacked plus packed) dimensions.
We produce a non-fatal warning because we're not sure in what contexts this will be used.
Example: Suppose our datatype is from a typedef
typedef bit [3:0] [4:2] foo [0:6] [0:8];
that is, it has one unpacked dimension
Function:
(defun vl-hidindex-datatype-resolve-dims (x type) (declare (xargs :guard (and (vl-expr-p x) (vl-datatype-p type)))) (declare (xargs :guard (vl-hidindex-p x))) (let ((__function__ 'vl-hidindex-datatype-resolve-dims)) (declare (ignorable __function__)) (b* ((idxcount (vl-hidindex-count-indices x)) (type (vl-datatype-fix type)) (x (vl-expr-fix x)) (unpacked-dims (vl-datatype->udims type)) (packed-dims (vl-datatype->pdims type)) (nunpacked (len unpacked-dims)) ((when (<= idxcount nunpacked)) (mv nil (vl-datatype-update-udims (nthcdr idxcount (list-fix unpacked-dims)) type))) (remaining-idxcount (- idxcount nunpacked)) ((unless (<= remaining-idxcount (len packed-dims))) (mv (make-vl-warning :type :vl-too-many-indices :msg "Too many indices on expression ~a0 ~ relative to dimensions of type ~a1 (with ~ ~x2 additional unpacked dimensions)." :args (list x type (len unpacked-dims)) :fn __function__) nil)) (type (vl-datatype-update-dims (nthcdr remaining-idxcount (list-fix packed-dims)) nil type))) (mv nil type))))
Theorem:
(defthm return-type-of-vl-hidindex-datatype-resolve-dims.warning (b* (((mv common-lisp::?warning ?type1) (vl-hidindex-datatype-resolve-dims x type))) (iff (vl-warning-p warning) warning)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-hidindex-datatype-resolve-dims.type1 (b* (((mv common-lisp::?warning ?type1) (vl-hidindex-datatype-resolve-dims x type))) (iff (vl-datatype-p type1) (not warning))) :rule-classes :rewrite)
Theorem:
(defthm vl-hidindex-datatype-resolve-dims-of-vl-expr-fix-x (equal (vl-hidindex-datatype-resolve-dims (vl-expr-fix x) type) (vl-hidindex-datatype-resolve-dims x type)))
Theorem:
(defthm vl-hidindex-datatype-resolve-dims-vl-expr-equiv-congruence-on-x (implies (vl-expr-equiv x x-equiv) (equal (vl-hidindex-datatype-resolve-dims x type) (vl-hidindex-datatype-resolve-dims x-equiv type))) :rule-classes :congruence)
Theorem:
(defthm vl-hidindex-datatype-resolve-dims-of-vl-datatype-fix-type (equal (vl-hidindex-datatype-resolve-dims x (vl-datatype-fix type)) (vl-hidindex-datatype-resolve-dims x type)))
Theorem:
(defthm vl-hidindex-datatype-resolve-dims-vl-datatype-equiv-congruence-on-type (implies (vl-datatype-equiv type type-equiv) (equal (vl-hidindex-datatype-resolve-dims x type) (vl-hidindex-datatype-resolve-dims x type-equiv))) :rule-classes :congruence)