		Search-engine friendly clone of the ACL2 documentation.

Read-write-variables

Read-var

Read a variable in a computation state.

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

First we try automatic storage (if there are frames), then static storage. Indeed, file scope is outside all the block scopes, so it must be tried last.

Definitions and Theorems

Function: read-var

(defun read-var (var compst)
  (declare (xargs :guard (and (identp var)
                              (compustatep compst))))
  (let ((__function__ 'read-var))
    (declare (ignorable __function__))
    (if (> (compustate-frames-number compst) 0)
        (b* ((val (read-auto-var var compst)))
          (or val (read-static-var var compst)))
      (read-static-var var compst))))

Theorem: value-resultp-of-read-var

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

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

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

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

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

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

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

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

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