		Search-engine friendly clone of the ACL2 documentation.

Delayredux

Vl-module-delayredux

Signature
(vl-module-delayredux x &key vecp state-onlyp) → (mv new-x addmods)
Arguments: x — Guard (vl-module-p x).
Returns: new-x — Type (vl-module-p new-x), given the guard.; addmods — Type (vl-modulelist-p addmods), given the guard.

Definitions and Theorems

Function: vl-module-delayredux-fn

(defun vl-module-delayredux-fn (x vecp state-onlyp)
  (declare (xargs :guard (vl-module-p x)))
  (let ((__function__ 'vl-module-delayredux))
    (declare (ignorable __function__))
    (b* (((vl-module x) x)
         ((when (vl-module->hands-offp x))
          (mv x nil))
         (delta (vl-starting-delta x))
         (delta (change-vl-delta delta
                                 :vardecls x.vardecls
                                 :modinsts x.modinsts))
         ((mv assigns delta)
          (vl-assignlist-delayredux x.assigns delta
                                    :vecp vecp
                                    :state-onlyp state-onlyp))
         ((mv gateinsts delta)
          (vl-gateinstlist-delayredux x.gateinsts delta
                                      :vecp vecp
                                      :state-onlyp state-onlyp))
         ((vl-delta delta) (vl-free-delta delta))
         (new-x (change-vl-module x
                                  :vardecls delta.vardecls
                                  :modinsts delta.modinsts
                                  :warnings delta.warnings
                                  :assigns assigns
                                  :gateinsts gateinsts)))
      (mv new-x delta.addmods))))

Theorem: vl-module-p-of-vl-module-delayredux.new-x

(defthm vl-module-p-of-vl-module-delayredux.new-x
  (implies (and (force (vl-module-p x)))
           (b* (((mv ?new-x ?addmods)
                 (vl-module-delayredux-fn x vecp state-onlyp)))
             (vl-module-p new-x)))
  :rule-classes :rewrite)

Theorem: vl-modulelist-p-of-vl-module-delayredux.addmods

(defthm vl-modulelist-p-of-vl-module-delayredux.addmods
  (implies (and (force (vl-module-p x)))
           (b* (((mv ?new-x ?addmods)
                 (vl-module-delayredux-fn x vecp state-onlyp)))
             (vl-modulelist-p addmods)))
  :rule-classes :rewrite)

Theorem: vl-module->name-of-vl-module-delayredux

(defthm vl-module->name-of-vl-module-delayredux
 (equal
      (vl-module->name
           (mv-nth 0
                   (vl-module-delayredux x
                                         :vecp vecp
                                         :state-onlyp state-onlyp)))
      (vl-module->name x)))