		Search-engine friendly clone of the ACL2 documentation.

Expression-sizing

Vl-plainarg-exprsize

Compute sizes and types of expressions throughout a vl-plainarg-p

Signature
(vl-plainarg-exprsize x ss ctx port submod-ss warnings) → (mv successp warnings new-x)
Arguments: x — Guard (vl-plainarg-p x).; ss — Guard (vl-scopestack-p ss).; ctx — Guard (vl-context-p ctx).; port — Guard (or (vl-port-p port) (not port)).; submod-ss — Guard (vl-scopestack-p submod-ss).; warnings — Guard (vl-warninglist-p warnings).
Returns: successp — Type (booleanp successp).; warnings — Type (vl-warninglist-p warnings).; new-x — Type (vl-plainarg-p new-x).

Additional Notes

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 FW or N * FW, where FW is the width of the formal and N is the size of the array, so it doesn't seem like the port's width could in any sensible way used to size the expression.

Definitions and Theorems

Function: vl-plainarg-exprsize

(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: booleanp-of-vl-plainarg-exprsize.successp

(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: vl-warninglist-p-of-vl-plainarg-exprsize.warnings

(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: vl-plainarg-p-of-vl-plainarg-exprsize.new-x

(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: vl-plainarg-exprsize-of-vl-plainarg-fix-x

(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: vl-plainarg-exprsize-vl-plainarg-equiv-congruence-on-x

(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: vl-plainarg-exprsize-of-vl-scopestack-fix-ss

(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: vl-plainarg-exprsize-vl-scopestack-equiv-congruence-on-ss

(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: vl-plainarg-exprsize-of-vl-context-fix-ctx

(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: vl-plainarg-exprsize-vl-context-equiv-congruence-on-ctx

(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: vl-plainarg-exprsize-of-vl-scopestack-fix-submod-ss

(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: vl-plainarg-exprsize-vl-scopestack-equiv-congruence-on-submod-ss

(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: vl-plainarg-exprsize-of-vl-warninglist-fix-warnings

(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: vl-plainarg-exprsize-vl-warninglist-equiv-congruence-on-warnings

(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)