		Search-engine friendly clone of the ACL2 documentation.

Execution

Write-location

Write a value into a location.

Signature
(write-location loc val env) → new-env
Arguments: loc — Guard (locationp loc).; val — Guard (valuep val).; env — Guard (denvp env).
Returns: new-env — Type (denv-resultp new-env).

If the location is a variable, we update its value.

If the location is a tuple or struct component, we read the tuple, we update its component, and recursively write the value into the enclosing location.

Definitions and Theorems

Function: write-location

(defun write-location (loc val env)
  (declare (xargs :guard (and (locationp loc)
                              (valuep val)
                              (denvp env))))
  (let ((__function__ 'write-location))
    (declare (ignorable __function__))
    (location-case loc :var
                   (update-variable-value loc.name val env)
                   :tuple-comp
                   (b* (((okf tuple)
                         (read-location loc.tuple env))
                        ((okf new-tuple)
                         (op-tuple-write tuple loc.index val)))
                     (write-location loc.tuple new-tuple env))
                   :struct-comp
                   (b* (((okf circ)
                         (read-location loc.struct env))
                        ((okf new-circ)
                         (op-struct-write circ loc.name val)))
                     (write-location loc.struct new-circ env)))))

Theorem: denv-resultp-of-write-location

(defthm denv-resultp-of-write-location
  (b* ((new-env (write-location loc val env)))
    (denv-resultp new-env))
  :rule-classes :rewrite)

Theorem: write-location-of-location-fix-loc

(defthm write-location-of-location-fix-loc
  (equal (write-location (location-fix loc)
                         val env)
         (write-location loc val env)))

Theorem: write-location-location-equiv-congruence-on-loc

(defthm write-location-location-equiv-congruence-on-loc
  (implies (location-equiv loc loc-equiv)
           (equal (write-location loc val env)
                  (write-location loc-equiv val env)))
  :rule-classes :congruence)

Theorem: write-location-of-value-fix-val

(defthm write-location-of-value-fix-val
  (equal (write-location loc (value-fix val) env)
         (write-location loc val env)))

Theorem: write-location-value-equiv-congruence-on-val

(defthm write-location-value-equiv-congruence-on-val
  (implies (value-equiv val val-equiv)
           (equal (write-location loc val env)
                  (write-location loc val-equiv env)))
  :rule-classes :congruence)

Theorem: write-location-of-denv-fix-env

(defthm write-location-of-denv-fix-env
  (equal (write-location loc val (denv-fix env))
         (write-location loc val env)))

Theorem: write-location-denv-equiv-congruence-on-env

(defthm write-location-denv-equiv-congruence-on-env
  (implies (denv-equiv env env-equiv)
           (equal (write-location loc val env)
                  (write-location loc val env-equiv)))
  :rule-classes :congruence)