		Search-engine friendly clone of the ACL2 documentation.

Vl-lexscopes

Vl-lexscopes-find

Recursively look up a name, going from inner to outer lexical scopes.

Signature
(vl-lexscopes-find name scopes) → (mv entry tail)
Arguments: name — Guard (stringp name).; scopes — Guard (vl-lexscopes-p scopes).
Returns: entry — Entry for this name, if it is declared.
Type (iff (vl-lexscope-entry-p entry) entry).; tail — The tail of scopes starting with the scope for this name.
Type (vl-lexscopes-p tail).

Definitions and Theorems

Function: vl-lexscopes-find

(defun vl-lexscopes-find (name scopes)
  (declare (xargs :guard (and (stringp name)
                              (vl-lexscopes-p scopes))))
  (let ((__function__ 'vl-lexscopes-find))
    (declare (ignorable __function__))
    (b* ((name (string-fix name))
         (scopes (vl-lexscopes-fix scopes))
         ((when (atom scopes)) (mv nil nil))
         (entry (vl-lexscope-find name (car scopes)))
         ((when entry) (mv entry scopes)))
      (vl-lexscopes-find name (cdr scopes)))))

Theorem: return-type-of-vl-lexscopes-find.entry

(defthm return-type-of-vl-lexscopes-find.entry
  (b* (((mv ?entry set::?tail)
        (vl-lexscopes-find name scopes)))
    (iff (vl-lexscope-entry-p entry) entry))
  :rule-classes :rewrite)

Theorem: vl-lexscopes-p-of-vl-lexscopes-find.tail

(defthm vl-lexscopes-p-of-vl-lexscopes-find.tail
  (b* (((mv ?entry set::?tail)
        (vl-lexscopes-find name scopes)))
    (vl-lexscopes-p tail))
  :rule-classes :rewrite)

Theorem: vl-lexscopes-find-of-str-fix-name

(defthm vl-lexscopes-find-of-str-fix-name
  (equal (vl-lexscopes-find (str-fix name)
                            scopes)
         (vl-lexscopes-find name scopes)))

Theorem: vl-lexscopes-find-streqv-congruence-on-name

(defthm vl-lexscopes-find-streqv-congruence-on-name
  (implies (streqv name name-equiv)
           (equal (vl-lexscopes-find name scopes)
                  (vl-lexscopes-find name-equiv scopes)))
  :rule-classes :congruence)

Theorem: vl-lexscopes-find-of-vl-lexscopes-fix-scopes

(defthm vl-lexscopes-find-of-vl-lexscopes-fix-scopes
  (equal (vl-lexscopes-find name (vl-lexscopes-fix scopes))
         (vl-lexscopes-find name scopes)))

Theorem: vl-lexscopes-find-vl-lexscopes-equiv-congruence-on-scopes

(defthm vl-lexscopes-find-vl-lexscopes-equiv-congruence-on-scopes
  (implies (vl-lexscopes-equiv scopes scopes-equiv)
           (equal (vl-lexscopes-find name scopes)
                  (vl-lexscopes-find name scopes-equiv)))
  :rule-classes :congruence)