		Search-engine friendly clone of the ACL2 documentation.

Execution

Read-location

Read the value stored in a location.

Signature
(read-location loc env) → val
Arguments: loc — Guard (locationp loc).; env — Guard (denvp env).
Returns: val — Type (value-resultp val).

If the location is a variable, we read its value. We retrieve the variable or constant with the given name (if any), and we ensure that it is a variable and not a constant; this should always be the case, for locations obtained by evaluating expressions without error, and we plan to formally prove that.

If the location is a tuple or struct component, we first read the tuple or struct value, then we extract the component.

Definitions and Theorems

Function: read-location

(defun read-location (loc env)
  (declare (xargs :guard (and (locationp loc) (denvp env))))
  (let ((__function__ 'read-location))
    (declare (ignorable __function__))
    (location-case loc :var
                   (b* ((var loc.name)
                        (info (get-var/const-dinfo var env))
                        ((when (not info))
                         (reserrf (list :var-not-found var)))
                        ((when (var/const-dinfo->constp info))
                         (reserrf (list :const-location var))))
                     (var/const-dinfo->value info))
                   :tuple-comp
                   (b* (((okf tuple)
                         (read-location loc.tuple env)))
                     (op-tuple-read tuple loc.index))
                   :struct-comp
                   (b* (((okf struct)
                         (read-location loc.struct env)))
                     (op-struct-read struct loc.name)))))

Theorem: value-resultp-of-read-location

(defthm value-resultp-of-read-location
  (b* ((val (read-location loc env)))
    (value-resultp val))
  :rule-classes :rewrite)

Theorem: read-location-of-location-fix-loc

(defthm read-location-of-location-fix-loc
  (equal (read-location (location-fix loc) env)
         (read-location loc env)))

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

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

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

(defthm read-location-of-denv-fix-env
  (equal (read-location loc (denv-fix env))
         (read-location loc env)))

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

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