Resolves a datatype of usertype kind to a concrete datatype, i.e. anything but a user typename.
(vl-usertype-resolve x ss rec-limit) → (mv warning type scope)
The input is guarded to be a usertype. If it is defined as another usertype (possibly with packed/unpacked dimensions), then we recur until it is defined as something other than a usertype. However, the final type may still have usertypes within it, i.e. as struct/union member types.
Also returns the scopestack representing the scope in which the final type declaration was found.
This function is strict with respect to packed vs. unpacked dimensions; i.e., if a usertype is defined as having unpacked dimensions, it will warn if any packed dimensions are applied to that type. Arguably this check should be done elsewhere, in which case this function could ignore the distinction between packed and unpacked dimensions. However, it is important to preserve the order of dimensions, and it's not clear how to handle cases that mix the two: packed dimensions are always treated as "inner" or "most rapidly varying" dimensions. So if we have (illegal) nested typedefs that place unpacked dimensions inside of packed dimensions, we have no way to express that as a single, usertype-free datatype, unless we change some packed dimensions into unpacked ones or vice versa:
typedef logic t1 [5:1]; // unpacked dimension typedef t1 [3:0] t2; // packed dimension applied to unpacked datatype typedef logic [3:0] t3 [5:1]; // not the same as t2 typedef logic [5:1] [3:0] t4; // same dimensions as t2, but all dimensions packed typedef logic t5 [5:1] [3:0]; // same dimensions as t2, but all dimensions unpacked
We don't have this problem for the (also illegal) case where packed dimensions are applied to an unpacked structure or union, so we don't warn in this case; this should be checked separately.
Function:
(defun vl-usertype-resolve (x ss rec-limit) (declare (xargs :guard (and (vl-datatype-p x) (vl-scopestack-p ss) (natp rec-limit)))) (declare (xargs :guard (eq (vl-datatype-kind x) :vl-usertype))) (let ((__function__ 'vl-usertype-resolve)) (declare (ignorable __function__)) (b* ((ss (vl-scopestack-fix ss)) (x (vl-datatype-fix x)) ((vl-usertype x)) ((when (zp rec-limit)) (mv (make-vl-warning :type :vl-resolve-usertypes-fail :msg "Rec-limit ran out: recursively defined ~ datatype? ~a0" :args (list x.kind)) x ss)) ((unless (and (vl-atom-p x.kind) (member (tag (vl-atom->guts x.kind)) '(:vl-id :vl-typename)))) (mv (make-vl-warning :type :vl-resolve-usertypes-fail :msg "We don't yet support usertypes that are ~ not simple identifiers: ~a0" :args (list x.kind)) x ss)) (guts (vl-atom->guts x.kind)) (name (if (eq (tag guts) :vl-id) (vl-id->name guts) (vl-typename->name guts))) ((mv item new-ss) (vl-scopestack-find-item/ss name ss)) ((unless item) (mv (make-vl-warning :type :vl-resolve-usertypes-fail :msg "No typedef found for ~a0" :args (list x.kind)) x ss)) ((unless (eq (tag item) :vl-typedef)) (mv (make-vl-warning :type :vl-resolve-usertypes-fail :msg "Didn't find a typedef ~a0, instead ~ found ~a1" :args (list x.kind item)) x ss)) ((vl-typedef item)) ((mv warning subtype final-ss) (if (eq (vl-datatype-kind item.type) :vl-usertype) (vl-usertype-resolve item.type new-ss (1- rec-limit)) (mv nil item.type new-ss))) ((when warning) (mv warning x ss)) (sub-udims (vl-datatype->udims subtype)) ((when (and (consp x.pdims) (consp (vl-datatype->udims item.type)))) (mv (make-vl-warning :type :vl-usertype-packed-dims :msg "Usertype ~a0 was declared with packed ~ dimensions, but its definition ~a1 already ~ has unpacked dimensions." :args (list x item.type)) x ss)) (subtype (mbe :logic (vl-datatype-update-dims (append-without-guard x.pdims (vl-datatype->pdims subtype)) (append-without-guard x.udims sub-udims) subtype) :exec (if (or x.udims x.pdims) (vl-datatype-update-dims (append-without-guard x.pdims (vl-datatype->pdims subtype)) (append-without-guard x.udims sub-udims) subtype) subtype)))) (mv nil subtype final-ss))))
Theorem:
(defthm return-type-of-vl-usertype-resolve.warning (b* (((mv common-lisp::?warning common-lisp::?type ?scope) (vl-usertype-resolve x ss rec-limit))) (iff (vl-warning-p warning) warning)) :rule-classes :rewrite)
Theorem:
(defthm vl-datatype-p-of-vl-usertype-resolve.type (b* (((mv common-lisp::?warning common-lisp::?type ?scope) (vl-usertype-resolve x ss rec-limit))) (vl-datatype-p type)) :rule-classes :rewrite)
Theorem:
(defthm vl-scopestack-p-of-vl-usertype-resolve.scope (b* (((mv common-lisp::?warning common-lisp::?type ?scope) (vl-usertype-resolve x ss rec-limit))) (vl-scopestack-p scope)) :rule-classes :rewrite)
Theorem:
(defthm vl-usertype-resolve-of-vl-datatype-fix-x (equal (vl-usertype-resolve (vl-datatype-fix x) ss rec-limit) (vl-usertype-resolve x ss rec-limit)))
Theorem:
(defthm vl-usertype-resolve-vl-datatype-equiv-congruence-on-x (implies (vl-datatype-equiv x x-equiv) (equal (vl-usertype-resolve x ss rec-limit) (vl-usertype-resolve x-equiv ss rec-limit))) :rule-classes :congruence)
Theorem:
(defthm vl-usertype-resolve-of-vl-scopestack-fix-ss (equal (vl-usertype-resolve x (vl-scopestack-fix ss) rec-limit) (vl-usertype-resolve x ss rec-limit)))
Theorem:
(defthm vl-usertype-resolve-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-usertype-resolve x ss rec-limit) (vl-usertype-resolve x ss-equiv rec-limit))) :rule-classes :congruence)
Theorem:
(defthm vl-usertype-resolve-of-nfix-rec-limit (equal (vl-usertype-resolve x ss (nfix rec-limit)) (vl-usertype-resolve x ss rec-limit)))
Theorem:
(defthm vl-usertype-resolve-nat-equiv-congruence-on-rec-limit (implies (acl2::nat-equiv rec-limit rec-limit-equiv) (equal (vl-usertype-resolve x ss rec-limit) (vl-usertype-resolve x ss rec-limit-equiv))) :rule-classes :congruence)