(vl-port-type-err-warn portname portdir x port-type type-err ss scopes) → warnings
Function:
(defun vl-port-type-err-warn (portname portdir x port-type type-err ss scopes) (declare (xargs :guard (and (stringp portname) (vl-maybe-direction-p portdir) (vl-plainarg-p x) (vl-datatype-p port-type) (vl-maybe-type-error-p type-err) (vl-scopestack-p ss) (vl-elabscopes-p scopes)))) (declare (xargs :guard (vl-plainarg->expr x))) (let ((__function__ 'vl-port-type-err-warn)) (declare (ignorable __function__)) (b* (((unless type-err) nil) (warnings nil) (expr (vl-plainarg->expr x))) (vl-type-error-case type-err :trunc/extend (b* (((when (vl-expr-is-extensional expr)) nil) (type (if (and (eql type-err.rhs-selfsize 32) (< type-err.lhs-size 32) (consp (vl-collect-unsized-ints (vl-expr-interesting-size-atoms expr) ss scopes))) :vl-port-size-mismatch-minor :vl-port-size-mismatch))) (warn :type type :msg "~s0ort ~s1 has size ~x2, but its connection expression ~a3 has size ~x4" :args (list (case (vl-maybe-direction-fix portdir) ((nil) "P") (:vl-input "Input p") (:vl-output "Output p") (otherwise "Inout p")) (string-fix portname) type-err.lhs-size expr type-err.rhs-selfsize))) :otherwise (vl-type-error-basic-warn expr nil type-err (vl-idexpr portname) port-type ss)))))
Theorem:
(defthm vl-warninglist-p-of-vl-port-type-err-warn (b* ((warnings (vl-port-type-err-warn portname portdir x port-type type-err ss scopes))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-port-type-err-warn-of-str-fix-portname (equal (vl-port-type-err-warn (str-fix portname) portdir x port-type type-err ss scopes) (vl-port-type-err-warn portname portdir x port-type type-err ss scopes)))
Theorem:
(defthm vl-port-type-err-warn-streqv-congruence-on-portname (implies (streqv portname portname-equiv) (equal (vl-port-type-err-warn portname portdir x port-type type-err ss scopes) (vl-port-type-err-warn portname-equiv portdir x port-type type-err ss scopes))) :rule-classes :congruence)
Theorem:
(defthm vl-port-type-err-warn-of-vl-maybe-direction-fix-portdir (equal (vl-port-type-err-warn portname (vl-maybe-direction-fix portdir) x port-type type-err ss scopes) (vl-port-type-err-warn portname portdir x port-type type-err ss scopes)))
Theorem:
(defthm vl-port-type-err-warn-vl-maybe-direction-equiv-congruence-on-portdir (implies (vl-maybe-direction-equiv portdir portdir-equiv) (equal (vl-port-type-err-warn portname portdir x port-type type-err ss scopes) (vl-port-type-err-warn portname portdir-equiv x port-type type-err ss scopes))) :rule-classes :congruence)
Theorem:
(defthm vl-port-type-err-warn-of-vl-plainarg-fix-x (equal (vl-port-type-err-warn portname portdir (vl-plainarg-fix x) port-type type-err ss scopes) (vl-port-type-err-warn portname portdir x port-type type-err ss scopes)))
Theorem:
(defthm vl-port-type-err-warn-vl-plainarg-equiv-congruence-on-x (implies (vl-plainarg-equiv x x-equiv) (equal (vl-port-type-err-warn portname portdir x port-type type-err ss scopes) (vl-port-type-err-warn portname portdir x-equiv port-type type-err ss scopes))) :rule-classes :congruence)
Theorem:
(defthm vl-port-type-err-warn-of-vl-datatype-fix-port-type (equal (vl-port-type-err-warn portname portdir x (vl-datatype-fix port-type) type-err ss scopes) (vl-port-type-err-warn portname portdir x port-type type-err ss scopes)))
Theorem:
(defthm vl-port-type-err-warn-vl-datatype-equiv-congruence-on-port-type (implies (vl-datatype-equiv port-type port-type-equiv) (equal (vl-port-type-err-warn portname portdir x port-type type-err ss scopes) (vl-port-type-err-warn portname portdir x port-type-equiv type-err ss scopes))) :rule-classes :congruence)
Theorem:
(defthm vl-port-type-err-warn-of-vl-maybe-type-error-fix-type-err (equal (vl-port-type-err-warn portname portdir x port-type (vl-maybe-type-error-fix type-err) ss scopes) (vl-port-type-err-warn portname portdir x port-type type-err ss scopes)))
Theorem:
(defthm vl-port-type-err-warn-vl-maybe-type-error-equiv-congruence-on-type-err (implies (vl-maybe-type-error-equiv type-err type-err-equiv) (equal (vl-port-type-err-warn portname portdir x port-type type-err ss scopes) (vl-port-type-err-warn portname portdir x port-type type-err-equiv ss scopes))) :rule-classes :congruence)
Theorem:
(defthm vl-port-type-err-warn-of-vl-scopestack-fix-ss (equal (vl-port-type-err-warn portname portdir x port-type type-err (vl-scopestack-fix ss) scopes) (vl-port-type-err-warn portname portdir x port-type type-err ss scopes)))
Theorem:
(defthm vl-port-type-err-warn-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-port-type-err-warn portname portdir x port-type type-err ss scopes) (vl-port-type-err-warn portname portdir x port-type type-err ss-equiv scopes))) :rule-classes :congruence)
Theorem:
(defthm vl-port-type-err-warn-of-vl-elabscopes-fix-scopes (equal (vl-port-type-err-warn portname portdir x port-type type-err ss (vl-elabscopes-fix scopes)) (vl-port-type-err-warn portname portdir x port-type type-err ss scopes)))
Theorem:
(defthm vl-port-type-err-warn-vl-elabscopes-equiv-congruence-on-scopes (implies (vl-elabscopes-equiv scopes scopes-equiv) (equal (vl-port-type-err-warn portname portdir x port-type type-err ss scopes) (vl-port-type-err-warn portname portdir x port-type type-err ss scopes-equiv))) :rule-classes :congruence)