(vl-instarray-plainarg-type-check arraysize y-type y-expr x-type x-expr portname) → (mv err multi x-size y-size)
Function:
(defun vl-instarray-plainarg-type-check (arraysize y-type y-expr x-type x-expr portname) (declare (xargs :guard (and (maybe-posp arraysize) (vl-datatype-p y-type) (vl-expr-p y-expr) (vl-datatype-p x-type) (vl-expr-p x-expr) (stringp portname)))) (declare (xargs :guard (and (vl-datatype-resolved-p y-type) (vl-datatype-resolved-p x-type)))) (let ((__function__ 'vl-instarray-plainarg-type-check)) (declare (ignorable __function__)) (b* (((mv err y-size) (vl-datatype-size y-type)) ((when (or err (not y-size) (eql 0 y-size))) (mv (vmsg "Couldn't size datatype ~a0 for ~s1 port expression ~a2" (vl-datatype-fix y-type) (string-fix portname) (vl-expr-fix y-expr)) nil nil nil)) (arraysize (acl2::maybe-posp-fix arraysize)) ((mv err x-size) (vl-datatype-size x-type)) ((when (or err (not x-size) (eql 0 x-size))) (mv (vmsg "Couldn't size datatype ~a0 for ~s1 port expression ~a2" (vl-datatype-fix x-type) (string-fix portname) (vl-expr-fix x-expr)) nil nil nil)) ((unless arraysize) (mv nil nil x-size y-size)) (y-packed (vl-datatype-packedp y-type)) (x-packed (vl-datatype-packedp x-type)) ((when (and x-packed y-packed)) (b* (((when (eql x-size y-size)) (mv nil nil x-size y-size)) ((when (eql x-size (* arraysize y-size))) (mv nil t x-size y-size))) (mv (vmsg "Bad instancearray port connection size on port ~s0: should be ~x1 (if replicated) or else ~x2, but is ~x3" (string-fix portname) y-size (* arraysize y-size) x-size) nil nil nil))) ((when x-packed) (mv (vmsg "Bad instancearray port connection: packed expression ~a0 ~ passed to unpacked port ~s1" (vl-expr-fix x-expr) (string-fix portname)) nil nil nil)) (compat-err (vl-check-datatype-compatibility y-type x-type :equiv)) ((unless compat-err) (mv nil nil x-size y-size)) ((mv err ?caveat x-basetype dim) (vl-datatype-remove-dim x-type)) ((when err) (mv (vmsg "Incompatible type for connection to instancearray port ~s0" (string-fix portname)) nil nil nil)) ((unless (vl-dimension-case dim :range)) (mv (vmsg "Incompatible type for connection to instancearray port ~s0 ~ (unsupported dimension)" (string-fix portname)) nil nil nil)) (range (vl-dimension->range dim)) ((when (or (not (vl-range-resolved-p range)) (not (eql (vl-range-size range) arraysize)))) (mv (vmsg "Incompatible type for connection to instancearray port ~s0 ~ (differing dimension sizes)." (string-fix portname)) nil nil nil)) (x-base-packed (vl-datatype-packedp x-basetype)) ((when (and x-base-packed y-packed (eql x-size (* arraysize y-size)))) (mv nil t x-size y-size)) (compat-err2 (vl-check-datatype-compatibility y-type x-basetype :equiv)) ((when compat-err2) (mv (vmsg "Incompatible type for connection to instancearray port ~s0 ~ (different slot types)." (string-fix portname)) nil nil nil))) (mv nil t x-size y-size))))
Theorem:
(defthm return-type-of-vl-instarray-plainarg-type-check.err (b* (((mv ?err ?multi ?x-size ?y-size) (vl-instarray-plainarg-type-check arraysize y-type y-expr x-type x-expr portname))) (iff (vl-msg-p err) err)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-instarray-plainarg-type-check.x-size (b* (((mv ?err ?multi ?x-size ?y-size) (vl-instarray-plainarg-type-check arraysize y-type y-expr x-type x-expr portname))) (implies (not err) (posp x-size))) :rule-classes :type-prescription)
Theorem:
(defthm return-type-of-vl-instarray-plainarg-type-check.y-size (b* (((mv ?err ?multi ?x-size ?y-size) (vl-instarray-plainarg-type-check arraysize y-type y-expr x-type x-expr portname))) (implies (not err) (posp y-size))) :rule-classes :type-prescription)
Theorem:
(defthm vl-instarray-plainarg-type-check-of-maybe-posp-fix-arraysize (equal (vl-instarray-plainarg-type-check (acl2::maybe-posp-fix arraysize) y-type y-expr x-type x-expr portname) (vl-instarray-plainarg-type-check arraysize y-type y-expr x-type x-expr portname)))
Theorem:
(defthm vl-instarray-plainarg-type-check-maybe-pos-equiv-congruence-on-arraysize (implies (acl2::maybe-pos-equiv arraysize arraysize-equiv) (equal (vl-instarray-plainarg-type-check arraysize y-type y-expr x-type x-expr portname) (vl-instarray-plainarg-type-check arraysize-equiv y-type y-expr x-type x-expr portname))) :rule-classes :congruence)
Theorem:
(defthm vl-instarray-plainarg-type-check-of-vl-datatype-fix-y-type (equal (vl-instarray-plainarg-type-check arraysize (vl-datatype-fix y-type) y-expr x-type x-expr portname) (vl-instarray-plainarg-type-check arraysize y-type y-expr x-type x-expr portname)))
Theorem:
(defthm vl-instarray-plainarg-type-check-vl-datatype-equiv-congruence-on-y-type (implies (vl-datatype-equiv y-type y-type-equiv) (equal (vl-instarray-plainarg-type-check arraysize y-type y-expr x-type x-expr portname) (vl-instarray-plainarg-type-check arraysize y-type-equiv y-expr x-type x-expr portname))) :rule-classes :congruence)
Theorem:
(defthm vl-instarray-plainarg-type-check-of-vl-expr-fix-y-expr (equal (vl-instarray-plainarg-type-check arraysize y-type (vl-expr-fix y-expr) x-type x-expr portname) (vl-instarray-plainarg-type-check arraysize y-type y-expr x-type x-expr portname)))
Theorem:
(defthm vl-instarray-plainarg-type-check-vl-expr-equiv-congruence-on-y-expr (implies (vl-expr-equiv y-expr y-expr-equiv) (equal (vl-instarray-plainarg-type-check arraysize y-type y-expr x-type x-expr portname) (vl-instarray-plainarg-type-check arraysize y-type y-expr-equiv x-type x-expr portname))) :rule-classes :congruence)
Theorem:
(defthm vl-instarray-plainarg-type-check-of-vl-datatype-fix-x-type (equal (vl-instarray-plainarg-type-check arraysize y-type y-expr (vl-datatype-fix x-type) x-expr portname) (vl-instarray-plainarg-type-check arraysize y-type y-expr x-type x-expr portname)))
Theorem:
(defthm vl-instarray-plainarg-type-check-vl-datatype-equiv-congruence-on-x-type (implies (vl-datatype-equiv x-type x-type-equiv) (equal (vl-instarray-plainarg-type-check arraysize y-type y-expr x-type x-expr portname) (vl-instarray-plainarg-type-check arraysize y-type y-expr x-type-equiv x-expr portname))) :rule-classes :congruence)
Theorem:
(defthm vl-instarray-plainarg-type-check-of-vl-expr-fix-x-expr (equal (vl-instarray-plainarg-type-check arraysize y-type y-expr x-type (vl-expr-fix x-expr) portname) (vl-instarray-plainarg-type-check arraysize y-type y-expr x-type x-expr portname)))
Theorem:
(defthm vl-instarray-plainarg-type-check-vl-expr-equiv-congruence-on-x-expr (implies (vl-expr-equiv x-expr x-expr-equiv) (equal (vl-instarray-plainarg-type-check arraysize y-type y-expr x-type x-expr portname) (vl-instarray-plainarg-type-check arraysize y-type y-expr x-type x-expr-equiv portname))) :rule-classes :congruence)
Theorem:
(defthm vl-instarray-plainarg-type-check-of-str-fix-portname (equal (vl-instarray-plainarg-type-check arraysize y-type y-expr x-type x-expr (str-fix portname)) (vl-instarray-plainarg-type-check arraysize y-type y-expr x-type x-expr portname)))
Theorem:
(defthm vl-instarray-plainarg-type-check-streqv-congruence-on-portname (implies (streqv portname portname-equiv) (equal (vl-instarray-plainarg-type-check arraysize y-type y-expr x-type x-expr portname) (vl-instarray-plainarg-type-check arraysize y-type y-expr x-type x-expr portname-equiv))) :rule-classes :congruence)