Checks two datatypes for compatibility. The compattype argument determines which kind of compatibility -- equivalence, assignment compatibility, or cast compatibility. For assignment and cast compatibility, B is the source type and A the destination type.
(vl-check-datatype-compatibility a b compattype) → msg
At the moment, cast compatibility doesn't check anything.
Function:
(defun vl-check-datatype-compatibility (a b compattype) (declare (xargs :guard (and (vl-datatype-p a) (vl-datatype-p b) (vl-typecompat-p compattype)))) (declare (xargs :guard (and (vl-datatype-resolved-p a) (vl-datatype-resolved-p b)))) (let ((__function__ 'vl-check-datatype-compatibility)) (declare (ignorable __function__)) (b* ((a (vl-datatype-fix a)) (b (vl-datatype-fix b)) (compattype (vl-typecompat-fix compattype)) (errmsg (case compattype (:assign (vl-check-datatype-assignment-compatibility a b)) (:cast nil) (t (vl-check-datatype-equivalence a b))))) (and errmsg (vmsg "Datatype ~a0 is not ~s1 to ~a2: ~@3" (if (vl-datatype->pdims b) (make-vl-structmember :type b :name "b") b) (case compattype (:equiv "equivalent") (:assign "assignment compatible") (otherwise "cast compatible")) (if (vl-datatype->udims a) (make-vl-structmember :type a :name "a") a) errmsg)))))
Theorem:
(defthm return-type-of-vl-check-datatype-compatibility (b* ((msg (vl-check-datatype-compatibility a b compattype))) (iff (vl-msg-p msg) msg)) :rule-classes :rewrite)
Theorem:
(defthm vl-check-datatype-compatibility-of-vl-datatype-fix-a (equal (vl-check-datatype-compatibility (vl-datatype-fix a) b compattype) (vl-check-datatype-compatibility a b compattype)))
Theorem:
(defthm vl-check-datatype-compatibility-vl-datatype-equiv-congruence-on-a (implies (vl-datatype-equiv a a-equiv) (equal (vl-check-datatype-compatibility a b compattype) (vl-check-datatype-compatibility a-equiv b compattype))) :rule-classes :congruence)
Theorem:
(defthm vl-check-datatype-compatibility-of-vl-datatype-fix-b (equal (vl-check-datatype-compatibility a (vl-datatype-fix b) compattype) (vl-check-datatype-compatibility a b compattype)))
Theorem:
(defthm vl-check-datatype-compatibility-vl-datatype-equiv-congruence-on-b (implies (vl-datatype-equiv b b-equiv) (equal (vl-check-datatype-compatibility a b compattype) (vl-check-datatype-compatibility a b-equiv compattype))) :rule-classes :congruence)
Theorem:
(defthm vl-check-datatype-compatibility-of-vl-typecompat-fix-compattype (equal (vl-check-datatype-compatibility a b (vl-typecompat-fix compattype)) (vl-check-datatype-compatibility a b compattype)))
Theorem:
(defthm vl-check-datatype-compatibility-vl-typecompat-equiv-congruence-on-compattype (implies (vl-typecompat-equiv compattype compattype-equiv) (equal (vl-check-datatype-compatibility a b compattype) (vl-check-datatype-compatibility a b compattype-equiv))) :rule-classes :congruence)