		Search-engine friendly clone of the ACL2 documentation.

Execution

Update-variable-value

Update the value in a variable in a dynamic environment.

Signature
(update-variable-value var val env) → new-env
Arguments: var — Guard (identifierp var).; val — Guard (valuep val).; env — Guard (denvp env).
Returns: new-env — Type (denv-resultp new-env).

The variable must be in the top call frame.

Definitions and Theorems

Function: update-variable-value

(defun update-variable-value (var val env)
  (declare (xargs :guard (and (identifierp var)
                              (valuep val)
                              (denvp env))))
  (let ((__function__ 'update-variable-value))
    (declare (ignorable __function__))
    (b* ((calls (denv->call-stack env))
         ((when (endp calls))
          (reserrf :empty-call-stack))
         (top-call (car calls))
         (scopes (call-dinfo->scopes top-call))
         ((okf new-scopes)
          (update-variable-value-in-scope-list var val 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-resultp-of-update-variable-value

(defthm denv-resultp-of-update-variable-value
  (b* ((new-env (update-variable-value var val env)))
    (denv-resultp new-env))
  :rule-classes :rewrite)

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

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

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

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

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

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

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

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

Theorem: update-variable-value-of-denv-fix-env

(defthm update-variable-value-of-denv-fix-env
  (equal (update-variable-value var val (denv-fix env))
         (update-variable-value var val env)))

Theorem: update-variable-value-denv-equiv-congruence-on-env

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