		Search-engine friendly clone of the ACL2 documentation.

Argresolve

Vl-annotate-plainargs

Annotates a plain argument list with port names and directions.

Signature
(vl-annotate-plainargs args ports scope) → annotated-args
Arguments: args — plainargs that typically have no :dir or :portname information; we want to annotate them.
Guard (vl-plainarglist-p args).; ports — corresponding ports for the submodule.
Guard (vl-portlist-p ports).; scope — Guard (vl-scope-p scope).
Returns: annotated-args — annotated version of args, semantically equivalent but typically has :dir and :portname information.
Type (and (vl-plainarglist-p annotated-args) (equal (len annotated-args) (len args))) .

This is a "best-effort" process which may fail to add annotations to any or all arguments. Such failures are expected, so we do not generate any warnings or errors in response to them.

What causes these failures?

Not all ports necessarily have a name, so we cannot add a :portname for every port.
The direction of a port may also not be apparent in some cases; see vl-port-direction for details.

Definitions and Theorems

Function: vl-annotate-plainargs

(defun vl-annotate-plainargs (args ports scope)
       (declare (xargs :guard (and (vl-plainarglist-p args)
                                   (vl-portlist-p ports)
                                   (vl-scope-p scope))))
       (declare (xargs :guard (same-lengthp args ports)))
       (let ((__function__ 'vl-annotate-plainargs))
            (declare (ignorable __function__))
            (b* (((when (atom args)) nil)
                 (name (vl-port->name (car ports)))
                 ((mv & dir)
                  (vl-port-direction (car ports)
                                     scope nil))
                 (arg-prime (change-vl-plainarg (car args)
                                                :dir dir
                                                :portname name)))
                (cons arg-prime
                      (vl-annotate-plainargs (cdr args)
                                             (cdr ports)
                                             scope)))))

Theorem: return-type-of-vl-annotate-plainargs

(defthm
     return-type-of-vl-annotate-plainargs
     (b* ((annotated-args (vl-annotate-plainargs args ports scope)))
         (and (vl-plainarglist-p annotated-args)
              (equal (len annotated-args)
                     (len args))))
     :rule-classes :rewrite)

Theorem: vl-annotate-plainargs-of-vl-plainarglist-fix-args

(defthm vl-annotate-plainargs-of-vl-plainarglist-fix-args
        (equal (vl-annotate-plainargs (vl-plainarglist-fix args)
                                      ports scope)
               (vl-annotate-plainargs args ports scope)))

Theorem: vl-annotate-plainargs-vl-plainarglist-equiv-congruence-on-args

(defthm
    vl-annotate-plainargs-vl-plainarglist-equiv-congruence-on-args
    (implies (vl-plainarglist-equiv args args-equiv)
             (equal (vl-annotate-plainargs args ports scope)
                    (vl-annotate-plainargs args-equiv ports scope)))
    :rule-classes :congruence)

Theorem: vl-annotate-plainargs-of-vl-portlist-fix-ports

(defthm vl-annotate-plainargs-of-vl-portlist-fix-ports
        (equal (vl-annotate-plainargs args (vl-portlist-fix ports)
                                      scope)
               (vl-annotate-plainargs args ports scope)))

Theorem: vl-annotate-plainargs-vl-portlist-equiv-congruence-on-ports

(defthm
    vl-annotate-plainargs-vl-portlist-equiv-congruence-on-ports
    (implies (vl-portlist-equiv ports ports-equiv)
             (equal (vl-annotate-plainargs args ports scope)
                    (vl-annotate-plainargs args ports-equiv scope)))
    :rule-classes :congruence)

Theorem: vl-annotate-plainargs-of-vl-scope-fix-scope

(defthm
     vl-annotate-plainargs-of-vl-scope-fix-scope
     (equal (vl-annotate-plainargs args ports (vl-scope-fix scope))
            (vl-annotate-plainargs args ports scope)))

Theorem: vl-annotate-plainargs-vl-scope-equiv-congruence-on-scope

(defthm
    vl-annotate-plainargs-vl-scope-equiv-congruence-on-scope
    (implies (vl-scope-equiv scope scope-equiv)
             (equal (vl-annotate-plainargs args ports scope)
                    (vl-annotate-plainargs args ports scope-equiv)))
    :rule-classes :congruence)