		Search-engine friendly clone of the ACL2 documentation.

Dynamic-environments

Get-var/const-dinfo

Get the information about a variable a constant from a dynamic environment.

Signature
(get-var/const-dinfo name env) → dinfo
Arguments: name — Guard (identifierp name).; env — Guard (denvp env).
Returns: dinfo — Type (var/const-dinfo-optionp dinfo).

We look through the scopes in the top call of the call stack. If the call stack is empty, the variable or constant is not found.

Definitions and Theorems

Function: get-var/const-dinfo

(defun get-var/const-dinfo (name env)
  (declare (xargs :guard (and (identifierp name) (denvp env))))
  (let ((__function__ 'get-var/const-dinfo))
    (declare (ignorable __function__))
    (b* ((calls (denv->call-stack env))
         ((when (endp calls)) nil)
         (top-call (car calls))
         (scopes (call-dinfo->scopes top-call)))
      (get-var/const-dinfo-from-scope-list name scopes))))

Theorem: var/const-dinfo-optionp-of-get-var/const-dinfo

(defthm var/const-dinfo-optionp-of-get-var/const-dinfo
  (b* ((dinfo (get-var/const-dinfo name env)))
    (var/const-dinfo-optionp dinfo))
  :rule-classes :rewrite)

Theorem: get-var/const-dinfo-of-identifier-fix-name

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

Theorem: get-var/const-dinfo-identifier-equiv-congruence-on-name

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

Theorem: get-var/const-dinfo-of-denv-fix-env

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

Theorem: get-var/const-dinfo-denv-equiv-congruence-on-env

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