		Search-engine friendly clone of the ACL2 documentation.

Read-write-variables

Read-static-var

Read a variable in static storage.

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

If the variable is not found, we return an error.

Definitions and Theorems

Function: read-static-var

(defun read-static-var (var compst)
  (declare (xargs :guard (and (identp var)
                              (compustatep compst))))
  (let ((__function__ 'read-static-var))
    (declare (ignorable __function__))
    (b* ((pair (omap::assoc (ident-fix var)
                            (compustate->static compst)))
         ((when (not pair))
          (error (list :static-var-not-found (ident-fix var)))))
      (cdr pair))))

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

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

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

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

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

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

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

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

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

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