Compute sizes and types of expressions throughout a vl-plainarg-p
(vl-plainarg-exprsize x ss ctx port submod-ss warnings) → (mv successp warnings new-x)
Minor note: We don't attempt to size blanks. If there is no expression, it remains as a blank.
Expressions in argument lists don't have a left-hand side. They do need to
ultimately agree with the target port, but I am feeling pretty confident that
the port's width does not play a role in sizing the expression. A good
reason for this is that, if you go and read xf-replicate-insts, and look at the
rules for splitting up instance arrays, it seems like there is more than one
possibility for the context width in this case, namely
Function:
(defun vl-plainarg-exprsize (x ss ctx port submod-ss warnings) (declare (xargs :guard (and (vl-plainarg-p x) (vl-scopestack-p ss) (vl-context-p ctx) (or (vl-port-p port) (not port)) (vl-scopestack-p submod-ss) (vl-warninglist-p warnings)))) (let ((__function__ 'vl-plainarg-exprsize)) (declare (ignorable __function__)) (b* ((x (vl-plainarg-fix x)) (warnings (vl-warninglist-fix warnings))) (b* (((vl-plainarg x) x) ((unless x.expr) (mv t warnings x)) (port (and port (vl-port-fix port))) ((when (eq (tag port) :vl-interfaceport)) (b* (((vl-interfaceport port)) ((when port.udims) (mv nil (fatal :type :vl-bad-interface-port :msg "~a0: Interface port with udims: ~a1" :args (list (vl-context-fix ctx) port)) x)) ((unless (vl-idexpr-p x.expr)) (mv nil (fatal :type :vl-bad-interface-port :msg "~a0: Non-ID expr ~a1 connected to interface port ~a2" :args (list (vl-context-fix ctx) x.expr port)) x)) (name (vl-idexpr->name x.expr)) (item (vl-scopestack-find-item name ss)) ((unless (and item (or (eq (tag item) :vl-modinst) (eq (tag item) :vl-interfaceport)))) (mv nil (fatal :type :vl-bad-interface-port :msg "~a0: Non-interface ~a1 connected to interface port ~a2" :args (list (vl-context-fix ctx) x.expr port)) x)) (interfacetype (if (eq (tag item) :vl-modinst) (vl-modinst->modname item) (vl-interfaceport->ifname item))) ((unless (equal interfacetype port.ifname)) (mv nil (fatal :type :vl-bad-interface-port :msg "~a0: Incompatible interface type for port ~a1; ~ expected ~a2 but found ~a3." :args (list (vl-context-fix ctx) port port.ifname interfacetype)) x))) (mv t warnings x))) (port-type (and port (vl-port-unpacked-datatype port submod-ss))) ((unless port-type) (b* (((mv successp warnings expr-prime) (vl-expr-size nil x.expr ss ctx warnings)) (x-prime (change-vl-plainarg x :expr expr-prime))) (mv successp warnings x-prime))) ((mv ok expr-prime warnings) (vl-expr-size-assigncontext port-type x.expr nil ss ctx warnings)) ((mv ok warnings expr-prime) (if ok (vl-expr-size nil expr-prime ss ctx warnings) (mv nil warnings expr-prime))) (x-prime (change-vl-plainarg x :expr expr-prime))) (mv ok warnings x-prime)))))
Theorem:
(defthm booleanp-of-vl-plainarg-exprsize.successp (b* (((mv ?successp ?warnings ?new-x) (vl-plainarg-exprsize x ss ctx port submod-ss warnings))) (booleanp successp)) :rule-classes :type-prescription)
Theorem:
(defthm vl-warninglist-p-of-vl-plainarg-exprsize.warnings (b* (((mv ?successp ?warnings ?new-x) (vl-plainarg-exprsize x ss ctx port submod-ss warnings))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-plainarg-p-of-vl-plainarg-exprsize.new-x (b* (((mv ?successp ?warnings ?new-x) (vl-plainarg-exprsize x ss ctx port submod-ss warnings))) (vl-plainarg-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm vl-plainarg-exprsize-of-vl-plainarg-fix-x (equal (vl-plainarg-exprsize (vl-plainarg-fix x) ss ctx port submod-ss warnings) (vl-plainarg-exprsize x ss ctx port submod-ss warnings)))
Theorem:
(defthm vl-plainarg-exprsize-vl-plainarg-equiv-congruence-on-x (implies (vl-plainarg-equiv x x-equiv) (equal (vl-plainarg-exprsize x ss ctx port submod-ss warnings) (vl-plainarg-exprsize x-equiv ss ctx port submod-ss warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-plainarg-exprsize-of-vl-scopestack-fix-ss (equal (vl-plainarg-exprsize x (vl-scopestack-fix ss) ctx port submod-ss warnings) (vl-plainarg-exprsize x ss ctx port submod-ss warnings)))
Theorem:
(defthm vl-plainarg-exprsize-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-plainarg-exprsize x ss ctx port submod-ss warnings) (vl-plainarg-exprsize x ss-equiv ctx port submod-ss warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-plainarg-exprsize-of-vl-context-fix-ctx (equal (vl-plainarg-exprsize x ss (vl-context-fix ctx) port submod-ss warnings) (vl-plainarg-exprsize x ss ctx port submod-ss warnings)))
Theorem:
(defthm vl-plainarg-exprsize-vl-context-equiv-congruence-on-ctx (implies (vl-context-equiv ctx ctx-equiv) (equal (vl-plainarg-exprsize x ss ctx port submod-ss warnings) (vl-plainarg-exprsize x ss ctx-equiv port submod-ss warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-plainarg-exprsize-of-vl-scopestack-fix-submod-ss (equal (vl-plainarg-exprsize x ss ctx port (vl-scopestack-fix submod-ss) warnings) (vl-plainarg-exprsize x ss ctx port submod-ss warnings)))
Theorem:
(defthm vl-plainarg-exprsize-vl-scopestack-equiv-congruence-on-submod-ss (implies (vl-scopestack-equiv submod-ss submod-ss-equiv) (equal (vl-plainarg-exprsize x ss ctx port submod-ss warnings) (vl-plainarg-exprsize x ss ctx port submod-ss-equiv warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-plainarg-exprsize-of-vl-warninglist-fix-warnings (equal (vl-plainarg-exprsize x ss ctx port submod-ss (vl-warninglist-fix warnings)) (vl-plainarg-exprsize x ss ctx port submod-ss warnings)))
Theorem:
(defthm vl-plainarg-exprsize-vl-warninglist-equiv-congruence-on-warnings (implies (vl-warninglist-equiv warnings warnings-equiv) (equal (vl-plainarg-exprsize x ss ctx port submod-ss warnings) (vl-plainarg-exprsize x ss ctx port submod-ss warnings-equiv))) :rule-classes :congruence)