		Search-engine friendly clone of the ACL2 documentation.

Vl-lexscopes

Vl-lexscopes-wild-import-names

Extend the lexscopes with a wildcard import of a list of names.

Signature
(vl-lexscopes-wild-import-names pkgname pkg-item-alist scopes ctx warnings) → (mv scopes warnings)
Arguments: pkgname — Name of the package being imported from.
Guard (stringp pkgname).; pkg-item-alist — Goofy, we only care about the names, but we take the whole alist to reuse vl-package-scope-item-alist.; scopes — Guard (vl-lexscopes-p scopes).; ctx — Guard (vl-import-p ctx).; warnings — Guard (vl-warninglist-p warnings).
Returns: scopes — Type (vl-lexscopes-p scopes).; warnings — Type (vl-warninglist-p warnings).

Definitions and Theorems

Function: vl-lexscopes-wild-import-names

(defun vl-lexscopes-wild-import-names
       (pkgname pkg-item-alist scopes ctx warnings)
 (declare (xargs :guard (and (stringp pkgname)
                             (vl-lexscopes-p scopes)
                             (vl-import-p ctx)
                             (vl-warninglist-p warnings))))
 (declare (ignorable ctx))
 (declare (xargs :guard (string-listp (alist-keys pkg-item-alist))))
 (let ((__function__ 'vl-lexscopes-wild-import-names))
  (declare (ignorable __function__))
  (b* (((when (atom pkg-item-alist))
        (mv (vl-lexscopes-fix scopes)
            (vl-warninglist-fix warnings)))
       ((when (atom (car pkg-item-alist)))
        (vl-lexscopes-wild-import-names pkgname (cdr pkg-item-alist)
                                        scopes ctx warnings))
       ((mv scopes warnings)
        (vl-lexscopes-wild-import-name pkgname (caar pkg-item-alist)
                                       scopes ctx warnings)))
    (vl-lexscopes-wild-import-names pkgname (cdr pkg-item-alist)
                                    scopes ctx warnings))))

Theorem: vl-lexscopes-p-of-vl-lexscopes-wild-import-names.scopes

(defthm vl-lexscopes-p-of-vl-lexscopes-wild-import-names.scopes
  (b* (((mv ?scopes ?warnings)
        (vl-lexscopes-wild-import-names
             pkgname
             pkg-item-alist scopes ctx warnings)))
    (vl-lexscopes-p scopes))
  :rule-classes :rewrite)

Theorem: vl-warninglist-p-of-vl-lexscopes-wild-import-names.warnings

(defthm vl-warninglist-p-of-vl-lexscopes-wild-import-names.warnings
  (b* (((mv ?scopes ?warnings)
        (vl-lexscopes-wild-import-names
             pkgname
             pkg-item-alist scopes ctx warnings)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: vl-lexscopes-wild-import-names-of-str-fix-pkgname

(defthm vl-lexscopes-wild-import-names-of-str-fix-pkgname
  (equal (vl-lexscopes-wild-import-names
              (str-fix pkgname)
              pkg-item-alist scopes ctx warnings)
         (vl-lexscopes-wild-import-names
              pkgname
              pkg-item-alist scopes ctx warnings)))

Theorem: vl-lexscopes-wild-import-names-streqv-congruence-on-pkgname

(defthm vl-lexscopes-wild-import-names-streqv-congruence-on-pkgname
  (implies (streqv pkgname pkgname-equiv)
           (equal (vl-lexscopes-wild-import-names
                       pkgname
                       pkg-item-alist scopes ctx warnings)
                  (vl-lexscopes-wild-import-names
                       pkgname-equiv
                       pkg-item-alist scopes ctx warnings)))
  :rule-classes :congruence)

Theorem: vl-lexscopes-wild-import-names-of-vl-lexscopes-fix-scopes

(defthm vl-lexscopes-wild-import-names-of-vl-lexscopes-fix-scopes
  (equal (vl-lexscopes-wild-import-names
              pkgname
              pkg-item-alist (vl-lexscopes-fix scopes)
              ctx warnings)
         (vl-lexscopes-wild-import-names
              pkgname
              pkg-item-alist scopes ctx warnings)))

Theorem: vl-lexscopes-wild-import-names-vl-lexscopes-equiv-congruence-on-scopes

(defthm
 vl-lexscopes-wild-import-names-vl-lexscopes-equiv-congruence-on-scopes
 (implies
   (vl-lexscopes-equiv scopes scopes-equiv)
   (equal
        (vl-lexscopes-wild-import-names
             pkgname
             pkg-item-alist scopes ctx warnings)
        (vl-lexscopes-wild-import-names pkgname pkg-item-alist
                                        scopes-equiv ctx warnings)))
 :rule-classes :congruence)

Theorem: vl-lexscopes-wild-import-names-of-vl-import-fix-ctx

(defthm vl-lexscopes-wild-import-names-of-vl-import-fix-ctx
  (equal (vl-lexscopes-wild-import-names pkgname pkg-item-alist
                                         scopes (vl-import-fix ctx)
                                         warnings)
         (vl-lexscopes-wild-import-names
              pkgname
              pkg-item-alist scopes ctx warnings)))

Theorem: vl-lexscopes-wild-import-names-vl-import-equiv-congruence-on-ctx

(defthm
   vl-lexscopes-wild-import-names-vl-import-equiv-congruence-on-ctx
 (implies
   (vl-import-equiv ctx ctx-equiv)
   (equal
        (vl-lexscopes-wild-import-names
             pkgname
             pkg-item-alist scopes ctx warnings)
        (vl-lexscopes-wild-import-names pkgname pkg-item-alist
                                        scopes ctx-equiv warnings)))
 :rule-classes :congruence)

Theorem: vl-lexscopes-wild-import-names-of-vl-warninglist-fix-warnings

(defthm
      vl-lexscopes-wild-import-names-of-vl-warninglist-fix-warnings
 (equal
  (vl-lexscopes-wild-import-names pkgname pkg-item-alist scopes
                                  ctx (vl-warninglist-fix warnings))
  (vl-lexscopes-wild-import-names
       pkgname
       pkg-item-alist scopes ctx warnings)))

Theorem: vl-lexscopes-wild-import-names-vl-warninglist-equiv-congruence-on-warnings

(defthm
 vl-lexscopes-wild-import-names-vl-warninglist-equiv-congruence-on-warnings
 (implies
   (vl-warninglist-equiv warnings warnings-equiv)
   (equal
        (vl-lexscopes-wild-import-names
             pkgname
             pkg-item-alist scopes ctx warnings)
        (vl-lexscopes-wild-import-names pkgname pkg-item-alist
                                        scopes ctx warnings-equiv)))
 :rule-classes :congruence)