		Search-engine friendly clone of the ACL2 documentation.

Scopestack

Vl-scope-find-item

Look up a plain identifier to find an item in a scope.

Signature
(vl-scope-find-item name scope design) → (mv pkg-name item)
Arguments: name — Guard (stringp name).; scope — Guard (vl-scope-p scope).; design — Guard (vl-maybe-design-p design).
Returns: pkg-name — The name of the package where the item was found, if applicable.
Type (iff (stringp pkg-name) pkg-name).; item — The declaration object for the given name, if found.
Type (iff (vl-scopeitem-p item) item).

Definitions and Theorems

Function: vl-scope-find-item

(defun vl-scope-find-item (name scope design)
 (declare (xargs :guard (and (stringp name)
                             (vl-scope-p scope)
                             (vl-maybe-design-p design))))
 (let ((__function__ 'vl-scope-find-item))
  (declare (ignorable __function__))
  (b* ((scope (vl-scope-fix scope)))
   (case
    (tag scope)
    (:vl-interface
     (b* (((vl-interface scope :quietp t))
          (item (vl-interface-scope-find-item name scope))
          ((when item) (mv nil item))
          ((mv pkg item)
           (vl-importlist-find-explicit-item
                name scope.imports design))
          ((when (or pkg item)) (mv pkg item)))
      (vl-importlist-find-implicit-item name scope.imports design)))
    (:vl-module
     (b* (((vl-module scope :quietp t))
          (item (vl-module-scope-find-item name scope))
          ((when item) (mv nil item))
          ((mv pkg item)
           (vl-importlist-find-explicit-item
                name scope.imports design))
          ((when (or pkg item)) (mv pkg item)))
      (vl-importlist-find-implicit-item name scope.imports design)))
    (:vl-genblob
     (b* (((vl-genblob scope :quietp t))
          (item (vl-genblob-scope-find-item name scope))
          ((when item) (mv nil item))
          ((mv pkg item)
           (vl-importlist-find-explicit-item
                name scope.imports design))
          ((when (or pkg item)) (mv pkg item)))
      (vl-importlist-find-implicit-item name scope.imports design)))
    (:vl-blockscope
     (b* (((vl-blockscope scope :quietp t))
          (item (vl-blockscope-scope-find-item name scope))
          ((when item) (mv nil item))
          ((mv pkg item)
           (vl-importlist-find-explicit-item
                name scope.imports design))
          ((when (or pkg item)) (mv pkg item)))
      (vl-importlist-find-implicit-item name scope.imports design)))
    (:vl-design
     (b* (((vl-design scope :quietp t))
          (item (vl-design-scope-find-item name scope))
          ((when item) (mv nil item))
          ((mv pkg item)
           (vl-importlist-find-explicit-item
                name scope.imports design))
          ((when (or pkg item)) (mv pkg item)))
      (vl-importlist-find-implicit-item name scope.imports design)))
    (:vl-package
     (b* (((vl-package scope :quietp t))
          (item (vl-package-scope-find-item name scope))
          ((when item) (mv nil item))
          ((mv pkg item)
           (vl-importlist-find-explicit-item
                name scope.imports design))
          ((when (or pkg item)) (mv pkg item)))
      (vl-importlist-find-implicit-item name scope.imports design)))
    (:vl-scopeinfo (vl-scopeinfo-find-item name scope design))
    (otherwise (mv nil nil))))))

Theorem: return-type-of-vl-scope-find-item.pkg-name

(defthm return-type-of-vl-scope-find-item.pkg-name
  (b* (((mv ?pkg-name ?item)
        (vl-scope-find-item name scope design)))
    (iff (stringp pkg-name) pkg-name))
  :rule-classes :rewrite)

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

(defthm return-type-of-vl-scope-find-item.item
  (b* (((mv ?pkg-name ?item)
        (vl-scope-find-item name scope design)))
    (iff (vl-scopeitem-p item) item))
  :rule-classes :rewrite)

Theorem: maybe-string-type-of-vl-scope-find-item-pkg-name

(defthm maybe-string-type-of-vl-scope-find-item-pkg-name
  (b* (((mv ?pkg-name ?item)
        (vl-scope-find-item name scope design)))
    (or (stringp pkg-name) (not pkg-name)))
  :rule-classes :type-prescription)

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

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

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

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

Theorem: vl-scope-find-item-of-vl-scope-fix-scope

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

Theorem: vl-scope-find-item-vl-scope-equiv-congruence-on-scope

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

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

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

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

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