Returns NIL if the datatypes are assignment compatible (an object of type B can be assigned to a variable of type A) or an explanatory message if not.
(vl-check-datatype-assignment-compatibility a b) → msg
Function:
(defun vl-check-datatype-assignment-compatibility (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-assignment-compatibility)) (declare (ignorable __function__)) (b* (((when (or (consp (vl-datatype->udims a)) (consp (vl-datatype->udims b)))) (vl-check-datatype-equivalence a b)) (a-core (vl-maybe-usertype-resolve a)) (b-core (vl-maybe-usertype-resolve 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 (and (vl-datatype-case a-core :vl-enum) (atom (vl-datatype->pdims a-core)))) "LHS may not be an enum unless RHS is the same enum")) nil)))
Theorem:
(defthm return-type-of-vl-check-datatype-assignment-compatibility (b* ((msg (vl-check-datatype-assignment-compatibility a b))) (iff (vl-msg-p msg) msg)) :rule-classes :rewrite)
Theorem:
(defthm vl-check-datatype-assignment-compatibility-of-vl-datatype-fix-a (equal (vl-check-datatype-assignment-compatibility (vl-datatype-fix a) b) (vl-check-datatype-assignment-compatibility a b)))
Theorem:
(defthm vl-check-datatype-assignment-compatibility-vl-datatype-equiv-congruence-on-a (implies (vl-datatype-equiv a a-equiv) (equal (vl-check-datatype-assignment-compatibility a b) (vl-check-datatype-assignment-compatibility a-equiv b))) :rule-classes :congruence)
Theorem:
(defthm vl-check-datatype-assignment-compatibility-of-vl-datatype-fix-b (equal (vl-check-datatype-assignment-compatibility a (vl-datatype-fix b)) (vl-check-datatype-assignment-compatibility a b)))
Theorem:
(defthm vl-check-datatype-assignment-compatibility-vl-datatype-equiv-congruence-on-b (implies (vl-datatype-equiv b b-equiv) (equal (vl-check-datatype-assignment-compatibility a b) (vl-check-datatype-assignment-compatibility a b-equiv))) :rule-classes :congruence)