		Search-engine friendly clone of the ACL2 documentation.

Execution

Update-variable-value-in-scope-list

Update the value in a variable in a list of scopes.

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

We return an error if we run out of scopes, i.e. if the variable is not found in any scope. This is justified by the fact that, when we call this updating function, the variable in question is from a location that results from the evaluation of an expression, and thus the variable must exist and be accessible. We plan to incorporate this expected invariant into the guard of this updating function.

Definitions and Theorems

Function: update-variable-value-in-scope-list

(defun update-variable-value-in-scope-list (var val scopes)
 (declare (xargs :guard (and (identifierp var)
                             (valuep val)
                             (vcscope-dinfo-listp scopes))))
 (let ((__function__ 'update-variable-value-in-scope-list))
  (declare (ignorable __function__))
  (b* (((when (endp scopes))
        (reserrf (list :no-var-to-update (identifier-fix var))))
       (scope (vcscope-dinfo-fix (car scopes)))
       ((okf new-scope)
        (update-variable-value-in-scope var val scope))
       ((when (vcscope-dinfo-option-case new-scope :some))
        (cons (vcscope-dinfo-option-some->get new-scope)
              (vcscope-dinfo-list-fix (cdr scopes))))
       ((okf new-scopes)
        (update-variable-value-in-scope-list var val (cdr scopes))))
    (cons scope new-scopes))))

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

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

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

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

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

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

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

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

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

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

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

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

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

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