		Search-engine friendly clone of the ACL2 documentation.

Dynamic-semantics

Read-var-value

Read a variable value from the computation state.

Signature
(read-var-value var cstate) → val
Arguments: var — Guard (identifierp var).; cstate — Guard (cstatep cstate).
Returns: val — Type (value-resultp val).

An error is returned if the variable does not exist.

Definitions and Theorems

Function: read-var-value

(defun read-var-value (var cstate)
 (declare (xargs :guard (and (identifierp var)
                             (cstatep cstate))))
 (let ((__function__ 'read-var-value))
   (declare (ignorable __function__))
   (b* ((lstate (cstate->local cstate))
        (var-val (omap::assoc (identifier-fix var)
                              lstate))
        ((unless (consp var-val))
         (reserrf (list :variable-not-found (identifier-fix var)))))
     (value-fix (cdr var-val)))))

Theorem: value-resultp-of-read-var-value

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

Theorem: error-info-wfp-of-read-var-value

(defthm error-info-wfp-of-read-var-value
  (b* ((?val (read-var-value var cstate)))
    (implies (reserrp val)
             (error-info-wfp val))))

Theorem: read-var-value-of-identifier-fix-var

(defthm read-var-value-of-identifier-fix-var
  (equal (read-var-value (identifier-fix var)
                         cstate)
         (read-var-value var cstate)))

Theorem: read-var-value-identifier-equiv-congruence-on-var

(defthm read-var-value-identifier-equiv-congruence-on-var
  (implies (identifier-equiv var var-equiv)
           (equal (read-var-value var cstate)
                  (read-var-value var-equiv cstate)))
  :rule-classes :congruence)

Theorem: read-var-value-of-cstate-fix-cstate

(defthm read-var-value-of-cstate-fix-cstate
  (equal (read-var-value var (cstate-fix cstate))
         (read-var-value var cstate)))

Theorem: read-var-value-cstate-equiv-congruence-on-cstate

(defthm read-var-value-cstate-equiv-congruence-on-cstate
  (implies (cstate-equiv cstate cstate-equiv)
           (equal (read-var-value var cstate)
                  (read-var-value var cstate-equiv)))
  :rule-classes :congruence)