		Search-engine friendly clone of the ACL2 documentation.

Execution

Exec-var/const

Execute a variable or constant expression.

Signature
(exec-var/const name env) → evalue+denv
Arguments: name — Guard (identifierp name).; env — Guard (denvp env).
Returns: evalue+denv — Type (evalue+denv-resultp evalue+denv).

This is an expression consisting of the name of a variable or constant. We attempt to retrieve the variable or constant from the environment. If it is a variable, we return its location; if it is a constant, we return its value. The environment is unchanged.

Definitions and Theorems

Function: exec-var/const

(defun exec-var/const (name env)
 (declare (xargs :guard (and (identifierp name) (denvp env))))
 (let ((__function__ 'exec-var/const))
  (declare (ignorable __function__))
  (b* ((info (get-var/const-dinfo name env))
       ((unless info)
        (reserrf (list :var/const-not-found (identifier-fix name))))
       ((var/const-dinfo info) info)
       (eval (if info.constp (expr-value-value info.value)
               (expr-value-location (location-var name)))))
    (make-evalue+denv :evalue eval
                      :denv (denv-fix env)))))

Theorem: evalue+denv-resultp-of-exec-var/const

(defthm evalue+denv-resultp-of-exec-var/const
  (b* ((evalue+denv (exec-var/const name env)))
    (evalue+denv-resultp evalue+denv))
  :rule-classes :rewrite)

Theorem: exec-var/const-of-identifier-fix-name

(defthm exec-var/const-of-identifier-fix-name
  (equal (exec-var/const (identifier-fix name)
                         env)
         (exec-var/const name env)))

Theorem: exec-var/const-identifier-equiv-congruence-on-name

(defthm exec-var/const-identifier-equiv-congruence-on-name
  (implies (identifier-equiv name name-equiv)
           (equal (exec-var/const name env)
                  (exec-var/const name-equiv env)))
  :rule-classes :congruence)

Theorem: exec-var/const-of-denv-fix-env

(defthm exec-var/const-of-denv-fix-env
  (equal (exec-var/const name (denv-fix env))
         (exec-var/const name env)))

Theorem: exec-var/const-denv-equiv-congruence-on-env

(defthm exec-var/const-denv-equiv-congruence-on-env
  (implies (denv-equiv env env-equiv)
           (equal (exec-var/const name env)
                  (exec-var/const name env-equiv)))
  :rule-classes :congruence)