		Search-engine friendly clone of the ACL2 documentation.

Shadowcheck

Vl-shadowcheck-module

Signature
(vl-shadowcheck-module x st) → (mv st new-x)
Arguments: x — Guard (vl-module-p x).; st — Guard (vl-shadowcheck-state-p st).
Returns: st — Type (vl-shadowcheck-state-p st).; new-x — Type (vl-module-p new-x).

Definitions and Theorems

Function: vl-shadowcheck-module

(defun vl-shadowcheck-module (x st)
  (declare (xargs :guard (and (vl-module-p x)
                              (vl-shadowcheck-state-p st))))
  (let ((__function__ 'vl-shadowcheck-module))
    (declare (ignorable __function__))
    (b* (((vl-module x) (vl-module-fix x))
         (- (vl-shadowcheck-debug "*** Shadowcheck module ~s0 ***~%"
                                  x.name))
         (warnings x.warnings)
         (st (vl-shadowcheck-push-scope x st))
         ((mv st warnings)
          (vl-shadowcheck-ports x.ports st warnings))
         ((mv st warnings)
          (vl-shadowcheck-aux x.loaditems st warnings))
         (st (vl-shadowcheck-pop-scope st))
         (new-x (change-vl-module x
                                  :warnings warnings
                                  :loaditems nil)))
      (mv st new-x))))

Theorem: vl-shadowcheck-state-p-of-vl-shadowcheck-module.st

(defthm vl-shadowcheck-state-p-of-vl-shadowcheck-module.st
  (b* (((mv ?st ?new-x)
        (vl-shadowcheck-module x st)))
    (vl-shadowcheck-state-p st))
  :rule-classes :rewrite)

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

(defthm vl-module-p-of-vl-shadowcheck-module.new-x
  (b* (((mv ?st ?new-x)
        (vl-shadowcheck-module x st)))
    (vl-module-p new-x))
  :rule-classes :rewrite)

Theorem: vl-shadowcheck-module-of-vl-module-fix-x

(defthm vl-shadowcheck-module-of-vl-module-fix-x
  (equal (vl-shadowcheck-module (vl-module-fix x)
                                st)
         (vl-shadowcheck-module x st)))

Theorem: vl-shadowcheck-module-vl-module-equiv-congruence-on-x

(defthm vl-shadowcheck-module-vl-module-equiv-congruence-on-x
  (implies (vl-module-equiv x x-equiv)
           (equal (vl-shadowcheck-module x st)
                  (vl-shadowcheck-module x-equiv st)))
  :rule-classes :congruence)

Theorem: vl-shadowcheck-module-of-vl-shadowcheck-state-fix-st

(defthm vl-shadowcheck-module-of-vl-shadowcheck-state-fix-st
  (equal (vl-shadowcheck-module x (vl-shadowcheck-state-fix st))
         (vl-shadowcheck-module x st)))

Theorem: vl-shadowcheck-module-vl-shadowcheck-state-equiv-congruence-on-st

(defthm
  vl-shadowcheck-module-vl-shadowcheck-state-equiv-congruence-on-st
  (implies (vl-shadowcheck-state-equiv st st-equiv)
           (equal (vl-shadowcheck-module x st)
                  (vl-shadowcheck-module x st-equiv)))
  :rule-classes :congruence)