		Search-engine friendly clone of the ACL2 documentation.

Scopestack

Vl-importlist->explicit-item-alist

Signature
(vl-importlist->explicit-item-alist x design acc) → alist
Arguments: x — Guard (vl-importlist-p x).; design — Guard (vl-maybe-design-p design).
Returns: alist — Type (implies (vl-importresult-alist-p acc) (vl-importresult-alist-p alist)) .

Definitions and Theorems

Function: vl-importlist->explicit-item-alist

(defun vl-importlist->explicit-item-alist (x design acc)
 (declare (xargs :guard (and (vl-importlist-p x)
                             (vl-maybe-design-p design))))
 (let ((__function__ 'vl-importlist->explicit-item-alist))
  (declare (ignorable __function__))
  (b*
   (((when (atom x)) acc)
    ((vl-import x1) (car x))
    ((unless (stringp x1.part))
     (vl-importlist->explicit-item-alist (cdr x)
                                         design acc))
    (package
     (and
       design
       (cdr (hons-get x1.pkg
                      (vl-design-scope-package-alist-top design)))))
    (item
     (and
       package
       (cdr (hons-get x1.part
                      (vl-package-scope-item-alist-top package))))))
   (hons-acons x1.part
               (make-vl-importresult :item item
                                     :pkg-name x1.pkg
                                     :loc x1.loc)
               (vl-importlist->explicit-item-alist (cdr x)
                                                   design acc)))))

Theorem: return-type-of-vl-importlist->explicit-item-alist

(defthm return-type-of-vl-importlist->explicit-item-alist
  (b* ((alist (vl-importlist->explicit-item-alist x design acc)))
    (implies (vl-importresult-alist-p acc)
             (vl-importresult-alist-p alist)))
  :rule-classes :rewrite)

Theorem: vl-importlist->explicit-item-alist-lookup-acc-elim

(defthm vl-importlist->explicit-item-alist-lookup-acc-elim
 (implies
  (syntaxp (not (equal acc ''nil)))
  (equal (hons-assoc-equal
              name
              (vl-importlist->explicit-item-alist x design acc))
         (or (hons-assoc-equal
                  name
                  (vl-importlist->explicit-item-alist x design nil))
             (hons-assoc-equal name acc)))))

Theorem: vl-importlist->explicit-item-alist-correct

(defthm vl-importlist->explicit-item-alist-correct
 (implies
     (stringp name)
     (equal (hons-assoc-equal
                 name
                 (vl-importlist->explicit-item-alist x design nil))
            (b* (((mv pkg item loc)
                  (vl-importlist-find-explicit-item name x design)))
              (and pkg
                   (cons name
                         (make-vl-importresult :item item
                                               :pkg-name pkg
                                               :loc loc)))))))

Theorem: vl-importlist->explicit-item-alist-of-vl-importlist-fix-x

(defthm vl-importlist->explicit-item-alist-of-vl-importlist-fix-x
  (equal (vl-importlist->explicit-item-alist (vl-importlist-fix x)
                                             design acc)
         (vl-importlist->explicit-item-alist x design acc)))

Theorem: vl-importlist->explicit-item-alist-vl-importlist-equiv-congruence-on-x

(defthm
 vl-importlist->explicit-item-alist-vl-importlist-equiv-congruence-on-x
 (implies
    (vl-importlist-equiv x x-equiv)
    (equal (vl-importlist->explicit-item-alist x design acc)
           (vl-importlist->explicit-item-alist x-equiv design acc)))
 :rule-classes :congruence)

Theorem: vl-importlist->explicit-item-alist-of-vl-maybe-design-fix-design

(defthm
   vl-importlist->explicit-item-alist-of-vl-maybe-design-fix-design
 (equal
  (vl-importlist->explicit-item-alist x (vl-maybe-design-fix design)
                                      acc)
  (vl-importlist->explicit-item-alist x design acc)))

Theorem: vl-importlist->explicit-item-alist-vl-maybe-design-equiv-congruence-on-design

(defthm
 vl-importlist->explicit-item-alist-vl-maybe-design-equiv-congruence-on-design
 (implies
    (vl-maybe-design-equiv design design-equiv)
    (equal (vl-importlist->explicit-item-alist x design acc)
           (vl-importlist->explicit-item-alist x design-equiv acc)))
 :rule-classes :congruence)