		Search-engine friendly clone of the ACL2 documentation.

Read-write-variables

Read-auto-var

Read a variable in automatic storage.

Signature
(read-auto-var var compst) → val
Arguments: var — Guard (identp var).; compst — Guard (compustatep compst).
Returns: val — Type (value-optionp val).

That is, read the variable in the scopes in the top frame. We search the scopes from innermost (leftmost) to outermost (rightmost), according to the scoping rules for variables, where variables in inner scopes may hide variables in outer scopes.

If the variable is not found, we return nil, not an error. The reason is that this ACL2 function is used as a subroutine of read-var, where if a variable is not found in automatic storage, it is looked up in static storage. Thus, not finding a variable in automatic storage, in this ACL2 function, is not necessarily an error.

We do not look at other frames, because the variables in other frames are not in scope when running in the top frame.

Definitions and Theorems

Function: read-auto-var-aux

(defun read-auto-var-aux (var scopes)
  (declare (xargs :guard (and (identp var)
                              (scope-listp scopes))))
  (let ((__function__ 'read-auto-var-aux))
    (declare (ignorable __function__))
    (b* (((when (endp scopes)) nil)
         (scope (car scopes))
         (pair (omap::assoc (ident-fix var)
                            (scope-fix scope)))
         ((when (not pair))
          (read-auto-var-aux var (cdr scopes))))
      (cdr pair))))

Theorem: value-optionp-of-read-auto-var-aux

(defthm value-optionp-of-read-auto-var-aux
  (b* ((val (read-auto-var-aux var scopes)))
    (value-optionp val))
  :rule-classes :rewrite)

Theorem: read-auto-var-aux-of-ident-fix-var

(defthm read-auto-var-aux-of-ident-fix-var
  (equal (read-auto-var-aux (ident-fix var)
                            scopes)
         (read-auto-var-aux var scopes)))

Theorem: read-auto-var-aux-ident-equiv-congruence-on-var

(defthm read-auto-var-aux-ident-equiv-congruence-on-var
  (implies (ident-equiv var var-equiv)
           (equal (read-auto-var-aux var scopes)
                  (read-auto-var-aux var-equiv scopes)))
  :rule-classes :congruence)

Theorem: read-auto-var-aux-of-scope-list-fix-scopes

(defthm read-auto-var-aux-of-scope-list-fix-scopes
  (equal (read-auto-var-aux var (scope-list-fix scopes))
         (read-auto-var-aux var scopes)))

Theorem: read-auto-var-aux-scope-list-equiv-congruence-on-scopes

(defthm read-auto-var-aux-scope-list-equiv-congruence-on-scopes
  (implies (scope-list-equiv scopes scopes-equiv)
           (equal (read-auto-var-aux var scopes)
                  (read-auto-var-aux var scopes-equiv)))
  :rule-classes :congruence)

Function: read-auto-var

(defun read-auto-var (var compst)
  (declare (xargs :guard (and (identp var)
                              (compustatep compst))))
  (declare (xargs :guard (> (compustate-frames-number compst)
                            0)))
  (let ((__function__ 'read-auto-var))
    (declare (ignorable __function__))
    (read-auto-var-aux var
                       (frame->scopes (top-frame compst)))))

Theorem: value-optionp-of-read-auto-var

(defthm value-optionp-of-read-auto-var
  (b* ((val (read-auto-var var compst)))
    (value-optionp val))
  :rule-classes :rewrite)

Theorem: read-auto-var-of-ident-fix-var

(defthm read-auto-var-of-ident-fix-var
  (equal (read-auto-var (ident-fix var) compst)
         (read-auto-var var compst)))

Theorem: read-auto-var-ident-equiv-congruence-on-var

(defthm read-auto-var-ident-equiv-congruence-on-var
  (implies (ident-equiv var var-equiv)
           (equal (read-auto-var var compst)
                  (read-auto-var var-equiv compst)))
  :rule-classes :congruence)

Theorem: read-auto-var-of-compustate-fix-compst

(defthm read-auto-var-of-compustate-fix-compst
  (equal (read-auto-var var (compustate-fix compst))
         (read-auto-var var compst)))

Theorem: read-auto-var-compustate-equiv-congruence-on-compst

(defthm read-auto-var-compustate-equiv-congruence-on-compst
  (implies (compustate-equiv compst compst-equiv)
           (equal (read-auto-var var compst)
                  (read-auto-var var compst-equiv)))
  :rule-classes :congruence)