		Search-engine friendly clone of the ACL2 documentation.

Semantics

Read-var

Read a variable's value from the environment.

Signature
(read-var var env) → val
Arguments: var — Guard (stringp var).; env — Guard (envp env).
Returns: val — Type (integerp val).

It is convenient to regard every possible variable to be explicitly or implicitly present in the environment, by regarding the value associated to a variable not explicitly present as 0, as if the variable were explicitly present and had value 0. This way, this reading function is total: it always yields an integer value for each variable and environment.

Definitions and Theorems

Function: read-var

(defun read-var (var env)
  (declare (xargs :guard (and (stringp var) (envp env))))
  (b* ((var-val (omap::assoc (str-fix var)
                             (env-fix env))))
    (if (null var-val) 0 (cdr var-val))))

Theorem: integerp-of-read-var

(defthm integerp-of-read-var
  (b* ((val (read-var var env)))
    (integerp val))
  :rule-classes :rewrite)

Theorem: read-var-of-str-fix-var

(defthm read-var-of-str-fix-var
  (equal (read-var (str-fix var) env)
         (read-var var env)))

Theorem: read-var-streqv-congruence-on-var

(defthm read-var-streqv-congruence-on-var
  (implies (acl2::streqv var var-equiv)
           (equal (read-var var env)
                  (read-var var-equiv env)))
  :rule-classes :congruence)

Theorem: read-var-of-env-fix-env

(defthm read-var-of-env-fix-env
  (equal (read-var var (env-fix env))
         (read-var var env)))

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

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