		Search-engine friendly clone of the ACL2 documentation.

Dynamic-environments

Update-var/const-dinfo

Update the dynamic information for a variable or constant in a dynamic environment.

Signature
(update-var/const-dinfo name info env) → new-env
Arguments: name — Guard (identifierp name).; info — Guard (var/const-dinfop info).; env — Guard (denvp env).
Returns: new-env — Type (denv-optionp new-env).

We return nil when the call stack is empty or no variable or constant with that name is found in the top frame.

Definitions and Theorems

Function: update-var/const-dinfo

(defun update-var/const-dinfo (name info env)
 (declare (xargs :guard (and (identifierp name)
                             (var/const-dinfop info)
                             (denvp env))))
 (let ((__function__ 'update-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))
       ((when (endp scopes)) nil)
       (new-scopes
            (update-var/const-dinfo-in-scope-list name info scopes))
       ((when (vcscope-dinfo-list-option-case new-scopes :none))
        nil)
       (new-scopes (vcscope-dinfo-list-option-some->get new-scopes))
       (new-top-call (change-call-dinfo top-call
                                        :scopes new-scopes))
       (new-calls (cons new-top-call (cdr calls)))
       (new-env (change-denv env
                             :call-stack new-calls)))
    new-env)))

Theorem: denv-optionp-of-update-var/const-dinfo

(defthm denv-optionp-of-update-var/const-dinfo
  (b* ((new-env (update-var/const-dinfo name info env)))
    (denv-optionp new-env))
  :rule-classes :rewrite)

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

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

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

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

Theorem: update-var/const-dinfo-of-var/const-dinfo-fix-info

(defthm update-var/const-dinfo-of-var/const-dinfo-fix-info
  (equal (update-var/const-dinfo name (var/const-dinfo-fix info)
                                 env)
         (update-var/const-dinfo name info env)))

Theorem: update-var/const-dinfo-var/const-dinfo-equiv-congruence-on-info

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

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

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

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

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