		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))
       (x.loaditems (and x.parse-temps
                         (vl-parse-temps->loaditems x.parse-temps)))
       (x.initial-imports
            (and x.parse-temps
                 (vl-parse-temps->imports x.parse-temps)))
       (- (vl-shadowcheck-debug "*** Shadowcheck module ~s0 ***~%"
                                x.name))
       (warnings x.warnings)
       ((mv st warnings)
        (vl-shadowcheck-push-scope x st warnings))
       ((mv st warnings)
        (vl-shadowcheck-imports x.initial-imports st warnings))
       ((mv st warnings)
        (vl-shadowcheck-ports x.ports st warnings))
       ((mv st warnings)
        (vl-shadowcheck-genelementlist x.loaditems st warnings))
       (st (vl-shadowcheck-pop-scope st))
       (new-x (change-vl-module x
                                :warnings warnings)))
    (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)