		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 ?loc)
        (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 ?loc)
        (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-class
     (b*
      (((vl-class scope :quietp t))
       (item (vl-class-scope-find-item name scope))
       ((when item) (mv nil item))
       ((mv pkg item ?loc)
        (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 ?loc)
        (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 ?loc)
        (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 ?loc)
        (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 ?loc)
        (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)