Returns NIL if the datatypes are equivalent, or an explanatory message if not.
(vl-check-datatype-equivalence a b) → msg
Function:
(defun vl-check-datatype-equivalence (a b) (declare (xargs :guard (and (vl-datatype-p a) (vl-datatype-p b)))) (declare (xargs :guard (and (vl-datatype-resolved-p a) (vl-datatype-resolved-p b)))) (let ((__function__ 'vl-check-datatype-equivalence)) (declare (ignorable __function__)) (b* ((udims-compatible (vl-dimensionlist-compare-sizes (vl-datatype->udims a) (vl-datatype->udims b))) ((unless udims-compatible) (vmsg "Unpacked dimensions mismatch")) (a-core (vl-maybe-usertype-resolve (vl-datatype-update-udims nil a))) (b-core (vl-maybe-usertype-resolve (vl-datatype-update-udims nil b))) ((when (vl-datatype-equiv (vl-datatype-strip a-core) (vl-datatype-strip b-core))) nil) ((unless (and (vl-datatype-packedp a-core) (vl-datatype-packedp b-core))) (vmsg "Unpacked base datatypes are unequal")) ((when (or (and (vl-datatype-case a-core :vl-enum) (atom (vl-datatype->pdims a-core))) (and (vl-datatype-case b-core :vl-enum) (atom (vl-datatype->pdims b-core))))) (if (and (vl-datatype-case a-core :vl-enum) (vl-datatype-case b-core :vl-enum)) "Different enums" "One is an enum and the other isn't")) ((mv erra asize) (vl-datatype-size a-core)) ((mv errb bsize) (vl-datatype-size b-core)) ((when (or erra errb)) (vmsg "Sizing failed: ~@0" (or erra errb))) ((when (or (not asize) (not bsize))) (vmsg "~s0 unsized" (cond (asize "b") (bsize "a") (t "a and b")))) ((unless (eql asize bsize)) (vmsg "Packed core datatypes differ in size: ~x0 versus ~x1" asize bsize))) nil)))
Theorem:
(defthm return-type-of-vl-check-datatype-equivalence (b* ((msg (vl-check-datatype-equivalence a b))) (iff (vl-msg-p msg) msg)) :rule-classes :rewrite)
Theorem:
(defthm vl-check-datatype-equivalence-of-vl-datatype-fix-a (equal (vl-check-datatype-equivalence (vl-datatype-fix a) b) (vl-check-datatype-equivalence a b)))
Theorem:
(defthm vl-check-datatype-equivalence-vl-datatype-equiv-congruence-on-a (implies (vl-datatype-equiv a a-equiv) (equal (vl-check-datatype-equivalence a b) (vl-check-datatype-equivalence a-equiv b))) :rule-classes :congruence)
Theorem:
(defthm vl-check-datatype-equivalence-of-vl-datatype-fix-b (equal (vl-check-datatype-equivalence a (vl-datatype-fix b)) (vl-check-datatype-equivalence a b)))
Theorem:
(defthm vl-check-datatype-equivalence-vl-datatype-equiv-congruence-on-b (implies (vl-datatype-equiv b b-equiv) (equal (vl-check-datatype-equivalence a b) (vl-check-datatype-equivalence a b-equiv))) :rule-classes :congruence)