		Search-engine friendly clone of the ACL2 documentation.

Vl-convert-namedargs

Vl-convert-namedargs-aux

Change a named argument list into an equivalent plain (positional) argument list.

Signature
(vl-convert-namedargs-aux args ports) → new-args
Arguments: args — Named arguments for some module instance.
Guard (vl-namedarglist-p args).; ports — Ports of the submodule.
Guard (vl-portlist-p ports).
Returns: new-args — Type (vl-plainarglist-p new-args).

We walk down the list of ports since they're in the "right" order. For each port, we look up the corresponding argument and build a plainarg for it.

Note: we assume here that .* style ports have already been expanded, i.e., if any port does is missing a corresponding argument, then there really is no argument to that port and we're to infer a blank connection.

Definitions and Theorems

Function: vl-convert-namedargs-aux

(defun vl-convert-namedargs-aux (args ports)
 (declare (xargs :guard (and (vl-namedarglist-p args)
                             (vl-portlist-p ports))))
 (declare
      (xargs :guard (not (member nil (vl-portlist->names ports)))))
 (let ((__function__ 'vl-convert-namedargs-aux))
   (declare (ignorable __function__))
   (b*
    (((when (atom ports)) nil)
     (namedarg (vl-find-namedarg (vl-port->name (car ports))
                                 args))
     (plainarg
          (if namedarg
              (make-vl-plainarg :expr (vl-namedarg->expr namedarg)
                                :atts (vl-namedarg->atts namedarg))
            (make-vl-plainarg :expr nil
                              :atts '(("VL_MISSING_CONNECTION"))))))
    (cons plainarg
          (vl-convert-namedargs-aux args (cdr ports))))))

Theorem: vl-plainarglist-p-of-vl-convert-namedargs-aux

(defthm vl-plainarglist-p-of-vl-convert-namedargs-aux
  (b* ((new-args (vl-convert-namedargs-aux args ports)))
    (vl-plainarglist-p new-args))
  :rule-classes :rewrite)

Theorem: len-of-vl-convert-namedargs-aux

(defthm len-of-vl-convert-namedargs-aux
  (equal (len (vl-convert-namedargs-aux args ports))
         (len ports)))

Theorem: vl-convert-namedargs-aux-of-vl-namedarglist-fix-args

(defthm vl-convert-namedargs-aux-of-vl-namedarglist-fix-args
  (equal (vl-convert-namedargs-aux (vl-namedarglist-fix args)
                                   ports)
         (vl-convert-namedargs-aux args ports)))

Theorem: vl-convert-namedargs-aux-vl-namedarglist-equiv-congruence-on-args

(defthm
  vl-convert-namedargs-aux-vl-namedarglist-equiv-congruence-on-args
  (implies (vl-namedarglist-equiv args args-equiv)
           (equal (vl-convert-namedargs-aux args ports)
                  (vl-convert-namedargs-aux args-equiv ports)))
  :rule-classes :congruence)

Theorem: vl-convert-namedargs-aux-of-vl-portlist-fix-ports

(defthm vl-convert-namedargs-aux-of-vl-portlist-fix-ports
  (equal (vl-convert-namedargs-aux args (vl-portlist-fix ports))
         (vl-convert-namedargs-aux args ports)))

Theorem: vl-convert-namedargs-aux-vl-portlist-equiv-congruence-on-ports

(defthm
     vl-convert-namedargs-aux-vl-portlist-equiv-congruence-on-ports
  (implies (vl-portlist-equiv ports ports-equiv)
           (equal (vl-convert-namedargs-aux args ports)
                  (vl-convert-namedargs-aux args ports-equiv)))
  :rule-classes :congruence)