		Search-engine friendly clone of the ACL2 documentation.

Execution

Update-variable-value-in-scope

Update the value in a variable in a scope.

Signature
(update-variable-value-in-scope var val scope) → new-scope
Arguments: var — Guard (identifierp var).; val — Guard (valuep val).; scope — Guard (vcscope-dinfop scope).
Returns: new-scope — Type (vcscope-dinfo-option-resultp new-scope).

If a variable with the given name is in the scope and the new value has the same type as the old value, we overwrite the value and return the scope. If the types differ, we return an error. If a constant with the given name (instead of a variable) is in the scope, we return an error. If no variable or constant in the scope has the given name, we return no scope, but not an error: this just means that we must look in another scope.

Definitions and Theorems

Function: update-variable-value-in-scope

(defun update-variable-value-in-scope (var val scope)
 (declare (xargs :guard (and (identifierp var)
                             (valuep val)
                             (vcscope-dinfop scope))))
 (let ((__function__ 'update-variable-value-in-scope))
  (declare (ignorable __function__))
  (b*
   ((info (get-var/const-dinfo-from-scope var scope))
    ((unless info)
     (vcscope-dinfo-option-none))
    ((var/const-dinfo info) info)
    ((when info.constp)
     (reserrf (list :update-constant-attempt (identifier-fix var))))
    ((unless (equal (type-of-value info.value)
                    (type-of-value val)))
     (reserrf (list :mismatch-value-update
                    (identifier-fix var)
                    info.value (value-fix val))))
    (new-info (change-var/const-dinfo info
                                      :value (value-fix val)))
    (new-scope (omap::update (identifier-fix var)
                             new-info (vcscope-dinfo-fix scope))))
   (vcscope-dinfo-option-some new-scope))))

Theorem: vcscope-dinfo-option-resultp-of-update-variable-value-in-scope

(defthm
     vcscope-dinfo-option-resultp-of-update-variable-value-in-scope
  (b* ((new-scope (update-variable-value-in-scope var val scope)))
    (vcscope-dinfo-option-resultp new-scope))
  :rule-classes :rewrite)

Theorem: update-variable-value-in-scope-of-identifier-fix-var

(defthm update-variable-value-in-scope-of-identifier-fix-var
  (equal (update-variable-value-in-scope (identifier-fix var)
                                         val scope)
         (update-variable-value-in-scope var val scope)))

Theorem: update-variable-value-in-scope-identifier-equiv-congruence-on-var

(defthm
  update-variable-value-in-scope-identifier-equiv-congruence-on-var
  (implies
       (identifier-equiv var var-equiv)
       (equal (update-variable-value-in-scope var val scope)
              (update-variable-value-in-scope var-equiv val scope)))
  :rule-classes :congruence)

Theorem: update-variable-value-in-scope-of-value-fix-val

(defthm update-variable-value-in-scope-of-value-fix-val
  (equal (update-variable-value-in-scope var (value-fix val)
                                         scope)
         (update-variable-value-in-scope var val scope)))

Theorem: update-variable-value-in-scope-value-equiv-congruence-on-val

(defthm update-variable-value-in-scope-value-equiv-congruence-on-val
  (implies
       (value-equiv val val-equiv)
       (equal (update-variable-value-in-scope var val scope)
              (update-variable-value-in-scope var val-equiv scope)))
  :rule-classes :congruence)

Theorem: update-variable-value-in-scope-of-vcscope-dinfo-fix-scope

(defthm update-variable-value-in-scope-of-vcscope-dinfo-fix-scope
 (equal
  (update-variable-value-in-scope var val (vcscope-dinfo-fix scope))
  (update-variable-value-in-scope var val scope)))

Theorem: update-variable-value-in-scope-vcscope-dinfo-equiv-congruence-on-scope

(defthm
 update-variable-value-in-scope-vcscope-dinfo-equiv-congruence-on-scope
 (implies
      (vcscope-dinfo-equiv scope scope-equiv)
      (equal (update-variable-value-in-scope var val scope)
             (update-variable-value-in-scope var val scope-equiv)))
 :rule-classes :congruence)