		Search-engine friendly clone of the ACL2 documentation.

Drop-blankports

Vl-modinst-drop-blankports

Drop arguments to blank ports from a module instance.

Signature
(vl-modinst-drop-blankports x ss warnings) → (mv warnings new-x)
Arguments: x — module instance to rewrite.
Guard (vl-modinst-p x).; ss — Guard (vl-scopestack-p ss).; warnings — Guard (vl-warninglist-p warnings).
Returns: warnings — Type (vl-warninglist-p warnings).; new-x — Type (vl-modinst-p new-x).

Definitions and Theorems

Function: vl-modinst-drop-blankports

(defun vl-modinst-drop-blankports (x ss warnings)
 (declare (xargs :guard (and (vl-modinst-p x)
                             (vl-scopestack-p ss)
                             (vl-warninglist-p warnings))))
 (let ((__function__ 'vl-modinst-drop-blankports))
  (declare (ignorable __function__))
  (b*
   ((x (vl-modinst-fix x))
    ((vl-modinst x) x)
    (target-mod (vl-scopestack-find-definition x.modname ss))
    ((unless (and target-mod
                  (eq (tag target-mod) :vl-module)))
     (mv (fatal :type :vl-bad-instance
                :msg "~a0 refers to undefined module ~m1."
                :args (list x x.modname))
         x))
    ((unless (eq (vl-arguments-kind x.portargs)
                 :vl-arguments-plain))
     (mv
      (fatal
       :type :vl-programming-error
       :msg
       "~a0: expected all modules to be using plain ~
                         arguments, but found named arguments.  Did you ~
                         forget to run the argresolve transform first?"
       :args (list x))
      x))
    (ports (vl-module->ports target-mod))
    (plainargs (vl-arguments-plain->args x.portargs))
    ((unless (same-lengthp plainargs ports))
     (mv
      (fatal
       :type :vl-bad-instance
       :msg
       "~a0: bad arity.  Expected ~x1 arguments but found ~
                         ~x2 arguments."
       :args (list x (len ports) (len plainargs)))
      x))
    (new-plainargs
         (vl-plainarglist-drop-blankports plainargs ports))
    (new-arguments (make-vl-arguments-plain :args new-plainargs))
    (new-x (change-vl-modinst x
                              :portargs new-arguments)))
   (mv (ok) new-x))))

Theorem: vl-warninglist-p-of-vl-modinst-drop-blankports.warnings

(defthm vl-warninglist-p-of-vl-modinst-drop-blankports.warnings
  (b* (((mv ?warnings ?new-x)
        (vl-modinst-drop-blankports x ss warnings)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: vl-modinst-p-of-vl-modinst-drop-blankports.new-x

(defthm vl-modinst-p-of-vl-modinst-drop-blankports.new-x
  (b* (((mv ?warnings ?new-x)
        (vl-modinst-drop-blankports x ss warnings)))
    (vl-modinst-p new-x))
  :rule-classes :rewrite)