		Search-engine friendly clone of the ACL2 documentation.

Shadowcheck

Vl-shadowcheck-design

Signature
(vl-shadowcheck-design x) → new-x
Arguments: x — Guard (vl-design-p x).
Returns: new-x — Type (vl-design-p new-x).

Definitions and Theorems

Function: vl-shadowcheck-design

(defun vl-shadowcheck-design (x)
  (declare (xargs :guard (vl-design-p x)))
  (let ((__function__ 'vl-shadowcheck-design))
    (declare (ignorable __function__))
    (b* (((vl-design x))
         (warnings x.warnings)
         (st (make-vl-shadowcheck-state
                  :lexscopes (list (vl-empty-lexscope))
                  :ss (vl-scopestack-init x)
                  :design x))
         (itemnames (append (vl-vardecllist->names x.vardecls)
                            (vl-paramdecllist->names x.paramdecls)
                            (vl-fundecllist->names x.fundecls)
                            (vl-taskdecllist->names x.taskdecls)
                            (vl-typedeflist->names x.typedefs)))
         (dupes (duplicated-members itemnames))
         (warnings (if (not dupes)
                       (ok)
                     (fatal :type :vl-name-clash
                            :msg "Name clash among globals: ~&0."
                            :args (list dupes))))
         ((mv st warnings)
          (vl-shadowcheck-declare-typedefs x.typedefs st warnings))
         ((mv st warnings)
          (vl-shadowcheck-vardecls x.vardecls st warnings))
         ((mv st warnings)
          (vl-shadowcheck-paramdecls x.paramdecls st warnings))
         ((mv st warnings)
          (vl-shadowcheck-fundecls x.fundecls st warnings))
         ((mv st warnings)
          (vl-shadowcheck-taskdecls x.taskdecls st warnings))
         ((mv st warnings)
          (vl-shadowcheck-imports x.imports st warnings))
         ((mv st mods)
          (vl-shadowcheck-modules x.mods st))
         (?st (vl-shadowcheck-pop-scope st))
         (- (vl-scopestacks-free)))
      (change-vl-design x
                        :mods mods
                        :warnings warnings))))

Theorem: vl-design-p-of-vl-shadowcheck-design

(defthm vl-design-p-of-vl-shadowcheck-design
  (b* ((new-x (vl-shadowcheck-design x)))
    (vl-design-p new-x))
  :rule-classes :rewrite)

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

(defthm vl-shadowcheck-design-of-vl-design-fix-x
  (equal (vl-shadowcheck-design (vl-design-fix x))
         (vl-shadowcheck-design x)))

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

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