		Search-engine friendly clone of the ACL2 documentation.

Dynamic-environments

Update-var/const-dinfo-in-scope

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

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

We return `none' if no variable or constant with that name is found.

Note that this may turn a constant into a variable or vice versa. However, this operation is never used in that way.

Definitions and Theorems

Function: update-var/const-dinfo-in-scope

(defun update-var/const-dinfo-in-scope (name info scope)
  (declare (xargs :guard (and (identifierp name)
                              (var/const-dinfop info)
                              (vcscope-dinfop scope))))
  (let ((__function__ 'update-var/const-dinfo-in-scope))
    (declare (ignorable __function__))
    (if (consp (omap::assoc (identifier-fix name)
                            (vcscope-dinfo-fix scope)))
        (vcscope-dinfo-option-some
             (omap::update (identifier-fix name)
                           (var/const-dinfo-fix info)
                           (vcscope-dinfo-fix scope)))
      (vcscope-dinfo-option-none))))

Theorem: vcscope-dinfo-optionp-of-update-var/const-dinfo-in-scope

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

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

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

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

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

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

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

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

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

Theorem: update-var/const-dinfo-in-scope-of-vcscope-dinfo-fix-scope

(defthm update-var/const-dinfo-in-scope-of-vcscope-dinfo-fix-scope
  (equal (update-var/const-dinfo-in-scope
              name info (vcscope-dinfo-fix scope))
         (update-var/const-dinfo-in-scope name info scope)))

Theorem: update-var/const-dinfo-in-scope-vcscope-dinfo-equiv-congruence-on-scope

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