		Search-engine friendly clone of the ACL2 documentation.

Vl-make-paramdecloverrides

Vl-make-paramdecloverrides-indexed

Line up positional parameter arguments with parameter declarations.

Signature
(vl-make-paramdecloverrides-indexed formals actuals) → overrides
Arguments: formals — In proper order, from the submodule.
Guard (vl-paramdecllist-p formals).; actuals — In proper order, from the instance.
Guard (vl-paramvaluelist-p actuals).
Returns: overrides — Type (vl-paramdecloverridelist-p overrides).

Definitions and Theorems

Function: vl-make-paramdecloverrides-indexed

(defun vl-make-paramdecloverrides-indexed (formals actuals)
 (declare (xargs :guard (and (vl-paramdecllist-p formals)
                             (vl-paramvaluelist-p actuals))))
 (declare
      (xargs :guard (<= (len actuals)
                        (len (vl-nonlocal-paramdecls formals)))))
 (let ((__function__ 'vl-make-paramdecloverrides-indexed))
  (declare (ignorable __function__))
  (b* (((when (atom formals)) nil)
       ((vl-paramdecl decl1)
        (vl-paramdecl-fix (car formals)))
       ((when decl1.localp)
        (cons (make-vl-paramdecloverride :decl decl1
                                         :override nil)
              (vl-make-paramdecloverrides-indexed (cdr formals)
                                                  actuals)))
       (value (and (consp actuals)
                   (vl-paramvalue-fix (first actuals)))))
   (cons
       (make-vl-paramdecloverride :decl decl1
                                  :override value)
       (vl-make-paramdecloverrides-indexed (cdr formals)
                                           (and (consp actuals)
                                                (rest actuals)))))))

Theorem: vl-paramdecloverridelist-p-of-vl-make-paramdecloverrides-indexed

(defthm
   vl-paramdecloverridelist-p-of-vl-make-paramdecloverrides-indexed
 (b*
  ((overrides (vl-make-paramdecloverrides-indexed formals actuals)))
  (vl-paramdecloverridelist-p overrides))
 :rule-classes :rewrite)

Theorem: vl-make-paramdecloverrides-indexed-of-vl-paramdecllist-fix-formals

(defthm
 vl-make-paramdecloverrides-indexed-of-vl-paramdecllist-fix-formals
 (equal
  (vl-make-paramdecloverrides-indexed (vl-paramdecllist-fix formals)
                                      actuals)
  (vl-make-paramdecloverrides-indexed formals actuals)))

Theorem: vl-make-paramdecloverrides-indexed-vl-paramdecllist-equiv-congruence-on-formals

(defthm
 vl-make-paramdecloverrides-indexed-vl-paramdecllist-equiv-congruence-on-formals
 (implies
   (vl-paramdecllist-equiv formals formals-equiv)
   (equal
        (vl-make-paramdecloverrides-indexed formals actuals)
        (vl-make-paramdecloverrides-indexed formals-equiv actuals)))
 :rule-classes :congruence)

Theorem: vl-make-paramdecloverrides-indexed-of-vl-paramvaluelist-fix-actuals

(defthm
 vl-make-paramdecloverrides-indexed-of-vl-paramvaluelist-fix-actuals
 (equal (vl-make-paramdecloverrides-indexed
             formals (vl-paramvaluelist-fix actuals))
        (vl-make-paramdecloverrides-indexed formals actuals)))

Theorem: vl-make-paramdecloverrides-indexed-vl-paramvaluelist-equiv-congruence-on-actuals

(defthm
 vl-make-paramdecloverrides-indexed-vl-paramvaluelist-equiv-congruence-on-actuals
 (implies
   (vl-paramvaluelist-equiv actuals actuals-equiv)
   (equal
        (vl-make-paramdecloverrides-indexed formals actuals)
        (vl-make-paramdecloverrides-indexed formals actuals-equiv)))
 :rule-classes :congruence)