		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

Var-table-lookup

Look up a variable in a variable table.

Signature
(var-table-lookup var vartab) → info
Arguments: var — Guard (identp var).; vartab — Guard (var-tablep vartab).
Returns: info — Type (var-sinfo-optionp info).

If the variable is found, we return its information; otherwise, we return nil. We search for the variable in the sequence of scopes in order, i.e. from innermost to outermost block.

Definitions and Theorems

Function: var-table-lookup

(defun var-table-lookup (var vartab)
  (declare (xargs :guard (and (identp var) (var-tablep vartab))))
  (let ((__function__ 'var-table-lookup))
    (declare (ignorable __function__))
    (b* (((unless (mbt (consp vartab))) nil)
         (varscope (var-table-scope-fix (car vartab)))
         (pair (omap::assoc (ident-fix var) varscope))
         ((when (consp pair)) (cdr pair))
         (vartab (cdr vartab))
         ((when (endp vartab)) nil))
      (var-table-lookup var vartab))))

Theorem: var-sinfo-optionp-of-var-table-lookup

(defthm var-sinfo-optionp-of-var-table-lookup
  (b* ((info (var-table-lookup var vartab)))
    (var-sinfo-optionp info))
  :rule-classes :rewrite)

Theorem: var-table-lookup-of-ident-fix-var

(defthm var-table-lookup-of-ident-fix-var
  (equal (var-table-lookup (ident-fix var)
                           vartab)
         (var-table-lookup var vartab)))

Theorem: var-table-lookup-ident-equiv-congruence-on-var

(defthm var-table-lookup-ident-equiv-congruence-on-var
  (implies (ident-equiv var var-equiv)
           (equal (var-table-lookup var vartab)
                  (var-table-lookup var-equiv vartab)))
  :rule-classes :congruence)

Theorem: var-table-lookup-of-var-table-fix-vartab

(defthm var-table-lookup-of-var-table-fix-vartab
  (equal (var-table-lookup var (var-table-fix vartab))
         (var-table-lookup var vartab)))

Theorem: var-table-lookup-var-table-equiv-congruence-on-vartab

(defthm var-table-lookup-var-table-equiv-congruence-on-vartab
  (implies (var-table-equiv vartab vartab-equiv)
           (equal (var-table-lookup var vartab)
                  (var-table-lookup var vartab-equiv)))
  :rule-classes :congruence)