		Search-engine friendly clone of the ACL2 documentation.

Vl-simple-instantiate

Vl-simple-instantiate-list

Generate a bunch of module instances.

Signature
(vl-simple-instantiate-list x prefix arglists &key (n '0) (loc '*vl-fakeloc*)) → insts
Arguments: x — module to instantiate.
Guard (vl-module-p x).; prefix — base name for instances, e.g., prefix_3, prefix_2.
Guard (stringp prefix).; arglists — actuals for each instance.
Guard (vl-exprlistlist-p arglists).; n — name index, counts up.
Guard (natp n).; loc — Guard (vl-location-p loc).
Returns: insts — Type (vl-modinstlist-p insts).

Definitions and Theorems

Function: vl-simple-instantiate-list-fn

(defun vl-simple-instantiate-list-fn (x prefix arglists n loc)
  (declare (xargs :guard (and (vl-module-p x)
                              (stringp prefix)
                              (vl-exprlistlist-p arglists)
                              (natp n)
                              (vl-location-p loc))))
  (let ((__function__ 'vl-simple-instantiate-list))
    (declare (ignorable __function__))
    (if (atom arglists)
        nil
      (cons (vl-simple-instantiate x (cat prefix (natstr n))
                                   (car arglists)
                                   :loc loc)
            (vl-simple-instantiate-list-fn x prefix (cdr arglists)
                                           (+ 1 (lnfix n))
                                           loc)))))

Theorem: vl-modinstlist-p-of-vl-simple-instantiate-list

(defthm vl-modinstlist-p-of-vl-simple-instantiate-list
  (b*
   ((insts (vl-simple-instantiate-list-fn x prefix arglists n loc)))
   (vl-modinstlist-p insts))
  :rule-classes :rewrite)

Theorem: vl-simple-instantiate-list-fn-of-vl-module-fix-x

(defthm vl-simple-instantiate-list-fn-of-vl-module-fix-x
  (equal (vl-simple-instantiate-list-fn (vl-module-fix x)
                                        prefix arglists n loc)
         (vl-simple-instantiate-list-fn x prefix arglists n loc)))

Theorem: vl-simple-instantiate-list-fn-vl-module-equiv-congruence-on-x

(defthm
      vl-simple-instantiate-list-fn-vl-module-equiv-congruence-on-x
 (implies
  (vl-module-equiv x x-equiv)
  (equal
     (vl-simple-instantiate-list-fn x prefix arglists n loc)
     (vl-simple-instantiate-list-fn x-equiv prefix arglists n loc)))
 :rule-classes :congruence)

Theorem: vl-simple-instantiate-list-fn-of-str-fix-prefix

(defthm vl-simple-instantiate-list-fn-of-str-fix-prefix
  (equal (vl-simple-instantiate-list-fn x (str-fix prefix)
                                        arglists n loc)
         (vl-simple-instantiate-list-fn x prefix arglists n loc)))

Theorem: vl-simple-instantiate-list-fn-streqv-congruence-on-prefix

(defthm vl-simple-instantiate-list-fn-streqv-congruence-on-prefix
 (implies
  (streqv prefix prefix-equiv)
  (equal
     (vl-simple-instantiate-list-fn x prefix arglists n loc)
     (vl-simple-instantiate-list-fn x prefix-equiv arglists n loc)))
 :rule-classes :congruence)

Theorem: vl-simple-instantiate-list-fn-of-vl-exprlistlist-fix-arglists

(defthm
      vl-simple-instantiate-list-fn-of-vl-exprlistlist-fix-arglists
  (equal (vl-simple-instantiate-list-fn
              x prefix (vl-exprlistlist-fix arglists)
              n loc)
         (vl-simple-instantiate-list-fn x prefix arglists n loc)))

Theorem: vl-simple-instantiate-list-fn-vl-exprlistlist-equiv-congruence-on-arglists

(defthm
 vl-simple-instantiate-list-fn-vl-exprlistlist-equiv-congruence-on-arglists
 (implies
  (vl-exprlistlist-equiv arglists arglists-equiv)
  (equal
     (vl-simple-instantiate-list-fn x prefix arglists n loc)
     (vl-simple-instantiate-list-fn x prefix arglists-equiv n loc)))
 :rule-classes :congruence)

Theorem: vl-simple-instantiate-list-fn-of-nfix-n

(defthm vl-simple-instantiate-list-fn-of-nfix-n
  (equal (vl-simple-instantiate-list-fn x prefix arglists (nfix n)
                                        loc)
         (vl-simple-instantiate-list-fn x prefix arglists n loc)))

Theorem: vl-simple-instantiate-list-fn-nat-equiv-congruence-on-n

(defthm vl-simple-instantiate-list-fn-nat-equiv-congruence-on-n
 (implies
  (acl2::nat-equiv n n-equiv)
  (equal
     (vl-simple-instantiate-list-fn x prefix arglists n loc)
     (vl-simple-instantiate-list-fn x prefix arglists n-equiv loc)))
 :rule-classes :congruence)

Theorem: vl-simple-instantiate-list-fn-of-vl-location-fix-loc

(defthm vl-simple-instantiate-list-fn-of-vl-location-fix-loc
  (equal (vl-simple-instantiate-list-fn
              x
              prefix arglists n (vl-location-fix loc))
         (vl-simple-instantiate-list-fn x prefix arglists n loc)))

Theorem: vl-simple-instantiate-list-fn-vl-location-equiv-congruence-on-loc

(defthm
  vl-simple-instantiate-list-fn-vl-location-equiv-congruence-on-loc
 (implies
  (vl-location-equiv loc loc-equiv)
  (equal
     (vl-simple-instantiate-list-fn x prefix arglists n loc)
     (vl-simple-instantiate-list-fn x prefix arglists n loc-equiv)))
 :rule-classes :congruence)