		Search-engine friendly clone of the ACL2 documentation.

Scopestack

Vl-scopeinfo-find-item

Signature
(vl-scopeinfo-find-item name x design) → (mv package item)
Arguments: name — Guard (stringp name).; x — Guard (vl-scopeinfo-p x).; design — Guard (vl-maybe-design-p design).
Returns: package — Type (iff (stringp package) package).; item — Type (iff (vl-scopeitem-p item) item).

Definitions and Theorems

Function: vl-scopeinfo-find-item

(defun
 vl-scopeinfo-find-item (name x design)
 (declare (xargs :guard (and (stringp name)
                             (vl-scopeinfo-p x)
                             (vl-maybe-design-p design))))
 (let ((__function__ 'vl-scopeinfo-find-item))
      (declare (ignorable __function__))
      (b* (((vl-scopeinfo x))
           (name (string-fix name))
           (local-item (cdr (hons-get name x.locals)))
           ((when local-item) (mv nil local-item))
           (import-item (cdr (hons-get name x.imports)))
           ((when import-item)
            (mv (vl-importresult->pkg-name import-item)
                (vl-importresult->item import-item))))
          (vl-import-stars-find-item name x.star-packages design))))

Theorem: return-type-of-vl-scopeinfo-find-item.package

(defthm return-type-of-vl-scopeinfo-find-item.package
        (b* (((mv common-lisp::?package ?item)
              (vl-scopeinfo-find-item name x design)))
            (iff (stringp package) package))
        :rule-classes :rewrite)

Theorem: return-type-of-vl-scopeinfo-find-item.item

(defthm return-type-of-vl-scopeinfo-find-item.item
        (b* (((mv common-lisp::?package ?item)
              (vl-scopeinfo-find-item name x design)))
            (iff (vl-scopeitem-p item) item))
        :rule-classes :rewrite)

Theorem: vl-scopeinfo-find-item-of-str-fix-name

(defthm vl-scopeinfo-find-item-of-str-fix-name
        (equal (vl-scopeinfo-find-item (str-fix name)
                                       x design)
               (vl-scopeinfo-find-item name x design)))

Theorem: vl-scopeinfo-find-item-streqv-congruence-on-name

(defthm
     vl-scopeinfo-find-item-streqv-congruence-on-name
     (implies (streqv name name-equiv)
              (equal (vl-scopeinfo-find-item name x design)
                     (vl-scopeinfo-find-item name-equiv x design)))
     :rule-classes :congruence)

Theorem: vl-scopeinfo-find-item-of-vl-scopeinfo-fix-x

(defthm vl-scopeinfo-find-item-of-vl-scopeinfo-fix-x
        (equal (vl-scopeinfo-find-item name (vl-scopeinfo-fix x)
                                       design)
               (vl-scopeinfo-find-item name x design)))

Theorem: vl-scopeinfo-find-item-vl-scopeinfo-equiv-congruence-on-x

(defthm
     vl-scopeinfo-find-item-vl-scopeinfo-equiv-congruence-on-x
     (implies (vl-scopeinfo-equiv x x-equiv)
              (equal (vl-scopeinfo-find-item name x design)
                     (vl-scopeinfo-find-item name x-equiv design)))
     :rule-classes :congruence)

Theorem: vl-scopeinfo-find-item-of-vl-maybe-design-fix-design

(defthm
 vl-scopeinfo-find-item-of-vl-maybe-design-fix-design
 (equal (vl-scopeinfo-find-item name x (vl-maybe-design-fix design))
        (vl-scopeinfo-find-item name x design)))

Theorem: vl-scopeinfo-find-item-vl-maybe-design-equiv-congruence-on-design

(defthm
   vl-scopeinfo-find-item-vl-maybe-design-equiv-congruence-on-design
   (implies (vl-maybe-design-equiv design design-equiv)
            (equal (vl-scopeinfo-find-item name x design)
                   (vl-scopeinfo-find-item name x design-equiv)))
   :rule-classes :congruence)