		Search-engine friendly clone of the ACL2 documentation.

Gate-elim

Vl-gateinstlist-gate-elim

Extends vl-gateinst-gate-elim to a list of gate instances.

Signature
(vl-gateinstlist-gate-elim x primalist warnings) → (mv warnings gateinsts modinsts addmods)
Arguments: x — Guard (vl-gateinstlist-p x).; primalist — Mapping from gate types to primitive modules.
Guard (vl-primalist-p primalist).; warnings — Guard (vl-warninglist-p warnings).
Returns: warnings — Type (vl-warninglist-p warnings).; gateinsts — Type (vl-gateinstlist-p gateinsts), given (force (vl-gateinstlist-p x)).; modinsts — Type (vl-modinstlist-p modinsts), given (force (vl-gateinstlist-p x)).; addmods — Type (vl-modulelist-p addmods), given (force (vl-gateinstlist-p x)).

Definitions and Theorems

Function: vl-gateinstlist-gate-elim

(defun vl-gateinstlist-gate-elim (x primalist warnings)
  (declare (xargs :guard (and (vl-gateinstlist-p x)
                              (vl-primalist-p primalist)
                              (vl-warninglist-p warnings))))
  (let ((__function__ 'vl-gateinstlist-gate-elim))
    (declare (ignorable __function__))
    (b* (((when (atom x)) (mv (ok) nil nil nil))
         ((mv warnings
              car-gateinsts car-modinsts car-addmods)
          (vl-gateinst-gate-elim (car x)
                                 primalist warnings))
         ((mv warnings
              cdr-gateinsts cdr-modinsts cdr-addmods)
          (vl-gateinstlist-gate-elim (cdr x)
                                     primalist warnings)))
      (mv warnings
          (append car-gateinsts cdr-gateinsts)
          (append car-modinsts cdr-modinsts)
          (append car-addmods cdr-addmods)))))

Theorem: vl-warninglist-p-of-vl-gateinstlist-gate-elim.warnings

(defthm vl-warninglist-p-of-vl-gateinstlist-gate-elim.warnings
  (b* (((mv ?warnings ?gateinsts ?modinsts ?addmods)
        (vl-gateinstlist-gate-elim x primalist warnings)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: vl-gateinstlist-p-of-vl-gateinstlist-gate-elim.gateinsts

(defthm vl-gateinstlist-p-of-vl-gateinstlist-gate-elim.gateinsts
  (implies (force (vl-gateinstlist-p x))
           (b* (((mv ?warnings ?gateinsts ?modinsts ?addmods)
                 (vl-gateinstlist-gate-elim x primalist warnings)))
             (vl-gateinstlist-p gateinsts)))
  :rule-classes :rewrite)

Theorem: vl-modinstlist-p-of-vl-gateinstlist-gate-elim.modinsts

(defthm vl-modinstlist-p-of-vl-gateinstlist-gate-elim.modinsts
  (implies (force (vl-gateinstlist-p x))
           (b* (((mv ?warnings ?gateinsts ?modinsts ?addmods)
                 (vl-gateinstlist-gate-elim x primalist warnings)))
             (vl-modinstlist-p modinsts)))
  :rule-classes :rewrite)

Theorem: vl-modulelist-p-of-vl-gateinstlist-gate-elim.addmods

(defthm vl-modulelist-p-of-vl-gateinstlist-gate-elim.addmods
  (implies (force (vl-gateinstlist-p x))
           (b* (((mv ?warnings ?gateinsts ?modinsts ?addmods)
                 (vl-gateinstlist-gate-elim x primalist warnings)))
             (vl-modulelist-p addmods)))
  :rule-classes :rewrite)

Theorem: vl-gateinstlist-gate-elim-mvtypes-1

(defthm vl-gateinstlist-gate-elim-mvtypes-1
  (true-listp
       (mv-nth 1
               (vl-gateinstlist-gate-elim x primalist warnings)))
  :rule-classes :type-prescription)

Theorem: vl-gateinstlist-gate-elim-mvtypes-2

(defthm vl-gateinstlist-gate-elim-mvtypes-2
  (true-listp
       (mv-nth 2
               (vl-gateinstlist-gate-elim x primalist warnings)))
  :rule-classes :type-prescription)

Theorem: vl-gateinstlist-gate-elim-mvtypes-3

(defthm vl-gateinstlist-gate-elim-mvtypes-3
  (true-listp
       (mv-nth 3
               (vl-gateinstlist-gate-elim x primalist warnings)))
  :rule-classes :type-prescription)