		Search-engine friendly clone of the ACL2 documentation.

Drop-blankports

Vl-plainarglist-drop-blankports

Drop arguments to blank ports from an plain argument list.

Signature
(vl-plainarglist-drop-blankports args ports) → new-args
Arguments: args — arguments to some module instance.
Guard (vl-plainarglist-p args).; ports — corresponding ports from the submodule.
Guard (vl-portlist-p ports).
Returns: new-args — copy of args with blank ports removed.
Type (vl-plainarglist-p new-args).

Definitions and Theorems

Function: vl-plainarglist-drop-blankports

(defun vl-plainarglist-drop-blankports (args ports)
  (declare (xargs :guard (and (vl-plainarglist-p args)
                              (vl-portlist-p ports))))
  (declare (xargs :guard (same-lengthp args ports)))
  (let ((__function__ 'vl-plainarglist-drop-blankports))
    (declare (ignorable __function__))
    (b* (((when (atom args)) nil)
         (port1 (vl-port-fix (car ports)))
         ((when (or (eq (tag port1) :vl-interfaceport)
                    (vl-regularport->expr port1)))
          (cons (vl-plainarg-fix (car args))
                (vl-plainarglist-drop-blankports (cdr args)
                                                 (cdr ports)))))
      (vl-plainarglist-drop-blankports (cdr args)
                                       (cdr ports)))))

Theorem: vl-plainarglist-p-of-vl-plainarglist-drop-blankports

(defthm vl-plainarglist-p-of-vl-plainarglist-drop-blankports
  (b* ((new-args (vl-plainarglist-drop-blankports args ports)))
    (vl-plainarglist-p new-args))
  :rule-classes :rewrite)