		Search-engine friendly clone of the ACL2 documentation.

Check-namespace

Vl-module-check-namespace

Signature
(vl-module-check-namespace x) → new-x
Arguments: x — Guard (vl-module-p x).
Returns: new-x — Perhaps extended with warnings.
Type (vl-module-p new-x).

Definitions and Theorems

Function: vl-module-check-namespace

(defun vl-module-check-namespace (x)
 (declare (xargs :guard (vl-module-p x)))
 (let ((__function__ 'vl-module-check-namespace))
  (declare (ignorable __function__))
  (b*
   (((vl-module x) (vl-module-fix x))
    (warnings x.warnings)
    (portdupes
     (duplicated-members (remove nil (vl-portlist->names x.ports))))
    (warnings (if portdupes (fatal :type :vl-bad-ports
                                   :msg "Duplicate port names: ~&0."
                                   :args (list portdupes))
                warnings))
    (pdnames (vl-portdecllist->names x.portdecls))
    (pdnames-s (mergesort pdnames))
    (warnings (if (mbe :logic (no-duplicatesp-equal pdnames)
                       :exec (same-lengthp pdnames pdnames-s))
                  warnings
                (fatal :type :vl-bad-portdecls
                       :msg "Duplicate port declaration names: ~&0."
                       :args (list (duplicated-members pdnames)))))
    (namespace (vl-module->modnamespace x))
    (namespace-s (mergesort namespace))
    (warnings
         (if (mbe :logic (no-duplicatesp-equal namespace)
                  :exec (same-lengthp namespace namespace-s))
             warnings
           (fatal :type :vl-namespace-error
                  :msg "Illegal redefinition of ~&0."
                  :args (list (duplicated-members namespace)))))
    (ss (vl-scopestack-push x (vl-scopestack-null)))
    (warnings
         (append-without-guard
              (vl-check-portdecl-overlap-compatible x.portdecls ss)
              warnings)))
   (change-vl-module x
                     :warnings warnings))))

Theorem: vl-module-p-of-vl-module-check-namespace

(defthm vl-module-p-of-vl-module-check-namespace
  (b* ((new-x (vl-module-check-namespace x)))
    (vl-module-p new-x))
  :rule-classes :rewrite)

Theorem: vl-module-check-namespace-of-vl-module-fix-x

(defthm vl-module-check-namespace-of-vl-module-fix-x
  (equal (vl-module-check-namespace (vl-module-fix x))
         (vl-module-check-namespace x)))

Theorem: vl-module-check-namespace-vl-module-equiv-congruence-on-x

(defthm vl-module-check-namespace-vl-module-equiv-congruence-on-x
  (implies (vl-module-equiv x x-equiv)
           (equal (vl-module-check-namespace x)
                  (vl-module-check-namespace x-equiv)))
  :rule-classes :congruence)